diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 55 |
1 files changed, 21 insertions, 34 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b5a2a1390..52922e2ca 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -14,51 +14,38 @@ ** The theory engine. **/ -#include <vector> -#include <list> +#include "theory/theory_engine.h" -#include "theory/arith/arith_ite_utils.h" +#include <list> +#include <vector> #include "decision/decision_engine.h" - #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "expr/resource_manager.h" +#include "options/bv_options.h" #include "options/options.h" -#include "util/lemma_output_channel.h" -#include "util/resource_manager.h" - -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/rewriter.h" -#include "theory/theory_traits.h" - -#include "smt/logic_exception.h" - +#include "options/quantifiers_options.h" #include "proof/proof_manager.h" - -#include "util/node_visitor.h" -#include "util/ite_removal.h" - -//#include "theory/ite_simplifier.h" -//#include "theory/ite_compressor.h" +#include "proof/proof_manager.h" +#include "smt/logic_exception.h" +#include "smt_util/ite_removal.h" +#include "smt_util/lemma_output_channel.h" +#include "smt_util/node_visitor.h" +#include "theory/arith/arith_ite_utils.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/ite_utilities.h" -#include "theory/unconstrained_simplifier.h" - -#include "theory/theory_model.h" - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/first_order_model.h" - +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/theory.h" +#include "theory/theory_model.h" +#include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -//#include "theory/rewriterules/efficient_e_matching.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/bv/options.h" - -#include "proof/proof_manager.h" +#include "theory/unconstrained_simplifier.h" using namespace std; |