24 #ifndef _cvc3__include__theory_quant_h_
25 #define _cvc3__include__theory_quant_h_
34 class QuantProofRules;
55 std::vector<Expr>
bvs;
70 std::vector<Expr>
getBVs();
174 bool hasMacros(
const std::vector<Expr>& asserts);
317 std::vector<Expr>& varReplacements);
480 int loc_gterm(
const std::vector<Expr>& border,
485 const std::vector<Expr>& mtrigs,
487 std::vector<std::vector<Expr> >& instSet,
488 std::vector<Expr>& cur_inst
492 const std::vector<Expr>& border,
493 std::vector<std::vector<Expr> >& instSet
547 void enqueueInst(
size_t univ_id ,
const std::vector<Expr>& bind,
const Expr& gterm);
550 const std::vector<Expr>& binds,
559 bool insted(
const Theorem & univ,
const std::vector<Expr>& binds);
568 void synNewInst(
size_t univ_id,
const std::vector<Expr>& binds,
const Expr& gterm,
const Trigger& trig );
577 const std::vector<Expr> & boundVars,
578 std::vector<std::vector<Expr> >& instBindsTerm,
579 std::vector<Expr>& instGterm,
583 const std::vector<Expr> & boundVars,
584 std::vector<std::vector<Expr> >& instBinds,
585 std::vector<Expr>& instGterms,
590 const std::vector<Expr> & boundVars,
591 std::vector<std::vector<Expr> >& instBinds,
592 std::vector<Expr>& instGterms,
649 std::vector<Expr> & boundVars,
650 std::vector<std::vector<Expr> >& instBinds,
651 std::vector<Expr>& instGterms,
656 const std::vector<Expr> & boundVars,
657 std::vector<std::vector<Expr> >& instBinds,
658 std::vector<Expr>& instGterms,
664 std::vector<Expr>& bVars,
665 std::vector<std::vector<Expr> >& instSet,
670 const std::vector<Expr>& bVars,
671 std::vector<Expr>& newInst,
672 std::set<std::vector<Expr> >& instSet);
675 std::vector<Expr>& bVars,
676 std::set<std::vector<Expr> >& instSet,
679 bool isTransLike (
const std::vector<Expr>& cur_trig);
695 const std::vector<Expr> thmBVs,
ExprMap< bool > d_hasMoreBVs
ExprMap< std::set< std::vector< Expr > > > d_instHistoryGlobal
std::string exprMap2string(const ExprMap< Expr > &vec)
std::queue< Theorem > d_univsQueue
universally quantified formulas to be instantiated, the var bindings is in d_bingQueue and the ground...
CDO< int > d_instCount
number of instantiations made in given context
std::vector< std::vector< size_t > > var_pos
void collectChangedTerms(CDList< Expr > &changed_terms)
void newTopMatchNoSig(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
bool synMatchTopPred(const Expr >erm, const Trigger trig, ExprMap< Expr > &env)
Data structure of expressions in CVC3.
ExprMap< CDMap< Expr, bool > * > d_bindHistory
typeMap d_savedMap
a map of types to positions in the d_savedTerms vector
QuantProofRules * d_quant_rules
void recGoodSemMatch(const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
~TheoryQuant()
Destructor.
QuantProofRules * d_rules
quantifier theorem production rules
std::map< ExprIndex, Expr > d_indexExpr
Expr getHeadExpr(const Expr &e)
void matchListNew(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs, const CDList< Expr > &list, size_t gbegin, size_t gend)
StatCounter d_totalInstCount
void collect_shield_index(const Expr &e)
void pushBackList(const Expr &node, Expr ex)
const bool * d_useManTrig
const bool * d_useInstLCache
dynTrig(Trigger t, ExprMap< Expr > b, size_t id)
ExprMap< std::hash_map< Expr, bool > * > d_bindGlobalHistory
CompleteInstPreProcessor(TheoryCore *, QuantProofRules *)
TheoryQuant(TheoryCore *core)
categorizes all the terms contained in an expressions by type.
const bool * d_useExprScore
Expr recInstMacros(const Expr &assert)
void synMultInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void combineOldNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
void newTopMatchSig(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
ExprMap< CDList< Expr > * > d_eq_list
bool hasGoodSemInst(const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
CDList< Expr > & backList(const Expr &ex)
Expr instMacros(const Expr &, const Expr)
substitute a macro in assert
Trigger(TheoryCore *core, Expr e, Polarity pol, std::set< Expr >)
bool operator()(const Type t1, const Type t2) const
< needed for typeMap
CDO< size_t > d_univsContextPos
tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed wh...
std::string exprMap2stringSig(const ExprMap< Expr > &vec)
std::vector< Expr > d_allInsts
void synFullInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
struct CVC3::dynTrig dynTrig
Expr substMacro(const Expr &)
void matchListOld(const CDList< Expr > &list, size_t gbegin, size_t gend)
void collectIndex(const Expr &e)
collect index for instantiation
Expr recSkolemize(const Expr &, ExprMap< Polarity > &)
CDList< Expr > null_cdlist
Expr pullVarOut(const Expr &)
ExprMap< CDList< Expr > * > d_parent_list
CDList< Expr > & forwList(const Expr &ex)
CDO< size_t > d_lastPartPredsPos
tracks the positions of preds for partial instantiation
const bool * d_usePolarity
CDO< size_t > d_savedTermsPos
tracks a possition in the savedTerms map
CDO< int > d_curMaxExprScore
std::map< Type, CDList< size_t > *,TypeComp > d_contextMap
a map of types to posisitions in the d_contextTerms list
void collect_forall_index(const Expr &forall_quant)
Expr recRewriteNot(const Expr &, ExprMap< Polarity > &)
ExprMap< CDList< std::vector< Expr > > * > d_mtrigs_inst
const int * d_useTrigLoop
MS C++ specific settings.
void debug(int i)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
void add_parent(const Expr &parent)
ExprMap< CDList< Expr > * > d_trans_forw
Expr computeTCC(const Expr &e)
void semInst(const Theorem &univ, size_t tBegin)
const bool * d_useSemMatch
use lazy instantiation
void synPartInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
ExprMap< std::vector< Trigger > > d_multTrigs
bool recMultMatchNewWay(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
ExprMap< std::vector< Expr > > d_insts
a map of instantiated universals to a vector of their instantiations
std::string exprMap2stringSimplify(const ExprMap< Expr > &vec)
const bool * d_useInstTrue
void assertFact(const Theorem &e)
Theory interface function to assert quantified formulas.
std::vector< std::vector< size_t > > common_pos
Description: Counters and flags for collecting run-time statistics.
CDList< Theorem > d_rawUnivs
std::vector< CDMap< Expr, bool > * > var_binds_found
void simplifyVectorExprMap(std::vector< ExprMap< Expr > > &orgVectorExprMap)
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
const bool * d_useInstAll
bool multMatchChild(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, bool top=false)
void addIndex(const Expr &e)
insert an index
void setTrans2Found(const Expr &comb)
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
CDMap< Expr, std::set< std::vector< Expr > > > d_instHistory
CDList< dynTrig > d_arrayTrigs
Expr d_mybvs[MAX_TRIG_BVS]
ExprMap< Polarity > d_expr_pol
ExprMap< std::hash_map< Expr, Theorem > * > d_bindGlobalThmHistory
const bool * d_translate
Try complete instantiation.
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)
ExprMap< CDO< size_t > * > d_eq_pos
std::queue< Theorem > d_simplifiedThmQueue
std::vector< ExprMap< CDList< Expr > * > * > uncomm_list
void recInstantiate(Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)
does most of the work of the instantiate function.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
StatCounter d_allInstCount
CDO< size_t > d_lastUsefulGtermsPos
tracks the position in d_usefulGterms
CDO< size_t > d_lastArrayPos
const Expr & getExpr() const
std::vector< Expr > getBVs()
ExprMap< Expr > d_macro_def
std::map< Type, std::vector< Expr >, TypeComp > d_typeExprMap
CDO< size_t > d_univsSavedPos
tracks a possition in the database of universals
CDO< size_t > d_rawUnivsSavedPos
void registerTrig(ExprMap< ExprMap< std::vector< dynTrig > * > * > &cur_trig_map, Trigger trig, const std::vector< Expr > thmBVs, size_t univ_id)
const bool * d_useLazyInst
use new way of instantiation
CDList< Theorem > d_univs
database of universally quantified theorems
std::vector< Expr > d_savedTerms
a vector of all of the terms that have produced conflicts.
Expr simplifyEq(const Expr &)
simplify a=a to True
Expr generalTrig(const Expr &trig, ExprMap< Expr > &bvs)
int getExprScore(const Expr &e)
ExprMap< CDList< Expr > * > d_trans_back
const bool * d_useCompleteInst
use semantic matching
void setGround(const Expr >erm, const Expr &trig, const Theorem &univ, const std::vector< Expr > &subTerms)
bool canMatch(const Expr &t1, const Expr &t2, ExprMap< Expr > &env)
Expr minusOne(const Expr &e)
return e-1
const bool * d_useInstGCache
bool recSynMatch(const Expr >erm, const Expr &vterm, ExprMap< Expr > &env)
int loc_gterm(const std::vector< Expr > &border, const Expr >erm, int pos)
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)
ExprMap< std::set< std::vector< Expr > > > d_tempBinds
Expr simplifyQuant(const Expr &)
put all quants in postive form and then skolemize all exists
Expr inst(const Expr &e)
inst forall quant using index from collectIndex
std::map< Type, std::vector< size_t >, TypeComp > typeMap
used to facilitate instantiation of universal quantifiers
void notifyInconsistent(const Theorem &thm)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a contex...
void addSharedTerm(const Expr &e)
Theory interface.
bool isMacro(const Expr &assert)
if assert is a macro definition
void collectHeads(const Expr &assert, std::set< Expr > &heads)
std::queue< Expr > d_gBindQueue
void newTopMatch(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
void synCheckSat(ExprMap< ExprMap< std::vector< dynTrig > * > * > &, bool)
void arrayHeuristic(const Trigger &trig, size_t univid)
int d_initMaxScore
all instantiations
std::vector< Expr > d_gnd_cache
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
ExprMap< CDList< Expr > * > d_same_head_expr
CDMap< Expr, bool > d_trans_found
ExprMap< Expr > d_quant_equiv_map
static const size_t MAX_TRIG_BVS
const bool * d_useInstThmCache
TheoryCore * d_theoryCore
Theorem theoryPreprocess(const Expr &e)
Theory-specific preprocessing.
CDMap< Expr, bool > d_trans2_found
void enqueueInst(const Theorem, const Theorem)
void registerTrigReal(Trigger trig, const std::vector< Expr >, size_t univ_id)
void computeType(const Expr &e)
computes the type of a quantified term. Always a boolean.
bool hasShieldVar(const Expr &e)
CDList< Trigger > d_alltrig_list
CDO< size_t > d_univsPartSavedPos
tracks a possition in the database of universals for partial instantiation
int d_inEnd
set if the fullEffort = 1
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)
std::map< ExprIndex, int > d_indexScore
StatCounter d_trueInstCount
void iterBKList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr >erm)
bool hasMacros(const std::vector< Expr > &asserts)
if there are macros
ExprMap< std::vector< Expr > > d_mtrigs_bvorder
bool hasGoodSynMultiInst(const Expr &e, std::vector< Expr > &bVars, std::vector< std::vector< Expr > > &instSet, const CDList< Expr > &allterms, size_t tBegin)
bool recMultMatchDebug(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDList< Expr > d_contextTerms
a list of all the terms appearing in the current context
ExprMap< size_t > d_totalThmCount
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)
const std::vector< Expr > & getSubTerms(const Expr &e)
void newTopMatchBackupOnly(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds, const Trigger &trig)
Expr simpRAWList(const Expr &org)
CDO< size_t > d_lastPartTermsPos
tracks the possition of terms for partial instantiation
std::set< std::string > cacheHead
bool transFound(const Expr &comb)
void mapTermsByType(const CDList< Expr > &terms)
categorizes all the terms contained in a vector of expressions by type.
CDMap< Expr, std::vector< Expr > > d_arrayIndic
Expr getHead(const Expr &e)
std::vector< multTrigsInfo > d_all_multTrigsInfo
bool isGood(const Expr &e)
if e is a formula in the array property fragment
bool multMatchTop(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
void pushForwList(const Expr &node, Expr ex)
ExprMap< bool > d_is_macro_def
CDList< Theorem > d_eqsUpdate
ExprMap< bool > d_hasTriggers
the score for a full trigger
Generic API for Theories plus methods commonly used by theories.
StatCounter d_abInstCount
bool isShield(const Expr &e)
if e satisfies the shiled property, that is all bound vars are parameters of uninterpreted functions/...
const int * d_maxQuantInst
Command line option.
void iterFWList(const Expr &sr, const Expr &dt, size_t univ_id, const Expr >erm)
bool d_all_good
if all formulas checked so far are good
CDO< size_t > d_lastEqsUpdatePos
CDO< bool > d_maxILReached
the max instantiation level reached
void simplifyExprMap(ExprMap< Expr > &orgExprMap)
void delNewTrigs(ExprMap< ExprMap< std::vector< dynTrig > * > * > &new_trigs)
const bool * d_usePart
translate only
void findInstAssumptions(const Theorem &thm)
A recursive function used to find instantiated universals in the hierarchy of assumptions.
const bool * d_usePullVar
void setupTriggers(ExprMap< ExprMap< std::vector< dynTrig > * > * > &trig_maps, const Theorem &thm, size_t univs_id)
void synInst(const Theorem &univ, const CDList< Expr > &allterms, size_t tBegin)
void addNotify(const Expr &e)
ExprMap< bool > d_savedCache
bool isGoodQuant(const Expr &e)
if e is a quant in the array property fragmenet
ExprMap< Expr > d_macro_lhs
void searchCover(const Expr &thm, const std::vector< Expr > &border, std::vector< std::vector< Expr > > &instSet)
CDList< Expr > d_usefulGterms
useful gterms for matching
bool recursiveMap(const Expr &term)
categorizes all the terms contained in an expressions by type.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr rewriteNot(const Expr &)
rewrite neg polarity forall / exists to pos polarity
QuantProofRules * createProofRules()
Destructor.
CDO< size_t > d_exprLastUpdatedPos
std::set< Expr > d_allIndex
void setTransFound(const Expr &comb)
bool trans2Found(const Expr &comb)
const bool * d_useNaiveInst
CDO< size_t > d_univsPosFull
tracks a possition in the database of universals
Expr plusOne(const Expr &e)
return e+1
CDMap< Expr, bool > d_contextCache
bool isTransLike(const std::vector< Expr > &cur_trig)
CDO< size_t > d_lastPartLevel
the last decision level on which partial instantion is called
void synNewInst(size_t univ_id, const std::vector< Expr > &binds, const Expr >erm, const Trigger &trig)
const int * d_maxNaiveCall
bool isTrans2Like(const std::vector< Expr > &all_terms, const Expr &tr2)
ExprMap< Expr > d_macro_quant
ExprMap< std::vector< Expr > > d_partTriggers
Expr recGeneralTrig(const Expr &trig, ExprMap< Expr > &bvs, size_t &mybvs_count)
bool recMultMatch(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
ExprMap< std::vector< Expr > > d_subTermsMap
StatCounter d_allInstCount2
const bool * d_useMult
use partial instantiaion
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
bool recMultMatchOldWay(const Expr >erm, const Expr &vterm, std::vector< ExprMap< Expr > > &binds)
CDO< size_t > d_lastTermsPos
tracks the possition of terms
ExprMap< CDMap< Expr, CDList< dynTrig > * > * > d_allmap_trigs
std::queue< Theorem > d_gUnivQueue
void instantiate(Theorem univ, bool all, bool savedMap, size_t newIndex)
Queues up all possible instantiations of bound variables.
bool recSynMatchBackupOnly(const Expr >erm, const Expr &vterm, ExprMap< Expr > &env)
ExprMap< std::vector< Trigger > > d_partTrigs
void arrayIndexName(const Expr &e)
CDO< size_t > d_lastPredsPos
tracks the possition of preds
std::vector< Theorem > d_cacheTheorem
This theory handles quantifiers.
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)
ExprMap< int > d_thmCount
bool insted(const Theorem &univ, const std::vector< Expr > &binds)
ExprMap< multTrigsInfo > d_multitrigs_maps
ExprMap< std::vector< Trigger > > d_fullTrigs
ExprMap< std::vector< Expr > > d_multTriggers
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.