Reenable repair const (#1983)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 4a70048217a1218943ef2bb72ec61dd1dac87313..107f3896ff7d8450d21e537c5bed049640ed0628 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -989,7 +989,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-repair-const"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use approach to repair constants in sygus candidate solutions"
 
 [[option]]

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index f66a97ce8a6cab0170d298f599d05f39c1b0eae7..ecb6db2fb07f3d5df1fb373025eb096960b36575 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -258,6 +258,33 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> candidate_values;
   bool constructed_cand = false;
 
+  // If a module is not trying to repair constants in solutions and the option
+  // sygusRepairConst  is true, we use a default scheme for trying to repair
+  // constants here.
+  if (options::sygusRepairConst() && !d_master->usingRepairConst())
+  {
+    Trace("cegqi-check") << "CegConjuncture : repair previous solution..."
+                         << std::endl;
+    // have we tried to repair the previous solution?
+    // if not, call the repair constant utility
+    unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
+    if (d_repair_index < ninst)
+    {
+      std::vector<Node> fail_cvs;
+      for (const Node& cprog : d_candidates)
+      {
+        Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
+        fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
+      }
+      d_repair_index++;
+      if (d_sygus_rconst->repairSolution(
+              d_candidates, fail_cvs, candidate_values))
+      {
+        constructed_cand = true;
+      }
+    }
+  }
+
   // get the model value of the relevant terms from the master module
   std::vector<Node> enum_values;
   getModelValues(terms, enum_values);

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 92ed41f3d2ea4b2b07d3cab3a34ad621ccfb09bf..ee54c329648f2082c2f9c8463ebe64ef21d75638 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -397,6 +397,8 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
   lems.push_back(rlem);
 }
 
+bool Cegis::usingRepairConst() { return d_using_gr_repair; }
+
 void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
                                     const std::vector<Node>& ms,
                                     std::vector<Node>& lems)

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index ca27a2281a3b972885b778b8827e993b5dfee276..856219b7364aa24c0d508d957db6552a329a6e91 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -63,6 +63,8 @@ class Cegis : public SygusModule
   virtual void registerRefinementLemma(const std::vector<Node>& vars,
                                        Node lem,
                                        std::vector<Node>& lems) override;
+  /** using repair const */
+  virtual bool usingRepairConst() override;
 
  protected:
   /** the evaluation unfold utility of d_tds */

diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 75be570e644985452a9739345cc28cdd094e693a..b01f8e1d051c41c6719e3c806e4c88f64e2ba267 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -122,6 +122,12 @@ class SygusModule
   {
     return Node::null();
   }
+  /**
+   * Are we trying to repair constants in candidate solutions?
+   * If we return true for usingRepairConst is true, then this module has
+   * attmepted to repair any solutions returned by constructCandidates.
+   */
+  virtual bool usingRepairConst() { return false; }
 
  protected:
   /** reference to quantifier engine */

diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 360474f84239ff799feed70e5ea9e2a2c06f89f8..24a0aab2ecdd8a2fd6a79905e95b7564bc43d518 100644 (file)
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-sygus-repair-const
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM

diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
index a27d8e0d6651f38d3d0add9cc43da2278ac22cff..6c5039c2b7d8680382ace1d8613a424506e8349b 100644 (file)
--- a/test/regress/regress1/quantifiers/horn-simple.smt2
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -6,7 +6,7 @@
 
 (assert (forall ((x Int)) (=> (= x 0) (I x))))
 
-(assert (forall ((x Int)) (=> (and (I x) (< x 1)) (I (+ x 1)))))
+(assert (forall ((x Int)) (=> (and (I x) (< x 6)) (I (+ x 1)))))
 
 (assert (forall ((x Int)) (=> (I x) (<= x 10))))
 

diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy
index 7f895fae41ce3d520c5ad0c3508567964d6929ca..d8d4ff9bb7d3d4a19bdf9791182d638c1cf53fc8 100644 (file)
--- a/test/regress/regress2/sygus/vcb.sy
+++ b/test/regress/regress2/sygus/vcb.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const
 (set-logic LIA)
 
 (synth-fun f1 ((x1 Int) (x2 Int)) Int)