CVC3
2.4.1
|
This theory handles quantifiers. More...
#include <theory_quant.h>
Classes | |
struct | multTrigsInfo |
class | TypeComp |
Public Member Functions | |
TheoryQuant (TheoryCore *core) | |
categorizes all the terms contained in an expressions by type. More... | |
~TheoryQuant () | |
Destructor. More... | |
QuantProofRules * | createProofRules () |
Destructor. More... | |
void | addSharedTerm (const Expr &e) |
Theory interface. More... | |
void | assertFact (const Theorem &e) |
Theory interface function to assert quantified formulas. More... | |
void | checkSat (bool fullEffort) |
Check for satisfiability in the theory. More... | |
void | setup (const Expr &e) |
Set up the term e for call-backs when e or its children change. More... | |
int | help (int i) |
void | update (const Theorem &e, const Expr &d) |
Notify a theory of a new equality. More... | |
void | debug (int i) |
Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent. More... | |
void | notifyInconsistent (const Theorem &thm) |
Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent. More... | |
void | computeType (const Expr &e) |
computes the type of a quantified term. Always a boolean. More... | |
Expr | computeTCC (const Expr &e) |
virtual Expr | parseExprOp (const Expr &e) |
Theory-specific parsing implemented by the DP. More... | |
ExprStream & | print (ExprStream &os, const Expr &e) |
Theory-specific pretty-printing. More... | |
![]() | |
Theory (TheoryCore *theoryCore, const std::string &name) | |
Whether theory has been used (for smtlib translator) More... | |
virtual | ~Theory (void) |
Destructor. More... | |
ExprManager * | getEM () |
Access to ExprManager. More... | |
TheoryCore * | theoryCore () |
Get a pointer to theoryCore. More... | |
CommonProofRules * | getCommonRules () |
Get a pointer to common proof rules. More... | |
const std::string & | getName () const |
Get the name of the theory (for debugging purposes) More... | |
virtual void | setUsed () |
Set the "used" flag on this theory (for smtlib translator) More... | |
virtual bool | theoryUsed () |
Get whether theory has been used (for smtlib translator) More... | |
virtual Theorem | solve (const Theorem &e) |
An optional solver. More... | |
virtual void | checkAssertEqInvariant (const Theorem &e) |
A debug check used by the primary solver. More... | |
virtual Theorem | simplifyOp (const Expr &e) |
Recursive simplification step. More... | |
virtual void | checkType (const Expr &e) |
Check that e is a valid Type expr. More... | |
virtual Cardinality | finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Compute information related to finiteness of types. More... | |
virtual Type | computeBaseType (const Type &tp) |
Compute the base type of the top-level operator of an arbitrary type. More... | |
virtual Expr | computeTypePred (const Type &t, const Expr &e) |
Theory specific computation of the subtyping predicate for type t applied to the expression e. More... | |
virtual void | computeModelTerm (const Expr &e, std::vector< Expr > &v) |
Add variables from 'e' to 'v' for constructing a concrete model. More... | |
virtual void | refineCounterExample () |
Process disequalities from the arrangement for model generation. More... | |
virtual void | computeModelBasic (const std::vector< Expr > &v) |
Assign concrete values to basic-type variables in v. More... | |
virtual void | computeModel (const Expr &e, std::vector< Expr > &vars) |
Compute the value of a compound variable from the more primitive ones. More... | |
virtual void | assertTypePred (const Expr &e, const Theorem &pred) |
Receives all the type predicates for the types of the given theory. More... | |
virtual Theorem | rewriteAtomic (const Expr &e) |
Theory-specific rewrites for atomic formulas. More... | |
virtual void | registerAtom (const Expr &e, const Theorem &thm) |
virtual void | registerAtom (const Expr &e) |
Theory-specific registration of atoms. More... | |
virtual bool | inconsistent () |
Check if the current context is inconsistent. More... | |
virtual void | setInconsistent (const Theorem &e) |
Make the context inconsistent; The formula proved by e must FALSE. More... | |
virtual void | setIncomplete (const std::string &reason) |
Mark the current decision branch as possibly incomplete. More... | |
virtual Theorem | simplify (const Expr &e) |
Simplify a term e and return a Theorem(e==e') More... | |
Expr | simplifyExpr (const Expr &e) |
Simplify a term e w.r.t. the current context. More... | |
virtual void | enqueueFact (const Theorem &e) |
Submit a derived fact to the core from a decision procedure. More... | |
virtual void | enqueueSE (const Theorem &e) |
Check if the current context is inconsistent. More... | |
virtual void | assertEqualities (const Theorem &e) |
Handle new equalities (usually asserted through addFact) More... | |
virtual Expr | parseExpr (const Expr &e) |
Parse the generic expression. More... | |
virtual void | assignValue (const Expr &t, const Expr &val) |
Assigns t a concrete value val. Used in model generation. More... | |
virtual void | assignValue (const Theorem &thm) |
Record a derived assignment to a variable (LHS). More... | |
void | registerKinds (Theory *theory, std::vector< int > &kinds) |
Register new kinds with the given theory. More... | |
void | unregisterKinds (Theory *theory, std::vector< int > &kinds) |
Unregister kinds for a theory. More... | |
void | registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false) |
Register a new theory. More... | |
void | unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver) |
Unregister a theory. More... | |
int | getNumTheories () |
Return the number of registered theories. More... | |
bool | hasTheory (int kind) |
Test whether a kind maps to any theory. More... | |
Theory * | theoryOf (int kind) |
Return the theory associated with a kind. More... | |
Theory * | theoryOf (const Type &e) |
Return the theory associated with a type. More... | |
Theory * | theoryOf (const Expr &e) |
Return the theory associated with an Expr. More... | |
Theorem | find (const Expr &e) |
Return the theorem that e is equal to its find. More... | |
const Theorem & | findRef (const Expr &e) |
Return the find as a reference: expr must have a find. More... | |
Theorem | findReduce (const Expr &e) |
Return find-reduced version of e. More... | |
bool | findReduced (const Expr &e) |
Return true iff e is find-reduced. More... | |
Expr | findExpr (const Expr &e) |
Return the find of e, or e if it has no find. More... | |
Expr | getTCC (const Expr &e) |
Compute the TCC of e, or the subtyping predicate, if e is a type. More... | |
Type | getBaseType (const Expr &e) |
Compute (or look up in cache) the base type of e and return the result. More... | |
Type | getBaseType (const Type &tp) |
Compute the base type from an arbitrary type. More... | |
Expr | getTypePred (const Type &t, const Expr &e) |
Calls the correct theory to compute a type predicate. More... | |
Theorem | updateHelper (const Expr &e) |
Update the children of the term e. More... | |
void | setupCC (const Expr &e) |
Setup a term for congruence closure (must have sig and rep attributes) More... | |
void | updateCC (const Theorem &e, const Expr &d) |
Update a term w.r.t. congruence closure (must be setup with setupCC()) More... | |
Theorem | rewriteCC (const Expr &e) |
Rewrite a term w.r.t. congruence closure (must be setup with setupCC()) More... | |
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. More... | |
Theorem | getModelValue (const Expr &e) |
Fetch the concrete assignment to the variable during model generation. More... | |
void | addSplitter (const Expr &e, int priority=0) |
Suggest a splitter to the SearchEngine. More... | |
void | addGlobalLemma (const Theorem &thm, int priority=0) |
Add a global lemma. More... | |
bool | isLeaf (const Expr &e) |
Test if e is an i-leaf term for the current theory. More... | |
bool | isLeafIn (const Expr &e1, const Expr &e2) |
Test if e1 is an i-leaf in e2. More... | |
bool | leavesAreSimp (const Expr &e) |
Test if all i-leaves of e are simplified. More... | |
Type | boolType () |
Return BOOLEAN type. More... | |
const Expr & | falseExpr () |
Return FALSE Expr. More... | |
const Expr & | trueExpr () |
Return TRUE Expr. More... | |
Expr | newVar (const std::string &name, const Type &type) |
Create a new variable given its name and type. More... | |
Expr | newVar (const std::string &name, const Type &type, const Expr &def) |
Create a new named expression given its name, type, and definition. More... | |
Op | newFunction (const std::string &name, const Type &type, bool computeTransClosure) |
Create a new uninterpreted function. More... | |
Op | lookupFunction (const std::string &name, Type *type) |
Look up a function by name. More... | |
Op | newFunction (const std::string &name, const Type &type, const Expr &def) |
Create a new defined function. More... | |
Expr | addBoundVar (const std::string &name, const Type &type) |
Create and add a new bound variable to the stack, for parseExprOp(). More... | |
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(). More... | |
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. More... | |
Type | newTypeExpr (const std::string &name) |
Create a new uninterpreted type with the given name. More... | |
Type | lookupTypeExpr (const std::string &name) |
Lookup type by name. Return Null if no such type exists. More... | |
Type | newTypeExpr (const std::string &name, const Type &def) |
Create a new type abbreviation with the given name. More... | |
Type | newSubtypeExpr (const Expr &pred, const Expr &witness) |
Create a new subtype expression. More... | |
Expr | resolveID (const std::string &name) |
Resolve an identifier, for use in parseExprOp() More... | |
void | installID (const std::string &name, const Expr &e) |
Install name as a new identifier associated with Expr e. More... | |
Theorem | typePred (const Expr &e) |
Return BOOLEAN type. More... | |
Theorem | reflexivityRule (const Expr &a) |
==> a == a More... | |
Theorem | symmetryRule (const Theorem &a1_eq_a2) |
a1 == a2 ==> a2 == a1 More... | |
Theorem | transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) |
(a1 == a2) & (a2 == a3) ==> (a1 == a3) More... | |
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) More... | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t) |
Special case for unary operators. More... | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2) |
Special case for binary operators. More... | |
Theorem | substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) |
Optimized: only positions which changed are included. More... | |
Theorem | substitutivityRule (const Expr &e, int changed, const Theorem &thm) |
Optimized: only a single position changed. More... | |
Theorem | iffMP (const Theorem &e1, const Theorem &e1_iff_e2) |
e1 AND (e1 IFF e2) ==> e2 More... | |
Theorem | rewriteAnd (const Expr &e) |
==> AND(e1,e2) IFF [simplified expr] More... | |
Theorem | rewriteOr (const Expr &e) |
==> OR(e1,...,en) IFF [simplified expr] More... | |
Theorem | rewriteIte (const Expr &e) |
Derived rule for rewriting ITE. More... | |
Theorem | renameExpr (const Expr &e) |
Derived rule to create a new name for an expression. More... | |
Private Types | |
typedef std::map< Type, std::vector< size_t > , TypeComp > | typeMap |
used to facilitate instantiation of universal quantifiers More... | |
Private Member Functions | |
Theorem | rewrite (const Expr &e) |
Theory-specific rewrite rules. More... | |
Theorem | theoryPreprocess (const Expr &e) |
Theory-specific preprocessing. More... | |
bool | recursiveMap (const Expr &term) |
categorizes all the terms contained in an expressions by type. More... | |
void | mapTermsByType (const CDList< Expr > &terms) |
categorizes all the terms contained in a vector of expressions by type. More... | |
void | instantiate (Theorem univ, bool all, bool savedMap, size_t newIndex) |
Queues up all possible instantiations of bound variables. More... | |
void | recInstantiate (Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements) |
does most of the work of the instantiate function. More... | |
void | findInstAssumptions (const Theorem &thm) |
A recursive function used to find instantiated universals in the hierarchy of assumptions. More... | |
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 >erm) |
void | iterBKList (const Expr &sr, const Expr &dt, size_t univ_id, const Expr >erm) |
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 >erm, 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 >erm) |
void | enqueueInst (size_t univ_id, const std::vector< Expr > &bind, const Expr >erm) |
void | enqueueInst (const Theorem &univ, Trigger &trig, const std::vector< Expr > &binds, const Expr >erm) |
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 >erm, 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 >erm) |
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 >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig) |
void | newTopMatchSig (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig) |
void | newTopMatchNoSig (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig) |
void | newTopMatchBackupOnly (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig) |
bool | synMatchTopPred (const Expr >erm, const Trigger trig, ExprMap< Expr > &env) |
bool | recSynMatch (const Expr >erm, const Expr &vterm, ExprMap< Expr > &env) |
bool | recMultMatch (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds) |
bool | recMultMatchDebug (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds) |
bool | recMultMatchNewWay (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds) |
bool | recMultMatchOldWay (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds) |
bool | multMatchChild (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false) |
bool | multMatchTop (const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds) |
bool | recSynMatchBackupOnly (const Expr >erm, 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 >erm, 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< Theorem > | d_univs |
database of universally quantified theorems More... | |
CDList< Theorem > | d_rawUnivs |
CDList< dynTrig > | d_arrayTrigs |
CDO< size_t > | d_lastArrayPos |
std::queue< Theorem > | d_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 More... | |
std::queue< Theorem > | d_simplifiedThmQueue |
std::queue< Theorem > | d_gUnivQueue |
std::queue< Expr > | d_gBindQueue |
ExprMap< std::set< std::vector < Expr > > > | d_tempBinds |
CDO< size_t > | d_lastPredsPos |
tracks the possition of preds More... | |
CDO< size_t > | d_lastTermsPos |
tracks the possition of terms More... | |
CDO< size_t > | d_lastPartPredsPos |
tracks the positions of preds for partial instantiation More... | |
CDO< size_t > | d_lastPartTermsPos |
tracks the possition of terms for partial instantiation More... | |
CDO< size_t > | d_univsPartSavedPos |
tracks a possition in the database of universals for partial instantiation More... | |
CDO< size_t > | d_lastPartLevel |
the last decision level on which partial instantion is called More... | |
CDO< bool > | d_partCalled |
CDO< bool > | d_maxILReached |
the max instantiation level reached More... | |
CDList< Expr > | d_usefulGterms |
useful gterms for matching More... | |
CDO< size_t > | d_lastUsefulGtermsPos |
tracks the position in d_usefulGterms More... | |
CDO< size_t > | d_savedTermsPos |
tracks a possition in the savedTerms map More... | |
CDO< size_t > | d_univsSavedPos |
tracks a possition in the database of universals More... | |
CDO< size_t > | d_rawUnivsSavedPos |
CDO< size_t > | d_univsPosFull |
tracks a possition in the database of universals More... | |
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. More... | |
CDO< int > | d_instCount |
number of instantiations made in given context More... | |
int | d_inEnd |
set if the fullEffort = 1 More... | |
int | d_allout |
std::map< Type, CDList< size_t > *,TypeComp > | d_contextMap |
a map of types to posisitions in the d_contextTerms list More... | |
CDList< Expr > | d_contextTerms |
a list of all the terms appearing in the current context More... | |
CDMap< Expr, bool > | d_contextCache |
typeMap | d_savedMap |
a map of types to positions in the d_savedTerms vector More... | |
ExprMap< bool > | d_savedCache |
std::vector< Expr > | d_savedTerms |
a vector of all of the terms that have produced conflicts. More... | |
ExprMap< std::vector< Expr > > | d_insts |
a map of instantiated universals to a vector of their instantiations More... | |
QuantProofRules * | d_rules |
quantifier theorem production rules More... | |
const int * | d_maxQuantInst |
Command line option. More... | |
const bool * | d_useNew |
const bool * | d_useLazyInst |
use new way of instantiation More... | |
const bool * | d_useSemMatch |
use lazy instantiation More... | |
const bool * | d_useCompleteInst |
use semantic matching More... | |
const bool * | d_translate |
Try complete instantiation. More... | |
const bool * | d_usePart |
translate only More... | |
const bool * | d_useMult |
use partial instantiaion More... | |
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< Expr > | d_allInsts |
int | d_initMaxScore |
all instantiations More... | |
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, Expr > | d_indexExpr |
ExprMap< bool > | d_hasTriggers |
the score for a full trigger More... | |
ExprMap< bool > | d_hasMoreBVs |
int | d_trans_num |
int | d_trans2_num |
ExprMap< multTrigsInfo > | d_multitrigs_maps |
std::vector< multTrigsInfo > | d_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< Expr > | null_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< Theorem > | d_eqsUpdate |
CDO< size_t > | d_lastEqsUpdatePos |
CDList< Expr > | d_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< Theorem > | d_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< Trigger > | d_alltrig_list |
Static Private Attributes | |
static const size_t | MAX_TRIG_BVS =15 |
Additional Inherited Members | |
![]() | |
bool | d_theoryUsed |
This theory handles quantifiers.
Author: Daniel Wichs
Created: Wednesday July 2, 2003
Definition at line 186 of file theory_quant.h.
|
private |
used to facilitate instantiation of universal quantifiers
Definition at line 199 of file theory_quant.h.
TheoryQuant::TheoryQuant | ( | TheoryCore * | core) |
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.Constructor
core | Constructor |
Definition at line 140 of file theory_quant.cpp.
References CVC3::TheoryCore::addNotifyEq(), 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, defaultDivideExpr, defaultMinusExpr, defaultMultExpr, defaultPlusExpr, defaultPowExpr, defaultReadExpr, defaultWriteExpr, EXISTS, FORALL, CVC3::Theory::getEM(), CVC3::TheoryCore::getFlags(), IF_DEBUG, CVC3::int2string(), MAX_TRIG_BVS, CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newStringExpr(), null_expr, CVC3::Theory::registerTheory(), and CVC3::Theory::theoryCore().
TheoryQuant::~TheoryQuant | ( | ) |
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().
Theory-specific preprocessing.
This gets called each time a new assumption or query is preprocessed. By default it does nothing.
Reimplemented from CVC3::Theory.
Definition at line 2343 of file theory_quant.cpp.
References CVC3::QuantProofRules::addNewConst(), AND, CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::Expr::containsBoundVar(), d_rules, flatAnds(), getBoundVars(), CVC3::CompleteInstPreProcessor::hasMacros(), CVC3::Expr::iffExpr(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::instMacros(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::Theory::reflexivityRule(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CompleteInstPreProcessor::simplifyQuant(), CVC3::Theory::theoryCore(), and CVC3::Theory::trueExpr().
|
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 8565 of file theory_quant.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), BOUND_VAR, 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().
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().
|
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().
|
private |
does most of the work of the instantiate function.
Definition at line 8466 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(), TRACE, and CVC3::QuantProofRules::universalInst().
Referenced by instantiate().
|
private |
A recursive function used to find instantiated universals in the hierarchy of assumptions.
Definition at line 8653 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 TRACE.
|
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().
|
inlineprivate |
Definition at line 274 of file theory_quant.cpp.
References CVC3::TheoryCore::getQuantLevelForTerm(), and CVC3::Theory::theoryCore().
Referenced by debug(), multMatchChild(), recMultMatch(), recMultMatchDebug(), recMultMatchOldWay(), and synCheckSat().
|
inlineprivate |
Definition at line 6973 of file theory_quant.cpp.
References d_trans_found.
Referenced by synNewInst().
|
inlineprivate |
Definition at line 6977 of file theory_quant.cpp.
References d_trans_found.
Referenced by synNewInst().
|
inlineprivate |
Definition at line 6981 of file theory_quant.cpp.
References d_trans2_found.
Referenced by synNewInst().
|
inlineprivate |
Definition at line 6985 of file theory_quant.cpp.
References d_trans2_found.
Referenced by synNewInst().
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().
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().
|
inlineprivate |
Definition at line 7224 of file theory_quant.cpp.
References enqueueInst(), forwList(), and CVC3::CDList< T >::size().
Referenced by synNewInst().
|
inlineprivate |
Definition at line 7235 of file theory_quant.cpp.
References backList(), enqueueInst(), and CVC3::CDList< T >::size().
Referenced by synNewInst().
Definition at line 1106 of file theory_quant.cpp.
References getHeadExpr().
Referenced by canMatch(), checkSat(), isTransLike(), matchListNew(), matchListOld(), multMatchChild(), recMultMatch(), recMultMatchDebug(), recMultMatchOldWay(), and setupTriggers().
Definition at line 1063 of file theory_quant.cpp.
References APPLY, defaultDivideExpr, defaultMinusExpr, defaultMultExpr, defaultPlusExpr, defaultPowExpr, defaultReadExpr, defaultWriteExpr, CVC3::Op::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::isDivide(), CVC3::isMinus(), CVC3::isMult(), CVC3::isPlus(), CVC3::isPow(), null_expr, CVC3::READ, and CVC3::WRITE.
Referenced by getHead(), and setupTriggers().
Definition at line 7008 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::count(), d_trans_back, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), and CVC3::Theory::theoryCore().
Referenced by synNewInst().
Definition at line 7018 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::count(), d_trans_forw, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), and CVC3::Theory::theoryCore().
Referenced by synNewInst().
Definition at line 3828 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_eqs, d_eqs_pos, d_parent_list, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::CDList< T >::push_back(), CVC3::CDO< T >::set(), and CVC3::CDList< T >::size().
Referenced by synCheckSat().
|
private |
Definition at line 6689 of file theory_quant.cpp.
References d_mtrigs_bvorder, and DebugAssert.
|
private |
|
private |
|
private |
Definition at line 1040 of file theory_quant.cpp.
|
private |
Definition at line 998 of file theory_quant.cpp.
References d_allInstCount, d_bindGlobalHistory, d_gBindQueue, d_gfactLimit, d_gUnivQueue, d_instThisRound, d_simplifiedThmQueue, d_thmCount, d_useGFact, d_useInstGCache, CVC3::Theory::enqueueFact(), and CVC3::Theorem::getExpr().
Referenced by checkSat(), and synCheckSat().
Definition at line 613 of file theory_quant.cpp.
References CVC3::Expr::clearFlags(), d_subTermsMap, recGetSubTerms(), and TRACE.
Referenced by arrayIndexName().
Definition at line 545 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::end(), and CVC3::Theory::simplifyExpr().
Referenced by simplifyVectorExprMap().
|
private |
Definition at line 553 of file theory_quant.cpp.
References simplifyExprMap().
Referenced by newTopMatch().
Definition at line 500 of file theory_quant.cpp.
Referenced by newTopMatch().
Definition at line 514 of file theory_quant.cpp.
Referenced by newTopMatch().
Definition at line 526 of file theory_quant.cpp.
Referenced by newTopMatch().
Referenced by arrayHeuristic(), checkSat(), enqueueInst(), iterBKList(), iterFWList(), recInstantiate(), and synNewInst().
|
private |
Definition at line 633 of file theory_quant.cpp.
References d_allInstCount, d_bindHistory, d_gfactLimit, d_instThisRound, d_rules, d_simplifiedThmQueue, d_thmCount, d_totalInstCount, d_totalThmCount, d_trueInstCount, d_useGFact, d_useInstLCache, d_useInstTrue, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::Theory::enqueueFact(), CVC3::CDMap< Key, Data, HashFcn >::find(), FOUND_FALSE, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), 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(), RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().
|
private |
Definition at line 733 of file theory_quant.cpp.
References d_allInstCount, d_allInstCount2, d_bindGlobalHistory, d_bindGlobalThmHistory, d_bindHistory, d_gBindQueue, d_gfactLimit, d_gUnivQueue, d_instThisRound, d_rules, d_simplifiedThmQueue, d_thmCount, d_totalInstCount, d_totalThmCount, d_trueInstCount, d_univs, d_useGFact, d_useInstGCache, d_useInstLCache, d_useInstThmCache, d_useInstTrue, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::Theory::enqueueFact(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::CDMap< Key, Data, HashFcn >::find(), FOUND_FALSE, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), 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(), RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().
|
private |
Definition at line 994 of file theory_quant.cpp.
References enqueueInst().
|
private |
Definition at line 8119 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_maxIL, d_maxILReached, d_univs, d_univsSavedPos, d_useExprScore, d_usefulGterms, d_useFullTrig, d_useGFact, CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), getExprScore(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), matchListNew(), matchListOld(), CVC3::CDList< T >::push_back(), sendInstNew(), CVC3::Theory::setIncomplete(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::Expr::toString(), TRACE, and usefulInMatch().
Referenced by checkSat().
|
private |
|
private |
Definition at line 8381 of file theory_quant.cpp.
Referenced by checkSat().
|
private |
Definition at line 8385 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(), CVC3::int2string(), mapTermsByType(), CVC3::CDO< T >::set(), CVC3::Theory::setIncomplete(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), and TRACE.
Referenced by checkSat().
|
private |
|
private |
|
private |
Definition at line 7212 of file theory_quant.cpp.
References d_arrayIndic, enqueueInst(), and CVC3::Trigger::head.
Referenced by synCheckSat().
Definition at line 7248 of file theory_quant.cpp.
References CVC3::Expr::arity(), null_expr, RAW_LIST, and CVC3::Theory::simplifyExpr().
Referenced by synNewInst().
|
private |
Definition at line 7258 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::TheoryQuant::multTrigsInfo::common_pos, d_all_multTrigsInfo, d_useNewEqu, CVC3::ExprMap< Data >::end(), CVC3::CDMap< Key, Data, HashFcn >::end(), enqueueInst(), FatalAssert, CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Expr::getEqNext(), CVC3::Theorem::getRHS(), CVC3::Trigger::hasT2, CVC3::Trigger::hasTrans, CVC3::Trigger::isMulti, iterBKList(), iterFWList(), CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, null_expr, CVC3::CDList< T >::push_back(), pushBackList(), pushForwList(), RAW_LIST, setTrans2Found(), setTransFound(), CVC3::Theory::simplifyExpr(), simpRAWList(), 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().
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
Definition at line 4075 of file theory_quant.cpp.
References CVC3::CDMap< Key, Data, HashFcn >::begin(), canGetHead(), d_allmap_trigs, d_allout, d_univs, CVC3::CDMap< Key, Data, HashFcn >::end(), FatalAssert, CVC3::ExprMap< Data >::find(), CVC3::Expr::getFind(), getHead(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::Expr::hasFind(), CVC3::Trigger::hasTrans, CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::Trigger::isMulti, CVC3::Theorem::isNull(), CVC3::Trigger::isSuperSimple, newTopMatch(), null_expr, CVC3::CDList< T >::size(), synNewInst(), and CVC3::Trigger::trig.
Referenced by synCheckSat().
|
private |
Definition at line 4271 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_allout, d_univs, CVC3::ExprMap< Data >::end(), FatalAssert, CVC3::ExprMap< Data >::find(), getHead(), CVC3::Expr::getKind(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::Trigger::hasTrans, CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::Theorem::isNull(), CVC3::Trigger::isSuperSimple, newTopMatch(), null_expr, synNewInst(), and CVC3::Trigger::trig.
Referenced by synCheckSat().
|
private |
Definition at line 4191 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::clear(), and CVC3::ExprMap< Data >::end().
Referenced by checkSat(), and combineOldNewTrigs().
|
private |
Definition at line 4210 of file theory_quant.cpp.
References CVC3::ExprMap< Data >::begin(), d_allmap_trigs, delNewTrigs(), CVC3::ExprMap< Data >::end(), 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().
|
inlineprivate |
Definition at line 3813 of file theory_quant.cpp.
References CVC3::Expr::arity(), d_parent_list, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), and CVC3::Theory::theoryCore().
Referenced by synCheckSat().
|
private |
Definition at line 4592 of file theory_quant.cpp.
References std::endl(), exprMap2string(), exprMap2stringSig(), exprMap2stringSimplify(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::hasSig(), CVC3::Expr::isApply(), newTopMatchNoSig(), newTopMatchSig(), and simplifyVectorExprMap().
Referenced by matchListNew(), and matchListOld().
|
private |
Definition at line 4671 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, d_useManTrig, d_usePolarity, std::endl(), CVC3::Theory::falseExpr(), FatalAssert, CVC3::Theory::findExpr(), CVC3::Theory::getBaseType(), getLeft(), CVC3::Theorem::getRHS(), getRight(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::Expr::hasSig(), CVC3::Expr::isApply(), CVC3::Type::isBool(), CVC3::isGE(), CVC3::isGT(), isIntx(), CVC3::isLE(), CVC3::isLT(), CVC3::Trigger::isSimple, CVC3::Trigger::isSuperSimple, isSysPred(), multMatchChild(), multMatchTop(), CVC3::Neg, null_expr, CVC3::Trigger::polarity, CVC3::Pos, CVC3::PosNeg, CVC3::Theory::simplifyExpr(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::trueExpr().
Referenced by newTopMatch().
|
private |
Definition at line 4377 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, d_usePolarity, CVC3::Theory::falseExpr(), FatalAssert, CVC3::Theory::findExpr(), CVC3::Theory::getBaseType(), getLeft(), getRight(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::isGE(), CVC3::isGT(), isIntx(), CVC3::isLE(), CVC3::isLT(), CVC3::Trigger::isSimple, CVC3::Trigger::isSuperSimple, isSysPred(), multMatchChild(), multMatchTop(), CVC3::Neg, null_expr, CVC3::Trigger::polarity, CVC3::Pos, CVC3::PosNeg, CVC3::Theory::simplifyExpr(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::trueExpr().
Referenced by newTopMatch().
|
private |
|
private |
|
private |
|
private |
Definition at line 5587 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), d_curMaxExprScore, d_useNewEqu, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getEqNext(), getExprScore(), getHead(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Expr::isAtomicFormula(), isSysPred(), multMatchChild(), CVC3::Theory::simplifyExpr(), CVC3::Expr::toString(), and TRACE.
Referenced by multMatchChild(), and multMatchTop().
|
private |
Definition at line 5310 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), CVC3::ExprMap< Data >::count(), d_curMaxExprScore, d_same_head_expr, d_useNewEqu, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getEqNext(), getExprScore(), getHead(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::isAtomicFormula(), isSysPred(), multMatchChild(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), and TRACE.
|
private |
|
private |
Definition at line 5478 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), CVC3::ExprMap< Data >::count(), d_curMaxExprScore, d_same_head_expr, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), getExprScore(), getHead(), CVC3::Expr::getKind(), CVC3::Expr::isAtomicFormula(), isSysPred(), multMatchChild(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), and TRACE.
|
inlineprivate |
Definition at line 3950 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, CVC3::Expr::containsBoundVar(), d_curMaxExprScore, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getEqNext(), getExprScore(), getHead(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::hasFind(), CVC3::Expr::isAtomicFormula(), CVC3::Theorem::isNull(), recMultMatch(), CVC3::Theory::simplifyExpr(), and TRACE.
Referenced by newTopMatchNoSig(), newTopMatchSig(), recMultMatch(), recMultMatchDebug(), and recMultMatchOldWay().
|
inlineprivate |
Definition at line 4045 of file theory_quant.cpp.
References recMultMatch().
Referenced by newTopMatchNoSig(), and newTopMatchSig().
|
private |
|
private |
|
private |
|
private |
|
private |
Definition at line 3700 of file theory_quant.cpp.
References d_typeExprMap, CVC3::Theory::getBaseType(), CVC3::Expr::hasFind(), CVC3::Theory::simplifyExpr(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and TRACE.
|
private |
|
private |
Definition at line 2823 of file theory_quant.cpp.
References canGetHead(), d_useTrans, getBoundVars(), and getHead().
Referenced by setupTriggers().
Definition at line 2866 of file theory_quant.cpp.
References d_useTrans2.
Referenced by setupTriggers().
|
private |
|
private |
Definition at line 2638 of file theory_quant.cpp.
References d_arrayTrigs, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Trigger::getEx(), CVC3::Trigger::getHead(), and CVC3::Trigger::hasRWOp.
Referenced by setupTriggers().
|
private |
Definition at line 2798 of file theory_quant.cpp.
References CVC3::Expr::arity(), BOUND_VAR, canGetHead(), CVC3::Theory::getBaseType(), getHead(), and CVC3::Expr::getKind().
Referenced by setupTriggers().
|
private |
|
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::READ, registerTrig(), CVC3::Trigger::setHead(), CVC3::Trigger::setMultiTrig(), CVC3::Trigger::setRWOp(), CVC3::Trigger::setSimp(), CVC3::Trigger::setSuperSimp(), CVC3::Trigger::setTrans(), CVC3::Trigger::setTrans2(), 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().
|
private |
Definition at line 8109 of file theory_quant.cpp.
References d_arrayTrigs, d_eqsUpdate, d_lastArrayPos, d_lastEqsUpdatePos, d_lastPredsPos, d_lastTermsPos, d_lastUsefulGtermsPos, d_rawUnivs, d_rawUnivsSavedPos, d_univs, d_univsSavedPos, d_usefulGterms, CVC3::CDO< T >::set(), CVC3::CDList< T >::size(), and CVC3::Theory::theoryCore().
Referenced by checkSat().
QuantProofRules * TheoryQuant::createProofRules | ( | ) |
|
inlinevirtual |
|
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 3502 of file theory_quant.cpp.
References CVC3::QuantProofRules::boundVarElim(), CVC3::CARD_FINITE, d_maxILReached, d_rawUnivs, d_rules, d_translate, d_univs, d_useGFact, d_useNew, DebugAssert, CVC3::Theory::enqueueFact(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), CVC3::Theory::iffMP(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::QuantProofRules::packVar(), CVC3::QuantProofRules::rewriteNotExists(), CVC3::QuantProofRules::rewriteNotForall(), CVC3::Theorem::toString(), CVC3::Expr::toString(), TRACE, and CVC3::QuantProofRules::universalInst().
|
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. |
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(), 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.
|
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 337 of file theory_quant.cpp.
int TheoryQuant::help | ( | int | i) |
Definition at line 339 of file theory_quant.cpp.
References d_curMaxExprScore.
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 419 of file theory_quant.cpp.
References backList(), d_eqsUpdate, forwList(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::CDList< T >::size(), and TRACE.
void TheoryQuant::debug | ( | int | i) |
Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.
Definition at line 343 of file theory_quant.cpp.
References d_curMaxExprScore, d_usefulGterms, std::endl(), getExprScore(), CVC3::TheoryCore::getPredicates(), CVC3::Expr::getRep(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::TheoryCore::getTerms(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::Expr::isApply(), CVC3::CDList< T >::size(), and CVC3::Theory::theoryCore().
|
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::Assumptions::toString(), CVC3::Theorem::toString(), and TRACE.
|
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().
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().
Theory-specific parsing implemented by the DP.
Reimplemented from CVC3::Theory.
Definition at line 9009 of file theory_quant.cpp.
References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::Theory::boolType(), DebugAssert, CVC3::Expr::end(), EXISTS, FORALL, CVC3::Theory::getEM(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), ID, CVC3::ExprManager::newClosureExpr(), CVC3::Theory::parseExpr(), RAW_LIST, CVC3::Theory::theoryCore(), CVC3::Expr::toString(), and TRACE.
|
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.
database of universally quantified theorems
Definition at line 202 of file theory_quant.h.
Referenced by assertFact(), checkSat(), enqueueInst(), mapTermsByType(), matchListNew(), matchListOld(), naiveCheckSat(), notifyInconsistent(), saveContext(), setupTriggers(), synCheckSat(), and TheoryQuant().
Definition at line 204 of file theory_quant.h.
Referenced by assertFact(), checkSat(), and saveContext().
Definition at line 206 of file theory_quant.h.
Referenced by registerTrig(), saveContext(), and synCheckSat().
|
private |
Definition at line 207 of file theory_quant.h.
Referenced by saveContext(), and synCheckSat().
|
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().
|
private |
Definition at line 212 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
|
private |
Definition at line 214 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
|
private |
Definition at line 216 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
Definition at line 219 of file theory_quant.h.
Referenced by checkSat().
|
private |
tracks the possition of preds
Definition at line 222 of file theory_quant.h.
Referenced by checkSat(), saveContext(), and synCheckSat().
|
private |
tracks the possition of terms
Definition at line 224 of file theory_quant.h.
Referenced by checkSat(), saveContext(), and synCheckSat().
|
private |
tracks the positions of preds for partial instantiation
Definition at line 227 of file theory_quant.h.
|
private |
tracks the possition of terms for partial instantiation
Definition at line 229 of file theory_quant.h.
|
private |
tracks a possition in the database of universals for partial instantiation
Definition at line 231 of file theory_quant.h.
|
private |
the last decision level on which partial instantion is called
Definition at line 234 of file theory_quant.h.
|
private |
Definition at line 236 of file theory_quant.h.
Referenced by TheoryQuant().
|
private |
the max instantiation level reached
Definition at line 239 of file theory_quant.h.
Referenced by assertFact(), checkSat(), and synCheckSat().
useful gterms for matching
Definition at line 244 of file theory_quant.h.
Referenced by debug(), saveContext(), and synCheckSat().
|
private |
tracks the position in d_usefulGterms
Definition at line 247 of file theory_quant.h.
Referenced by saveContext(), and synCheckSat().
|
private |
tracks a possition in the savedTerms map
Definition at line 250 of file theory_quant.h.
Referenced by naiveCheckSat().
|
private |
tracks a possition in the database of universals
Definition at line 252 of file theory_quant.h.
Referenced by naiveCheckSat(), saveContext(), and synCheckSat().
|
private |
Definition at line 253 of file theory_quant.h.
Referenced by saveContext().
|
private |
tracks a possition in the database of universals
Definition at line 255 of file theory_quant.h.
|
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().
|
private |
number of instantiations made in given context
Definition at line 261 of file theory_quant.h.
Referenced by naiveCheckSat(), recInstantiate(), and TheoryQuant().
|
private |
set if the fullEffort = 1
Definition at line 264 of file theory_quant.h.
Referenced by checkSat(), and synCheckSat().
|
private |
Definition at line 266 of file theory_quant.h.
Referenced by matchListNew(), matchListOld(), and synCheckSat().
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().
a list of all the terms appearing in the current context
chache of expressions
Definition at line 271 of file theory_quant.h.
Referenced by instantiate(), mapTermsByType(), naiveCheckSat(), recInstantiate(), and recursiveMap().
Definition at line 273 of file theory_quant.h.
Referenced by recursiveMap().
|
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().
|
private |
cache of expressions
Definition at line 277 of file theory_quant.h.
Referenced by findInstAssumptions(), and recursiveMap().
|
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().
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().
|
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().
|
private |
Command line option.
Definition at line 287 of file theory_quant.h.
Referenced by naiveCheckSat(), and recInstantiate().
|
private |
Definition at line 325 of file theory_quant.h.
Referenced by assertFact(), and checkSat().
|
private |
use new way of instantiation
Definition at line 326 of file theory_quant.h.
Referenced by checkSat().
|
private |
|
private |
use semantic matching
Definition at line 328 of file theory_quant.h.
|
private |
Try complete instantiation.
Definition at line 329 of file theory_quant.h.
Referenced by assertFact(), checkSat(), and print().
|
private |
translate only
Definition at line 331 of file theory_quant.h.
|
private |
use partial instantiaion
Definition at line 332 of file theory_quant.h.
|
private |
Definition at line 334 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 335 of file theory_quant.h.
Referenced by enqueueInst(), and sendInstNew().
|
private |
Definition at line 336 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 337 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 338 of file theory_quant.h.
|
private |
Definition at line 339 of file theory_quant.h.
Referenced by synCheckSat().
|
private |
Definition at line 340 of file theory_quant.h.
|
private |
Definition at line 341 of file theory_quant.h.
|
private |
Definition at line 343 of file theory_quant.h.
Referenced by synCheckSat().
|
private |
Definition at line 344 of file theory_quant.h.
Referenced by isTransLike().
|
private |
Definition at line 345 of file theory_quant.h.
Referenced by isTrans2Like(), and setupTriggers().
|
private |
Definition at line 346 of file theory_quant.h.
Referenced by newTopMatchSig(), and setupTriggers().
|
private |
Definition at line 347 of file theory_quant.h.
Referenced by assertFact(), checkSat(), enqueueInst(), sendInstNew(), and synCheckSat().
|
private |
Definition at line 348 of file theory_quant.h.
Referenced by enqueueInst(), and sendInstNew().
|
private |
Definition at line 349 of file theory_quant.h.
|
private |
Definition at line 350 of file theory_quant.h.
Referenced by newTopMatchNoSig(), newTopMatchSig(), and setupTriggers().
|
private |
Definition at line 351 of file theory_quant.h.
|
private |
Definition at line 352 of file theory_quant.h.
Referenced by recMultMatch(), recMultMatchDebug(), and synNewInst().
|
private |
Definition at line 353 of file theory_quant.h.
Referenced by checkSat().
|
private |
Definition at line 354 of file theory_quant.h.
Referenced by checkSat().
|
private |
Definition at line 357 of file theory_quant.h.
Referenced by debug(), help(), multMatchChild(), recMultMatch(), recMultMatchDebug(), recMultMatchOldWay(), and synCheckSat().
|
private |
Definition at line 359 of file theory_quant.h.
Referenced by checkSat(), and synCheckSat().
|
private |
Definition at line 360 of file theory_quant.h.
|
private |
Definition at line 361 of file theory_quant.h.
Definition at line 364 of file theory_quant.h.
Referenced by arrayHeuristic(), and arrayIndexName().
|
private |
Definition at line 367 of file theory_quant.h.
|
private |
|
private |
Definition at line 370 of file theory_quant.h.
Referenced by setupTriggers(), and TheoryQuant().
|
private |
Definition at line 372 of file theory_quant.h.
Referenced by checkSat(), enqueueInst(), and sendInstNew().
|
private |
Definition at line 373 of file theory_quant.h.
Referenced by synCheckSat().
|
private |
Definition at line 375 of file theory_quant.h.
Definition at line 381 of file theory_quant.h.
Referenced by setupTriggers().
Definition at line 382 of file theory_quant.h.
Definition at line 384 of file theory_quant.h.
Referenced by setupTriggers().
Definition at line 386 of file theory_quant.h.
Referenced by setupTriggers().
Definition at line 387 of file theory_quant.h.
|
private |
Definition at line 390 of file theory_quant.h.
|
private |
Definition at line 392 of file theory_quant.h.
Definition at line 394 of file theory_quant.h.
|
private |
the score for a full trigger
Definition at line 400 of file theory_quant.h.
Referenced by setupTriggers().
|
private |
Definition at line 401 of file theory_quant.h.
|
private |
Definition at line 403 of file theory_quant.h.
Referenced by setupTriggers(), and TheoryQuant().
|
private |
Definition at line 404 of file theory_quant.h.
Referenced by setupTriggers(), and TheoryQuant().
|
private |
Definition at line 417 of file theory_quant.h.
Referenced by setupTriggers().
|
private |
Definition at line 418 of file theory_quant.h.
Referenced by checkSat(), setupTriggers(), and synNewInst().
Definition at line 420 of file theory_quant.h.
Referenced by backList(), and pushBackList().
Definition at line 421 of file theory_quant.h.
Referenced by forwList(), and pushForwList().
Definition at line 422 of file theory_quant.h.
Referenced by setTransFound(), and transFound().
Definition at line 423 of file theory_quant.h.
Referenced by setTrans2Found(), and trans2Found().
|
private |
Definition at line 442 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 443 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 444 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 445 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 446 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 447 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
|
private |
Definition at line 448 of file theory_quant.h.
Referenced by getHeadExpr(), and TheoryQuant().
Definition at line 455 of file theory_quant.h.
Referenced by backList(), and forwList().
|
private |
Definition at line 457 of file theory_quant.h.
Referenced by setupTriggers().
Definition at line 463 of file theory_quant.h.
Definition at line 465 of file theory_quant.h.
Referenced by checkSat(), recMultMatchDebug(), and recMultMatchOldWay().
Definition at line 466 of file theory_quant.h.
Definition at line 468 of file theory_quant.h.
Referenced by checkSat(), saveContext(), and update().
|
private |
Definition at line 469 of file theory_quant.h.
Referenced by checkSat(), and saveContext().
Definition at line 471 of file theory_quant.h.
Referenced by checkSat(), and collectChangedTerms().
|
private |
Definition at line 472 of file theory_quant.h.
Referenced by collectChangedTerms().
Definition at line 474 of file theory_quant.h.
Definition at line 476 of file theory_quant.h.
Referenced by add_parent(), and collectChangedTerms().
Definition at line 478 of file theory_quant.h.
Referenced by loc_gterm().
Definition at line 497 of file theory_quant.h.
Referenced by recGoodSemMatch().
|
private |
Definition at line 498 of file theory_quant.h.
|
private |
Definition at line 500 of file theory_quant.h.
Referenced by enqueueInst(), and sendInstNew().
|
private |
Definition at line 501 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 502 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 503 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 504 of file theory_quant.h.
Referenced by checkSat().
|
private |
Definition at line 512 of file theory_quant.h.
|
private |
Definition at line 513 of file theory_quant.h.
Referenced by TheoryQuant().
Definition at line 519 of file theory_quant.h.
|
private |
Definition at line 522 of file theory_quant.h.
Referenced by enqueueInst(), and sendInstNew().
|
private |
Definition at line 523 of file theory_quant.h.
Referenced by enqueueInst().
Definition at line 525 of file theory_quant.h.
Referenced by enqueueInst().
|
private |
Definition at line 526 of file theory_quant.h.
Referenced by enqueueInst(), and sendInstNew().
|
private |
Definition at line 528 of file theory_quant.h.
Referenced by enqueueInst().
Definition at line 530 of file theory_quant.h.
Definition at line 533 of file theory_quant.h.
Referenced by getSubTerms().
|
staticprivate |
Definition at line 683 of file theory_quant.h.
Referenced by TheoryQuant().
|
private |
Definition at line 684 of file theory_quant.h.
Referenced by TheoryQuant().
Definition at line 689 of file theory_quant.h.
Referenced by combineOldNewTrigs(), and matchListOld().
Definition at line 691 of file theory_quant.h.