CVC3
2.4.1
|
Public Attributes | |
std::vector< std::vector < size_t > > | common_pos |
std::vector< std::vector < size_t > > | var_pos |
std::vector< CDMap< Expr, bool > * > | var_binds_found |
std::vector< ExprMap< CDList < Expr > * > * > | uncomm_list |
Theorem | univThm |
size_t | univ_id |
Definition at line 406 of file theory_quant.h.
std::vector<std::vector<size_t> > CVC3::TheoryQuant::multTrigsInfo::common_pos |
Definition at line 407 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().
std::vector<std::vector<size_t> > CVC3::TheoryQuant::multTrigsInfo::var_pos |
Definition at line 408 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().
Definition at line 410 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().
Definition at line 412 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().
Theorem CVC3::TheoryQuant::multTrigsInfo::univThm |
Definition at line 413 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::checkSat(), and CVC3::TheoryQuant::setupTriggers().
size_t CVC3::TheoryQuant::multTrigsInfo::univ_id |
Definition at line 414 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::checkSat(), and CVC3::TheoryQuant::setupTriggers().