/********************* */
/*! \file quantifiers_engine.h
** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters, bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Francois Bobot
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
/* Call during quantifier engine's check */
virtual void check( Theory::Effort e ) = 0;
/* Called for new quantifiers */
- virtual void registerQuantifier( Node n ) = 0;
+ virtual void registerQuantifier( Node q ) = 0;
virtual void assertNode( Node n ) = 0;
virtual void propagate( Theory::Effort level ){}
virtual Node getNextDecisionRequest() { return TNode::null(); }
- virtual Node explain(TNode n) = 0;
+ virtual Node explain(TNode n) { return TNode::null(); }
};/* class QuantifiersModule */
namespace quantifiers {
- class InstantiationEngine;
- class ModelEngine;
class TermDb;
class FirstOrderModel;
+ //modules
+ class InstantiationEngine;
+ class ModelEngine;
+ class BoundedIntegers;
+ class QuantConflictFind;
+ class RewriteEngine;
+ class RelevantDomain;
}/* CVC4::theory::quantifiers */
namespace inst {
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
friend class quantifiers::ModelEngine;
+ friend class quantifiers::RewriteEngine;
friend class inst::InstMatch;
private:
typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
TheoryEngine* d_te;
/** vector of modules for quantifiers */
std::vector< QuantifiersModule* > d_modules;
- /** instantiation engine */
- quantifiers::InstantiationEngine* d_inst_engine;
- /** model engine */
- quantifiers::ModelEngine* d_model_engine;
/** equality query class */
EqualityQueryQuantifiersEngine* d_eq_query;
/** for computing relevance of quantifiers */
- QuantRelevance d_quant_rel;
+ QuantRelevance * d_quant_rel;
+ /** relevant domain */
+ quantifiers::RelevantDomain* d_rel_dom;
/** phase requirements for each quantifier for each instantiation literal */
std::map< Node, QuantPhaseReq* > d_phase_reqs;
/** efficient e-matcher */
EfficientEMatcher* d_eem;
+ /** instantiation engine */
+ quantifiers::InstantiationEngine* d_inst_engine;
+ /** model engine */
+ quantifiers::ModelEngine* d_model_engine;
+ /** bounded integers utility */
+ quantifiers::BoundedIntegers * d_bint;
+ /** Conflict find mechanism for quantifiers */
+ quantifiers::QuantConflictFind* d_qcf;
+ /** rewrite rules utility */
+ quantifiers::RewriteEngine * d_rr_engine;
private:
/** list of all quantifiers seen */
std::vector< Node > d_quants;
/** list of all lemmas produced */
- std::map< Node, bool > d_lemmas_produced;
+ //std::map< Node, bool > d_lemmas_produced;
BoolMap d_lemmas_produced_c;
/** lemmas waiting */
std::vector< Node > d_lemmas_waiting;
/** has added lemma this round */
bool d_hasAddedLemma;
/** list of all instantiations produced for each quantifier */
- std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie;
+ std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
+ std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
/** term database */
quantifiers::TermDb* d_term_db;
/** all triggers will be stored in this trie */
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
generic one */
- EqualityQuery* getEqualityQuery();
+ EqualityQueryQuantifiersEngine* getEqualityQuery();
/** get instantiation engine */
quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
/** get model engine */
OutputChannel& getOutputChannel();
/** get default valuation for the quantifiers engine */
Valuation& getValuation();
+ /** get relevant domain */
+ quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
/** get quantifier relevance */
- QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; }
+ QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
/** get phase requirement information */
QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
/** get phase requirement terms */
void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
/** get efficient e-matching utility */
EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
+ /** get bounded integers utility */
+ quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
+ /** Conflict find mechanism for quantifiers */
+ quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
public:
/** initialize */
void finishInit();
bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
/** set instantiation level attr */
void setInstantiationLevelAttr( Node n, uint64_t level );
+ /** do substitution */
+ Node doSubstitute( Node n, std::vector< Node >& terms );
public:
/** get instantiation */
Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
/** get instantiation */
Node getInstantiation( Node f, InstMatch& m );
+ /** get instantiation */
+ Node getInstantiation( Node f, std::vector< Node >& terms );
/** exist instantiation ? */
bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
/** add lemma lem */
bool addLemma( Node lem );
/** do instantiation specified by m */
- bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true );
+ bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
+ /** add instantiation */
+ bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
/** has added lemma */
bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
/** flush lemmas */
- void flushLemmas( OutputChannel* out );
+ void flushLemmas( OutputChannel* out = NULL );
/** get number of waiting lemmas */
int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
public:
IntStat d_instantiation_rounds;
IntStat d_instantiation_rounds_lc;
IntStat d_instantiations;
- IntStat d_max_instantiation_level;
- IntStat d_splits;
- IntStat d_total_inst_var;
- IntStat d_total_inst_var_unspec;
- IntStat d_inst_unspec;
IntStat d_inst_duplicate;
+ IntStat d_inst_duplicate_eq;
IntStat d_lit_phase_req;
IntStat d_lit_phase_nreq;
IntStat d_triggers;
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** internal representatives */
- std::map< int, std::map< Node, Node > > d_int_rep;
+ std::map< Node, Node > d_int_rep;
/** rep score */
std::map< Node, int > d_rep_score;
/** reset count */
Node getInstance( Node n, std::vector< Node >& eqc );
/** get score */
int getRepScore( Node n, Node f, int index );
- /** choose rep based on sort inference */
- bool optInternalRepSortInference();
public:
EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
~EqualityQueryQuantifiersEngine(){}
not contain instantiation constants, if such a term exists.
*/
Node getInternalRepresentative( Node a, Node f, int index );
+ /** flatten representatives */
+ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
void setLiberal( bool l ) { d_liberal = l; }
}; /* EqualityQueryQuantifiersEngine */
projects / cvc5.git / blobdiff