Cleanup some includes (#5847)

In particular, theory_engine.h is included many places spuriously.

A few blocks of code changed indentation, updated to guidelines.

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index af6cae7966b10a539afd771880af4bff567b53ef..075a50e0699b7978b9e9521da599b061da407dd7 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -26,6 +26,7 @@
 #include "base/check.h"
 #include "expr/node_algorithm.h"
 #include "options/options.h"
+#include "options/smt_options.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 04d6b7a0ca295f43438fed28ad30627522f719c6..f5d840a4907cc4bc44c9173a93757e7329019134 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"

diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index f1cdd5b5dc80275c00e3f3e009785d98e1caac6b..95e10732861c440166bf63a86e64b03f170cb3cd 100644 (file)
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
+#include "options/smt_options.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index fd0800f23b980c91b12d3a6b5a612110973c7cfd..5b046577293afa68eae6d09992c2a581bfa234d5 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 66a32472b48915b9c3bc4b269bb665f81049b937..c8b71389441468ba23ce46cb5193816f149fab2f 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -17,6 +17,7 @@
 
 #include "preprocessing/passes/ite_removal.h"
 
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
 

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 746bf33bde1134b27195acd08625fa10c13d1fee..2a1f4c3e6e771a9057fa0f5bef4888a2a16005ee 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -16,6 +16,7 @@
 
 #include <vector>
 
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 23a17c939f6d3267f0d5c1d59cf1f5414683c493..50dbc4a2778c6d74fc191e765327968a81e32d8c 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_self_iterator.h"
 #include "options/arith_options.h"
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 65682229952ccc83bf35cb63af5b04436abd1962..6db70156575f63ef92e170aec34523521ba0e650 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "context/cdo.h"
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 35eeac125cf4b4c37f6ee068a7cd90504c4b378e..69b6658548e9b52a4b17d780310782bdbe4df749 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 4552d13fc7462ebcf3cd9920afc952b80d5f0002..50831f585c3a4222bea42d8c06495b72f8c397f9 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/theory_preprocess.h"
 
+#include "options/smt_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index a6d570bc228516fb5bad20beebda46e43d4eb9d1..06e7297141b4f30ee0aeba54aa6e627bd6a73f96 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -19,6 +19,7 @@
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "options/decision_options.h"
+#include "options/smt_options.h"
 #include "proof/cnf_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 433eb9cd0cb61fc7af624dd981f4e6ead8909edb..c47d1c62416b1b495a21166506a5a075c084cb45 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/smt_solver.h"
 
+#include "options/smt_options.h"
 #include "prop/prop_engine.h"
 #include "smt/assertions.h"
 #include "smt/preprocessor.h"

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 402eeeb26306afb09c2dcb0a8c0e6801c7d2d6f0..1ebffc8c25291c1f69e7f34811ed6f7b2d6f9d2c 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -15,6 +15,7 @@
 #include "theory/combination_care_graph.h"
 
 #include "expr/node_visitor.h"
+#include "prop/prop_engine.h"
 #include "theory/care_graph.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index e4dddfdbf5d73169f322402b7631e5c42573c3c9..295b7309e892dcf623891d4653b9ba93309cc306 100644 (file)
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/model_manager.h"
 
+#include "options/smt_options.h"
 #include "options/theory_options.h"
+#include "prop/prop_engine.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index cb31e80d3148f2565be233ee66848900fd0abda3..c539bfdb019e98d0254f1caf2ca28c966c38bf28 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -15,7 +15,6 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
-#include "smt/term_formula_removal.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
@@ -26,7 +25,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 0fe1e6abef853c999ec51ac5ed971268af0e6b5e..97693fae08526157df880a4eedb130f2ffdecff4 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -22,8 +22,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 6d13ef2ee0f1bc52834787652ee43a60f1e17ee4..7479d005a8bfbcbc36f1e60d02a9ac9dbc29a07f 100644 (file)
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -19,8 +19,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
 

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 48c02f2884deacd029ff67d06ef927e50900c711..69c33d329b196de6cdd5c6af1a6c7325abd1d779 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -23,7 +23,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 427d82e7cb4b75b0e716051357f888a939bc8e03..715002f7b86be038ce84f4b2277e28abfeff6d2a 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -23,8 +23,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
 
 using namespace std;
 using namespace CVC4;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 4359b8b1900f5561d52da38c136e0925b4dfa9a4..c025dc29e5573b0436e43001c9f7fd944979dcf1 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -26,7 +26,6 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -643,31 +642,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
 bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
   Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
   Node rew = Rewriter::rewrite( lit );
-  if( rew==p->d_false ){
-    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
-    return false;
-  }else if( rew!=p->d_true ){
-    //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed 
-    if( !chEnt ){
-      rew = Rewriter::rewrite( rew.negate() );
-    }
-    //check if it is entailed
-    Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
-    std::pair<bool, Node> et =
-        p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(
-            options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
-    ++(p->d_statistics.d_entailment_checks);
-    Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
-    if( !et.first ){
-      Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
-      return !chEnt;
-    }else{
-      return chEnt;
-    }
-  }else{
-    Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
-    return true;
+  if (rew.isConst())
+  {
+    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to "
+                                   << rew << "." << std::endl;
+    return rew.getConst<bool>();
+  }
+  // if checking for conflicts, we must be sure that the (negation of)
+  // constraint is (not) entailed
+  if (!chEnt)
+  {
+    rew = Rewriter::rewrite(rew.negate());
+  }
+  // check if it is entailed
+  Trace("qcf-tconstraint-debug")
+      << "Check entailment of " << rew << "..." << std::endl;
+  std::pair<bool, Node> et = p->getState().getValuation().entailmentCheck(
+      options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
+  ++(p->d_statistics.d_entailment_checks);
+  Trace("qcf-tconstraint-debug")
+      << "ET result : " << et.first << " " << et.second << std::endl;
+  if (!et.first)
+  {
+    Trace("qcf-tconstraint-debug")
+        << "...cannot show entailment of " << rew << "." << std::endl;
+    return !chEnt;
   }
+  return chEnt;
 }
 
 bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 3ddfc4c9fde472f02866b3fd7efc98a18a70cadb..4f9a0ee91fe598938af3d7de525d09b4cf6890c8 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 9470b4e49d16328944cb00e0bca8fe513ae8ac3d..c09c78158699ab8e3a30a38dc82b2cd8d19c1d83 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 42e7e2f1316d7dd20d8f9ee2cc69bc25b326545d..239fa3c94cffc51f8662bcb53565bfbf465f2c81 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index b007f8716710159476ef06d95d111ca216d7bc63..c1333b85fc41fd2d71373b1d0dbae0dbe2ae4d59 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -18,7 +18,6 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
-#include "prop/prop_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -33,7 +32,6 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/smt_engine_subsolver.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 43051eb99c3deb25755cde1b754e9400c47348fd..4b35bc5452252deb47aae774c447d1e416805449 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -21,7 +21,6 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index c4c722ab253fa6dc9a6ea9488853593f7976381c..66c9cbf7913da91e585bc76db27106d274e84f20 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -24,7 +24,6 @@
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c39654aa582e1222f52b19ea5087f8ec38c9be91..5a6e38b780e8d476098241f9ec878277a53e6651 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -16,6 +16,7 @@
 
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index d01d6a83f4ebd6facf50b1183a25d29fae057230..b0a067630580390ebda3bff1b0139bc3420a7146 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
-#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6338c30b3840f25561b63f57b5a659925c60960f..28397fd14db95428d59dd005416b5836b6a3cfef 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -16,6 +16,7 @@
 
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bd03a4d03aafa3eb645b72ef0a5440ba40c720b6..66c9b9f20a1d5dcb44aea4dd1fece6732c9ae70f 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -16,33 +16,23 @@
 
 #include "theory/theory_engine.h"
 
-#include <list>
-#include <vector>
-
 #include "base/map_util.h"
 #include "decision/decision_engine.h"
 #include "expr/attribute.h"
 #include "expr/lazy_proof.h"
-#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_visitor.h"
 #include "expr/proof_ensure_closed.h"
-#include "options/bv_options.h"
-#include "options/options.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"
+#include "prop/prop_engine.h"
 #include "smt/dump.h"
 #include "smt/logic_exception.h"
-#include "smt/term_formula_removal.h"
-#include "theory/arith/arith_ite_utils.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/care_graph.h"
 #include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1a944768157abdc9e6e5fb5bbe19d6b07f3e0b7e..d72a999b2c218fd295f06e0c9036f8f8b358d045 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -19,20 +19,13 @@
 #ifndef CVC4__THEORY_ENGINE_H
 #define CVC4__THEORY_ENGINE_H
 
-#include <deque>
 #include <memory>
-#include <set>
-#include <unordered_map>
-#include <utility>
 #include <vector>
 
 #include "base/check.h"
-#include "context/cdhashset.h"
+#include "context/cdhashmap.h"
 #include "expr/node.h"
-#include "options/options.h"
-#include "options/smt_options.h"
 #include "options/theory_options.h"
-#include "prop/prop_engine.h"
 #include "theory/atom_requests.h"
 #include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
@@ -46,13 +39,13 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
-#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
 class ResourceManager;
+class OutputManager;
 class TheoryEngineProofGenerator;
 
 /**
@@ -92,11 +85,12 @@ class SharedSolver;
 class DecisionManager;
 class RelevanceManager;
 
-namespace eq {
-class EqualityEngine;
-}  // namespace eq
 }/* CVC4::theory namespace */
 
+namespace prop {
+class PropEngine;
+}
+
 /**
  * This is essentially an abstraction for a collection of theories.  A
  * TheoryEngine provides services to a PropEngine, making various

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 3ea4c88e604fa8fa9810f901a3d74e73a061f313..bd69245b8cc25928e76ba2bef96c0f4592839b5d 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -14,13 +14,14 @@
 
 #include "theory/uf/cardinality_extension.h"
 
+#include "options/smt_options.h"
 #include "options/uf_options.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index a014cccb239fbdf94d69b68f8bc23b5be68bf32d..043ab0daba2d253bbefade4f05aea07316687439 100644 (file)
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -15,21 +15,15 @@
 #include "theory/uf/theory_uf_model.h"
 
 #include <stack>
-#include <vector>
 
 #include "expr/attribute.h"
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
 
-using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
 
 //clear
 void UfModelTreeNode::clear(){
@@ -63,14 +57,17 @@ Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node
       defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
     }
 
-    vector<Node> caseArgs;
-    map<Node, Node> caseValues;
+    std::vector<Node> caseArgs;
+    std::map<Node, Node> caseValues;
 
-    for(map< Node, UfModelTreeNode>::iterator it = d_data.begin(); it != d_data.end(); ++it) {
-      if(!it->first.isNull()) {
-        Node val = it->second.getFunctionValue(args, index + 1, defaultValue, simplify);
-        caseArgs.push_back(it->first);
-        caseValues[it->first] = val;
+    for (std::pair<const Node, UfModelTreeNode>& p : d_data)
+    {
+      if (!p.first.isNull())
+      {
+        Node val =
+            p.second.getFunctionValue(args, index + 1, defaultValue, simplify);
+        caseArgs.push_back(p.first);
+        caseValues[p.first] = val;
       }
     }
 
@@ -86,7 +83,7 @@ Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node
         Node val = caseValues[ caseArgs[ i ] ];
         if(val.getKind() == ITE) {
           // use a stack to reverse the order, since we're traversing outside-in
-          stack<TNode> stk;
+          std::stack<TNode> stk;
           do {
             stk.push(val);
             val = val[2];
@@ -237,3 +234,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
   }
   return getFunctionValue( vars, simplify );
 }
+
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC4

diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 1165f310c338b86c71ef478cbe58a9a804678129..a1576a26d6ad998ce46f64fc3847e0cda304bcb6 100644 (file)
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -17,6 +17,9 @@
 #ifndef CVC4__THEORY_UF_MODEL_H
 #define CVC4__THEORY_UF_MODEL_H
 
+#include <vector>
+
+#include "expr/node.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 6fae8421dac37585263ad4937bcc5ae86719f504..1926c836ed5fd213e30da3378dcf2c6a85d67ead 100644 (file)
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "options/theory_options.h"
+#include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"