Remove forward declarations in quantifiers engine (#3156)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 914e20b0540966bd19902cf360425539a65dd73e..b66d230b77dd93ef2078a73a11df3b4f3b4a08c5 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -102,6 +102,7 @@
 #include "theory/quantifiers/sygus/sygus_abduct.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index ea3bb5f72930ec30a0c41ff60003e144367a1e9c..334b3d63886fe03c4224fce343785894af58d7d7 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index f7d433078a1cd9c475d84bd8ef56dbe95f86502b..9d516de61667500f00ce7e819fd65809eff27878 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/alpha_equivalence.h"
 
+#include "theory/quantifiers_engine.h"
+
 using namespace CVC4;
 using namespace std;
 using namespace CVC4::theory;

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 5ef778b8dd051bcea9a829dafd80a69a236f3583..3f92350de90889f92cffb18561cca7adfa7cb804 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -17,8 +17,7 @@
 #ifndef CVC4__ALPHA_EQUIVALENCE_H
 #define CVC4__ALPHA_EQUIVALENCE_H
 
-
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include "expr/term_canonize.h"
 

diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 3a7dc2da848d0a7211730c1b1a2991a197a7705c..60b5571c551240a8d725beb50a4391f743f53fa8 100644 (file)
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -24,8 +24,8 @@
 #include "context/cdo.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/single_inv_partition.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index fa02c6d09d3bbcff7541e9c58feea6994efb2178..3a498277ae8178e0bec8125f08823bd16509d28c 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -21,6 +21,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 28a24d8849efda5025312278a03ebc14b06e6c8c..90b7002b32d8336cd28c63a3bffcbc59ba201105 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -18,12 +18,13 @@
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 
 using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 0bdcbe0d7a15fb4eb1d61acd0326d6d8c1d4bc6e..6c4f2c620aebbaf15cb4469b142b0ac563b58df7 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -18,7 +18,6 @@
 
 using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
index f0ea7ab7b80d9be1645d2474c3298bcfb71e1ae3..2aa2a927bd7f2d1a140e4f2b98cf1483a91f1408 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
@@ -18,6 +18,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index b113585434586eaf3460b6becc5482de2e2f0ae1..6427b52d51919ca2904e4d33eeb90afc5c746d0d 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -23,18 +23,18 @@
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
-using namespace CVC4::context;
 
 namespace CVC4 {
 namespace theory {
@@ -79,6 +79,63 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status)
   return os;
 }
 
+void TermProperties::composeProperty(TermProperties& p)
+{
+  if (p.d_coeff.isNull())
+  {
+    return;
+  }
+  if (d_coeff.isNull())
+  {
+    d_coeff = p.d_coeff;
+  }
+  else
+  {
+    d_coeff = NodeManager::currentNM()->mkNode(MULT, d_coeff, p.d_coeff);
+    d_coeff = Rewriter::rewrite(d_coeff);
+  }
+}
+
+// push the substitution pv_prop.getModifiedTerm(pv) -> n
+void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
+{
+  d_vars.push_back(pv);
+  d_subs.push_back(n);
+  d_props.push_back(pv_prop);
+  if (pv_prop.isBasic())
+  {
+    return;
+  }
+  d_non_basic.push_back(pv);
+  // update theta value
+  Node new_theta = getTheta();
+  if (new_theta.isNull())
+  {
+    new_theta = pv_prop.d_coeff;
+  }
+  else
+  {
+    new_theta =
+        NodeManager::currentNM()->mkNode(MULT, new_theta, pv_prop.d_coeff);
+    new_theta = Rewriter::rewrite(new_theta);
+  }
+  d_theta.push_back(new_theta);
+}
+// pop the substitution pv_prop.getModifiedTerm(pv) -> n
+void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
+{
+  d_vars.pop_back();
+  d_subs.pop_back();
+  d_props.pop_back();
+  if (pv_prop.isBasic())
+  {
+    return;
+  }
+  d_non_basic.pop_back();
+  // update theta value
+  d_theta.pop_back();
+}
+
 CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
                                  CegqiOutput* out,
                                  bool use_vts_delta,

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 0a09f39c75983aefaac70a8c5466188b90fdc110..da57cdd169e90f97bbd365e6b1bce267d9196730 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -18,11 +18,16 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
 #define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
 
-#include "theory/quantifiers_engine.h"
+#include <vector>
+
+#include "expr/node.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class CegqiOutput {
@@ -70,15 +75,7 @@ public:
   }
   // compose property, should be such that: 
   //   p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x )
-  virtual void composeProperty( TermProperties& p ){
-    if( !p.d_coeff.isNull() ){
-      if( d_coeff.isNull() ){
-        d_coeff = p.d_coeff;
-      }else{
-        d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) );
-      }
-    }
-  }
+  virtual void composeProperty(TermProperties& p);
 };
 
 /** Solved form
@@ -97,34 +94,9 @@ public:
   //   an example is for linear arithmetic, we store "substitution with coefficients".
   std::vector<Node> d_non_basic;
   // push the substitution pv_prop.getModifiedTerm(pv) -> n
-  void push_back( Node pv, Node n, TermProperties& pv_prop ){
-    d_vars.push_back( pv );
-    d_subs.push_back( n );
-    d_props.push_back( pv_prop );
-    if( !pv_prop.isBasic() ){
-      d_non_basic.push_back( pv );
-      // update theta value
-      Node new_theta = getTheta();
-      if( new_theta.isNull() ){
-        new_theta = pv_prop.d_coeff;
-      }else{
-        new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff );
-        new_theta = Rewriter::rewrite( new_theta );
-      }
-      d_theta.push_back( new_theta );
-    }
-  }
+  void push_back(Node pv, Node n, TermProperties& pv_prop);
   // pop the substitution pv_prop.getModifiedTerm(pv) -> n
-  void pop_back( Node pv, Node n, TermProperties& pv_prop ){
-    d_vars.pop_back();
-    d_subs.pop_back();
-    d_props.pop_back();
-    if( !pv_prop.isBasic() ){
-      d_non_basic.pop_back();
-      // update theta value
-      d_theta.pop_back();
-    }
-  }
+  void pop_back(Node pv, Node n, TermProperties& pv_prop);
   // is this solved form empty?
   bool empty() { return d_vars.empty(); }
 public:

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 7cfda5ba18b1fe9dba08cb653438956df8d5411a..0f866208de0f8bef2f3668d75b3ab768761d7a0e 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #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;

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index ebebb808d1437ceed002924f56df22792ef4e342..c6a9ddd1156a59203b6518cc9dc545bc2d21e677 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -20,6 +20,7 @@
 
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 2dbc2627bbf1f0df4fea32c964c97fd510caf5ea..400db4a8ed094a978d2524b06618a3fc307c61f7 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "util/random.h"
 

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 236c08138f53d6842f68450c98e68fc4296f06a6..3845337259be8467646fc5479f4a9ea20a25754d 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -19,7 +19,7 @@
 
 #include "context/cdhashmap.h"
 #include "expr/node_trie.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/type_enumerator.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index ce328df2e5df9d4791fe07839181715ca00b7523..c4b15a852890797c28abab8427626c96d277bd02 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "util/random.h"
 

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 5eb992368246be29bb7a6d1fe31cb7652e500638..b71b8ee477b54b5f6af4a1755bdd6c067abf177d 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -21,7 +21,6 @@
 #include "context/context_mm.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers_engine.h"
 #include "util/statistics_registry.h"
 #include "options/quantifiers_options.h"
 

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d2650f01f4a85b57ba65c96eb879a063b4a1574c..bb70002a0d54f2928cf46a8c197a23c6175833a3 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -15,11 +15,12 @@
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 139adcb0468f98ddc43cc956a438b5167414fabc..b959bef2d8a8004b78e71290dfac8509928d7e08 100644 (file)
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -17,10 +17,9 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 #define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 
-#include <memory>
+#include <vector>
 
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -64,7 +63,6 @@ class InstantiationEngine : public QuantifiersModule {
   /** auto gen triggers; only kept for destructor cleanup */
   std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
 
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   /** current processing quantified formulas */
   std::vector<Node> d_quants;
 

diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 030b0dccb446aaa3847e6dc826cff416fa713162..22d6a378220e268f65cf099af6239000d76af15a 100644 (file)
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #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"
 

diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index e4eeeffa71c38c2d23ad8b01dff8fce3bca41233..1000b97e9950cbf3e7092bc02a0a48b00c8199bb 100644 (file)
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -21,7 +21,6 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index 1c8aab82690faf5f5a6f7122a6d014d430f22c47..b9c772f00a4f27ddb682d8dc321d9d67dbabf979 100644 (file)
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -23,10 +23,12 @@
 #include "theory/quantifiers/query_generator.h"
 #include "theory/quantifiers/solution_filter.h"
 #include "theory/quantifiers/sygus_sampler.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 /** ExpressionMinerManager

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index dbf368e6634dd7ce959d73aceac4c4729ff1d720..b2b4c967bceb10bf5d8d4d156b172350a8e09f70 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 27d21218da59f3564d21d51670c9db6d3117fbc3..51b40f589891935c87cb52773442f44f8e519d9f 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -18,7 +18,6 @@
 #define CVC4__FIRST_ORDER_MODEL_H
 
 #include "expr/attribute.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
 

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index f873b94f252e0a0736104aa987c63a8a23898897..879771903f2b6894e68e10237b4a1712e2c92125 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4;

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 55ed5bdd2f9e9cee68f7ee0b6452d4a8881c9ca8..8e6738e9ed950ed3c1e73f9bc6561d206f2a8126 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -18,8 +18,7 @@
 #ifndef CVC4__BOUNDED_INTEGERS_H
 #define CVC4__BOUNDED_INTEGERS_H
 
-
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 #include "context/context.h"
 #include "context/context_mm.h"

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index ace5c2b26ba74324ee1ac4890e1318402f84a838..0f06cef74436caa16570fe5015463657e3ad7af7 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "theory/quantifiers/fmf/full_model_check.h"
+
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
@@ -20,6 +21,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4;

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 51cd8481f58edd69b5f009dce813148627464a1e..cdbc5e391b31fd95423ababe0503d60278f55342 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -15,13 +15,14 @@
 #include "theory/quantifiers/fmf/model_builder.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/fmf/model_engine.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 1b4d24779c370ab6de54c0677cb492a49834a5de..c8f59defeb5d09af9ef61945eb736647e9df1961 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -17,9 +17,10 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
-#include "theory/quantifiers_engine.h"
+#include "expr/node.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_match.h"
 #include "theory/theory_model_builder.h"
-#include "theory/uf/theory_uf_model.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 5609cade63b5f43912a79bcbdc55b7175f74e81e..f34dc1b8528bf7e16dcf3ac89b23f6ed01aa7594 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #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.h"

diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 41bc312e7e9c861bbd08d1af12a06a057209ed85..b39dd03f8a00efca6ad9c398140eea52f686adda 100644 (file)
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 #define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
-#include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 56be1506c8debadfb08aafa81f4c5f557d21a917..a3c114d90c4556dc7cf121aa4240489ac8b7e371 100644 (file)
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers/inst_propagator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4;

diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index d45b078ce9166b1874d34037d389694732045731..d69439ae670230d752f7e027edfbb33f3bdcd6f4 100644 (file)
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -25,7 +25,7 @@
 #include "expr/node_trie.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 7a2f62864f9e40cbab36fd9668cddbd3a6d1ad89..70d855f45a2eb2a29eda8939db20d355afe18ea6 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 920e643bca530afe618b966c797a59fd9d53b7db..e58993182df6f6df716d846f213748eaed543f94 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -19,7 +19,7 @@
 
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 7ecf9866a59c8207ed90dbf441cd11d0f3807e6a..df23adcdd620522c28be5c5155d830c5b4e05385 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -16,13 +16,14 @@
 
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 using namespace CVC4::context;

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 2fdb494e97c533b06d239326a491c3cc3fed7eba..769ae4ea32e567081831cca05d06089fa4e19fef 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -22,11 +22,13 @@
 #include "expr/node.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers_engine.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class TermDb;

diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 9793ea0a7acb9cea5920f72f95ccc7269b2f9119..1cad52b4356a625fa817cd1b8d886d50c81f2d1d 100644 (file)
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -19,7 +19,7 @@
 
 #include "context/cdo.h"
 #include "expr/node_trie.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 07f7548103b5cacad54253481e88cd68623e1793..2044fe22af7229253f53c41ab7492a0f45d60e89 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -15,8 +15,6 @@
 
 #include "theory/quantifiers/quant_conflict_find.h"
 
-#include <vector>
-
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -26,6 +24,7 @@
 #include "theory/quantifiers/quant_util.h"
 #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;

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 7e4eb517d85bcd93538301061d8c49975a3d58b3..836bba80e49ba414e19b40ccef5bf5a5632aa373 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -23,7 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node_trie.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 1a2aaa6cfe52746f7ed0fda4b001a26997e4654c..e88e99a83a95a8c609edc9013f45102eeb14375d 100644 (file)
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -17,11 +17,14 @@
 #ifndef CVC4__THEORY__QUANT_SPLIT_H
 #define CVC4__THEORY__QUANT_SPLIT_H
 
-#include "theory/quantifiers_engine.h"
 #include "context/cdo.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class QuantDSplit : public QuantifiersModule {

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index f916300974e95999fdfd13681e70fbedd5badae8..b72619392273321f3d51ae0093c1faa4aa1be59f 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -20,7 +20,6 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
 
 #include "theory/rewriter.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index d92f36afbbe7d8cd2adea9bbe90015048e373742..10157c3b30c4e4ba2be24dbfe1a029323c48f1c8 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -17,15 +17,16 @@
 #include "theory/quantifiers/rewrite_engine.h"
 
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
-#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #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;

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index bbd6a1534053b2105063d499f9f1a760aab145da..717f4009b2bc7a24b6a6fe142ef86826e26df807 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -22,7 +22,7 @@
 #include "context/context_mm.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quant_conflict_find.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index e4f16de6515e39164008ee672ded9e6af56a9682..24a594351d7d120d4ad27d752fb034b28d645ace 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 4b24cbb1cf6996cbc690d5eec998fdf69db35a2f..b6f282c651b903823894da587dd956e7f87be26f 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/single_inv_partition.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b74caf49a182f7b6319f8c319960e2fa9f5b24ed..9802ce049fcae377a8ac03218bdc9442ebedc2af 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 6a00bc46733e4254be006909e96427214b3c4509..d8239b53048ffbc3f260416649f87066e8272139 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -17,11 +17,17 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
 #define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
 
+#include <map>
+#include <vector>
+
 #include "context/cdhashmap.h"
-#include "theory/quantifiers_engine.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class CegSingleInv;

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 314b437110d79b448bbb0c2bd0adaaeb36d342dc..301d772bff52213dd43e2cd3252004cda6b2bda9 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -19,6 +19,7 @@
 #include "printer/printer.h"
 #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;

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index b72e5048458f9e762bca74334dcfe662a8119532..6e9467b7c67bec4357e47586f14cfa8496231105 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #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/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index 687641e6064f4aa1eb57b701493e7448d6f1c3e2..8f978dda6c10ab8df2b04f66d1361b7f31fa85d7 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index bb8da59da149338c432af89ae46e2b0879d31030..a6b051e58703433dec0e7a60ad8240411881815c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index c01731d1bd159a00f06d84c4e7d392635b268357..b9f50f228ff67c2b5df85203a94466ee7b0f419f 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -18,10 +18,16 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
 
-#include "theory/quantifiers_engine.h"
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class SynthConjecture;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index fb6b23132676b562da82d1d990f7441fa80c2742..ebb92b34b9c00b17f49fa9c3688e45d8ff3b55a9 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 #include <numeric>  // for std::iota
 
@@ -67,6 +68,11 @@ bool OpPosTrie::getOrMakeType(TypeNode tn,
   return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
 }
 
+SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe)
+    : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
+{
+}
+
 Kind SygusGrammarNorm::TypeObject::getEliminateKind(Kind ok)
 {
   Kind nk = ok;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index ae701113ce62dde70d853e50b99f177dbb19f152..00c501cfedde96f5a37fcdd1936af5045b4fd06f 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -28,13 +28,13 @@
 #include "expr/type.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 class SygusGrammarNorm;
+class TermDbSygus;
 
 /** Operator position trie class
  *
@@ -130,10 +130,7 @@ class OpPosTrie
 class SygusGrammarNorm
 {
  public:
-  SygusGrammarNorm(QuantifiersEngine* qe)
-      : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
-  {
-  }
+  SygusGrammarNorm(QuantifiersEngine* qe);
   ~SygusGrammarNorm() {}
   /** creates a normalized typenode from a given one.
    *

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 2b2c87f3834abd7656bef9a5119494435dae5251..a566ebffff98582cf5890c68eda436ae00b6c39d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -17,6 +17,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 8ed080a300efa6c1b204ee33c481ac968a615196..317892723a1ec5ee53e946ede71fa1b038447844 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -18,12 +18,20 @@
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
 
 #include <map>
-#include "theory/quantifiers_engine.h"
+#include <vector>
+
+#include "expr/datatype.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
+class TermDbSygus;
+
 /** SygusRedundantCons
  *
  * This class computes the subset of indices of the constructors of a sygus type

diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 42a125ae5bbea24c348795bdd2fc10cbfdf79d0d..0c9d23b6cf25b13ebad532eec0c5b4de5226cd37 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/sygus/sygus_module.h"
 
+#include "theory/quantifiers_engine.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {

diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index d5e1de3fc562642d8eacad7dbe87f1a3648be2e2..10c0104bc66b5ce724512680acbcb4ab98aa3e14 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -18,14 +18,19 @@
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 
 #include <map>
+#include <vector>
+
 #include "expr/node.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class SynthConjecture;
+class TermDbSygus;
 
 /** SygusModule
  *

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index e9ee340f49b931e98fb5590ef1345c340b77b98f..d096befed2c7221dfd2526f44d2210dd16dd6856 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -25,10 +25,12 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 /** This file contains techniques that compute

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 85a0a4bf8c3e672ff6718f4536075670e115a270..4c5baa4bb257e21921721b4823fc06d78b42f31f 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index bc3a58f9e9b1f4c7d0f0ea5640d2e2d9c8265ccb..26b7234a9602af3986485037096fba8995b77db3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -20,13 +20,16 @@
 #include <unordered_set>
 #include "expr/node.h"
 #include "theory/logic_info.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 class CegConjecture;
+class TermDbSygus;
 
 /** SygusRepairConst
  *

diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 2eb508fde436ec54e98a3300f6e9bd18cb1f454f..008947adb354867a1664e3e64abce5d0e383cd29 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index a5215628cd64186e68621585bda2b0f5bcc9894f..185a927dfd9d57fae8f7e84e7c2fcce79a54f175 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -20,12 +20,16 @@
 #include <map>
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
+class TermDbSygus;
+
 /** Sygus unification utility
  *
  * This utility implements synthesis-by-unification style approaches for a

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index ada99dbaf4ebf9b29d08903fb315719933492671..c5b02a481642c251f52f46d7624a74486fc5c30d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
 #include "theory/quantifiers/lazy_trie.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index acf5a2d7f121fc20d46e4850ee8a47c6615b33b0..a41d895b34a80ec7fd080e1c8626feff56432311 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 1c691bd84ccf6fd34c896999da8f171967328255..e32fbe022546c4f0f7665ad83a83ee6fb8ae279f 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -19,10 +19,12 @@
 
 #include <map>
 #include "expr/node.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
+
+class QuantifiersEngine;
+
 namespace quantifiers {
 
 /** roles for enumerators

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ee5af62c91a31f0a61062ca5bf01e8c6a9959d4c..41caf8c6c3a4de55ca337e6ec0d23ccb70f861b5 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -33,6 +33,7 @@
 #include "theory/quantifiers/sygus/synth_engine.h"
 #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;

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 83a7eaa45ba3020fbf55d38937294eedb2b88754..1cc3702b6128a6eb7c869e0ef4a19a87001fdc30 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -29,7 +29,6 @@
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index fc1ed938d23f22d731553bfb64b7e847c3d9c6ff..afa40bdd8acb90a5876730d5859a802a16d3cb9a 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #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;

diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index d5337e5d15ef34e3e4dca1dc6ad732b4174ab89d..c4c09e7e68fea635bb367581c86b1382c5d1b92f 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -19,8 +19,8 @@
 #define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
 
 #include "context/cdhashmap.h"
+#include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
-#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0281f50ec8ffb5d775e57cc7e96d0767e59f627a..0af120f5a270f95251d84ca97446c6f7dc37a945 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -14,50 +14,12 @@
 
 #include "theory/quantifiers_engine.h"
 
-#include "expr/term_canonize.h"
 #include "options/quantifiers_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/datatypes/theory_datatypes.h"
-#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/bv_inverter.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
-#include "theory/quantifiers/conjecture_generator.h"
-#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
-#include "theory/quantifiers/ematching/trigger.h"
-#include "theory/quantifiers/equality_infer.h"
-#include "theory/quantifiers/equality_query.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
-#include "theory/quantifiers/fmf/full_model_check.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/inst_strategy_enumerative.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/local_theory_ext.h"
-#include "theory/quantifiers/quant_conflict_find.h"
-#include "theory/quantifiers/quant_epr.h"
-#include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quant_split.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/rewrite_engine.h"
-#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index da207c58a4dacd2439c790087b5f6d6c0eb19d5e..e0669c0d4247f51ed1d6fe5ec58b4d9b6181ae50 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -25,9 +25,43 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "expr/term_canonize.h"
 #include "options/quantifiers_modes.h"
+#include "theory/quantifiers/alpha_equivalence.h"
+#include "theory/quantifiers/anti_skolem.h"
+#include "theory/quantifiers/bv_inverter.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/equality_query.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/inst_propagator.h"
+#include "theory/quantifiers/inst_strategy_enumerative.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/local_theory_ext.h"
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers/quant_epr.h"
+#include "theory/quantifiers/quant_relevance.h"
+#include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/theory.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"
@@ -36,56 +70,9 @@ namespace CVC4 {
 
 class TheoryEngine;
 
-namespace expr {
-class TermCanonize;
-}
-
 namespace theory {
 
-class QuantifiersEngine;
-
-namespace quantifiers {
-  //TODO: organize this more/review this, github issue #1163
-  //TODO: include these instead of doing forward declarations? #1307
-  //utilities
-  class TermDb;
-  class TermDbSygus;
-  class TermUtil;
-  class Instantiate;
-  class Skolemize;
-  class TermEnumeration;
-  class FirstOrderModel;
-  class QuantAttributes;
-  class QuantEPR;
-  class QuantRelevance;
-  class RelevantDomain;
-  class BvInverter;
-  class InstPropagator;
-  class EqualityInference;
-  class EqualityQueryQuantifiersEngine;
-  //modules, these are "subsolvers" of the quantifiers theory.
-  class InstantiationEngine;
-  class ModelEngine;
-  class BoundedIntegers;
-  class QuantConflictFind;
-  class RewriteEngine;
-  class QModelBuilder;
-  class ConjectureGenerator;
-  class SynthEngine;
-  class LtePartialInst;
-  class AlphaEquivalence;
-  class InstStrategyEnum;
-  class InstStrategyCegqi;
-  class QuantDSplit;
-  class QuantAntiSkolem;
-  class EqualityInference;
-}/* CVC4::theory::quantifiers */
-
-namespace inst {
-  class TriggerTrie;
-}/* CVC4::theory::inst */
-
-
+// TODO: organize this more/review this, github issue #1163
 class QuantifiersEngine {
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDList<Node> NodeList;