diff options
author | Tim King <taking@google.com> | 2017-04-02 19:29:36 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-04-02 19:29:36 -0700 |
commit | f278f060c177593a1835422e688fe2a022c40e2f (patch) | |
tree | cc2eaa62bfc4c581643cbd237d93247b8c40134f /src/theory/theory.h | |
parent | e9f3b6a54e4bf35f915c46d822ed9ee051cc7df3 (diff) |
Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 445d184e4..611e487f1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -843,6 +843,9 @@ public: return false; } + /* is extended function reduced */ + virtual bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) { return n.isConst(); } + /** * Get reduction for node * If return value is not 0, then n is reduced. @@ -940,9 +943,6 @@ private: //set of terms from d_ext_func_terms that are SAT-context-independently inactive // (e.g. term t when a reduction lemma of the form t = t' was added) NodeSet d_ci_inactive; - //cache of all lemmas sent - NodeSet d_lemmas; - NodeSet d_pp_lemmas; //watched term for checking if any non-reduced extended functions exist context::CDO< Node > d_has_extf; //extf kind @@ -955,8 +955,21 @@ private: }; std::map< Node, ExtfInfo > d_extf_info; + //cache of all lemmas sent + NodeSet d_lemmas; + NodeSet d_pp_lemmas; + bool d_cacheEnabled; + // if d_cacheEnabled=true : + //cache for getSubstitutedTerms + class SubsTermInfo { + public: + Node d_sterm; + std::vector< Node > d_exp; + }; + std::map< int, std::map< Node, SubsTermInfo > > d_gst_cache; + public: - ExtTheory(Theory* p); + ExtTheory(Theory* p, bool cacheEnabled = false ); virtual ~ExtTheory() {} // add extf kind void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -972,13 +985,13 @@ private: void markReduced( Node n, bool contextDepend = true ); // mark that a and b are congruent terms: set b inactive, set a to inactive if b was inactive void markCongruent( Node a, Node b ); - //getSubstitutedTerms // input : effort, terms // output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + Node getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache = false ); void getSubstitutedTerms(int effort, const std::vector<Node>& terms, std::vector<Node>& sterms, - std::vector<std::vector<Node> >& exp); + std::vector<std::vector<Node> >& exp, bool useCache = false); // doInferences // * input : effort, terms, batch (whether to send one lemma or lemmas for // all terms) @@ -996,6 +1009,8 @@ private: std::vector<Node>& nred, bool batch = true); bool doReductions(int effort, std::vector<Node>& nred, bool batch = true); + //get the set of terms from d_ext_func_terms + void getTerms( std::vector< Node >& terms ); // has active term bool hasActiveTerm(); // is n active @@ -1004,6 +1019,8 @@ private: std::vector<Node> getActive() const; // get the set of active terms from d_ext_func_terms of kind k std::vector<Node> getActive(Kind k) const; + //clear cache + void clearCache(); }; }/* CVC4::theory namespace */ |