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)
- Expr & build_tree ()
Private Attributes
- const Expr & d_body
- const std::vector< Expr > & d_bvs
- std::vector< Expr > d_buff
- const std::set< Expr > & d_all_index
- std::vector< Expr > d_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:
