diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 12:32:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 12:33:07 -0500 |
commit | 358e453bda62923fd0be94af5317b24a7281014b (patch) | |
tree | f2fdb4efc7a97341c2b77dca0fce96b28e7f591b /src/theory/quantifiers/term_database.h | |
parent | 4a00ff296240ff81ee909937ade8cc8aa88561df (diff) |
Implement equality inference module for arithmetic terms. Optimization for entailment checks. Other minor infrastructure.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 6b8f9c783..62da8c347 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -174,8 +174,14 @@ private: std::hash_set< Node, NodeHashFunction > d_iclosure_processed; /** select op map */ std::map< Node, std::map< TypeNode, Node > > d_par_op_map; + /** whether master equality engine is UF-inconsistent */ + bool d_consistent_ee; /** 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 ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -213,7 +219,7 @@ public: /** presolve (called once per user check-sat) */ void presolve(); /** reset (calculate which terms are active) */ - void reset( Theory::Effort effort ); + bool reset( Theory::Effort effort ); /** get match operator */ Node getMatchOperator( Node n ); /** get term arg index */ @@ -228,9 +234,9 @@ public: /** evaluate a term under a substitution. Return representative in EE if possible. * subsRep is whether subs contains only representatives */ - TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ); + Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false ); /** same as above, but without substitution */ - TNode evaluateTerm( TNode n ); + Node evaluateTerm( TNode n, bool mkNewTerms = false ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ |