#include <theory_quant.h>
Inheritance diagram for CVC3::TheoryQuant:
Author: Daniel Wichs
Created: Wednesday July 2, 2003
Definition at line 97 of file theory_quant.h.
typedef std::map<Type, std::vector<size_t>, TypeComp > CVC3::TheoryQuant::typeMap [private] |
used to facilitate instantiation of universal quantifiers
Definition at line 106 of file theory_quant.h.
TheoryQuant::TheoryQuant | ( | TheoryCore * | core | ) |
categorizes all the terms contained in an expressions by type. Constructor
Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.
core | Constructor |
Definition at line 138 of file theory_quant.cpp.
References CVC3::Type::anyType(), createProofRules(), d_cacheThmPos, d_initMaxScore, d_instCount, d_mybvs, d_offset_multi_trig, d_partCalled, d_rules, d_trans2_num, d_trans_num, d_univs, CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getEM(), CVC3::TheoryCore::getFlags(), IF_DEBUG, MAX_TRIG_BVS, CVC3::Theory::registerTheory(), and CVC3::Theory::theoryCore().
TheoryQuant::~TheoryQuant | ( | ) |
bool TheoryQuant::recursiveMap | ( | const Expr & | term | ) | [private] |
categorizes all the terms contained in an expressions by type.
Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.
Definition at line 4757 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BOUND_VAR, CVC3::ExprMap< Data >::count(), d_contextCache, d_contextMap, d_contextTerms, d_savedCache, CVC3::Expr::end(), CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Expr::getKind(), CVC3::Type::isBool(), CVC3::Theory::theoryCore(), CVC3::Type::toString(), and CVC3::TRACE.
Referenced by mapTermsByType().
categorizes all the terms contained in a vector of expressions by type.
Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
Definition at line 4729 of file theory_quant.cpp.
References CVC3::Theory::boolType(), d_contextMap, d_contextTerms, d_univs, CVC3::Theory::falseExpr(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), recursiveMap(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), and CVC3::Theory::trueExpr().
Referenced by naiveCheckSat().
void TheoryQuant::instantiate | ( | Theorem | univ, | |
bool | all, | |||
bool | savedMap, | |||
size_t | newIndex | |||
) | [private] |
Queues up all possible instantiations of bound variables.
The savedMap boolean indicates whether to use savedMap or d_contextMap the all boolean indicates weather to use all instantiation or only new ones and newIndex is the index where new instantiations begin.
Definition at line 4642 of file theory_quant.cpp.
References d_contextTerms, d_savedTerms, recInstantiate(), and CVC3::TRACE.
Referenced by naiveCheckSat().
void TheoryQuant::recInstantiate | ( | Theorem & | univ, | |
bool | all, | |||
bool | savedMap, | |||
size_t | newIndex, | |||
std::vector< Expr > & | varReplacements | |||
) | [private] |
does most of the work of the instantiate function.
Definition at line 4658 of file theory_quant.cpp.
References d_contextMap, d_contextTerms, d_instCount, d_insts, d_maxQuantInst, d_rules, d_savedMap, d_savedTerms, enqueueInst(), CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), null_expr, CVC3::CDList< T >::size(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::QuantProofRules::universalInst().
Referenced by instantiate().
void TheoryQuant::findInstAssumptions | ( | const Theorem & | thm | ) | [private] |
A recursive function used to find instantiated universals in the hierarchy of assumptions.
Definition at line 4845 of file theory_quant.cpp.
References CVC3::Assumptions::begin(), CVC3::ExprMap< Data >::count(), d_insts, d_savedCache, d_savedMap, d_savedTerms, CVC3::Assumptions::end(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theorem::isNull(), CVC3::Theorem::isRefl(), CVC3::Theorem::setFlag(), and CVC3::TRACE.
void TheoryQuant::arrayIndexName | ( | const Expr & | e | ) | [private] |
Definition at line 860 of file theory_quant.cpp.
References d_arrayIndic, getBoundVars(), getSubTerms(), CVC3::READ, and CVC3::WRITE.
Referenced by checkSat(), and setupTriggers().
int TheoryQuant::getExprScore | ( | const Expr & | e | ) | [private] |
Definition at line 225 of file theory_quant.cpp.
References CVC3::TheoryCore::getQuantLevelForTerm(), and CVC3::Theory::theoryCore().
Referenced by synCheckSat().
bool TheoryQuant::transFound | ( | const Expr & | comb | ) | [inline, private] |
Definition at line 3510 of file theory_quant.cpp.
References d_trans_found.
Referenced by synNewInst().
void TheoryQuant::setTransFound | ( | const Expr & | comb | ) | [inline, private] |
Definition at line 3514 of file theory_quant.cpp.
References d_trans_found.
Referenced by synNewInst().
bool TheoryQuant::trans2Found | ( | const Expr & | comb | ) | [inline, private] |
Definition at line 3518 of file theory_quant.cpp.
References d_trans2_found.
Referenced by synNewInst().
void TheoryQuant::setTrans2Found | ( | const Expr & | comb | ) | [inline, private] |
Definition at line 3522 of file theory_quant.cpp.
References d_trans2_found.
Referenced by synNewInst().
Definition at line 3527 of file theory_quant.cpp.
References d_trans_back, and null_cdlist.
Referenced by synNewInst().
Definition at line 3536 of file theory_quant.cpp.
References d_trans_forw, and null_cdlist.
Referenced by synNewInst().
Definition at line 3545 of file theory_quant.cpp.
References d_trans_back, and CVC3::Theory::theoryCore().
Referenced by synNewInst().
Definition at line 3555 of file theory_quant.cpp.
References d_trans_forw, and CVC3::Theory::theoryCore().
Referenced by synNewInst().
Definition at line 1850 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_eqs, d_eqs_pos, d_parent_list, CVC3::ExprMap< Data >::end(), CVC3::CDList< T >::push_back(), and CVC3::CDO< T >::set().
Referenced by synCheckSat().
int TheoryQuant::loc_gterm | ( | const std::vector< Expr > & | border, | |
const Expr & | gterm, | |||
int | pos | |||
) | [private] |
Definition at line 3237 of file theory_quant.cpp.
References d_mtrigs_bvorder, and DebugAssert.
Referenced by recSearchCover().
void TheoryQuant::recSearchCover | ( | const std::vector< Expr > & | border, | |
const std::vector< Expr > & | mtrigs, | |||
int | cur_depth, | |||
std::vector< std::vector< Expr > > & | instSet, | |||
std::vector< Expr > & | cur_inst | |||
) | [private] |
Definition at line 3250 of file theory_quant.cpp.
References d_mtrigs_inst, loc_gterm(), null_expr, and CVC3::CDList< T >::size().
Referenced by searchCover().
void TheoryQuant::searchCover | ( | const Expr & | thm, | |
const std::vector< Expr > & | border, | |||
std::vector< std::vector< Expr > > & | instSet | |||
) | [private] |
Definition at line 3314 of file theory_quant.cpp.
References d_multTriggers, null_expr, and recSearchCover().
Referenced by hasGoodSynMultiInst().
void TheoryQuant::addNotify | ( | const Expr & | e | ) | [private] |
Definition at line 536 of file theory_quant.cpp.
int TheoryQuant::sendInstNew | ( | ) | [private] |
Definition at line 520 of file theory_quant.cpp.
References d_allInstCount, d_instThisRound, d_simplifiedThmQueue, and CVC3::Theory::enqueueFact().
Referenced by checkSat(), and synCheckSat().
Definition at line 334 of file theory_quant.cpp.
References CVC3::Expr::clearFlags(), d_subTermsMap, recGetSubTerms(), and CVC3::TRACE.
Referenced by arrayIndexName().
void CVC3::TheoryQuant::enqueueInst | ( | const | Theorem, | |
const | Theorem | |||
) | [private] |
Referenced by arrayHeuristic(), enqueueInst(), recInstantiate(), and synNewInst().
void TheoryQuant::enqueueInst | ( | const Theorem & | univ, | |
const std::vector< Expr > & | bind, | |||
const Expr & | gterm | |||
) | [private] |
Definition at line 354 of file theory_quant.cpp.
References d_allInstCount, d_bindHistory, d_instThisRound, d_rules, d_simplifiedThmQueue, d_useInstLCache, d_useInstTrue, CVC3::Theory::enqueueFact(), FOUND_FALSE, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theorem::getRHS(), CVC3::Expr::getVars(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), null_expr, CVC3::QuantProofRules::partialUniversalInst(), CVC3::RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), CVC3::TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().
void TheoryQuant::enqueueInst | ( | size_t | univ_id, | |
const std::vector< Expr > & | bind, | |||
const Expr & | gterm | |||
) | [private] |
Definition at line 432 of file theory_quant.cpp.
References d_allInstCount, d_bindHistory, d_instThisRound, d_rules, d_simplifiedThmQueue, d_univs, d_useInstLCache, d_useInstTrue, CVC3::Theory::enqueueFact(), FOUND_FALSE, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theorem::getRHS(), CVC3::Expr::getVars(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), null_expr, CVC3::QuantProofRules::partialUniversalInst(), CVC3::RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), CVC3::TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().
void TheoryQuant::synCheckSat | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | , | |
bool | ||||
) | [private] |
Definition at line 4394 of file theory_quant.cpp.
References add_parent(), arrayHeuristic(), collectChangedTerms(), d_allout, d_arrayTrigs, d_callThisRound, d_curMaxExprScore, d_inEnd, d_lastArrayPos, d_lastPredsPos, d_lastTermsPos, d_lastUsefulGtermsPos, d_univs, d_univsSavedPos, d_useExprScore, d_usefulGterms, d_useFullTrig, d_useInstEnd, getExprScore(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), matchListNew(), matchListOld(), sendInstNew(), CVC3::Theory::setIncomplete(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::TRACE, and usefulInMatch().
Referenced by checkSat().
void CVC3::TheoryQuant::synCheckSat | ( | bool | ) | [private] |
void TheoryQuant::semCheckSat | ( | bool | ) | [private] |
void TheoryQuant::naiveCheckSat | ( | bool | ) | [private] |
Definition at line 4578 of file theory_quant.cpp.
References d_contextTerms, d_instCount, d_maxQuantInst, d_savedTerms, d_savedTermsPos, d_univs, d_univsContextPos, d_univsSavedPos, CVC3::CDO< T >::get(), CVC3::TheoryCore::getTerms(), IF_DEBUG, instantiate(), mapTermsByType(), CVC3::CDO< T >::set(), CVC3::Theory::setIncomplete(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), and CVC3::TRACE.
Referenced by checkSat().
bool CVC3::TheoryQuant::insted | ( | const Theorem & | univ, | |
const std::vector< Expr > & | binds | |||
) | [private] |
void CVC3::TheoryQuant::synInst | ( | const Theorem & | univ, | |
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
void CVC3::TheoryQuant::synFullInst | ( | const Theorem & | univ, | |
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
void TheoryQuant::arrayHeuristic | ( | const Trigger & | trig, | |
size_t | univid | |||
) | [private] |
Definition at line 3748 of file theory_quant.cpp.
References d_arrayIndic, enqueueInst(), and CVC3::Trigger::head.
Referenced by synCheckSat().
void TheoryQuant::synNewInst | ( | size_t | univ_id, | |
const std::vector< Expr > & | binds, | |||
const Expr & | gterm, | |||
const Trigger & | trig | |||
) | [private] |
Definition at line 3760 of file theory_quant.cpp.
References backList(), CVC3::TheoryQuant::multTrigsInfo::common_pos, d_all_multTrigsInfo, CVC3::CDMap< Key, Data, HashFcn >::end(), std::endl(), enqueueInst(), FatalAssert, CVC3::CDMap< Key, Data, HashFcn >::find(), forwList(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Trigger::hasT2, CVC3::Trigger::hasTrans, CVC3::Trigger::isMulti, CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, null_expr, CVC3::CDList< T >::push_back(), pushBackList(), pushForwList(), CVC3::RAW_LIST, setTrans2Found(), setTransFound(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), trans2Found(), transFound(), CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::var_binds_found, and CVC3::TheoryQuant::multTrigsInfo::var_pos.
Referenced by matchListNew(), and matchListOld().
void CVC3::TheoryQuant::synMultInst | ( | const Theorem & | univ, | |
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
void CVC3::TheoryQuant::synPartInst | ( | const Theorem & | univ, | |
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
void TheoryQuant::semInst | ( | const Theorem & | univ, | |
size_t | tBegin | |||
) | [private] |
Definition at line 4115 of file theory_quant.cpp.
void TheoryQuant::goodSynMatch | ( | const Expr & | e, | |
const std::vector< Expr > & | boundVars, | |||
std::vector< std::vector< Expr > > & | instBindsTerm, | |||
std::vector< Expr > & | instGterm, | |||
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
Definition at line 3115 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::clear(), DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), recSynMatch(), CVC3::Theory::simplifyExpr(), CVC3::ExprMap< Data >::size(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), CVC3::TRACE, and usefulInMatch().
Referenced by hasGoodSynMultiInst().
void CVC3::TheoryQuant::goodSynMatchNewTrig | ( | const Trigger & | trig, | |
const std::vector< Expr > & | boundVars, | |||
std::vector< std::vector< Expr > > & | instBinds, | |||
std::vector< Expr > & | instGterms, | |||
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
bool CVC3::TheoryQuant::goodSynMatchNewTrig | ( | const Trigger & | trig, | |
const std::vector< Expr > & | boundVars, | |||
std::vector< std::vector< Expr > > & | instBinds, | |||
std::vector< Expr > & | instGterms, | |||
const Expr & | gterm | |||
) | [private] |
void TheoryQuant::matchListOld | ( | const CDList< Expr > & | list, | |
size_t | gbegin, | |||
size_t | gend | |||
) | [private] |
Definition at line 1967 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_allmap_trigs, d_allout, d_univs, FatalAssert, CVC3::ExprMap< Data >::find(), getHead(), CVC3::Expr::getType(), CVC3::Type::isBool(), newTopMatch(), null_expr, and synNewInst().
Referenced by synCheckSat().
void TheoryQuant::matchListNew | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | new_trigs, | |
const CDList< Expr > & | list, | |||
size_t | gbegin, | |||
size_t | gend | |||
) | [private] |
Definition at line 2125 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_univs, FatalAssert, CVC3::ExprMap< Data >::find(), getHead(), CVC3::Expr::getType(), CVC3::Type::isBool(), newTopMatch(), null_expr, and synNewInst().
Referenced by synCheckSat().
void TheoryQuant::delNewTrigs | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | new_trigs | ) | [private] |
Definition at line 2045 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin().
Referenced by checkSat(), and combineOldNewTrigs().
void TheoryQuant::combineOldNewTrigs | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | new_trigs | ) | [private] |
Definition at line 2064 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_allmap_trigs, delNewTrigs(), CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::CDList< T >::push_back(), and CVC3::Theory::theoryCore().
Referenced by checkSat().
void TheoryQuant::newTopMatch | ( | const Expr & | gterm, | |
const Expr & | vterm, | |||
std::vector< ExprMap< Expr > > & | binds, | |||
const Trigger & | trig | |||
) | [private] |
Definition at line 2210 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::BOUND_VAR, d_usePolarity, CVC3::Theory::falseExpr(), FatalAssert, CVC3::Theory::findExpr(), getLeft(), getRight(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::isGE(), CVC3::isGT(), isIntx(), CVC3::isLE(), CVC3::isLT(), CVC3::Trigger::isSimple, CVC3::Trigger::isSuperSimple, isSysPred(), matchChild(), CVC3::Neg, null_expr, CVC3::Trigger::polarity, CVC3::Pos, CVC3::PosNeg, recSynMatch(), CVC3::Theory::simplifyExpr(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::Theory::trueExpr().
Referenced by matchListNew(), and matchListOld().
bool CVC3::TheoryQuant::synMatchTopPred | ( | const Expr & | gterm, | |
const Trigger | trig, | |||
ExprMap< Expr > & | env | |||
) | [private] |
bool TheoryQuant::matchChild | ( | const Expr & | gterm, | |
const Expr & | vterm, | |||
ExprMap< Expr > & | env | |||
) | [inline, private] |
Definition at line 1897 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::BOUND_VAR, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), recSynMatch(), and CVC3::Theory::simplifyExpr().
Referenced by newTopMatch(), and recSynMatch().
void TheoryQuant::matchChild | ( | const Expr & | gterm, | |
const Expr & | vterm, | |||
std::vector< ExprMap< Expr > > & | env | |||
) | [inline, private] |
Definition at line 1929 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::BOUND_VAR, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), recSynMatch(), and CVC3::Theory::simplifyExpr().
void TheoryQuant::add_parent | ( | const Expr & | parent | ) | [inline, private] |
Definition at line 1835 of file theory_quant.cpp.
References d_parent_list, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), MiniSat::parent(), and CVC3::Theory::theoryCore().
Referenced by synCheckSat().
bool TheoryQuant::recSynMatch | ( | const Expr & | gterm, | |
const Expr & | vterm, | |||
ExprMap< Expr > & | env | |||
) | [private] |
Definition at line 2604 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), d_same_head_expr, d_useEqu, DebugAssert, CVC3::ExprMap< Data >::end(), FatalAssert, CVC3::ExprMap< Data >::find(), getHead(), CVC3::Expr::getKind(), CVC3::Expr::isAtomicFormula(), isSysPred(), matchChild(), CVC3::Theory::simplifyExpr(), CVC3::Expr::toString(), and CVC3::TRACE.
Referenced by goodSynMatch(), matchChild(), and newTopMatch().
bool CVC3::TheoryQuant::hasGoodSynInstNewTrigOld | ( | Trigger & | trig, | |
std::vector< Expr > & | boundVars, | |||
std::vector< std::vector< Expr > > & | instBinds, | |||
std::vector< Expr > & | instGterms, | |||
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
bool CVC3::TheoryQuant::hasGoodSynInstNewTrig | ( | Trigger & | trig, | |
const std::vector< Expr > & | boundVars, | |||
std::vector< std::vector< Expr > > & | instBinds, | |||
std::vector< Expr > & | instGterms, | |||
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
bool TheoryQuant::hasGoodSynMultiInst | ( | const Expr & | e, | |
std::vector< Expr > & | bVars, | |||
std::vector< std::vector< Expr > > & | instSet, | |||
const CDList< Expr > & | allterms, | |||
size_t | tBegin | |||
) | [private] |
Definition at line 3326 of file theory_quant.cpp.
References d_mtrigs_bvorder, d_mtrigs_inst, d_multTriggers, getBoundVars(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), goodSynMatch(), searchCover(), and CVC3::Theory::theoryCore().
void TheoryQuant::recGoodSemMatch | ( | const Expr & | e, | |
const std::vector< Expr > & | bVars, | |||
std::vector< Expr > & | newInst, | |||
std::set< std::vector< Expr > > & | instSet | |||
) | [private] |
Definition at line 1725 of file theory_quant.cpp.
References d_typeExprMap, CVC3::Theory::getBaseType(), CVC3::Theory::simplifyExpr(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::TRACE.
bool TheoryQuant::hasGoodSemInst | ( | const Expr & | e, | |
std::vector< Expr > & | bVars, | |||
std::set< std::vector< Expr > > & | instSet, | |||
size_t | tBegin | |||
) | [private] |
Definition at line 3415 of file theory_quant.cpp.
bool TheoryQuant::isTransLike | ( | const std::vector< Expr > & | cur_trig | ) | [private] |
Definition at line 1043 of file theory_quant.cpp.
References canGetHead(), d_useTrans, getBoundVars(), and getHead().
Referenced by setupTriggers().
bool TheoryQuant::isTrans2Like | ( | const std::vector< Expr > & | all_terms, | |
const Expr & | tr2 | |||
) | [private] |
Definition at line 1086 of file theory_quant.cpp.
References d_useTrans2.
Referenced by setupTriggers().
Expr TheoryQuant::recGeneralTrig | ( | const Expr & | trig, | |
ExprMap< Expr > & | bvs, | |||
size_t & | mybvs_count | |||
) | [private] |
Definition at line 976 of file theory_quant.cpp.
References CVC3::Expr::begin(), CVC3::BOUND_VAR, CVC3::Expr::containsBoundVar(), d_mybvs, CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), MAX_TRIG_BVS, and null_expr.
Referenced by generalTrig().
Definition at line 969 of file theory_quant.cpp.
References getBoundVars(), and recGeneralTrig().
Referenced by registerTrig().
void TheoryQuant::registerTrig | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | cur_trig_map, | |
Trigger | trig, | |||
const std::vector< Expr > | thmBVs, | |||
size_t | univ_id | |||
) | [private] |
Definition at line 881 of file theory_quant.cpp.
References d_arrayTrigs, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), generalTrig(), CVC3::Trigger::getEx(), CVC3::Trigger::getHead(), CVC3::Trigger::hasRWOp, and null_expr.
Referenced by setupTriggers().
void CVC3::TheoryQuant::registerTrigReal | ( | Trigger | trig, | |
const std::vector< Expr > | , | |||
size_t | univ_id | |||
) | [private] |
Definition at line 1018 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Theory::getBaseType(), getHead(), and CVC3::Expr::getKind().
Referenced by setupTriggers().
void CVC3::TheoryQuant::setGround | ( | const Expr & | gterm, | |
const Expr & | trig, | |||
const Theorem & | univ, | |||
const std::vector< Expr > & | subTerms | |||
) | [private] |
void TheoryQuant::setupTriggers | ( | const Theorem & | thm, | |
size_t | univ_id | |||
) | [private] |
void TheoryQuant::setupTriggers | ( | ExprMap< ExprMap< std::vector< dynTrig > * > * > & | trig_maps, | |
const Theorem & | thm, | |||
size_t | univs_id | |||
) | [private] |
Definition at line 1139 of file theory_quant.cpp.
References arrayIndexName(), CVC3::BOUND_VAR, canGetHead(), canMatch(), CVC3::TheoryQuant::multTrigsInfo::common_pos, CVC3::ExprMap< Data >::count(), d_all_multTrigsInfo, d_fullTrigs, d_hasTriggers, d_multitrigs_maps, d_multTriggers, d_multTrigs, d_offset_multi_trig, d_partTriggers, d_partTrigs, d_trans2_num, d_trans_num, d_univs, d_usePart, d_usePolarity, d_useTrans2, DebugAssert, CVC3::debugger, std::endl(), exprScore(), CVC3::Theory::findExpr(), findPolarity(), getBoundVars(), CVC3::Theorem::getExpr(), getHead(), getHeadExpr(), getSubTrig(), CVC3::Expr::getType(), CVC3::Expr::getVars(), goodMultiTriggers(), CVC3::Type::isBool(), isGoodFullTrigger(), isGoodMultiTrigger(), isGoodPartTrigger(), isSimpleTrig(), isSuperSimpleTrig(), isSysPred(), isTrans2Like(), isTransLike(), locVar(), CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, CVC3::Neg, CVC3::Pos, CVC3::PosNeg, CVC3::READ, registerTrig(), CVC3::Trigger::setHead(), CVC3::Trigger::setMultiTrig(), CVC3::Trigger::setRWOp(), CVC3::Trigger::setSimp(), CVC3::Trigger::setSuperSimp(), CVC3::Trigger::setTrans(), CVC3::Trigger::setTrans2(), CVC3::Theory::theoryCore(), CVC3::Expr::toString(), CVC3::TRACE, trigInitScore(), CVC3::Ukn, CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::var_binds_found, CVC3::TheoryQuant::multTrigsInfo::var_pos, and CVC3::WRITE.
void TheoryQuant::saveContext | ( | ) | [private] |
Definition at line 4382 of file theory_quant.cpp.
References d_arrayTrigs, d_lastArrayPos, d_lastPredsPos, d_lastTermsPos, d_lastUsefulGtermsPos, d_rawUnivs, d_rawUnivsSavedPos, d_univs, d_univsSavedPos, d_usefulGterms, CVC3::CDO< T >::set(), and CVC3::Theory::theoryCore().
Referenced by checkSat().
QuantProofRules * TheoryQuant::createProofRules | ( | ) |
Destructor.
Definition at line 39 of file quant_theorem_producer.cpp.
References CVC3::Theory::theoryCore().
Referenced by TheoryQuant().
void CVC3::TheoryQuant::addSharedTerm | ( | const Expr & | e | ) | [inline, virtual] |
void TheoryQuant::assertFact | ( | const Theorem & | e | ) | [virtual] |
Theory interface function to assert quantified formulas.
pushes in negations and converts to either universally or existentially quantified theorems. Universals are stored in a database while existentials are enqueued to be handled by the search engine.
Implements CVC3::Theory.
Definition at line 1627 of file theory_quant.cpp.
References CVC3::QuantProofRules::boundVarElim(), d_hasMoreBVs, d_rawUnivs, d_rules, d_translate, d_univs, d_useNew, d_usePullVar, DebugAssert, CVC3::Theory::enqueueFact(), CVC3::Theorem::getExpr(), hasMoreBVs(), CVC3::Theory::iffMP(), CVC3::Expr::isAnd(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isImpl(), CVC3::Expr::isNot(), CVC3::QuantProofRules::packVar(), CVC3::QuantProofRules::pullVarOut(), CVC3::QuantProofRules::rewriteNotExists(), CVC3::QuantProofRules::rewriteNotForall(), setupTriggers(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TRACE.
void TheoryQuant::checkSat | ( | bool | fullEffort | ) | [virtual] |
Check for satisfiability in the theory.
fullEffort | when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing. |
Implements CVC3::Theory.
Definition at line 4118 of file theory_quant.cpp.
References CVC3::QuantProofRules::addNewConst(), arrayIndexName(), canGetHead(), combineOldNewTrigs(), d_eqs, d_inEnd, d_instThisRound, d_lastPredsPos, d_lastTermsPos, d_maxNaiveCall, d_rawUnivs, d_rules, d_same_head_expr, d_simplifiedThmQueue, d_tempBinds, d_translate, d_univs, d_univsQueue, d_useFullTrig, d_useLazyInst, d_useMult, d_useMultTrig, d_useNew, d_usePart, d_usePartTrig, d_useSemMatch, DebugAssert, CVC3::debugger, delNewTrigs(), std::endl(), CVC3::Theory::enqueueFact(), CVC3::Expr::eqExpr(), CVC3::Theory::findExpr(), CVC3::Theory::getEM(), getHead(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), naiveCheckSat(), CVC3::ExprManager::newVarExpr(), CVC3::READ, saveContext(), semCheckSat(), sendInstNew(), CVC3::Expr::setType(), setupTriggers(), CVC3::CDList< T >::size(), synCheckSat(), CVC3::Theory::theoryCore(), and CVC3::WRITE.
void TheoryQuant::setup | ( | const Expr & | e | ) | [virtual] |
Set up the term e for call-backs when e or its children change.
setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.
Reimplemented from CVC3::Theory.
Definition at line 270 of file theory_quant.cpp.
Notify a theory of a new equality.
update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.
To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.
Reimplemented from CVC3::Theory.
Definition at line 272 of file theory_quant.cpp.
void TheoryQuant::notifyInconsistent | ( | const Theorem & | thm | ) | [virtual] |
Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.
Reimplemented from CVC3::Theory.
Definition at line 4813 of file theory_quant.cpp.
References d_savedTerms, d_univs, DebugAssert, CVC3::debugger, std::endl(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Expr::isFalse(), CVC3::Theorem::toString(), CVC3::Assumptions::toString(), and CVC3::TRACE.
void TheoryQuant::computeType | ( | const Expr & | e | ) | [virtual] |
computes the type of a quantified term. Always a boolean.
Reimplemented from CVC3::Theory.
Definition at line 4875 of file theory_quant.cpp.
References DebugAssert, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::setType(), CVC3::Type::toString(), and CVC3::Expr::toString().
TCC(forall x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & !phi(x)) TCC(exists x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & phi(x))
Reimplemented from CVC3::Theory.
Definition at line 4906 of file theory_quant.cpp.
References DebugAssert, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Theory::getTCC(), CVC3::Expr::getVars(), CVC3::Expr::isQuantifier(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
Theory-specific parsing implemented by the DP.
Reimplemented from CVC3::Theory.
Definition at line 5074 of file theory_quant.cpp.
References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::Theory::boolType(), DebugAssert, CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getEM(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::ID, CVC3::ExprManager::newClosureExpr(), CVC3::Theory::parseExpr(), CVC3::RAW_LIST, and CVC3::TRACE.
ExprStream & TheoryQuant::print | ( | ExprStream & | os, | |
const Expr & | e | |||
) | [virtual] |
Theory-specific pretty-printing.
By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer.
Reimplemented from CVC3::Theory.
Definition at line 4921 of file theory_quant.cpp.
References CVC3::Theory::d_theoryUsed, d_translate, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getVars(), CVC3::Expr::isQuantifier(), CVC3::ExprStream::lang(), CVC3::LISP_LANG, CVC3::pop(), CVC3::popdag(), CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::push(), CVC3::pushdag(), CVC3::SIMPLIFY_LANG, CVC3::SMTLIB_LANG, and CVC3::space().
CDList<Theorem> CVC3::TheoryQuant::d_univs [private] |
database of universally quantified theorems
Definition at line 109 of file theory_quant.h.
Referenced by assertFact(), checkSat(), enqueueInst(), mapTermsByType(), matchListNew(), matchListOld(), naiveCheckSat(), notifyInconsistent(), saveContext(), setupTriggers(), synCheckSat(), and TheoryQuant().
CDList<Theorem> CVC3::TheoryQuant::d_rawUnivs [private] |
Definition at line 111 of file theory_quant.h.
Referenced by assertFact(), checkSat(), and saveContext().
CDList<dynTrig> CVC3::TheoryQuant::d_arrayTrigs [private] |
Definition at line 113 of file theory_quant.h.
Referenced by registerTrig(), saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_lastArrayPos [private] |
std::queue<Theorem> CVC3::TheoryQuant::d_univsQueue [private] |
universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground term matched with the trigger is in d_gtermQueue
Definition at line 117 of file theory_quant.h.
Referenced by checkSat().
std::queue<Theorem> CVC3::TheoryQuant::d_simplifiedThmQueue [private] |
Definition at line 119 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
ExprMap<std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_tempBinds [private] |
CDO<size_t> CVC3::TheoryQuant::d_lastPredsPos [private] |
tracks the possition of preds
Definition at line 124 of file theory_quant.h.
Referenced by checkSat(), saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_lastTermsPos [private] |
tracks the possition of terms
Definition at line 126 of file theory_quant.h.
Referenced by checkSat(), saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_lastPartPredsPos [private] |
tracks the positions of preds for partial instantiation
Definition at line 129 of file theory_quant.h.
CDO<size_t> CVC3::TheoryQuant::d_lastPartTermsPos [private] |
tracks the possition of terms for partial instantiation
Definition at line 131 of file theory_quant.h.
CDO<size_t> CVC3::TheoryQuant::d_univsPartSavedPos [private] |
tracks a possition in the database of universals for partial instantiation
Definition at line 133 of file theory_quant.h.
CDO<size_t> CVC3::TheoryQuant::d_lastPartLevel [private] |
the last decision level on which partial instantion is called
Definition at line 136 of file theory_quant.h.
CDList<Expr> CVC3::TheoryQuant::d_usefulGterms [private] |
useful gterms for matching
Definition at line 139 of file theory_quant.h.
Referenced by saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_lastUsefulGtermsPos [private] |
tracks the position in d_usefulGterms
Definition at line 142 of file theory_quant.h.
Referenced by saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_savedTermsPos [private] |
tracks a possition in the savedTerms map
Definition at line 145 of file theory_quant.h.
Referenced by naiveCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_univsSavedPos [private] |
tracks a possition in the database of universals
Definition at line 147 of file theory_quant.h.
Referenced by naiveCheckSat(), saveContext(), and synCheckSat().
CDO<size_t> CVC3::TheoryQuant::d_rawUnivsSavedPos [private] |
CDO<size_t> CVC3::TheoryQuant::d_univsPosFull [private] |
CDO<size_t> CVC3::TheoryQuant::d_univsContextPos [private] |
tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.
Definition at line 153 of file theory_quant.h.
Referenced by naiveCheckSat().
CDO<int> CVC3::TheoryQuant::d_instCount [private] |
number of instantiations made in given context
Definition at line 156 of file theory_quant.h.
Referenced by naiveCheckSat(), recInstantiate(), and TheoryQuant().
int CVC3::TheoryQuant::d_inEnd [private] |
set if the fullEffort = 1
Definition at line 159 of file theory_quant.h.
Referenced by checkSat(), and synCheckSat().
int CVC3::TheoryQuant::d_allout [private] |
std::map<Type, CDList<size_t>* ,TypeComp> CVC3::TheoryQuant::d_contextMap [private] |
a map of types to posisitions in the d_contextTerms list
Definition at line 164 of file theory_quant.h.
Referenced by mapTermsByType(), recInstantiate(), recursiveMap(), and ~TheoryQuant().
CDList<Expr> CVC3::TheoryQuant::d_contextTerms [private] |
a list of all the terms appearing in the current context chache of expressions
Definition at line 167 of file theory_quant.h.
Referenced by instantiate(), mapTermsByType(), naiveCheckSat(), recInstantiate(), and recursiveMap().
CDMap<Expr, bool> CVC3::TheoryQuant::d_contextCache [private] |
typeMap CVC3::TheoryQuant::d_savedMap [private] |
a map of types to positions in the d_savedTerms vector
Definition at line 171 of file theory_quant.h.
Referenced by findInstAssumptions(), and recInstantiate().
ExprMap<bool> CVC3::TheoryQuant::d_savedCache [private] |
cache of expressions
Definition at line 172 of file theory_quant.h.
Referenced by findInstAssumptions(), and recursiveMap().
std::vector<Expr> CVC3::TheoryQuant::d_savedTerms [private] |
a vector of all of the terms that have produced conflicts.
Definition at line 174 of file theory_quant.h.
Referenced by findInstAssumptions(), instantiate(), naiveCheckSat(), notifyInconsistent(), and recInstantiate().
ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_insts [private] |
a map of instantiated universals to a vector of their instantiations
Definition at line 177 of file theory_quant.h.
Referenced by findInstAssumptions(), and recInstantiate().
QuantProofRules* CVC3::TheoryQuant::d_rules [private] |
quantifier theorem production rules
Definition at line 180 of file theory_quant.h.
Referenced by assertFact(), checkSat(), enqueueInst(), recInstantiate(), TheoryQuant(), and ~TheoryQuant().
const int* CVC3::TheoryQuant::d_maxQuantInst [private] |
Command line option.
Definition at line 182 of file theory_quant.h.
Referenced by naiveCheckSat(), and recInstantiate().
const bool* CVC3::TheoryQuant::d_useNew [private] |
const bool* CVC3::TheoryQuant::d_useLazyInst [private] |
use new way of instantiation
Definition at line 222 of file theory_quant.h.
Referenced by checkSat().
const bool* CVC3::TheoryQuant::d_useSemMatch [private] |
const bool* CVC3::TheoryQuant::d_useAtomSem [private] |
const bool* CVC3::TheoryQuant::d_translate [private] |
const bool* CVC3::TheoryQuant::d_useTrigNew [private] |
const bool* CVC3::TheoryQuant::d_usePart [private] |
use new trig class, to be deleted
Definition at line 228 of file theory_quant.h.
Referenced by checkSat(), and setupTriggers().
const bool* CVC3::TheoryQuant::d_useMult [private] |
const bool* CVC3::TheoryQuant::d_useInstEnd [private] |
const bool* CVC3::TheoryQuant::d_useInstLCache [private] |
const bool* CVC3::TheoryQuant::d_useInstGCache [private] |
Definition at line 232 of file theory_quant.h.
const bool* CVC3::TheoryQuant::d_useInstTrue [private] |
const bool* CVC3::TheoryQuant::d_usePullVar [private] |
const bool* CVC3::TheoryQuant::d_useExprScore [private] |
const int* CVC3::TheoryQuant::d_useTrigLoop [private] |
Definition at line 236 of file theory_quant.h.
const int* CVC3::TheoryQuant::d_maxInst [private] |
Definition at line 237 of file theory_quant.h.
const bool* CVC3::TheoryQuant::d_useTrans [private] |
const bool* CVC3::TheoryQuant::d_useTrans2 [private] |
const bool* CVC3::TheoryQuant::d_useInstAll [private] |
Definition at line 241 of file theory_quant.h.
const bool* CVC3::TheoryQuant::d_usePolarity [private] |
const bool* CVC3::TheoryQuant::d_useEqu [private] |
const int* CVC3::TheoryQuant::d_maxNaiveCall [private] |
CDO<int> CVC3::TheoryQuant::d_curMaxExprScore [private] |
bool CVC3::TheoryQuant::d_useFullTrig [private] |
bool CVC3::TheoryQuant::d_usePartTrig [private] |
bool CVC3::TheoryQuant::d_useMultTrig [private] |
CDMap<Expr, std::vector<Expr> > CVC3::TheoryQuant::d_arrayIndic [private] |
Definition at line 253 of file theory_quant.h.
Referenced by arrayHeuristic(), and arrayIndexName().
std::vector<Expr> CVC3::TheoryQuant::d_allInsts [private] |
Definition at line 256 of file theory_quant.h.
int CVC3::TheoryQuant::d_initMaxScore [private] |
int CVC3::TheoryQuant::d_offset_multi_trig [private] |
int CVC3::TheoryQuant::d_instThisRound [private] |
Definition at line 261 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
int CVC3::TheoryQuant::d_callThisRound [private] |
int CVC3::TheoryQuant::partial_called [private] |
Definition at line 264 of file theory_quant.h.
ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_multTriggers [private] |
Definition at line 270 of file theory_quant.h.
Referenced by hasGoodSynMultiInst(), searchCover(), and setupTriggers().
ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_partTriggers [private] |
ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_fullTrigs [private] |
ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_multTrigs [private] |
ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_partTrigs [private] |
CDO<size_t> CVC3::TheoryQuant::d_exprLastUpdatedPos [private] |
Definition at line 279 of file theory_quant.h.
std::map<ExprIndex, int> CVC3::TheoryQuant::d_indexScore [private] |
Definition at line 281 of file theory_quant.h.
std::map<ExprIndex, Expr> CVC3::TheoryQuant::d_indexExpr [private] |
Definition at line 283 of file theory_quant.h.
ExprMap<bool> CVC3::TheoryQuant::d_hasTriggers [private] |
the score for a full trigger
Definition at line 289 of file theory_quant.h.
Referenced by setupTriggers().
ExprMap<bool> CVC3::TheoryQuant::d_hasMoreBVs [private] |
int CVC3::TheoryQuant::d_trans_num [private] |
int CVC3::TheoryQuant::d_trans2_num [private] |
std::vector<multTrigsInfo> CVC3::TheoryQuant::d_all_multTrigsInfo [private] |
ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_trans_back [private] |
ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_trans_forw [private] |
CDMap<Expr,bool > CVC3::TheoryQuant::d_trans_found [private] |
CDMap<Expr,bool > CVC3::TheoryQuant::d_trans2_found [private] |
CDList<Expr> CVC3::TheoryQuant::null_cdlist [private] |
ExprMap<CDList<std::vector<Expr> >* > CVC3::TheoryQuant::d_mtrigs_inst [private] |
Definition at line 333 of file theory_quant.h.
Referenced by hasGoodSynMultiInst(), and recSearchCover().
ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_same_head_expr [private] |
ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_eq_list [private] |
Definition at line 336 of file theory_quant.h.
CDList<Expr > CVC3::TheoryQuant::d_eqs [private] |
CDO<size_t > CVC3::TheoryQuant::d_eqs_pos [private] |
ExprMap<CDO<size_t>* > CVC3::TheoryQuant::d_eq_pos [private] |
Definition at line 341 of file theory_quant.h.
ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_parent_list [private] |
Definition at line 343 of file theory_quant.h.
Referenced by add_parent(), and collectChangedTerms().
ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_mtrigs_bvorder [private] |
Definition at line 345 of file theory_quant.h.
Referenced by hasGoodSynMultiInst(), and loc_gterm().
std::map<Type, std::vector<Expr>,TypeComp > CVC3::TheoryQuant::d_typeExprMap [private] |
std::set<std::string> CVC3::TheoryQuant::cacheHead [private] |
Definition at line 365 of file theory_quant.h.
StatCounter CVC3::TheoryQuant::d_allInstCount [private] |
CDO<bool> CVC3::TheoryQuant::d_partCalled [private] |
std::vector<Theorem> CVC3::TheoryQuant::d_cacheTheorem [private] |
Definition at line 369 of file theory_quant.h.
size_t CVC3::TheoryQuant::d_cacheThmPos [private] |
CDMap<Expr, std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_instHistory [private] |
Definition at line 378 of file theory_quant.h.
ExprMap<CDMap<Expr, bool>* > CVC3::TheoryQuant::d_bindHistory [private] |
ExprMap<std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_instHistoryGlobal [private] |
Definition at line 383 of file theory_quant.h.
ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_subTermsMap [private] |
const size_t CVC3::TheoryQuant::MAX_TRIG_BVS = 15 [static, private] |
Expr CVC3::TheoryQuant::d_mybvs[MAX_TRIG_BVS] [private] |
Definition at line 505 of file theory_quant.h.
Referenced by combineOldNewTrigs(), and matchListOld().
CDList<Trigger> CVC3::TheoryQuant::d_alltrig_list [private] |
Definition at line 507 of file theory_quant.h.