diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-13 17:44:19 -0500 |
| commit | 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 (patch) | |
| tree | 9cc4ed5a09640c3dbb8df9cbaf242ade0f8acc4f /src/theory/theory.h | |
| parent | 7e750757ac9832b70b5c6ca1d15e17cddbd2e6c0 (diff) | |
Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 5d64c6446..28552ed79 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -1016,6 +1016,8 @@ protected: bool doInferencesInternal( int effort, 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::map< Node, bool >& visited ); public: ExtTheory( Theory * p ); virtual ~ExtTheory(){} @@ -1024,6 +1026,7 @@ public: //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 ); |