CVC3  2.4.1
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | Static Private Attributes
CVC3::TheoryQuant Class Reference

This theory handles quantifiers. More...

#include <theory_quant.h>

Inheritance diagram for CVC3::TheoryQuant:
CVC3::Theory

List of all members.

Classes

struct  multTrigsInfo
class  TypeComp

Public Member Functions

 TheoryQuant (TheoryCore *core)
 categorizes all the terms contained in an expressions by *type.
 ~TheoryQuant ()
 Destructor.
QuantProofRulescreateProofRules ()
 Destructor.
void addSharedTerm (const Expr &e)
 Theory interface.
void assertFact (const Theorem &e)
 Theory interface function to assert quantified formulas.
void checkSat (bool fullEffort)
 Check for satisfiability in the theory.
void setup (const Expr &e)
 Set up the term e for call-backs when e or its children change.
int help (int i)
void update (const Theorem &e, const Expr &d)
 Notify a theory of a new equality.
void debug (int i)
 Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.
void notifyInconsistent (const Theorem &thm)
 Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.
void computeType (const Expr &e)
 computes the type of a quantified term. Always a boolean.
Expr computeTCC (const Expr &e)
virtual Expr parseExprOp (const Expr &e)
 Theory-specific parsing implemented by the DP.
ExprStreamprint (ExprStream &os, const Expr &e)
 Theory-specific pretty-printing.
- Public Member Functions inherited from CVC3::Theory
 Theory (TheoryCore *theoryCore, const std::string &name)
 Whether theory has been used (for smtlib translator)
virtual ~Theory (void)
 Destructor.
ExprManagergetEM ()
 Access to ExprManager.
TheoryCoretheoryCore ()
 Get a pointer to theoryCore.
CommonProofRulesgetCommonRules ()
 Get a pointer to common proof rules.
const std::string & getName () const
 Get the name of the theory (for debugging purposes)
virtual void setUsed ()
 Set the "used" flag on this theory (for smtlib translator)
virtual bool theoryUsed ()
 Get whether theory has been used (for smtlib translator)
virtual Theorem solve (const Theorem &e)
 An optional solver.
virtual void checkAssertEqInvariant (const Theorem &e)
 A debug check used by the primary solver.
virtual Theorem simplifyOp (const Expr &e)
 Recursive simplification step.
virtual void checkType (const Expr &e)
 Check that e is a valid Type expr.
virtual Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)
 Compute information related to finiteness of types.
virtual Type computeBaseType (const Type &tp)
 Compute the base type of the top-level operator of an arbitrary type.
virtual Expr computeTypePred (const Type &t, const Expr &e)
 Theory specific computation of the subtyping predicate for type t applied to the expression e.
virtual void computeModelTerm (const Expr &e, std::vector< Expr > &v)
 Add variables from 'e' to 'v' for constructing a concrete model.
virtual void refineCounterExample ()
 Process disequalities from the arrangement for model generation.
virtual void computeModelBasic (const std::vector< Expr > &v)
 Assign concrete values to basic-type variables in v.
virtual void computeModel (const Expr &e, std::vector< Expr > &vars)
 Compute the value of a compound variable from the more primitive ones.
virtual void assertTypePred (const Expr &e, const Theorem &pred)
 Receives all the type predicates for the types of the given theory.
virtual Theorem rewriteAtomic (const Expr &e)
 Theory-specific rewrites for atomic formulas.
virtual void registerAtom (const Expr &e, const Theorem &thm)
virtual void registerAtom (const Expr &e)
 Theory-specific registration of atoms.
virtual bool inconsistent ()
 Check if the current context is inconsistent.
virtual void setInconsistent (const Theorem &e)
 Make the context inconsistent; The formula proved by e must FALSE.
virtual void setIncomplete (const std::string &reason)
 Mark the current decision branch as possibly incomplete.
virtual Theorem simplify (const Expr &e)
 Simplify a term e and return a Theorem(e==e')
Expr simplifyExpr (const Expr &e)
 Simplify a term e w.r.t. the current context.
virtual void enqueueFact (const Theorem &e)
 Submit a derived fact to the core from a decision procedure.
virtual void enqueueSE (const Theorem &e)
 Check if the current context is inconsistent.
virtual void assertEqualities (const Theorem &e)
 Handle new equalities (usually asserted through addFact)
virtual Expr parseExpr (const Expr &e)
 Parse the generic expression.
virtual void assignValue (const Expr &t, const Expr &val)
 Assigns t a concrete value val. Used in model generation.
virtual void assignValue (const Theorem &thm)
 Record a derived assignment to a variable (LHS).
void registerKinds (Theory *theory, std::vector< int > &kinds)
 Register new kinds with the given theory.
void unregisterKinds (Theory *theory, std::vector< int > &kinds)
 Unregister kinds for a theory.
void registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
 Register a new theory.
void unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver)
 Unregister a theory.
int getNumTheories ()
 Return the number of registered theories.
bool hasTheory (int kind)
 Test whether a kind maps to any theory.
TheorytheoryOf (int kind)
 Return the theory associated with a kind.
TheorytheoryOf (const Type &e)
 Return the theory associated with a type.
TheorytheoryOf (const Expr &e)
 Return the theory associated with an Expr.
Theorem find (const Expr &e)
 Return the theorem that e is equal to its find.
const TheoremfindRef (const Expr &e)
 Return the find as a reference: expr must have a find.
Theorem findReduce (const Expr &e)
 Return find-reduced version of e.
bool findReduced (const Expr &e)
 Return true iff e is find-reduced.
Expr findExpr (const Expr &e)
 Return the find of e, or e if it has no find.
Expr getTCC (const Expr &e)
 Compute the TCC of e, or the subtyping predicate, if e is a type.
Type getBaseType (const Expr &e)
 Compute (or look up in cache) the base type of e and return the result.
Type getBaseType (const Type &tp)
 Compute the base type from an arbitrary type.
Expr getTypePred (const Type &t, const Expr &e)
 Calls the correct theory to compute a type predicate.
Theorem updateHelper (const Expr &e)
 Update the children of the term e.
void setupCC (const Expr &e)
 Setup a term for congruence closure (must have sig and rep attributes)
void updateCC (const Theorem &e, const Expr &d)
 Update a term w.r.t. congruence closure (must be setup with setupCC())
Theorem rewriteCC (const Expr &e)
 Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
void getModelTerm (const Expr &e, std::vector< Expr > &v)
 Calls the correct theory to get all of the terms that need to be assigned values in the concrete model.
Theorem getModelValue (const Expr &e)
 Fetch the concrete assignment to the variable during model generation.
void addSplitter (const Expr &e, int priority=0)
 Suggest a splitter to the SearchEngine.
void addGlobalLemma (const Theorem &thm, int priority=0)
 Add a global lemma.
bool isLeaf (const Expr &e)
 Test if e is an i-leaf term for the current theory.
bool isLeafIn (const Expr &e1, const Expr &e2)
 Test if e1 is an i-leaf in e2.
bool leavesAreSimp (const Expr &e)
 Test if all i-leaves of e are simplified.
Type boolType ()
 Return BOOLEAN type.
const ExprfalseExpr ()
 Return FALSE Expr.
const ExprtrueExpr ()
 Return TRUE Expr.
Expr newVar (const std::string &name, const Type &type)
 Create a new variable given its name and type.
Expr newVar (const std::string &name, const Type &type, const Expr &def)
 Create a new named expression given its name, type, and definition.
Op newFunction (const std::string &name, const Type &type, bool computeTransClosure)
 Create a new uninterpreted function.
Op lookupFunction (const std::string &name, Type *type)
 Look up a function by name.
Op newFunction (const std::string &name, const Type &type, const Expr &def)
 Create a new defined function.
Expr addBoundVar (const std::string &name, const Type &type)
 Create and add a new bound variable to the stack, for parseExprOp().
Expr addBoundVar (const std::string &name, const Type &type, const Expr &def)
 Create and add a new bound named def to the stack, for parseExprOp().
Expr lookupVar (const std::string &name, Type *type)
 Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Type newTypeExpr (const std::string &name)
 Create a new uninterpreted type with the given name.
Type lookupTypeExpr (const std::string &name)
 Lookup type by name. Return Null if no such type exists.
Type newTypeExpr (const std::string &name, const Type &def)
 Create a new type abbreviation with the given name.
Type newSubtypeExpr (const Expr &pred, const Expr &witness)
 Create a new subtype expression.
Expr resolveID (const std::string &name)
 Resolve an identifier, for use in parseExprOp()
void installID (const std::string &name, const Expr &e)
 Install name as a new identifier associated with Expr e.
Theorem typePred (const Expr &e)
 Return BOOLEAN type.
Theorem reflexivityRule (const Expr &a)
 ==> a == a
Theorem symmetryRule (const Theorem &a1_eq_a2)
 a1 == a2 ==> a2 == a1
Theorem transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
 (a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem substitutivityRule (const Op &op, const std::vector< Theorem > &thms)
 (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Theorem substitutivityRule (const Expr &e, const Theorem &t)
 Special case for unary operators.
Theorem substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2)
 Special case for binary operators.
Theorem substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
 Optimized: only positions which changed are included.
Theorem substitutivityRule (const Expr &e, int changed, const Theorem &thm)
 Optimized: only a single position changed.
Theorem iffMP (const Theorem &e1, const Theorem &e1_iff_e2)
 e1 AND (e1 IFF e2) ==> e2
Theorem rewriteAnd (const Expr &e)
 ==> AND(e1,e2) IFF [simplified expr]
Theorem rewriteOr (const Expr &e)
 ==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIte (const Expr &e)
 Derived rule for rewriting ITE.
Theorem renameExpr (const Expr &e)
 Derived rule to create a new name for an expression.

Private Types

typedef std::map< Type,
std::vector< size_t >
, TypeComp
typeMap
 used to facilitate instantiation of universal quantifiers

Private Member Functions

Theorem rewrite (const Expr &e)
 Theory-specific rewrite rules.
Theorem theoryPreprocess (const Expr &e)
 Theory-specific preprocessing.
bool recursiveMap (const Expr &term)
 categorizes all the terms contained in an expressions by *type.
void mapTermsByType (const CDList< Expr > &terms)
 categorizes all the terms contained in a vector of expressions by type.
void instantiate (Theorem univ, bool all, bool savedMap, size_t newIndex)
 Queues up all possible instantiations of bound variables.
void recInstantiate (Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)
 does most of the work of the instantiate function.
void findInstAssumptions (const Theorem &thm)
 A recursive function used to find instantiated universals in the hierarchy of assumptions.
void arrayIndexName (const Expr &e)
int getExprScore (const Expr &e)
bool transFound (const Expr &comb)
void setTransFound (const Expr &comb)
bool trans2Found (const Expr &comb)
void setTrans2Found (const Expr &comb)
CDList< Expr > & backList (const Expr &ex)
CDList< Expr > & forwList (const Expr &ex)
void iterFWList (const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)
void iterBKList (const Expr &sr, const Expr &dt, size_t univ_id, const Expr &gterm)
Expr getHead (const Expr &e)
Expr getHeadExpr (const Expr &e)
void pushBackList (const Expr &node, Expr ex)
void pushForwList (const Expr &node, Expr ex)
void collectChangedTerms (CDList< Expr > &changed_terms)
int loc_gterm (const std::vector< Expr > &border, const Expr &gterm, int pos)
void 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)
void searchCover (const Expr &thm, const std::vector< Expr > &border, std::vector< std::vector< Expr > > &instSet)
void addNotify (const Expr &e)
int sendInstNew ()
const std::vector< Expr > & getSubTerms (const Expr &e)
void simplifyExprMap (ExprMap< Expr > &orgExprMap)
void simplifyVectorExprMap (std::vector< ExprMap< Expr > > &orgVectorExprMap)
std::string exprMap2string (const ExprMap< Expr > &vec)
std::string exprMap2stringSimplify (const ExprMap< Expr > &vec)
std::string exprMap2stringSig (const ExprMap< Expr > &vec)
void enqueueInst (const Theorem, const Theorem)
void enqueueInst (const Theorem &univ, const std::vector< Expr > &bind, const Expr &gterm)
void enqueueInst (size_t univ_id, const std::vector< Expr > &bind, const Expr &gterm)
void enqueueInst (const Theorem &univ, Trigger &trig, const std::vector< Expr > &binds, const Expr &gterm)
void synCheckSat (ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)
void synCheckSat (bool)
void semCheckSat (bool)
void naiveCheckSat (bool)
bool insted (const Theorem &univ, const std::vector< Expr > &binds)
void synInst (const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void synFullInst (const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void arrayHeuristic (const Trigger &trig, size_t univid)
Expr simpRAWList (const Expr &org)
void synNewInst (size_t univ_id, const std::vector< Expr > &binds, const Expr &gterm, const Trigger &trig)
void synMultInst (const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void synPartInst (const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void semInst (const Theorem &univ, size_t tBegin)
void 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)
void 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)
bool goodSynMatchNewTrig (const Trigger &trig, const std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const Expr &gterm)
void matchListOld (const CDList< Expr > &list, size_t gbegin, size_t gend)
void matchListNew (ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)
void delNewTrigs (ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
void combineOldNewTrigs (ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
void add_parent (const Expr &parent)
void newTopMatch (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void newTopMatchSig (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void newTopMatchNoSig (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void newTopMatchBackupOnly (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
bool synMatchTopPred (const Expr &gterm, const Trigger trig, ExprMap< Expr > &env)
bool recSynMatch (const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)
bool recMultMatch (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
bool recMultMatchDebug (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
bool recMultMatchNewWay (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
bool recMultMatchOldWay (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
bool multMatchChild (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)
bool multMatchTop (const Expr &gterm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
bool recSynMatchBackupOnly (const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)
bool hasGoodSynInstNewTrigOld (Trigger &trig, std::vector< Expr > &boundVars, std::vector< std::vector< Expr > > &instBinds, std::vector< Expr > &instGterms, const CDList< Expr > &allterms, size_t tBegin)
bool 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)
bool hasGoodSynMultiInst (const Expr &e, std::vector< Expr > &bVars, std::vector< std::vector< Expr > > &instSet, const CDList< Expr > &allterms, size_t tBegin)
void recGoodSemMatch (const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)
bool hasGoodSemInst (const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
bool isTransLike (const std::vector< Expr > &cur_trig)
bool isTrans2Like (const std::vector< Expr > &all_terms, const Expr &tr2)
Expr recGeneralTrig (const Expr &trig, ExprMap< Expr > &bvs, size_t &mybvs_count)
Expr generalTrig (const Expr &trig, ExprMap< Expr > &bvs)
void registerTrig (ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)
void registerTrigReal (Trigger trig, const std::vector< Expr >, size_t univ_id)
bool canMatch (const Expr &t1, const Expr &t2, ExprMap< Expr > &env)
void setGround (const Expr &gterm, const Expr &trig, const Theorem &univ, const std::vector< Expr > &subTerms)
void setupTriggers (ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)
void saveContext ()

Private Attributes

CDList< Theoremd_univs
 database of universally quantified theorems
CDList< Theoremd_rawUnivs
CDList< dynTrigd_arrayTrigs
CDO< size_t > d_lastArrayPos
std::queue< Theoremd_univsQueue
 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
std::queue< Theoremd_simplifiedThmQueue
std::queue< Theoremd_gUnivQueue
std::queue< Exprd_gBindQueue
ExprMap< std::set< std::vector
< Expr > > > 
d_tempBinds
CDO< size_t > d_lastPredsPos
 tracks the possition of preds
CDO< size_t > d_lastTermsPos
 tracks the possition of terms
CDO< size_t > d_lastPartPredsPos
 tracks the positions of preds for partial instantiation
CDO< size_t > d_lastPartTermsPos
 tracks the possition of terms for partial instantiation
CDO< size_t > d_univsPartSavedPos
 tracks a possition in the database of universals for partial instantiation
CDO< size_t > d_lastPartLevel
 the last decision level on which partial instantion is called
CDO< bool > d_partCalled
CDO< bool > d_maxILReached
 the max instantiation level reached
CDList< Exprd_usefulGterms
 useful gterms for matching
CDO< size_t > d_lastUsefulGtermsPos
 tracks the position in d_usefulGterms
CDO< size_t > d_savedTermsPos
 tracks a possition in the savedTerms map
CDO< size_t > d_univsSavedPos
 tracks a possition in the database of universals
CDO< size_t > d_rawUnivsSavedPos
CDO< size_t > d_univsPosFull
 tracks a possition in the database of universals
CDO< size_t > d_univsContextPos
 tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.
CDO< int > d_instCount
 number of instantiations made in given context
int d_inEnd
 set if the fullEffort = 1
int d_allout
std::map< Type, CDList< size_t >
*,TypeComp
d_contextMap
 a map of types to posisitions in the d_contextTerms list
CDList< Exprd_contextTerms
 a list of all the terms appearing in the current context
CDMap< Expr, bool > d_contextCache
typeMap d_savedMap
 a map of types to positions in the d_savedTerms vector
ExprMap< bool > d_savedCache
std::vector< Exprd_savedTerms
 a vector of all of the terms that have produced conflicts.
ExprMap< std::vector< Expr > > d_insts
 a map of instantiated universals to a vector of their instantiations
QuantProofRulesd_rules
 quantifier theorem production rules
const int * d_maxQuantInst
 Command line option.
const bool * d_useNew
const bool * d_useLazyInst
 use new way of instantiation
const bool * d_useSemMatch
 use lazy instantiation
const bool * d_useCompleteInst
 use semantic matching
const bool * d_translate
 Try complete instantiation.
const bool * d_usePart
 translate only
const bool * d_useMult
 use partial instantiaion
const bool * d_useInstLCache
const bool * d_useInstGCache
const bool * d_useInstThmCache
const bool * d_useInstTrue
const bool * d_usePullVar
const bool * d_useExprScore
const int * d_useTrigLoop
const int * d_maxInst
const int * d_maxIL
const bool * d_useTrans
const bool * d_useTrans2
const bool * d_useManTrig
const bool * d_useGFact
const int * d_gfactLimit
const bool * d_useInstAll
const bool * d_usePolarity
const bool * d_useEqu
const bool * d_useNewEqu
const int * d_maxNaiveCall
const bool * d_useNaiveInst
CDO< int > d_curMaxExprScore
bool d_useFullTrig
bool d_usePartTrig
bool d_useMultTrig
CDMap< Expr, std::vector< Expr > > d_arrayIndic
std::vector< Exprd_allInsts
int d_initMaxScore
 all instantiations
int d_offset_multi_trig
int d_instThisRound
int d_callThisRound
int partial_called
ExprMap< std::vector< Expr > > d_multTriggers
ExprMap< std::vector< Expr > > d_partTriggers
ExprMap< std::vector< Trigger > > d_fullTrigs
ExprMap< std::vector< Trigger > > d_multTrigs
ExprMap< std::vector< Trigger > > d_partTrigs
CDO< size_t > d_exprLastUpdatedPos
std::map< ExprIndex, int > d_indexScore
std::map< ExprIndex, Exprd_indexExpr
ExprMap< bool > d_hasTriggers
 the score for a full trigger
ExprMap< bool > d_hasMoreBVs
int d_trans_num
int d_trans2_num
ExprMap< multTrigsInfod_multitrigs_maps
std::vector< multTrigsInfod_all_multTrigsInfo
ExprMap< CDList< Expr > * > d_trans_back
ExprMap< CDList< Expr > * > d_trans_forw
CDMap< Expr, bool > d_trans_found
CDMap< Expr, bool > d_trans2_found
Expr defaultWriteExpr
Expr defaultReadExpr
Expr defaultPlusExpr
Expr defaultMinusExpr
Expr defaultMultExpr
Expr defaultDivideExpr
Expr defaultPowExpr
CDList< Exprnull_cdlist
Theorem d_transThm
ExprMap< CDList< std::vector
< Expr > > * > 
d_mtrigs_inst
ExprMap< CDList< Expr > * > d_same_head_expr
ExprMap< CDList< Expr > * > d_eq_list
CDList< Theoremd_eqsUpdate
CDO< size_t > d_lastEqsUpdatePos
CDList< Exprd_eqs
CDO< size_t > d_eqs_pos
ExprMap< CDO< size_t > * > d_eq_pos
ExprMap< CDList< Expr > * > d_parent_list
ExprMap< std::vector< Expr > > d_mtrigs_bvorder
std::map< Type, std::vector
< Expr >, TypeComp
d_typeExprMap
std::set< std::string > cacheHead
StatCounter d_allInstCount
StatCounter d_allInstCount2
StatCounter d_totalInstCount
StatCounter d_trueInstCount
StatCounter d_abInstCount
std::vector< Theoremd_cacheTheorem
size_t d_cacheThmPos
CDMap< Expr, std::set
< std::vector< Expr > > > 
d_instHistory
ExprMap< int > d_thmCount
ExprMap< size_t > d_totalThmCount
ExprMap< CDMap< Expr, bool > * > d_bindHistory
ExprMap< std::hash_map< Expr,
bool > * > 
d_bindGlobalHistory
ExprMap< std::hash_map< Expr,
Theorem > * > 
d_bindGlobalThmHistory
ExprMap< std::set< std::vector
< Expr > > > 
d_instHistoryGlobal
ExprMap< std::vector< Expr > > d_subTermsMap
Expr d_mybvs [MAX_TRIG_BVS]
ExprMap< CDMap< Expr, CDList
< dynTrig > * > * > 
d_allmap_trigs
CDList< Triggerd_alltrig_list

Static Private Attributes

static const size_t MAX_TRIG_BVS = 15

Additional Inherited Members

- Protected Attributes inherited from CVC3::Theory
bool d_theoryUsed

Detailed Description

This theory handles quantifiers.

Author: Daniel Wichs

Created: Wednesday July 2, 2003

Definition at line 186 of file theory_quant.h.


Member Typedef Documentation

typedef std::map<Type, std::vector<size_t>, TypeComp > CVC3::TheoryQuant::typeMap
private

used to facilitate instantiation of universal quantifiers

Definition at line 199 of file theory_quant.h.


Constructor & Destructor Documentation

TheoryQuant::TheoryQuant ( TheoryCore core)
TheoryQuant::~TheoryQuant ( )

Destructor.

Definition at line 234 of file theory_quant.cpp.

References d_contextMap, and d_rules.


Member Function Documentation

Theorem TheoryQuant::rewrite ( const Expr e)
privatevirtual

Theory-specific rewrite rules.

By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done.

Reimplemented from CVC3::Theory.

Definition at line 254 of file theory_quant.cpp.

References d_rules, CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::QuantProofRules::normalizeQuant(), and CVC3::Theory::reflexivityRule().

Theorem TheoryQuant::theoryPreprocess ( const Expr e)
privatevirtual
bool TheoryQuant::recursiveMap ( const Expr e)
private

categorizes all the terms contained in an expressions by *type.

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 8565 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), BOUND_VAR, CVC3::CDMap< Key, Data, HashFcn >::count(), CVC3::ExprMap< Data >::count(), d_contextCache, d_contextMap, d_contextTerms, d_savedCache, CVC3::Expr::end(), EXISTS, FORALL, CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Expr::getKind(), CVC3::Type::isBool(), CVC3::CDList< T >::push_back(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::Type::toString(), CVC3::Expr::toString(), and TRACE.

Referenced by mapTermsByType().

void TheoryQuant::mapTermsByType ( const CDList< Expr > &  terms)
private

categorizes all the terms contained in a vector of expressions by type.

Updates d_contextTerms, d_contextMap, d_contextCache accordingly.

Definition at line 8537 of file theory_quant.cpp.

References CVC3::Theory::boolType(), d_contextMap, d_contextTerms, d_univs, CVC3::Theory::falseExpr(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::CDList< T >::push_back(), 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 8450 of file theory_quant.cpp.

References d_contextTerms, d_savedTerms, recInstantiate(), CVC3::CDList< T >::size(), and TRACE.

Referenced by naiveCheckSat().

void TheoryQuant::recInstantiate ( Theorem univ,
bool  all,
bool  savedMap,
size_t  newIndex,
std::vector< Expr > &  varReplacements 
)
private
void TheoryQuant::findInstAssumptions ( const Theorem thm)
private
void TheoryQuant::arrayIndexName ( const Expr e)
private

Definition at line 2617 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)
inlineprivate
bool TheoryQuant::transFound ( const Expr comb)
inlineprivate

Definition at line 6973 of file theory_quant.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::count(), and d_trans_found.

Referenced by synNewInst().

void TheoryQuant::setTransFound ( const Expr comb)
inlineprivate

Definition at line 6977 of file theory_quant.cpp.

References d_trans_found.

Referenced by synNewInst().

bool TheoryQuant::trans2Found ( const Expr comb)
inlineprivate

Definition at line 6981 of file theory_quant.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::count(), and d_trans2_found.

Referenced by synNewInst().

void TheoryQuant::setTrans2Found ( const Expr comb)
inlineprivate

Definition at line 6985 of file theory_quant.cpp.

References d_trans2_found.

Referenced by synNewInst().

CDList< Expr > & TheoryQuant::backList ( const Expr ex)
inlineprivate

Definition at line 6990 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::count(), d_trans_back, and null_cdlist.

Referenced by iterBKList(), and update().

CDList< Expr > & TheoryQuant::forwList ( const Expr ex)
inlineprivate

Definition at line 6999 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::count(), d_trans_forw, and null_cdlist.

Referenced by iterFWList(), and update().

void TheoryQuant::iterFWList ( const Expr sr,
const Expr dt,
size_t  univ_id,
const Expr gterm 
)
inlineprivate

Definition at line 7224 of file theory_quant.cpp.

References enqueueInst(), forwList(), and CVC3::CDList< T >::size().

Referenced by synNewInst().

void TheoryQuant::iterBKList ( const Expr sr,
const Expr dt,
size_t  univ_id,
const Expr gterm 
)
inlineprivate

Definition at line 7235 of file theory_quant.cpp.

References backList(), enqueueInst(), and CVC3::CDList< T >::size().

Referenced by synNewInst().

Expr TheoryQuant::getHead ( const Expr e)
private
Expr TheoryQuant::getHeadExpr ( const Expr e)
private
void TheoryQuant::pushBackList ( const Expr node,
Expr  ex 
)
inlineprivate
void TheoryQuant::pushForwList ( const Expr node,
Expr  ex 
)
inlineprivate
void TheoryQuant::collectChangedTerms ( CDList< Expr > &  changed_terms)
private
int TheoryQuant::loc_gterm ( const std::vector< Expr > &  border,
const Expr gterm,
int  pos 
)
private

Definition at line 6689 of file theory_quant.cpp.

References d_mtrigs_bvorder, and DebugAssert.

void CVC3::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
void CVC3::TheoryQuant::searchCover ( const Expr thm,
const std::vector< Expr > &  border,
std::vector< std::vector< Expr > > &  instSet 
)
private
void TheoryQuant::addNotify ( const Expr e)
private

Definition at line 1040 of file theory_quant.cpp.

int TheoryQuant::sendInstNew ( )
private
const std::vector< Expr > & TheoryQuant::getSubTerms ( const Expr e)
private
void TheoryQuant::simplifyExprMap ( ExprMap< Expr > &  orgExprMap)
private
void TheoryQuant::simplifyVectorExprMap ( std::vector< ExprMap< Expr > > &  orgVectorExprMap)
private

Definition at line 553 of file theory_quant.cpp.

References simplifyExprMap().

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2string ( const ExprMap< Expr > &  vec)
private

Definition at line 500 of file theory_quant.cpp.

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2stringSimplify ( const ExprMap< Expr > &  vec)
private

Definition at line 514 of file theory_quant.cpp.

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2stringSig ( const ExprMap< Expr > &  vec)
private

Definition at line 526 of file theory_quant.cpp.

Referenced by newTopMatch().

void CVC3::TheoryQuant::enqueueInst ( const Theorem  ,
const Theorem   
)
private
void TheoryQuant::enqueueInst ( const Theorem univ,
const std::vector< Expr > &  bind,
const Expr gterm 
)
private
void TheoryQuant::enqueueInst ( size_t  univ_id,
const std::vector< Expr > &  bind,
const Expr gterm 
)
private
void TheoryQuant::enqueueInst ( const Theorem univ,
Trigger trig,
const std::vector< Expr > &  binds,
const Expr gterm 
)
private

Definition at line 994 of file theory_quant.cpp.

References enqueueInst().

void TheoryQuant::synCheckSat ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  new_trigs,
bool  fullEffort 
)
private
void CVC3::TheoryQuant::synCheckSat ( bool  )
private
void TheoryQuant::semCheckSat ( bool  fullEffort)
private

Definition at line 8381 of file theory_quant.cpp.

Referenced by checkSat().

void TheoryQuant::naiveCheckSat ( bool  fullEffort)
private
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 7212 of file theory_quant.cpp.

References d_arrayIndic, enqueueInst(), and CVC3::Trigger::head.

Referenced by synCheckSat().

Expr TheoryQuant::simpRAWList ( const Expr org)
private

Definition at line 7248 of file theory_quant.cpp.

References CVC3::Expr::arity(), null_expr, RAW_LIST, and CVC3::Theory::simplifyExpr().

Referenced by synNewInst().

void TheoryQuant::synNewInst ( size_t  univ_id,
const std::vector< Expr > &  binds,
const Expr gterm,
const Trigger trig 
)
private
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 CVC3::TheoryQuant::semInst ( const Theorem univ,
size_t  tBegin 
)
private
void CVC3::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
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
void TheoryQuant::matchListNew ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  new_trigs,
const CDList< Expr > &  list,
size_t  gbegin,
size_t  gend 
)
private
void TheoryQuant::delNewTrigs ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  new_trigs)
private
void TheoryQuant::combineOldNewTrigs ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  new_trigs)
private
void TheoryQuant::add_parent ( const Expr parent)
inlineprivate
void TheoryQuant::newTopMatch ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds,
const Trigger trig 
)
private
void TheoryQuant::newTopMatchSig ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds,
const Trigger trig 
)
private
void TheoryQuant::newTopMatchNoSig ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds,
const Trigger trig 
)
private
void CVC3::TheoryQuant::newTopMatchBackupOnly ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds,
const Trigger trig 
)
private
bool CVC3::TheoryQuant::synMatchTopPred ( const Expr gterm,
const Trigger  trig,
ExprMap< Expr > &  env 
)
private
bool CVC3::TheoryQuant::recSynMatch ( const Expr gterm,
const Expr vterm,
ExprMap< Expr > &  env 
)
private
bool TheoryQuant::recMultMatch ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds 
)
private
bool TheoryQuant::recMultMatchDebug ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds 
)
private
bool CVC3::TheoryQuant::recMultMatchNewWay ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds 
)
private
bool TheoryQuant::recMultMatchOldWay ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds 
)
private
bool TheoryQuant::multMatchChild ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds,
bool  top = false 
)
inlineprivate
bool TheoryQuant::multMatchTop ( const Expr gterm,
const Expr vterm,
std::vector< ExprMap< Expr > > &  binds 
)
inlineprivate

Definition at line 4045 of file theory_quant.cpp.

References recMultMatch().

Referenced by newTopMatchNoSig(), and newTopMatchSig().

bool CVC3::TheoryQuant::recSynMatchBackupOnly ( const Expr gterm,
const Expr vterm,
ExprMap< Expr > &  env 
)
private
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 CVC3::TheoryQuant::hasGoodSynMultiInst ( const Expr e,
std::vector< Expr > &  bVars,
std::vector< std::vector< Expr > > &  instSet,
const CDList< Expr > &  allterms,
size_t  tBegin 
)
private
void TheoryQuant::recGoodSemMatch ( const Expr e,
const std::vector< Expr > &  bVars,
std::vector< Expr > &  newInst,
std::set< std::vector< Expr > > &  instSet 
)
private
bool CVC3::TheoryQuant::hasGoodSemInst ( const Expr e,
std::vector< Expr > &  bVars,
std::set< std::vector< Expr > > &  instSet,
size_t  tBegin 
)
private
bool TheoryQuant::isTransLike ( const std::vector< Expr > &  cur_trig)
private

Definition at line 2823 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 2866 of file theory_quant.cpp.

References d_useTrans2.

Referenced by setupTriggers().

Expr CVC3::TheoryQuant::recGeneralTrig ( const Expr trig,
ExprMap< Expr > &  bvs,
size_t &  mybvs_count 
)
private
Expr CVC3::TheoryQuant::generalTrig ( const Expr trig,
ExprMap< Expr > &  bvs 
)
private
void TheoryQuant::registerTrig ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  cur_trig_map,
Trigger  trig,
const std::vector< Expr thmBVs,
size_t  univ_id 
)
private
void CVC3::TheoryQuant::registerTrigReal ( Trigger  trig,
const std::vector< Expr ,
size_t  univ_id 
)
private
bool TheoryQuant::canMatch ( const Expr t1,
const Expr t2,
ExprMap< Expr > &  env 
)
private
void CVC3::TheoryQuant::setGround ( const Expr gterm,
const Expr trig,
const Theorem univ,
const std::vector< Expr > &  subTerms 
)
private
void TheoryQuant::setupTriggers ( ExprMap< ExprMap< std::vector< dynTrig > * > * > &  trig_maps,
const Theorem thm,
size_t  univs_id 
)
private

Definition at line 2917 of file theory_quant.cpp.

References arrayIndexName(), 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_trans2_num, d_trans_num, d_transThm, d_univs, d_useManTrig, d_usePolarity, d_useTrans2, DebugAssert, exprScore(), findPolarity(), getBoundVars(), CVC3::Theorem::getExpr(), getHead(), getHeadExpr(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), getSubTrig(), CVC3::Expr::getTriggers(), CVC3::Expr::getType(), CVC3::Expr::getVars(), goodMultiTriggers(), CVC3::int2string(), CVC3::Type::isBool(), isGoodFullTrigger(), isGoodMultiTrigger(), isSimpleTrig(), isSuperSimpleTrig(), isSysPred(), isTrans2Like(), isTransLike(), locVar(), CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, CVC3::Neg, CVC3::Pos, CVC3::PosNeg, CVC3::CDList< T >::push_back(), 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::ExprMap< Data >::size(), CVC3::Expr::subExprOf(), CVC3::Theory::theoryCore(), CVC3::Expr::toString(), TRACE, trigInitScore(), CVC3::Ukn, CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::univ_id, CVC3::TheoryQuant::multTrigsInfo::univThm, CVC3::TheoryQuant::multTrigsInfo::var_binds_found, CVC3::TheoryQuant::multTrigsInfo::var_pos, and CVC3::WRITE.

Referenced by checkSat().

void TheoryQuant::saveContext ( )
private
QuantProofRules * TheoryQuant::createProofRules ( )

Destructor.

Definition at line 39 of file quant_theorem_producer.cpp.

Referenced by TheoryQuant().

void CVC3::TheoryQuant::addSharedTerm ( const Expr e)
inlinevirtual

Theory interface.

Reimplemented from CVC3::Theory.

Definition at line 728 of file theory_quant.h.

void TheoryQuant::assertFact ( const Theorem thm)
virtual
void TheoryQuant::checkSat ( bool  fullEffort)
virtual

Check for satisfiability in the theory.

Parameters:
fullEffortwhen 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.

If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called.

Implements CVC3::Theory.

Definition at line 7647 of file theory_quant.cpp.

References CVC3::QuantProofRules::addNewConst(), arrayIndexName(), CVC3::ExprMap< Data >::begin(), canGetHead(), CVC3::ExprMap< Data >::clear(), combineOldNewTrigs(), CVC3::ExprMap< Data >::count(), d_abInstCount, d_all_multTrigsInfo, d_eqs, d_eqsUpdate, d_gBindQueue, d_gUnivQueue, d_inEnd, d_instThisRound, d_lastEqsUpdatePos, d_lastPredsPos, d_lastTermsPos, d_maxILReached, d_maxNaiveCall, d_rawUnivs, d_rules, d_same_head_expr, d_simplifiedThmQueue, d_tempBinds, d_translate, d_univs, d_univsQueue, d_useFullTrig, d_useGFact, d_useLazyInst, d_useNaiveInst, d_useNew, d_useSemMatch, DebugAssert, delNewTrigs(), CVC3::ExprMap< Data >::end(), std::endl(), CVC3::Theory::enqueueFact(), enqueueInst(), CVC3::Expr::eqExpr(), FatalAssert, CVC3::Theory::findExpr(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Theory::getEM(), getHead(), CVC3::Expr::getKind(), CVC3::TheoryCore::getPredicates(), CVC3::Theorem::getRHS(), CVC3::TheoryCore::getTerms(), CVC3::Expr::getVars(), CVC3::Expr::isEq(), naiveCheckSat(), CVC3::ExprManager::newVarExpr(), CVC3::CDList< T >::push_back(), CVC3::READ, saveContext(), semCheckSat(), sendInstNew(), CVC3::Expr::setType(), setupTriggers(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::ExprMap< Data >::size(), synCheckSat(), CVC3::Theory::theoryCore(), CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::univ_id, CVC3::TheoryQuant::multTrigsInfo::univThm, 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.

See also:
update

Reimplemented from CVC3::Theory.

Definition at line 337 of file theory_quant.cpp.

int TheoryQuant::help ( int  i)

Definition at line 339 of file theory_quant.cpp.

References d_curMaxExprScore.

void TheoryQuant::update ( const Theorem e,
const Expr d 
)
virtual

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.

See also:
setup

Reimplemented from CVC3::Theory.

Definition at line 419 of file theory_quant.cpp.

References backList(), d_eqsUpdate, forwList(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::CDList< T >::push_back(), CVC3::CDList< T >::size(), and TRACE.

void TheoryQuant::debug ( int  i)
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 8621 of file theory_quant.cpp.

References d_savedTerms, d_univs, DebugAssert, std::endl(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Expr::isFalse(), CVC3::CDList< T >::size(), CVC3::Assumptions::toString(), CVC3::Theorem::toString(), and 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 8683 of file theory_quant.cpp.

References DebugAssert, EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::setType(), CVC3::Type::toString(), and CVC3::Expr::toString().

Expr TheoryQuant::computeTCC ( const Expr e)
virtual

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 8714 of file theory_quant.cpp.

References DebugAssert, EXISTS, 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().

Expr TheoryQuant::parseExprOp ( const Expr e)
virtual
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 8729 of file theory_quant.cpp.

References CVC3::Theory::d_theoryUsed, d_translate, EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getTriggers(), CVC3::Expr::getVars(), CVC3::Expr::isQuantifier(), CVC3::ExprStream::lang(), CVC3::LISP_LANG, CVC3::nodag(), CVC3::pop(), CVC3::popdag(), CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::push(), CVC3::pushdag(), CVC3::SIMPLIFY_LANG, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), and CVC3::TPTP_LANG.


Member Data Documentation

CDList<Theorem> CVC3::TheoryQuant::d_univs
private
CDList<Theorem> CVC3::TheoryQuant::d_rawUnivs
private

Definition at line 204 of file theory_quant.h.

Referenced by assertFact(), checkSat(), and saveContext().

CDList<dynTrig> CVC3::TheoryQuant::d_arrayTrigs
private

Definition at line 206 of file theory_quant.h.

Referenced by registerTrig(), saveContext(), and synCheckSat().

CDO<size_t> CVC3::TheoryQuant::d_lastArrayPos
private

Definition at line 207 of file theory_quant.h.

Referenced by saveContext(), and synCheckSat().

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 210 of file theory_quant.h.

Referenced by checkSat().

std::queue<Theorem> CVC3::TheoryQuant::d_simplifiedThmQueue
private

Definition at line 212 of file theory_quant.h.

Referenced by checkSat(), enqueueInst(), and sendInstNew().

std::queue<Theorem> CVC3::TheoryQuant::d_gUnivQueue
private

Definition at line 214 of file theory_quant.h.

Referenced by checkSat(), enqueueInst(), and sendInstNew().

std::queue<Expr> CVC3::TheoryQuant::d_gBindQueue
private

Definition at line 216 of file theory_quant.h.

Referenced by checkSat(), enqueueInst(), and sendInstNew().

ExprMap<std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_tempBinds
private

Definition at line 219 of file theory_quant.h.

Referenced by checkSat().

CDO<size_t> CVC3::TheoryQuant::d_lastPredsPos
private

tracks the possition of preds

Definition at line 222 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 224 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 227 of file theory_quant.h.

CDO<size_t> CVC3::TheoryQuant::d_lastPartTermsPos
private

tracks the possition of terms for partial instantiation

Definition at line 229 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 231 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 234 of file theory_quant.h.

CDO<bool> CVC3::TheoryQuant::d_partCalled
private

Definition at line 236 of file theory_quant.h.

Referenced by TheoryQuant().

CDO<bool> CVC3::TheoryQuant::d_maxILReached
private

the max instantiation level reached

Definition at line 239 of file theory_quant.h.

Referenced by assertFact(), checkSat(), and synCheckSat().

CDList<Expr> CVC3::TheoryQuant::d_usefulGterms
private

useful gterms for matching

Definition at line 244 of file theory_quant.h.

Referenced by debug(), saveContext(), and synCheckSat().

CDO<size_t> CVC3::TheoryQuant::d_lastUsefulGtermsPos
private

tracks the position in d_usefulGterms

Definition at line 247 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 250 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 252 of file theory_quant.h.

Referenced by naiveCheckSat(), saveContext(), and synCheckSat().

CDO<size_t> CVC3::TheoryQuant::d_rawUnivsSavedPos
private

Definition at line 253 of file theory_quant.h.

Referenced by saveContext().

CDO<size_t> CVC3::TheoryQuant::d_univsPosFull
private

tracks a possition in the database of universals

Definition at line 255 of file theory_quant.h.

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 258 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 261 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 264 of file theory_quant.h.

Referenced by checkSat(), and synCheckSat().

int CVC3::TheoryQuant::d_allout
private

Definition at line 266 of file theory_quant.h.

Referenced by matchListNew(), matchListOld(), and synCheckSat().

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 269 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 272 of file theory_quant.h.

Referenced by instantiate(), mapTermsByType(), naiveCheckSat(), recInstantiate(), and recursiveMap().

CDMap<Expr, bool> CVC3::TheoryQuant::d_contextCache
private

Definition at line 273 of file theory_quant.h.

Referenced by recursiveMap().

typeMap CVC3::TheoryQuant::d_savedMap
private

a map of types to positions in the d_savedTerms vector

Definition at line 276 of file theory_quant.h.

Referenced by findInstAssumptions(), and recInstantiate().

ExprMap<bool> CVC3::TheoryQuant::d_savedCache
private

cache of expressions

Definition at line 277 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 279 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 282 of file theory_quant.h.

Referenced by findInstAssumptions(), and recInstantiate().

QuantProofRules* CVC3::TheoryQuant::d_rules
private

quantifier theorem production rules

Definition at line 285 of file theory_quant.h.

Referenced by assertFact(), checkSat(), enqueueInst(), recInstantiate(), rewrite(), theoryPreprocess(), TheoryQuant(), and ~TheoryQuant().

const int* CVC3::TheoryQuant::d_maxQuantInst
private

Command line option.

Definition at line 287 of file theory_quant.h.

Referenced by naiveCheckSat(), and recInstantiate().

const bool* CVC3::TheoryQuant::d_useNew
private

Definition at line 325 of file theory_quant.h.

Referenced by assertFact(), and checkSat().

const bool* CVC3::TheoryQuant::d_useLazyInst
private

use new way of instantiation

Definition at line 326 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useSemMatch
private

use lazy instantiation

Definition at line 327 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useCompleteInst
private

use semantic matching

Definition at line 328 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_translate
private

Try complete instantiation.

Definition at line 329 of file theory_quant.h.

Referenced by assertFact(), checkSat(), and print().

const bool* CVC3::TheoryQuant::d_usePart
private

translate only

Definition at line 331 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useMult
private

use partial instantiaion

Definition at line 332 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useInstLCache
private

Definition at line 334 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_useInstGCache
private

Definition at line 335 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

const bool* CVC3::TheoryQuant::d_useInstThmCache
private

Definition at line 336 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_useInstTrue
private

Definition at line 337 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_usePullVar
private

Definition at line 338 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useExprScore
private

Definition at line 339 of file theory_quant.h.

Referenced by synCheckSat().

const int* CVC3::TheoryQuant::d_useTrigLoop
private

Definition at line 340 of file theory_quant.h.

const int* CVC3::TheoryQuant::d_maxInst
private

Definition at line 341 of file theory_quant.h.

const int* CVC3::TheoryQuant::d_maxIL
private

Definition at line 343 of file theory_quant.h.

Referenced by synCheckSat().

const bool* CVC3::TheoryQuant::d_useTrans
private

Definition at line 344 of file theory_quant.h.

Referenced by isTransLike().

const bool* CVC3::TheoryQuant::d_useTrans2
private

Definition at line 345 of file theory_quant.h.

Referenced by isTrans2Like(), and setupTriggers().

const bool* CVC3::TheoryQuant::d_useManTrig
private

Definition at line 346 of file theory_quant.h.

Referenced by newTopMatchSig(), and setupTriggers().

const bool* CVC3::TheoryQuant::d_useGFact
private

Definition at line 347 of file theory_quant.h.

Referenced by assertFact(), checkSat(), enqueueInst(), sendInstNew(), and synCheckSat().

const int* CVC3::TheoryQuant::d_gfactLimit
private

Definition at line 348 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

const bool* CVC3::TheoryQuant::d_useInstAll
private

Definition at line 349 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_usePolarity
private

Definition at line 350 of file theory_quant.h.

Referenced by newTopMatchNoSig(), newTopMatchSig(), and setupTriggers().

const bool* CVC3::TheoryQuant::d_useEqu
private

Definition at line 351 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useNewEqu
private

Definition at line 352 of file theory_quant.h.

Referenced by recMultMatch(), recMultMatchDebug(), and synNewInst().

const int* CVC3::TheoryQuant::d_maxNaiveCall
private

Definition at line 353 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useNaiveInst
private

Definition at line 354 of file theory_quant.h.

Referenced by checkSat().

CDO<int> CVC3::TheoryQuant::d_curMaxExprScore
private
bool CVC3::TheoryQuant::d_useFullTrig
private

Definition at line 359 of file theory_quant.h.

Referenced by checkSat(), and synCheckSat().

bool CVC3::TheoryQuant::d_usePartTrig
private

Definition at line 360 of file theory_quant.h.

bool CVC3::TheoryQuant::d_useMultTrig
private

Definition at line 361 of file theory_quant.h.

CDMap<Expr, std::vector<Expr> > CVC3::TheoryQuant::d_arrayIndic
private

Definition at line 364 of file theory_quant.h.

Referenced by arrayHeuristic(), and arrayIndexName().

std::vector<Expr> CVC3::TheoryQuant::d_allInsts
private

Definition at line 367 of file theory_quant.h.

int CVC3::TheoryQuant::d_initMaxScore
private

all instantiations

Definition at line 369 of file theory_quant.h.

Referenced by TheoryQuant().

int CVC3::TheoryQuant::d_offset_multi_trig
private

Definition at line 370 of file theory_quant.h.

Referenced by setupTriggers(), and TheoryQuant().

int CVC3::TheoryQuant::d_instThisRound
private

Definition at line 372 of file theory_quant.h.

Referenced by checkSat(), enqueueInst(), and sendInstNew().

int CVC3::TheoryQuant::d_callThisRound
private

Definition at line 373 of file theory_quant.h.

Referenced by synCheckSat().

int CVC3::TheoryQuant::partial_called
private

Definition at line 375 of file theory_quant.h.

ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_multTriggers
private

Definition at line 381 of file theory_quant.h.

Referenced by setupTriggers().

ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_partTriggers
private

Definition at line 382 of file theory_quant.h.

ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_fullTrigs
private

Definition at line 384 of file theory_quant.h.

Referenced by setupTriggers().

ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_multTrigs
private

Definition at line 386 of file theory_quant.h.

Referenced by setupTriggers().

ExprMap<std::vector<Trigger> > CVC3::TheoryQuant::d_partTrigs
private

Definition at line 387 of file theory_quant.h.

CDO<size_t> CVC3::TheoryQuant::d_exprLastUpdatedPos
private

Definition at line 390 of file theory_quant.h.

std::map<ExprIndex, int> CVC3::TheoryQuant::d_indexScore
private

Definition at line 392 of file theory_quant.h.

std::map<ExprIndex, Expr> CVC3::TheoryQuant::d_indexExpr
private

Definition at line 394 of file theory_quant.h.

ExprMap<bool> CVC3::TheoryQuant::d_hasTriggers
private

the score for a full trigger

Definition at line 400 of file theory_quant.h.

Referenced by setupTriggers().

ExprMap<bool> CVC3::TheoryQuant::d_hasMoreBVs
private

Definition at line 401 of file theory_quant.h.

int CVC3::TheoryQuant::d_trans_num
private

Definition at line 403 of file theory_quant.h.

Referenced by setupTriggers(), and TheoryQuant().

int CVC3::TheoryQuant::d_trans2_num
private

Definition at line 404 of file theory_quant.h.

Referenced by setupTriggers(), and TheoryQuant().

ExprMap<multTrigsInfo> CVC3::TheoryQuant::d_multitrigs_maps
private

Definition at line 417 of file theory_quant.h.

Referenced by setupTriggers().

std::vector<multTrigsInfo> CVC3::TheoryQuant::d_all_multTrigsInfo
private

Definition at line 418 of file theory_quant.h.

Referenced by checkSat(), setupTriggers(), and synNewInst().

ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_trans_back
private

Definition at line 420 of file theory_quant.h.

Referenced by backList(), and pushBackList().

ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_trans_forw
private

Definition at line 421 of file theory_quant.h.

Referenced by forwList(), and pushForwList().

CDMap<Expr,bool > CVC3::TheoryQuant::d_trans_found
private

Definition at line 422 of file theory_quant.h.

Referenced by setTransFound(), and transFound().

CDMap<Expr,bool > CVC3::TheoryQuant::d_trans2_found
private

Definition at line 423 of file theory_quant.h.

Referenced by setTrans2Found(), and trans2Found().

Expr CVC3::TheoryQuant::defaultWriteExpr
private

Definition at line 442 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultReadExpr
private

Definition at line 443 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultPlusExpr
private

Definition at line 444 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultMinusExpr
private

Definition at line 445 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultMultExpr
private

Definition at line 446 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultDivideExpr
private

Definition at line 447 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultPowExpr
private

Definition at line 448 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

CDList<Expr> CVC3::TheoryQuant::null_cdlist
private

Definition at line 455 of file theory_quant.h.

Referenced by backList(), and forwList().

Theorem CVC3::TheoryQuant::d_transThm
private

Definition at line 457 of file theory_quant.h.

Referenced by setupTriggers().

ExprMap<CDList<std::vector<Expr> >* > CVC3::TheoryQuant::d_mtrigs_inst
private

Definition at line 463 of file theory_quant.h.

ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_same_head_expr
private

Definition at line 465 of file theory_quant.h.

Referenced by checkSat(), recMultMatchDebug(), and recMultMatchOldWay().

ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_eq_list
private

Definition at line 466 of file theory_quant.h.

CDList<Theorem> CVC3::TheoryQuant::d_eqsUpdate
private

Definition at line 468 of file theory_quant.h.

Referenced by checkSat(), saveContext(), and update().

CDO<size_t> CVC3::TheoryQuant::d_lastEqsUpdatePos
private

Definition at line 469 of file theory_quant.h.

Referenced by checkSat(), and saveContext().

CDList<Expr > CVC3::TheoryQuant::d_eqs
private

Definition at line 471 of file theory_quant.h.

Referenced by checkSat(), and collectChangedTerms().

CDO<size_t > CVC3::TheoryQuant::d_eqs_pos
private

Definition at line 472 of file theory_quant.h.

Referenced by collectChangedTerms().

ExprMap<CDO<size_t>* > CVC3::TheoryQuant::d_eq_pos
private

Definition at line 474 of file theory_quant.h.

ExprMap<CDList<Expr>* > CVC3::TheoryQuant::d_parent_list
private

Definition at line 476 of file theory_quant.h.

Referenced by add_parent(), and collectChangedTerms().

ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_mtrigs_bvorder
private

Definition at line 478 of file theory_quant.h.

Referenced by loc_gterm().

std::map<Type, std::vector<Expr>,TypeComp > CVC3::TheoryQuant::d_typeExprMap
private

Definition at line 497 of file theory_quant.h.

Referenced by recGoodSemMatch().

std::set<std::string> CVC3::TheoryQuant::cacheHead
private

Definition at line 498 of file theory_quant.h.

StatCounter CVC3::TheoryQuant::d_allInstCount
private

Definition at line 500 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

StatCounter CVC3::TheoryQuant::d_allInstCount2
private

Definition at line 501 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_totalInstCount
private

Definition at line 502 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_trueInstCount
private

Definition at line 503 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_abInstCount
private

Definition at line 504 of file theory_quant.h.

Referenced by checkSat().

std::vector<Theorem> CVC3::TheoryQuant::d_cacheTheorem
private

Definition at line 512 of file theory_quant.h.

size_t CVC3::TheoryQuant::d_cacheThmPos
private

Definition at line 513 of file theory_quant.h.

Referenced by TheoryQuant().

CDMap<Expr, std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_instHistory
private

Definition at line 519 of file theory_quant.h.

ExprMap<int> CVC3::TheoryQuant::d_thmCount
private

Definition at line 522 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

ExprMap<size_t> CVC3::TheoryQuant::d_totalThmCount
private

Definition at line 523 of file theory_quant.h.

Referenced by enqueueInst().

ExprMap<CDMap<Expr, bool>* > CVC3::TheoryQuant::d_bindHistory
private

Definition at line 525 of file theory_quant.h.

Referenced by enqueueInst().

ExprMap<std::hash_map<Expr, bool>* > CVC3::TheoryQuant::d_bindGlobalHistory
private

Definition at line 526 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

ExprMap<std::hash_map<Expr, Theorem>* > CVC3::TheoryQuant::d_bindGlobalThmHistory
private

Definition at line 528 of file theory_quant.h.

Referenced by enqueueInst().

ExprMap<std::set<std::vector<Expr> > > CVC3::TheoryQuant::d_instHistoryGlobal
private

Definition at line 530 of file theory_quant.h.

ExprMap<std::vector<Expr> > CVC3::TheoryQuant::d_subTermsMap
private

Definition at line 533 of file theory_quant.h.

Referenced by getSubTerms().

const size_t CVC3::TheoryQuant::MAX_TRIG_BVS = 15
staticprivate

Definition at line 683 of file theory_quant.h.

Referenced by TheoryQuant().

Expr CVC3::TheoryQuant::d_mybvs[MAX_TRIG_BVS]
private

Definition at line 684 of file theory_quant.h.

Referenced by TheoryQuant().

ExprMap<CDMap<Expr, CDList<dynTrig>* >* > CVC3::TheoryQuant::d_allmap_trigs
private

Definition at line 689 of file theory_quant.h.

Referenced by combineOldNewTrigs(), and matchListOld().

CDList<Trigger> CVC3::TheoryQuant::d_alltrig_list
private

Definition at line 691 of file theory_quant.h.


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