CVC3
Public Member Functions | Private Member Functions | Private Attributes | List of all members
recCompleteInster Class Reference
Collaboration diagram for recCompleteInster:
Collaboration graph

Public Member Functions

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

Private Member Functions

void inst_helper (int num_vars)
 
Exprbuild_tree ()
 

Private Attributes

const Exprd_body
 
const std::vector< Expr > & d_bvs
 
std::vector< Exprd_buff
 
const std::set< Expr > & d_all_index
 
std::vector< Exprd_exprs
 
Expr d_result
 

Detailed Description

Definition at line 2173 of file theory_quant.cpp.

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_body, d_buff, d_bvs, d_exprs, and CVC3::Expr::substExpr().

Referenced by inst().

Expr & recCompleteInster::build_tree ( )
private

Definition at line 2211 of file theory_quant.cpp.

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

Referenced by inst().

Expr recCompleteInster::inst ( )

Definition at line 2189 of file theory_quant.cpp.

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

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().

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

Definition at line 2175 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

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

Definition at line 2176 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

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

Definition at line 2177 of file theory_quant.cpp.

Referenced by inst_helper().

std::vector<Expr> recCompleteInster::d_exprs
private

Definition at line 2178 of file theory_quant.cpp.

Referenced by build_tree(), and inst_helper().

Expr recCompleteInster::d_result
private

Definition at line 2179 of file theory_quant.cpp.

Referenced by build_tree().


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