Make construct solution behavior specific to SygusIO (#1827)

diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index ab2b06a82e2e670f9559fdcd4a21bc5574fedf52..9a017d21b61766eb80842725684a020611de0090 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -26,10 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnif::SygusUnif()
-    : d_qe(nullptr), d_tds(nullptr), d_check_sol(false), d_cond_count(0)
-{
-}
+SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
 
 SygusUnif::~SygusUnif() {}
 
@@ -48,50 +45,11 @@ void SygusUnif::initialize(QuantifiersEngine* qe,
 
 Node SygusUnif::constructSolution()
 {
-  Node c = d_candidate;
-  if (!d_solution.isNull())
-  {
-    // already has a solution
-    return d_solution;
-  }
-  // only check if an enumerator updated
-  if (d_check_sol)
-  {
-    Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
-                       << std::endl;
-    d_check_sol = false;
-    // try multiple times if we have done multiple conditions, due to
-    // non-determinism
-    Node vc;
-    for (unsigned i = 0; i <= d_cond_count; i++)
-    {
-      Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
-      Node e = d_strategy.getRootEnumerator();
-      // initialize a call to construct solution
-      initializeConstructSol();
-      // call the virtual construct solution method
-      Node vcc = constructSol(e, role_equal, 1);
-      // if we constructed the solution, and we either did not previously have
-      // a solution, or the new solution is better (smaller).
-      if (!vcc.isNull()
-          && (vc.isNull() || (!vc.isNull()
-                              && d_tds->getSygusTermSize(vcc)
-                                     < d_tds->getSygusTermSize(vc))))
-      {
-        Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
-                           << std::endl;
-        Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
-        vc = vcc;
-      }
-    }
-    if (!vc.isNull())
-    {
-      d_solution = vc;
-      return vc;
-    }
-    Trace("sygus-pbe") << "...failed to solve." << std::endl;
-  }
-  return Node::null();
+  // initialize a call to construct solution
+  initializeConstructSol();
+  // call the virtual construct solution method
+  Node e = d_strategy.getRootEnumerator();
+  return constructSol(e, role_equal, 1);
 }
 
 Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)

diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 728d613b2256fed859543849c83087738e790c1b..beb2023f967fdc8b6240cdec306b5c1f83f06b02 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -99,18 +99,6 @@ class SygusUnif
                         std::vector<Node>& vals,
                         bool pol = true);
   //-----------------------end debug printing
-
-
-  /**
-   * Whether we will try to construct solution on the next call to
-   * constructSolution. This flag is set to true when we successfully
-   * register a new value for an enumerator.
-   */
-  bool d_check_sol;
-  /** The number of values we have enumerated for all enumerators. */
-  unsigned d_cond_count;
-  /** The solution for the function of this class, if one has been found */
-  Node d_solution;
   /** the candidate for this class */
   Node d_candidate;
   /** maps a function-to-synthesize to the above information */

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index abdaf0cb23280f84e05925bae0e5f5c16fa7cf4f..7a134b1c078a8aa9d9a53f6de9dfe0c5c302bade 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -459,7 +459,7 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
   getLeavesInternal(vals, pol, v, 0, -2);
 }
 
-SygusUnifIo::SygusUnifIo()
+SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -677,6 +677,54 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   lemmas.push_back(exp_exc);
 }
 
+Node SygusUnifIo::constructSolution()
+{
+  Node c = d_candidate;
+  if (!d_solution.isNull())
+  {
+    // already has a solution
+    return d_solution;
+  }
+  // only check if an enumerator updated
+  if (d_check_sol)
+  {
+    Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
+                       << std::endl;
+    d_check_sol = false;
+    // try multiple times if we have done multiple conditions, due to
+    // non-determinism
+    Node vc;
+    for (unsigned i = 0; i <= d_cond_count; i++)
+    {
+      Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
+      // initialize a call to construct solution
+      initializeConstructSol();
+      // call the virtual construct solution method
+      Node e = d_strategy.getRootEnumerator();
+      Node vcc = constructSol(e, role_equal, 1);
+      // if we constructed the solution, and we either did not previously have
+      // a solution, or the new solution is better (smaller).
+      if (!vcc.isNull()
+          && (vc.isNull() || (!vc.isNull()
+                              && d_tds->getSygusTermSize(vcc)
+                                     < d_tds->getSygusTermSize(vc))))
+      {
+        Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
+                           << std::endl;
+        Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
+        vc = vcc;
+      }
+    }
+    if (!vc.isNull())
+    {
+      d_solution = vc;
+      return vc;
+    }
+    Trace("sygus-pbe") << "...failed to solve." << std::endl;
+  }
+  return Node::null();
+}
+
 // ------------------------------------ solution construction from enumeration
 
 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 94fb2e75414cf1a1265a1ac1777c39f4d2640439..276cc9da2d7f08e90b0ef41d5633abc33454e3dc 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -271,6 +271,9 @@ class SygusUnifIo : public SygusUnif
                                  Node v,
                                  std::vector<Node>& lemmas) override;
 
+  /** Construct solution */
+  virtual Node constructSolution() override;
+
   /** add example
    *
    * This adds input -> output to the specification for f. The arity of
@@ -281,6 +284,16 @@ class SygusUnifIo : public SygusUnif
   void addExample(const std::vector<Node>& input, Node output);
 
  protected:
+  /**
+   * Whether we will try to construct solution on the next call to
+   * constructSolution. This flag is set to true when we successfully
+   * register a new value for an enumerator.
+   */
+  bool d_check_sol;
+  /** The number of values we have enumerated for all enumerators. */
+  unsigned d_cond_count;
+  /** The solution for the function of this class, if one has been found */
+  Node d_solution;
   /** true and false nodes */
   Node d_true;
   Node d_false;