diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-06 20:58:31 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-06 20:58:31 +0100 |
commit | 97ab81d20887f58c90365ba622c7c84148ca8033 (patch) | |
tree | 3a0783de8a7e04c3e9af81394acbc6ed328f3660 /src/theory/theory.h | |
parent | c7b228cb620cdb7736cdcc30e486797cf6282b66 (diff) |
Split ext theory to own file and document (#1809)
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 104 |
1 files changed, 0 insertions, 104 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 231a56967..3721806ad 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -900,110 +900,6 @@ public: virtual ~EntailmentCheckSideEffects(); };/* class EntailmentCheckSideEffects */ - -class ExtTheory { - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; - typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; -private: - // collect variables - static std::vector<Node> collectVars(Node n); - // is context dependent inactive - bool isContextIndependentInactive( Node n ) const; - //do inferences internal - bool doInferencesInternal(int effort, const std::vector<Node>& terms, - std::vector<Node>& nred, bool batch, bool isRed); - // send lemma - bool sendLemma( Node lem, bool preprocess = false ); - // register term (recursive) - void registerTermRec(Node n, std::set<Node>* visited); - - Theory * d_parent; - Node d_true; - //extended string terms, map to whether they are active - NodeBoolMap d_ext_func_terms; - //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; - //watched term for checking if any non-reduced extended functions exist - context::CDO< Node > d_has_extf; - //extf kind - std::map< Kind, bool > d_extf_kind; - //information for each term in d_ext_func_terms - class ExtfInfo { - public: - //all variables in this term - std::vector< Node > d_vars; - }; - 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, bool cacheEnabled = false ); - virtual ~ExtTheory() {} - // add extf kind - void addFunctionKind(Kind k) { d_extf_kind[k] = true; } - bool hasFunctionKind(Kind k) const { - return d_extf_kind.find(k) != d_extf_kind.end(); - } - // register term - // adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called - void registerTerm( Node n ); - void registerTermRec( Node n ); - // set n as reduced/inactive - // if contextDepend = false, then n remains inactive in the duration of this user-context level - 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, bool useCache = false); - // doInferences - // * input : effort, terms, batch (whether to send one lemma or lemmas for - // all terms) - // * sends rewriting lemmas of the form ( exp => t = c ) where t is in terms - // and c is a constant, c = rewrite( t*sigma ) where exp |= sigma - // * output : nred (the terms that are still active) - // * return : true iff lemma is sent - bool doInferences(int effort, const std::vector<Node>& terms, - std::vector<Node>& nred, bool batch = true); - bool doInferences(int effort, std::vector<Node>& nred, bool batch = true); - //doReductions - // same as doInferences, but will send reduction lemmas of the form ( t = t' ) - // where t is in terms, t' is equivalent, reduced term. - bool doReductions(int effort, const std::vector<Node>& terms, - 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 - bool isActive(Node n); - // get the set of active terms from d_ext_func_terms - 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 */ }/* CVC4 namespace */ |