recCompleteInster Class Reference

Collaboration diagram for recCompleteInster:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 2140 of file theory_quant.cpp.


Constructor & Destructor Documentation

recCompleteInster::recCompleteInster ( const Expr ,
const std::vector< Expr > &  ,
std::set< Expr > &  ,
Expr   
)

Definition at line 2152 of file theory_quant.cpp.


Member Function Documentation

void recCompleteInster::inst_helper ( int  num_vars  )  [private]

Definition at line 2161 of file theory_quant.cpp.

References CVC3::Expr::andExpr(), d_all_index, d_body, d_buff, d_bvs, d_result, and CVC3::Expr::substExpr().

Referenced by inst().

Expr recCompleteInster::inst (  ) 

Definition at line 2154 of file theory_quant.cpp.

References d_buff, d_bvs, d_result, and inst_helper().

Referenced by CVC3::CompleteInstPreProcessor::inst().


Member Data Documentation

const Expr& recCompleteInster::d_body [private]

Definition at line 2141 of file theory_quant.cpp.

Referenced by inst_helper().

const std::vector<Expr>& recCompleteInster::d_bvs [private]

Definition at line 2142 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

std::vector<Expr> recCompleteInster::d_buff [private]

Definition at line 2143 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

const std::set<Expr>& recCompleteInster::d_all_index [private]

Definition at line 2144 of file theory_quant.cpp.

Referenced by inst_helper().

Expr recCompleteInster::d_result [private]

Definition at line 2145 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().


The documentation for this class was generated from the following file:
Generated on Wed Nov 18 16:14:15 2009 for CVC3 by  doxygen 1.5.2