CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
recCompleteInster Class Reference

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

recCompleteInster::recCompleteInster ( const Expr body,
const std::vector< Expr > &  bvs,
std::set< Expr > &  all_index,
Expr  res 
)

Definition at line 2187 of file theory_quant.cpp.


Member Function Documentation

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

Definition at line 2196 of file theory_quant.cpp.

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

Referenced by inst().

Expr & recCompleteInster::build_tree ( ) [private]

Definition at line 2211 of file theory_quant.cpp.

References d_exprs, CVC3::andExpr(), d_result, and CVC3::Expr::andExpr().

Referenced by inst().

Expr recCompleteInster::inst ( )

Definition at line 2189 of file theory_quant.cpp.

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

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


Member Data Documentation

const Expr& recCompleteInster::d_body [private]

Definition at line 2174 of file theory_quant.cpp.

Referenced by inst_helper().

Definition at line 2175 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

Definition at line 2176 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

Definition at line 2177 of file theory_quant.cpp.

Referenced by inst_helper().

Definition at line 2178 of file theory_quant.cpp.

Referenced by inst_helper(), and build_tree().

Definition at line 2179 of file theory_quant.cpp.

Referenced by build_tree().


The documentation for this class was generated from the following file: