CVC3::TheoryQuant Class Reference
[Theories]

This theory handles quantifiers. More...

#include <theory_quant.h>

Inheritance diagram for CVC3::TheoryQuant:

[legend]Collaboration diagram for CVC3::TheoryQuant:

[legend]List of all members.

Public Member Functions

• TheoryQuant (TheoryCore *core)

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

• ~TheoryQuant ()

  Destructor.
  

• QuantProofRules * createProofRules ()

  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.
  

• ExprStream & print (ExprStream &os, const Expr &e)

  Theory-specific pretty-printing.
  

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< Theorem > d_univs

  database of universally quantified theorems
  

• 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
  

• 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
  

• 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< Expr > d_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< Expr > d_contextTerms

  a list of all the terms appearing in the current context chache of expressions
  

• 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< Expr > d_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
  

• QuantProofRules * d_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< Expr > d_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, Expr > d_indexExpr
• ExprMap< bool > d_hasTriggers

  the score for a full trigger
  

• 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

Classes

• struct multTrigsInfo
• class TypeComp

---

Detailed Description

This theory handles quantifiers.

Author: Daniel Wichs

Created: Wednesday July 2, 2003

Definition at line 184 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 197 of file theory_quant.h.

---

Constructor & Destructor Documentation

TheoryQuant::TheoryQuant

(

TheoryCore *

core

)

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

Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.

Parameters:

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, CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getEM(), CVC3::TheoryCore::getFlags(), IF_DEBUG, MAX_TRIG_BVS, CVC3::ExprManager::newStringExpr(), null_expr, CVC3::Theory::registerTheory(), and CVC3::Theory::theoryCore().

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

)

[private, virtual]

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

)

[private, virtual]

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

References CVC3::QuantProofRules::addNewConst(), CVC3::AND, CVC3::CompleteInstPreProcessor::collectIndex(), 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().

bool TheoryQuant::recursiveMap

(

const Expr &

term

)

[private]

categorizes all the terms contained in an expressions by type.

Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.

Definition at line 8433 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BOUND_VAR, CVC3::ExprMap< Data >::count(), CVC3::CDMap< Key, Data, HashFcn >::count(), d_contextCache, d_contextMap, d_contextTerms, d_savedCache, CVC3::Expr::end(), CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Expr::getKind(), CVC3::Type::isBool(), CVC3::CDList< T >::push_back(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::Type::toString(), and CVC3::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 8405 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 8318 of file theory_quant.cpp.

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

Referenced by naiveCheckSat().

void TheoryQuant::recInstantiate	(	Theorem &	univ,
		bool	all,
		bool	savedMap,
		size_t	newIndex,
		std::vector< Expr > &	varReplacements
	)			[private]

does most of the work of the instantiate function.

Definition at line 8334 of file theory_quant.cpp.

References d_contextMap, d_contextTerms, d_instCount, d_insts, d_maxQuantInst, d_rules, d_savedMap, d_savedTerms, enqueueInst(), CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), null_expr, CVC3::CDList< T >::size(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::QuantProofRules::universalInst().

Referenced by instantiate().

void TheoryQuant::findInstAssumptions

(

const Theorem &

thm

)

[private]

A recursive function used to find instantiated universals in the hierarchy of assumptions.

Definition at line 8521 of file theory_quant.cpp.

References CVC3::Assumptions::begin(), CVC3::ExprMap< Data >::count(), d_insts, d_savedCache, d_savedMap, d_savedTerms, CVC3::Assumptions::end(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theorem::isNull(), CVC3::Theorem::isRefl(), CVC3::Theorem::setFlag(), and CVC3::TRACE.

void TheoryQuant::arrayIndexName

(

const Expr &

e

)

[private]

Definition at line 2563 of file theory_quant.cpp.

References d_arrayIndic, getBoundVars(), getSubTerms(), CVC3::READ, and CVC3::WRITE.

Referenced by checkSat().

int TheoryQuant::getExprScore

(

const Expr &

e

)

[inline, private]

Definition at line 274 of file theory_quant.cpp.

References CVC3::TheoryCore::getQuantLevelForTerm(), and CVC3::Theory::theoryCore().

Referenced by debug(), multMatchChild(), recMultMatch(), recMultMatchDebug(), and recMultMatchOldWay().

bool TheoryQuant::transFound

(

const Expr &

comb

)

[inline, private]

Definition at line 6842 of file theory_quant.cpp.

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

void TheoryQuant::setTransFound

(

const Expr &

comb

)

[inline, private]

Definition at line 6846 of file theory_quant.cpp.

References d_trans_found.

bool TheoryQuant::trans2Found

(

const Expr &

comb

)

[inline, private]

Definition at line 6850 of file theory_quant.cpp.

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

void TheoryQuant::setTrans2Found

(

const Expr &

comb

)

[inline, private]

Definition at line 6854 of file theory_quant.cpp.

References d_trans2_found.

CDList< Expr > & TheoryQuant::backList

(

const Expr &

ex

)

[inline, private]

Definition at line 6859 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

)

[inline, private]

Definition at line 6868 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
	)			[inline, private]

Definition at line 7093 of file theory_quant.cpp.

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

void TheoryQuant::iterBKList	(	const Expr &	sr,
		const Expr &	dt,
		size_t	univ_id,
		const Expr &	gterm
	)			[inline, private]

Definition at line 7104 of file theory_quant.cpp.

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

Expr TheoryQuant::getHead

(

const Expr &

e

)

[private]

Definition at line 1099 of file theory_quant.cpp.

References getHeadExpr().

Referenced by canMatch(), checkSat(), isTransLike(), matchListOld(), multMatchChild(), recMultMatch(), recMultMatchDebug(), and recMultMatchOldWay().

Expr TheoryQuant::getHeadExpr

(

const Expr &

e

)

[private]

Definition at line 1056 of file theory_quant.cpp.

References CVC3::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().

void TheoryQuant::pushBackList	(	const Expr &	node,
		Expr	ex
	)			[inline, private]

Definition at line 6877 of file theory_quant.cpp.

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

void TheoryQuant::pushForwList	(	const Expr &	node,
		Expr	ex
	)			[inline, private]

Definition at line 6887 of file theory_quant.cpp.

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

void TheoryQuant::collectChangedTerms

(

CDList< Expr > &

changed_terms

)

[private]

Definition at line 3697 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().

int TheoryQuant::loc_gterm	(	const std::vector< Expr > &	border,
		const Expr &	gterm,
		int	pos
	)			[private]

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

int TheoryQuant::sendInstNew

(

)

[private]

Definition at line 991 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::ExprMap< Data >::end(), CVC3::Theory::enqueueFact(), CVC3::ExprMap< Data >::find(), and CVC3::Theorem::getExpr().

Referenced by checkSat().

const std::vector< Expr > & TheoryQuant::getSubTerms

(

const Expr &

e

)

[private]

Definition at line 606 of file theory_quant.cpp.

References CVC3::Expr::clearFlags(), d_subTermsMap, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), recGetSubTerms(), and CVC3::TRACE.

Referenced by arrayIndexName().

void TheoryQuant::simplifyExprMap

(

ExprMap< Expr > &

orgExprMap

)

[private]

Definition at line 538 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::end(), and CVC3::Theory::simplifyExpr().

Referenced by simplifyVectorExprMap().

void TheoryQuant::simplifyVectorExprMap

(

std::vector< ExprMap< Expr > > &

orgVectorExprMap

)

[private]

Definition at line 546 of file theory_quant.cpp.

References simplifyExprMap().

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2string

(

const ExprMap< Expr > &

vec

)

[private]

Definition at line 493 of file theory_quant.cpp.

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2stringSimplify

(

const ExprMap< Expr > &

vec

)

[private]

Definition at line 507 of file theory_quant.cpp.

Referenced by newTopMatch().

std::string TheoryQuant::exprMap2stringSig

(

const ExprMap< Expr > &

vec

)

[private]

Definition at line 519 of file theory_quant.cpp.

Referenced by newTopMatch().

void CVC3::TheoryQuant::enqueueInst	(	const	Theorem,
		const	Theorem
	)			[private]

Referenced by arrayHeuristic(), checkSat(), enqueueInst(), iterBKList(), iterFWList(), recInstantiate(), and synNewInst().

void TheoryQuant::enqueueInst	(	const Theorem &	univ,
		const std::vector< Expr > &	bind,
		const Expr &	gterm
	)			[private]

Definition at line 626 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::ExprMap< Data >::end(), CVC3::Theory::enqueueFact(), CVC3::ExprMap< Data >::find(), FOUND_FALSE, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theorem::getRHS(), CVC3::Expr::getVars(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), null_expr, CVC3::QuantProofRules::partialUniversalInst(), CVC3::RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), CVC3::TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().

void TheoryQuant::enqueueInst	(	size_t	univ_id,
		const std::vector< Expr > &	bind,
		const Expr &	gterm
	)			[private]

Definition at line 726 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, CVC3::ExprMap< Data >::end(), CVC3::Theory::enqueueFact(), CVC3::ExprMap< Data >::find(), FOUND_FALSE, CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theorem::getRHS(), CVC3::Expr::getVars(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), null_expr, CVC3::QuantProofRules::partialUniversalInst(), CVC3::RAW_LIST, CVC3::Theory::simplify(), CVC3::Theory::simplifyExpr(), CVC3::Theory::theoryCore(), CVC3::TRACE, CVC3::QuantProofRules::universalInst(), and vectorExpr2string().

void TheoryQuant::enqueueInst	(	const Theorem &	univ,
		Trigger &	trig,
		const std::vector< Expr > &	binds,
		const Expr &	gterm
	)			[private]

Definition at line 987 of file theory_quant.cpp.

References enqueueInst().

void CVC3::TheoryQuant::synCheckSat	(	ExprMap< ExprMap< std::vector< dynTrig > * > * > &	,
		bool
	)			[private]

Referenced by checkSat().

void CVC3::TheoryQuant::synCheckSat

(

bool

)

[private]

void TheoryQuant::semCheckSat

(

bool

)

[private]

Definition at line 8249 of file theory_quant.cpp.

Referenced by checkSat().

void TheoryQuant::naiveCheckSat

(

bool

)

[private]

Definition at line 8253 of file theory_quant.cpp.

References d_contextTerms, d_instCount, d_maxQuantInst, d_savedTerms, d_savedTermsPos, d_univs, d_univsContextPos, d_univsSavedPos, CVC3::CDO< T >::get(), CVC3::TheoryCore::getTerms(), IF_DEBUG, instantiate(), mapTermsByType(), CVC3::CDO< T >::set(), CVC3::Theory::setIncomplete(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), and CVC3::TRACE.

Referenced by checkSat().

bool CVC3::TheoryQuant::insted	(	const Theorem &	univ,
		const std::vector< Expr > &	binds
	)			[private]

void CVC3::TheoryQuant::synInst	(	const Theorem &	univ,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)			[private]

void CVC3::TheoryQuant::synFullInst	(	const Theorem &	univ,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)			[private]

void TheoryQuant::arrayHeuristic	(	const Trigger &	trig,
		size_t	univid
	)			[private]

Definition at line 7081 of file theory_quant.cpp.

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

Expr TheoryQuant::simpRAWList

(

const Expr &

org

)

[private]

Definition at line 7117 of file theory_quant.cpp.

References CVC3::Expr::arity(), null_expr, CVC3::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]

Definition at line 7127 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::TheoryQuant::multTrigsInfo::common_pos, d_all_multTrigsInfo, 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::Trigger::isMulti, CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, null_expr, CVC3::CDList< T >::push_back(), CVC3::RAW_LIST, simpRAWList(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::var_binds_found, and CVC3::TheoryQuant::multTrigsInfo::var_pos.

Referenced by matchListOld().

void CVC3::TheoryQuant::synMultInst	(	const Theorem &	univ,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)			[private]

void CVC3::TheoryQuant::synPartInst	(	const Theorem &	univ,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)			[private]

void 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]

Definition at line 3944 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), canGetHead(), d_allmap_trigs, d_allout, d_univs, CVC3::ExprMap< Data >::end(), FatalAssert, CVC3::ExprMap< Data >::find(), getHead(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isBool(), newTopMatch(), null_expr, CVC3::CDList< T >::push_back(), and synNewInst().

void CVC3::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]

Definition at line 4060 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin().

Referenced by checkSat(), and combineOldNewTrigs().

void TheoryQuant::combineOldNewTrigs

(

ExprMap< ExprMap< std::vector< dynTrig > * > * > &

new_trigs

)

[private]

Definition at line 4079 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), d_allmap_trigs, delNewTrigs(), CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::ExprMap< Data >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::ExprMap< Data >::find(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::CDList< T >::push_back(), and CVC3::Theory::theoryCore().

Referenced by checkSat().

void TheoryQuant::add_parent

(

const Expr &

parent

)

[inline, private]

Definition at line 3682 of file theory_quant.cpp.

References d_parent_list, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), MiniSat::parent(), and CVC3::Theory::theoryCore().

void TheoryQuant::newTopMatch	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds,
		const Trigger &	trig
	)			[private]

Definition at line 4461 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 matchListOld().

void TheoryQuant::newTopMatchSig	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds,
		const Trigger &	trig
	)			[private]

Definition at line 4540 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::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(), CVC3::TRACE, and CVC3::Theory::trueExpr().

Referenced by newTopMatch().

void TheoryQuant::newTopMatchNoSig	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds,
		const Trigger &	trig
	)			[private]

Definition at line 4246 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::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(), CVC3::TRACE, and CVC3::Theory::trueExpr().

Referenced by newTopMatch().

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]

Definition at line 5456 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), d_curMaxExprScore, d_useNewEqu, DebugAssert, CVC3::ExprMap< Data >::end(), 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 CVC3::TRACE.

Referenced by multMatchChild(), and multMatchTop().

bool TheoryQuant::recMultMatchDebug	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds
	)			[private]

Definition at line 5179 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), CVC3::ExprMap< Data >::count(), d_curMaxExprScore, d_same_head_expr, d_useNewEqu, DebugAssert, CVC3::ExprMap< Data >::end(), 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 CVC3::TRACE.

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]

Definition at line 5347 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Expr::containsBoundVar(), CVC3::ExprMap< Data >::count(), d_curMaxExprScore, d_same_head_expr, DebugAssert, CVC3::ExprMap< Data >::end(), getExprScore(), getHead(), CVC3::Expr::getKind(), CVC3::Expr::isAtomicFormula(), isSysPred(), multMatchChild(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::Expr::toString(), and CVC3::TRACE.

bool TheoryQuant::multMatchChild	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds,
		bool	top = false
	)			[inline, private]

Definition at line 3819 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, d_curMaxExprScore, CVC3::Expr::getEqNext(), getExprScore(), getHead(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::hasFind(), CVC3::Expr::isAtomicFormula(), CVC3::Theorem::isNull(), recMultMatch(), CVC3::Theory::simplifyExpr(), and CVC3::TRACE.

Referenced by newTopMatchNoSig(), newTopMatchSig(), recMultMatch(), recMultMatchDebug(), and recMultMatchOldWay().

bool TheoryQuant::multMatchTop	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds
	)			[inline, private]

Definition at line 3914 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]

Definition at line 3569 of file theory_quant.cpp.

References d_typeExprMap, CVC3::Theory::getBaseType(), CVC3::Theory::simplifyExpr(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::TRACE.

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

References canGetHead(), d_useTrans, getBoundVars(), and getHead().

bool TheoryQuant::isTrans2Like	(	const std::vector< Expr > &	all_terms,
		const Expr &	tr2
	)			[private]

Definition at line 2812 of file theory_quant.cpp.

References d_useTrans2.

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]

Definition at line 2584 of file theory_quant.cpp.

References d_arrayTrigs, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Trigger::getEx(), CVC3::Trigger::getHead(), CVC3::Trigger::hasRWOp, and CVC3::CDList< T >::push_back().

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]

Definition at line 2744 of file theory_quant.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, canGetHead(), CVC3::Theory::getBaseType(), getHead(), and CVC3::Expr::getKind().

void CVC3::TheoryQuant::setGround	(	const Expr &	gterm,
		const Expr &	trig,
		const Theorem &	univ,
		const std::vector< Expr > &	subTerms
	)			[private]

void CVC3::TheoryQuant::setupTriggers	(	ExprMap< ExprMap< std::vector< dynTrig > * > * > &	trig_maps,
		const Theorem &	thm,
		size_t	univs_id
	)			[private]

Referenced by checkSat().

void TheoryQuant::saveContext

(

)

[private]

Definition at line 7977 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

(

)

Destructor.

Definition at line 39 of file quant_theorem_producer.cpp.

References CVC3::Theory::theoryCore().

Referenced by TheoryQuant().

void CVC3::TheoryQuant::addSharedTerm

(

const Expr &

e

)

[inline, virtual]

Theory interface.

Reimplemented from CVC3::Theory.

Definition at line 726 of file theory_quant.h.

void TheoryQuant::assertFact

(

const Theorem &

e

)

[virtual]

Theory interface function to assert quantified formulas.

pushes in negations and converts to either universally or existentially quantified theorems. Universals are stored in a database while existentials are enqueued to be handled by the search engine.

Implements CVC3::Theory.

Definition at line 3435 of file theory_quant.cpp.

References CVC3::QuantProofRules::boundVarElim(), d_maxILReached, d_rawUnivs, d_rules, d_translate, d_univs, d_useGFact, d_useNew, DebugAssert, CVC3::Theory::enqueueFact(), CVC3::Theorem::getExpr(), CVC3::Theory::iffMP(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::QuantProofRules::packVar(), CVC3::CDList< T >::push_back(), CVC3::QuantProofRules::rewriteNotExists(), CVC3::QuantProofRules::rewriteNotForall(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TRACE.

void TheoryQuant::checkSat

(

bool

fullEffort

)

[virtual]

Check for satisfiability in the theory.

Parameters:

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 7516 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::Theory::getEM(), getHead(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), naiveCheckSat(), CVC3::ExprManager::newVarExpr(), CVC3::CDList< T >::push_back(), CVC3::READ, saveContext(), semCheckSat(), sendInstNew(), CVC3::Expr::setType(), setupTriggers(), CVC3::Theory::simplifyExpr(), CVC3::ExprMap< Data >::size(), CVC3::CDList< T >::size(), synCheckSat(), CVC3::Theory::theoryCore(), and CVC3::WRITE.

void TheoryQuant::setup

(

const Expr &

e

)

[virtual]

Set up the term e for call-backs when e or its children change.

setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.

See also:

update

Reimplemented from CVC3::Theory.

Definition at line 331 of file theory_quant.cpp.

int TheoryQuant::help

(

int

i

)

Definition at line 333 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 412 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 CVC3::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 337 of file theory_quant.cpp.

References d_curMaxExprScore, d_usefulGterms, std::endl(), getExprScore(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), CVC3::CDList< T >::size(), and CVC3::Theory::theoryCore().

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 8489 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::Theorem::toString(), CVC3::Assumptions::toString(), and CVC3::TRACE.

void TheoryQuant::computeType

(

const Expr &

e

)

[virtual]

computes the type of a quantified term. Always a boolean.

Reimplemented from CVC3::Theory.

Definition at line 8551 of file theory_quant.cpp.

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

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

References DebugAssert, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Theory::getTCC(), CVC3::Expr::getVars(), CVC3::Expr::isQuantifier(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().

Expr TheoryQuant::parseExprOp

(

const Expr &

e

)

[virtual]

Theory-specific parsing implemented by the DP.

Reimplemented from CVC3::Theory.

Definition at line 8814 of file theory_quant.cpp.

References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::Theory::boolType(), DebugAssert, CVC3::EXISTS, CVC3::FORALL, CVC3::Theory::getEM(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::ID, CVC3::ExprManager::newClosureExpr(), CVC3::Theory::parseExpr(), CVC3::RAW_LIST, and CVC3::TRACE.

ExprStream & TheoryQuant::print	(	ExprStream &	os,
		const Expr &	e
	)			[virtual]

Theory-specific pretty-printing.

By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer.

Reimplemented from CVC3::Theory.

Definition at line 8597 of file theory_quant.cpp.

References CVC3::Theory::d_theoryUsed, d_translate, CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::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::space(), and CVC3::TPTP_LANG.

---

Member Data Documentation

CDList<Theorem> CVC3::TheoryQuant::d_univs [private]

database of universally quantified theorems

Definition at line 200 of file theory_quant.h.

Referenced by assertFact(), checkSat(), enqueueInst(), mapTermsByType(), matchListOld(), naiveCheckSat(), notifyInconsistent(), saveContext(), and TheoryQuant().

CDList<Theorem> CVC3::TheoryQuant::d_rawUnivs [private]

Definition at line 202 of file theory_quant.h.

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

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

Definition at line 204 of file theory_quant.h.

Referenced by registerTrig(), and saveContext().

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

Definition at line 205 of file theory_quant.h.

Referenced by saveContext().

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

Referenced by checkSat().

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

Definition at line 210 of file theory_quant.h.

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

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

Definition at line 212 of file theory_quant.h.

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

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

Definition at line 214 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 217 of file theory_quant.h.

Referenced by checkSat().

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

tracks the possition of preds

Definition at line 220 of file theory_quant.h.

Referenced by checkSat(), and saveContext().

CDO<size_t> CVC3::TheoryQuant::d_lastTermsPos [private]

tracks the possition of terms

Definition at line 222 of file theory_quant.h.

Referenced by checkSat(), and saveContext().

CDO<size_t> CVC3::TheoryQuant::d_lastPartPredsPos [private]

tracks the positions of preds for partial instantiation

Definition at line 225 of file theory_quant.h.

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

tracks the possition of terms for partial instantiation

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

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

Definition at line 234 of file theory_quant.h.

Referenced by TheoryQuant().

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

the max instantiation level reached

Definition at line 237 of file theory_quant.h.

Referenced by assertFact(), and checkSat().

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

useful gterms for matching

Definition at line 242 of file theory_quant.h.

Referenced by debug(), and saveContext().

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

tracks the position in d_usefulGterms

Definition at line 245 of file theory_quant.h.

Referenced by saveContext().

CDO<size_t> CVC3::TheoryQuant::d_savedTermsPos [private]

tracks a possition in the savedTerms map

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

Referenced by naiveCheckSat(), and saveContext().

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

Definition at line 251 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 253 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 256 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 259 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 262 of file theory_quant.h.

Referenced by checkSat().

int CVC3::TheoryQuant::d_allout [private]

Definition at line 264 of file theory_quant.h.

Referenced by matchListOld().

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

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

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

Definition at line 271 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 274 of file theory_quant.h.

Referenced by findInstAssumptions(), and recInstantiate().

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

cache of expressions

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

Referenced by findInstAssumptions(), and recInstantiate().

QuantProofRules* CVC3::TheoryQuant::d_rules [private]

quantifier theorem production rules

Definition at line 283 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 285 of file theory_quant.h.

Referenced by naiveCheckSat(), and recInstantiate().

const bool* CVC3::TheoryQuant::d_useNew [private]

Definition at line 323 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 324 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useSemMatch [private]

use lazy instantiation

Definition at line 325 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useCompleteInst [private]

use semantic matching

Definition at line 326 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_translate [private]

Try complete instantiation.

Definition at line 327 of file theory_quant.h.

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

const bool* CVC3::TheoryQuant::d_usePart [private]

translate only

Definition at line 329 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useMult [private]

use partial instantiaion

Definition at line 330 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useInstLCache [private]

Definition at line 332 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_useInstGCache [private]

Definition at line 333 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

const bool* CVC3::TheoryQuant::d_useInstThmCache [private]

Definition at line 334 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_useInstTrue [private]

Definition at line 335 of file theory_quant.h.

Referenced by enqueueInst().

const bool* CVC3::TheoryQuant::d_usePullVar [private]

Definition at line 336 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useExprScore [private]

Definition at line 337 of file theory_quant.h.

const int* CVC3::TheoryQuant::d_useTrigLoop [private]

Definition at line 338 of file theory_quant.h.

const int* CVC3::TheoryQuant::d_maxInst [private]

Definition at line 339 of file theory_quant.h.

const int* CVC3::TheoryQuant::d_maxIL [private]

Definition at line 341 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useTrans [private]

Definition at line 342 of file theory_quant.h.

Referenced by isTransLike().

const bool* CVC3::TheoryQuant::d_useTrans2 [private]

Definition at line 343 of file theory_quant.h.

Referenced by isTrans2Like().

const bool* CVC3::TheoryQuant::d_useManTrig [private]

Definition at line 344 of file theory_quant.h.

Referenced by newTopMatchSig().

const bool* CVC3::TheoryQuant::d_useGFact [private]

Definition at line 345 of file theory_quant.h.

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

const int* CVC3::TheoryQuant::d_gfactLimit [private]

Definition at line 346 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

const bool* CVC3::TheoryQuant::d_useInstAll [private]

Definition at line 347 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_usePolarity [private]

Definition at line 348 of file theory_quant.h.

Referenced by newTopMatchNoSig(), and newTopMatchSig().

const bool* CVC3::TheoryQuant::d_useEqu [private]

Definition at line 349 of file theory_quant.h.

const bool* CVC3::TheoryQuant::d_useNewEqu [private]

Definition at line 350 of file theory_quant.h.

Referenced by recMultMatch(), and recMultMatchDebug().

const int* CVC3::TheoryQuant::d_maxNaiveCall [private]

Definition at line 351 of file theory_quant.h.

Referenced by checkSat().

const bool* CVC3::TheoryQuant::d_useNaiveInst [private]

Definition at line 352 of file theory_quant.h.

Referenced by checkSat().

CDO<int> CVC3::TheoryQuant::d_curMaxExprScore [private]

Definition at line 355 of file theory_quant.h.

Referenced by debug(), help(), multMatchChild(), recMultMatch(), recMultMatchDebug(), and recMultMatchOldWay().

bool CVC3::TheoryQuant::d_useFullTrig [private]

Definition at line 357 of file theory_quant.h.

Referenced by checkSat().

bool CVC3::TheoryQuant::d_usePartTrig [private]

Definition at line 358 of file theory_quant.h.

bool CVC3::TheoryQuant::d_useMultTrig [private]

Definition at line 359 of file theory_quant.h.

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

Definition at line 362 of file theory_quant.h.

Referenced by arrayHeuristic(), and arrayIndexName().

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

Definition at line 365 of file theory_quant.h.

int CVC3::TheoryQuant::d_initMaxScore [private]

all instantiations

Definition at line 367 of file theory_quant.h.

Referenced by TheoryQuant().

int CVC3::TheoryQuant::d_offset_multi_trig [private]

Definition at line 368 of file theory_quant.h.

Referenced by TheoryQuant().

int CVC3::TheoryQuant::d_instThisRound [private]

Definition at line 370 of file theory_quant.h.

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

int CVC3::TheoryQuant::d_callThisRound [private]

Definition at line 371 of file theory_quant.h.

int CVC3::TheoryQuant::partial_called [private]

Definition at line 373 of file theory_quant.h.

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

Definition at line 379 of file theory_quant.h.

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

Definition at line 380 of file theory_quant.h.

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

Definition at line 382 of file theory_quant.h.

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

Definition at line 384 of file theory_quant.h.

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

Definition at line 385 of file theory_quant.h.

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

Definition at line 388 of file theory_quant.h.

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

Definition at line 390 of file theory_quant.h.

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

Definition at line 392 of file theory_quant.h.

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

the score for a full trigger

Definition at line 398 of file theory_quant.h.

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

Definition at line 399 of file theory_quant.h.

int CVC3::TheoryQuant::d_trans_num [private]

Definition at line 401 of file theory_quant.h.

Referenced by TheoryQuant().

int CVC3::TheoryQuant::d_trans2_num [private]

Definition at line 402 of file theory_quant.h.

Referenced by TheoryQuant().

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

Definition at line 415 of file theory_quant.h.

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

Definition at line 416 of file theory_quant.h.

Referenced by checkSat(), and synNewInst().

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

Definition at line 418 of file theory_quant.h.

Referenced by backList(), and pushBackList().

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

Definition at line 419 of file theory_quant.h.

Referenced by forwList(), and pushForwList().

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

Definition at line 420 of file theory_quant.h.

Referenced by setTransFound(), and transFound().

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

Definition at line 421 of file theory_quant.h.

Referenced by setTrans2Found(), and trans2Found().

Expr CVC3::TheoryQuant::defaultWriteExpr [private]

Definition at line 440 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultReadExpr [private]

Definition at line 441 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultPlusExpr [private]

Definition at line 442 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultMinusExpr [private]

Definition at line 443 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultMultExpr [private]

Definition at line 444 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultDivideExpr [private]

Definition at line 445 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

Expr CVC3::TheoryQuant::defaultPowExpr [private]

Definition at line 446 of file theory_quant.h.

Referenced by getHeadExpr(), and TheoryQuant().

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

Definition at line 453 of file theory_quant.h.

Referenced by backList(), and forwList().

Theorem CVC3::TheoryQuant::d_transThm [private]

Definition at line 455 of file theory_quant.h.

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

Definition at line 461 of file theory_quant.h.

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

Definition at line 463 of file theory_quant.h.

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

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

Definition at line 464 of file theory_quant.h.

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

Definition at line 466 of file theory_quant.h.

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

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

Definition at line 467 of file theory_quant.h.

Referenced by checkSat(), and saveContext().

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

Definition at line 469 of file theory_quant.h.

Referenced by checkSat(), and collectChangedTerms().

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

Definition at line 470 of file theory_quant.h.

Referenced by collectChangedTerms().

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

Definition at line 472 of file theory_quant.h.

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

Definition at line 474 of file theory_quant.h.

Referenced by add_parent(), and collectChangedTerms().

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

Definition at line 476 of file theory_quant.h.

Referenced by loc_gterm().

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

Definition at line 495 of file theory_quant.h.

Referenced by recGoodSemMatch().

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

Definition at line 496 of file theory_quant.h.

StatCounter CVC3::TheoryQuant::d_allInstCount [private]

Definition at line 498 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

StatCounter CVC3::TheoryQuant::d_allInstCount2 [private]

Definition at line 499 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_totalInstCount [private]

Definition at line 500 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_trueInstCount [private]

Definition at line 501 of file theory_quant.h.

Referenced by enqueueInst().

StatCounter CVC3::TheoryQuant::d_abInstCount [private]

Definition at line 502 of file theory_quant.h.

Referenced by checkSat().

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

Definition at line 510 of file theory_quant.h.

size_t CVC3::TheoryQuant::d_cacheThmPos [private]

Definition at line 511 of file theory_quant.h.

Referenced by TheoryQuant().

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

Definition at line 517 of file theory_quant.h.

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

Definition at line 520 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

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

Definition at line 521 of file theory_quant.h.

Referenced by enqueueInst().

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

Definition at line 523 of file theory_quant.h.

Referenced by enqueueInst().

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

Definition at line 524 of file theory_quant.h.

Referenced by enqueueInst(), and sendInstNew().

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

Definition at line 526 of file theory_quant.h.

Referenced by enqueueInst().

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

Definition at line 528 of file theory_quant.h.

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

Definition at line 531 of file theory_quant.h.

Referenced by getSubTerms().

const size_t CVC3::TheoryQuant::MAX_TRIG_BVS = 15 [static, private]

Definition at line 681 of file theory_quant.h.

Referenced by TheoryQuant().

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

Definition at line 682 of file theory_quant.h.

Referenced by TheoryQuant().

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

Definition at line 687 of file theory_quant.h.

Referenced by combineOldNewTrigs(), and matchListOld().

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

Definition at line 689 of file theory_quant.h.

---

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

• theory_quant.h
• quant_theorem_producer.cpp
• theory_quant.cpp

---