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/term_database.h | |
parent | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (diff) |
Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9177d3a1a..76bd623a8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -164,7 +164,7 @@ namespace fmcheck { class TermDbSygus; -class TermDb { +class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; @@ -183,9 +183,9 @@ private: /** set has term */ void setHasTerm( Node n ); /** evaluate term */ - TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); - Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ); - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); + Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ); + TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -224,13 +224,16 @@ public: void presolve(); /** reset (calculate which terms are active) */ bool reset( Theory::Effort effort ); + /** identify */ + std::string identify() const { return "TermDb"; } /** get match operator */ Node getMatchOperator( Node n ); /** get term arg index */ TermArgTrie * getTermArgTrie( Node f ); TermArgTrie * getTermArgTrie( Node eqc, Node f ); /** exists term */ - TNode existsTerm( Node f, Node n ); + TNode getCongruentTerm( Node f, Node n ); + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); /** compute arg reps */ void computeArgReps( TNode n ); /** compute uf eqc terms */ @@ -238,10 +241,12 @@ public: /** evaluate a term under a substitution. Return representative in EE if possible. * subsRep is whether subs contains only representatives */ - Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL ); - /** same as above, but without substitution */ - Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL ); + Node evaluateTerm( TNode n, EqualityQuery * qy = NULL ); + /** get entailed term, does not construct new terms, less aggressive */ + TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL ); + TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL ); /** is entailed (incomplete check) */ + bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL ); bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); |