diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-09 09:51:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-09 09:51:52 -0600 |
| commit | 22b211647501a4dad5cec66c2ea6383ea8e7b7bd (patch) | |
| tree | c4d3f95a8706dfd3c74d73e2d875bda09ef0fd90 /src/theory/quantifiers/term_database.cpp | |
| parent | a9cf481470c324a04f2254c5745eee26c45cb309 (diff) | |
Decouple sygus term database and term database. (#1317)
* Decouple sygus term database and term database.
* Clang format
* Fix include
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index a3225e404..5db58067f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,20 +14,12 @@ #include "theory/quantifiers/term_database.h" -#include "expr/datatype.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "options/datatypes_options.h" #include "options/uf_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" @@ -250,10 +242,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_ops.push_back(op); d_op_map[op].push_back( n ); added.insert( n ); - - if( d_quantEngine->getTermDatabaseSygus() ){ - d_quantEngine->getTermDatabaseSygus()->registerEvalTerm( n ); - } } }else{ setTermInactive( n ); |