** 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
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
class QuantifiersEngine;
+namespace quantifiers {
+ class TermDb;
+}
+
class QuantifiersModule {
protected:
QuantifiersEngine* d_quantEngine;
/* reset at a round */
virtual void reset_round( Theory::Effort e ){}
/* Call during quantifier engine's check */
- virtual void check( Theory::Effort e ) = 0;
+ virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
/* Called for new quantifiers */
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) { return TNode::null(); }
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const = 0;
+public:
+ eq::EqualityEngine * getEqualityEngine();
+ bool areDisequal( TNode n1, TNode n2 );
+ bool areEqual( TNode n1, TNode n2 );
+ TNode getRepresentative( TNode n );
+ quantifiers::TermDb * getTermDatabase();
};/* class QuantifiersModule */
namespace quantifiers {
- class TermDb;
class FirstOrderModel;
//modules
class InstantiationEngine;
class QuantConflictFind;
class RewriteEngine;
class RelevantDomain;
+ class ConjectureGenerator;
+ class CegInstantiation;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::QuantConflictFind* d_qcf;
/** rewrite rules utility */
quantifiers::RewriteEngine * d_rr_engine;
+ /** subgoal generator */
+ quantifiers::ConjectureGenerator * d_sg_gen;
+ /** ceg instantiation */
+ quantifiers::CegInstantiation * d_ceg_inst;
+public: //effort levels
+ enum {
+ QEFFORT_CONFLICT,
+ QEFFORT_STANDARD,
+ QEFFORT_MODEL,
+ };
private:
/** list of all quantifiers seen */
std::vector< Node > d_quants;
BoolMap d_lemmas_produced_c;
/** lemmas waiting */
std::vector< Node > d_lemmas_waiting;
+ /** phase requirements waiting */
+ std::map< Node, bool > d_phase_req_waiting;
/** has added lemma this round */
bool d_hasAddedLemma;
+ /** has a conflict been found */
+ bool d_conflict;
/** list of all instantiations produced for each quantifier */
std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
+ /** quantifiers that have been skolemized */
+ std::map< Node, bool > d_skolemized;
/** term database */
quantifiers::TermDb* d_term_db;
/** all triggers will be stored in this trie */
/** get equality query object for the given type. The default is the
generic one */
EqualityQueryQuantifiersEngine* getEqualityQuery();
- /** get instantiation engine */
- quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
- /** get model engine */
- quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
/** get default sat context for quantifiers engine */
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 );
+public: //modules
+ /** get instantiation engine */
+ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
+ /** get model engine */
+ quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
/** get bounded integers utility */
quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
/** Conflict find mechanism for quantifiers */
quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+ /** rewrite rules utility */
+ quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
+ /** subgoal generator */
+ quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+ /** ceg instantiation */
+ quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+private:
+ /** owner of quantified formulas */
+ std::map< Node, QuantifiersModule * > d_owner;
+public:
+ /** get owner */
+ QuantifiersModule * getOwner( Node q );
+ /** set owner */
+ void setOwner( Node q, QuantifiersModule * m );
+ /** considers */
+ bool hasOwnership( Node q, QuantifiersModule * m = NULL );
public:
/** initialize */
void finishInit();
/** register quantifier */
void registerPattern( std::vector<Node> & pattern);
/** assert universal quantifier */
- void assertNode( Node f );
+ void assertQuantifier( Node q, bool pol );
/** propagate */
void propagate( Theory::Effort level );
/** get next decision request */
/** instantiate f with arguments terms */
bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
/** set instantiation level attr */
- void setInstantiationLevelAttr( Node n, uint64_t level );
+ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
+ /** flush lemmas */
+ void flushLemmas();
public:
/** get instantiation */
Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
/** add lemma lem */
bool addLemma( Node lem, bool doCache = true );
+ /** add require phase */
+ void addRequirePhase( Node lit, bool req );
/** do instantiation specified by m */
bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
/** add instantiation */
bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
/** has added lemma */
bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
- /** flush lemmas */
- void flushLemmas( OutputChannel* out = NULL );
/** get number of waiting lemmas */
int getNumLemmasWaiting() { return (int)d_lemmas_waiting.size(); }
+ /** set instantiation level attr */
+ static void setInstantiationLevelAttr( Node n, uint64_t level );
+ /** is term eligble for instantiation? */
+ bool isTermEligibleForInstantiation( Node n, Node f, bool print = false );
public:
/** get number of quantifiers */
int getNumQuantifiers() { return (int)d_quants.size(); }
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
public:
+ /** print instantiations */
+ void printInstantiations( std::ostream& out );
/** statistics class */
class Statistics {
public:
~Statistics();
};/* class QuantifiersEngine::Statistics */
Statistics d_statistics;
-public:
- /** options */
- bool d_optInstCheckDuplicate;
- bool d_optInstMakeRepresentative;
- bool d_optInstAddSplits;
- bool d_optMatchIgnoreModelBasis;
- bool d_optInstLimitActive;
- int d_optInstLimit;
};/* class QuantifiersEngine */
bool d_liberal;
private:
/** node contains */
- Node getInstance( Node n, std::vector< Node >& eqc );
+ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
/** get score */
int getRepScore( Node n, Node f, int index );
public:
projects / cvc5.git / blobdiff