CVC3
|
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 |
Definition at line 2173 of file theory_quant.cpp.
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.
|
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().
|
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().
|
private |
Definition at line 2174 of file theory_quant.cpp.
Referenced by inst_helper().
|
private |
Definition at line 2175 of file theory_quant.cpp.
Referenced by inst(), and inst_helper().
|
private |
Definition at line 2176 of file theory_quant.cpp.
Referenced by inst(), and inst_helper().
|
private |
Definition at line 2177 of file theory_quant.cpp.
Referenced by inst_helper().
|
private |
Definition at line 2178 of file theory_quant.cpp.
Referenced by build_tree(), and inst_helper().
|
private |
Definition at line 2179 of file theory_quant.cpp.
Referenced by build_tree().