diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 724f16947..f3bbc65cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -13,22 +13,23 @@ **/ #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "util/datatype.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" //for sygus +#include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" -#include "smt/smt_engine_scope.h" using namespace std; using namespace CVC4; @@ -2807,4 +2808,3 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << n; } } - |