This theory handles quantifiers. More...

#include <theory_quant.h>

Inherits CVC3::Theory.

Collaboration diagram for CVC3::TheoryQuant:

[legend]

List of all members.

Classes

struct multTrigsInfo
class TypeComp

Public Member Functions

TheoryQuant (TheoryCore *core)
categorizes all the terms contained in an expressions by type.
~TheoryQuant ()
Destructor.
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
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

Detailed Description

This theory handles quantifiers.

Author: Daniel Wichs

Created: Wednesday July 2, 2003

Definition at line 186 of file theory_quant.h.

Member Typedef Documentation

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

used to facilitate instantiation of universal quantifiers

Definition at line 199 of file theory_quant.h.

Constructor & Destructor Documentation

TheoryQuant::TheoryQuant ( TheoryCore * core )

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

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, 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 ( )

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 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().

bool TheoryQuant::recursiveMap ( const Expr & e ) [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(), CVC3::CDMap< Key, Data, HashFcn >::count(), d_contextCache, d_contextMap, d_contextTerms, d_savedCache, CVC3::Expr::end(), EXISTS, FORALL, CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Expr::getKind(), CVC3::Type::isBool(), CVC3::CDList< T >::push_back(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), CVC3::Type::toString(), CVC3::Expr::toString(), and TRACE.

Referenced by mapTermsByType().

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

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

Updates d_contextTerms, d_contextMap, d_contextCache accordingly.

Definition at line 8537 of file theory_quant.cpp.

References CVC3::Theory::boolType(), d_contextMap, d_contextTerms, d_univs, CVC3::Theory::falseExpr(), CVC3::TheoryCore::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::CDList< T >::push_back(), recursiveMap(), CVC3::CDList< T >::size(), CVC3::Theory::theoryCore(), and CVC3::Theory::trueExpr().

Referenced by naiveCheckSat().

void TheoryQuant::instantiate	(	Theorem	univ,
		bool	all,
		bool	savedMap,
		size_t	newIndex
	)		`[private]`

Queues up all possible instantiations of bound variables.

The savedMap boolean indicates whether to use savedMap or d_contextMap the all boolean indicates weather to use all instantiation or only new ones and newIndex is the index where new instantiations begin.

Definition at line 8450 of file theory_quant.cpp.

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

Referenced by naiveCheckSat().

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

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().

void TheoryQuant::findInstAssumptions ( const Theorem & thm ) [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.

void TheoryQuant::arrayIndexName ( const Expr & e ) [private]

Definition at line 2617 of file theory_quant.cpp.

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

Referenced by checkSat(), and setupTriggers().

int TheoryQuant::getExprScore ( const Expr & e ) [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(), recMultMatchOldWay(), and synCheckSat().

bool TheoryQuant::transFound ( const Expr & comb ) [inline, private]

Definition at line 6973 of file theory_quant.cpp.

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

Referenced by synNewInst().

void TheoryQuant::setTransFound ( const Expr & comb ) [inline, private]

Definition at line 6977 of file theory_quant.cpp.

References d_trans_found.

Referenced by synNewInst().

bool TheoryQuant::trans2Found ( const Expr & comb ) [inline, private]

Definition at line 6981 of file theory_quant.cpp.

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

Referenced by synNewInst().

void TheoryQuant::setTrans2Found ( const Expr & comb ) [inline, private]

Definition at line 6985 of file theory_quant.cpp.

References d_trans2_found.

Referenced by synNewInst().

CDList< Expr > & TheoryQuant::backList ( const Expr & ex ) [inline, private]

Definition at line 6990 of file theory_quant.cpp.

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

Referenced by iterBKList(), and update().

CDList< Expr > & TheoryQuant::forwList ( const Expr & ex ) [inline, private]

Definition at line 6999 of file theory_quant.cpp.

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

Referenced by iterFWList(), and update().

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

Definition at line 7224 of file theory_quant.cpp.

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

Referenced by synNewInst().

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

Definition at line 7235 of file theory_quant.cpp.

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

Referenced by synNewInst().

Expr TheoryQuant::getHead ( const Expr & e ) [private]

Definition at line 1106 of file theory_quant.cpp.

References getHeadExpr().

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

Expr TheoryQuant::getHeadExpr ( const Expr & e ) [private]

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().

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

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().

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

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().

void TheoryQuant::collectChangedTerms ( CDList< Expr > & changed_terms ) [private]

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().

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

Definition at line 6689 of file theory_quant.cpp.

References d_mtrigs_bvorder, and DebugAssert.

void CVC3::TheoryQuant::recSearchCover	(	const std::vector< Expr > &	border,
		const std::vector< Expr > &	mtrigs,
		int	cur_depth,
		std::vector< std::vector< Expr > > &	instSet,
		std::vector< Expr > &	cur_inst
	)		`[private]`

void CVC3::TheoryQuant::searchCover	(	const Expr &	thm,
		const std::vector< Expr > &	border,
		std::vector< std::vector< Expr > > &	instSet
	)		`[private]`

void TheoryQuant::addNotify ( const Expr & e ) [private]

Definition at line 1040 of file theory_quant.cpp.

int TheoryQuant::sendInstNew ( ) [private]

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

Referenced by checkSat(), and synCheckSat().

const std::vector< Expr > & TheoryQuant::getSubTerms ( const Expr & e ) [private]

Definition at line 613 of file theory_quant.cpp.

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

Referenced by arrayIndexName().

void TheoryQuant::simplifyExprMap ( ExprMap< Expr > & orgExprMap ) [private]

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().

void TheoryQuant::simplifyVectorExprMap ( std::vector< ExprMap< Expr > > & orgVectorExprMap ) [private]

Definition at line 553 of file theory_quant.cpp.

References simplifyExprMap().

Referenced by newTopMatch().

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

Definition at line 500 of file theory_quant.cpp.

Referenced by newTopMatch().

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

Definition at line 514 of file theory_quant.cpp.

Referenced by newTopMatch().

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

Definition at line 526 of file theory_quant.cpp.

Referenced by newTopMatch().

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

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 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::ExprMap< Data >::end(), CVC3::Theory::enqueueFact(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::ExprMap< Data >::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().

void TheoryQuant::enqueueInst	(	size_t	univ_id,
		const std::vector< Expr > &	bind,
		const Expr &	gterm
	)		`[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::ExprMap< Data >::end(), CVC3::Theory::enqueueFact(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::ExprMap< Data >::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().

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

Definition at line 994 of file theory_quant.cpp.

References enqueueInst().

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

void CVC3::TheoryQuant::synCheckSat ( bool ) [private]

void TheoryQuant::semCheckSat ( bool fullEffort ) [private]

Definition at line 8381 of file theory_quant.cpp.

Referenced by checkSat().

void TheoryQuant::naiveCheckSat ( bool fullEffort ) [private]

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().

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

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

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

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

Definition at line 7212 of file theory_quant.cpp.

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

Referenced by synCheckSat().

Expr TheoryQuant::simpRAWList ( const Expr & org ) [private]

Definition at line 7248 of file theory_quant.cpp.

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

Referenced by synNewInst().

void TheoryQuant::synNewInst	(	size_t	univ_id,
		const std::vector< Expr > &	binds,
		const Expr &	gterm,
		const Trigger &	trig
	)		`[private]`

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().

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

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

void CVC3::TheoryQuant::semInst	(	const Theorem &	univ,
		size_t	tBegin
	)		`[private]`

void CVC3::TheoryQuant::goodSynMatch	(	const Expr &	e,
		const std::vector< Expr > &	boundVars,
		std::vector< std::vector< Expr > > &	instBindsTerm,
		std::vector< Expr > &	instGterm,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)		`[private]`

void CVC3::TheoryQuant::goodSynMatchNewTrig	(	const Trigger &	trig,
		const std::vector< Expr > &	boundVars,
		std::vector< std::vector< Expr > > &	instBinds,
		std::vector< Expr > &	instGterms,
		const CDList< Expr > &	allterms,
		size_t	tBegin
	)		`[private]`

bool CVC3::TheoryQuant::goodSynMatchNewTrig	(	const Trigger &	trig,
		const std::vector< Expr > &	boundVars,
		std::vector< std::vector< Expr > > &	instBinds,
		std::vector< Expr > &	instGterms,
		const Expr &	gterm
	)		`[private]`

void TheoryQuant::matchListOld	(	const CDList< Expr > &	list,
		size_t	gbegin,
		size_t	gend
	)		`[private]`

void TheoryQuant::matchListNew	(	ExprMap< ExprMap< std::vector< dynTrig > * > * > &	new_trigs,
		const CDList< Expr > &	list,
		size_t	gbegin,
		size_t	gend
	)		`[private]`

void TheoryQuant::delNewTrigs ( ExprMap< ExprMap< std::vector< dynTrig > * > * > & new_trigs ) [private]

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().

void TheoryQuant::combineOldNewTrigs ( ExprMap< ExprMap< std::vector< dynTrig > * > * > & new_trigs ) [private]

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

void TheoryQuant::newTopMatch	(	const Expr &	gterm,
		const Expr &	vterm,
		std::vector< ExprMap< Expr > > &	binds,
		const Trigger &	trig
	)		`[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().

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

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

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

bool CVC3::TheoryQuant::synMatchTopPred	(	const Expr &	gterm,
		const Trigger	trig,
		ExprMap< Expr > &	env
	)		`[private]`

bool CVC3::TheoryQuant::recSynMatch	(	const Expr &	gterm,
		const Expr &	vterm,
		ExprMap< Expr > &	env
	)		`[private]`

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

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().

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

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

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

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

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

Definition at line 4045 of file theory_quant.cpp.

References CVC3::ExprMap< Data >::begin(), and 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 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.

bool CVC3::TheoryQuant::hasGoodSemInst	(	const Expr &	e,
		std::vector< Expr > &	bVars,
		std::set< std::vector< Expr > > &	instSet,
		size_t	tBegin
	)		`[private]`

bool TheoryQuant::isTransLike ( const std::vector< Expr > & cur_trig ) [private]

Definition at line 2823 of file theory_quant.cpp.

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

Referenced by setupTriggers().

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

Definition at line 2866 of file theory_quant.cpp.

References d_useTrans2.

Referenced by setupTriggers().

Expr CVC3::TheoryQuant::recGeneralTrig	(	const Expr &	trig,
		ExprMap< Expr > &	bvs,
		size_t &	mybvs_count
	)		`[private]`

Expr CVC3::TheoryQuant::generalTrig	(	const Expr &	trig,
		ExprMap< Expr > &	bvs
	)		`[private]`

void TheoryQuant::registerTrig	(	ExprMap< ExprMap< std::vector< dynTrig > * > * > &	cur_trig_map,
		Trigger	trig,
		const std::vector< Expr >	thmBVs,
		size_t	univ_id
	)		`[private]`

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(), CVC3::Trigger::hasRWOp, and CVC3::CDList< T >::push_back().

Referenced by setupTriggers().

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

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

Referenced by setupTriggers().

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

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

Definition at line 2917 of file theory_quant.cpp.

References arrayIndexName(), BOUND_VAR, canGetHead(), canMatch(), CVC3::TheoryQuant::multTrigsInfo::common_pos, CVC3::ExprMap< Data >::count(), d_all_multTrigsInfo, d_fullTrigs, d_hasTriggers, d_multitrigs_maps, d_multTriggers, d_multTrigs, d_offset_multi_trig, d_trans2_num, d_trans_num, d_transThm, d_univs, d_useManTrig, d_usePolarity, d_useTrans2, DebugAssert, exprScore(), findPolarity(), getBoundVars(), CVC3::Theorem::getExpr(), getHead(), getHeadExpr(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), getSubTrig(), CVC3::Expr::getTriggers(), CVC3::Expr::getType(), CVC3::Expr::getVars(), goodMultiTriggers(), CVC3::int2string(), CVC3::Type::isBool(), isGoodFullTrigger(), isGoodMultiTrigger(), isSimpleTrig(), isSuperSimpleTrig(), isSysPred(), isTrans2Like(), isTransLike(), locVar(), CVC3::Trigger::multiId, CVC3::Trigger::multiIndex, CVC3::Neg, CVC3::Pos, CVC3::PosNeg, CVC3::CDList< T >::push_back(), CVC3::READ, registerTrig(), CVC3::Trigger::setHead(), CVC3::Trigger::setMultiTrig(), CVC3::Trigger::setRWOp(), CVC3::Trigger::setSimp(), CVC3::Trigger::setSuperSimp(), CVC3::Trigger::setTrans(), CVC3::Trigger::setTrans2(), CVC3::ExprMap< Data >::size(), CVC3::Expr::subExprOf(), CVC3::Theory::theoryCore(), CVC3::Expr::toString(), TRACE, trigInitScore(), CVC3::Ukn, CVC3::TheoryQuant::multTrigsInfo::uncomm_list, CVC3::TheoryQuant::multTrigsInfo::univ_id, CVC3::TheoryQuant::multTrigsInfo::univThm, CVC3::TheoryQuant::multTrigsInfo::var_binds_found, CVC3::TheoryQuant::multTrigsInfo::var_pos, and CVC3::WRITE.

Referenced by checkSat().

void TheoryQuant::saveContext ( ) [private]

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 ( )

Destructor.

Definition at line 39 of file quant_theorem_producer.cpp.

Referenced by TheoryQuant().

void CVC3::TheoryQuant::addSharedTerm ( const Expr & e ) [inline, virtual]

Theory interface.

Reimplemented from CVC3::Theory.

Definition at line 728 of file theory_quant.h.

void TheoryQuant::assertFact ( const Theorem & thm ) [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::CDList< T >::push_back(), CVC3::QuantProofRules::rewriteNotExists(), CVC3::QuantProofRules::rewriteNotForall(), CVC3::Expr::toString(), CVC3::Theorem::toString(), TRACE, and CVC3::QuantProofRules::universalInst().

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

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

void TheoryQuant::setup ( const Expr & e ) [virtual]

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

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

See also:: update

Reimplemented from CVC3::Theory.

Definition at line 337 of file theory_quant.cpp.

int TheoryQuant::help ( int i )

Definition at line 339 of file theory_quant.cpp.

References d_curMaxExprScore.

void TheoryQuant::update	(	const Theorem &	e,
		const Expr &	d
	)		`[virtual]`

Notify a theory of a new equality.

update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.

To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.

See also:: setup

Reimplemented from CVC3::Theory.

Definition at line 419 of file theory_quant.cpp.

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

void TheoryQuant::debug ( int i )

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().

void TheoryQuant::notifyInconsistent ( const Theorem & thm ) [virtual]

Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 8621 of file theory_quant.cpp.

References d_savedTerms, d_univs, DebugAssert, std::endl(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), CVC3::Expr::isFalse(), CVC3::CDList< T >::size(), CVC3::Theorem::toString(), CVC3::Assumptions::toString(), and TRACE.

void TheoryQuant::computeType ( const Expr & e ) [virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 8683 of file theory_quant.cpp.

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

Expr TheoryQuant::computeTCC ( const Expr & e ) [virtual]

TCC(forall x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & !phi(x)) TCC(exists x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & phi(x))

Reimplemented from CVC3::Theory.

Definition at line 8714 of file theory_quant.cpp.

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

Expr TheoryQuant::parseExprOp ( const Expr & e ) [virtual]

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.

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

Theory-specific pretty-printing.

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

Reimplemented from CVC3::Theory.

Definition at line 8729 of file theory_quant.cpp.

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

Member Data Documentation

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

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().

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

Definition at line 204 of file theory_quant.h.

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

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

Definition at line 206 of file theory_quant.h.

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

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

Definition at line 207 of file theory_quant.h.

Referenced by saveContext(), and synCheckSat().

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

universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground term matched with the trigger is in d_gtermQueue

Definition at line 210 of file theory_quant.h.

Referenced by checkSat().

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

Definition at line 212 of file theory_quant.h.

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

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

Definition at line 214 of file theory_quant.h.

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

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

Definition at line 216 of file theory_quant.h.

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

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