diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
| commit | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (patch) | |
| tree | 57cee5cddf68999e20553ee9746f4a83183e8b99 /src/theory/quantifiers/term_database.h | |
| parent | 576d50ac7c13233a589771401537b587eb36361e (diff) | |
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 4cba619a8..9177d3a1a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -20,6 +20,7 @@ #include "expr/attribute.h" #include "theory/theory.h" #include "theory/type_enumerator.h" +#include "theory/quantifiers/quant_util.h" #include <map> @@ -182,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 ); - Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited ); - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ); + 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 ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -237,11 +238,11 @@ 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 ); + 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 ); + Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL ); /** is entailed (incomplete check) */ - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); + 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 ); /** is term eligble for instantiation? */ |