diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-09 13:07:11 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-09 13:07:11 -0500 |
commit | 67623ee1e6d62b36cb598c28ad9b871b6957a9dd (patch) | |
tree | 3ea7e16b6b1f8e2073ad9265741fa7853b63c0df /src/theory/quantifiers/quant_util.h | |
parent | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (diff) |
Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 56 |
1 files changed, 55 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 8db79db9c..79cdae437 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -29,6 +29,58 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { + class TermDb; +} + +class QuantifiersModule { +protected: + QuantifiersEngine* d_quantEngine; +public: + QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + virtual ~QuantifiersModule(){} + //get quantifiers engine + QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + /** presolve */ + virtual void presolve() {} + /* whether this module needs to check this round */ + virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } + /* whether this module needs a model built */ + virtual unsigned needsModel( Theory::Effort e ); + /* reset at a round */ + virtual void reset_round( Theory::Effort e ){} + /* Call during quantifier engine's check */ + virtual void check( Theory::Effort e, unsigned quant_e ) = 0; + /* check was complete (e.g. no lemmas implies a model) */ + virtual bool checkComplete() { return true; } + /* Called for new quantified formulas */ + virtual void preRegisterQuantifier( Node q ) { } + /* Called for new quantifiers after owners are finalized */ + virtual void registerQuantifier( Node q ) = 0; + virtual void assertNode( Node n ) {} + virtual void propagate( Theory::Effort level ){} + virtual Node getNextDecisionRequest() { 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 */ + +class QuantifiersUtil { +public: + QuantifiersUtil(){} + virtual ~QuantifiersUtil(){} + /* reset at a round */ + virtual bool reset( Theory::Effort e ) = 0; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; +}; + + class QuantArith { public: @@ -97,7 +149,7 @@ public: }; -class EqualityQuery { +class EqualityQuery : public QuantifiersUtil{ public: EqualityQuery(){} virtual ~EqualityQuery(){}; @@ -115,6 +167,8 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; + /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */ + virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ |