From 7c26406e8f2952197037b152272988f2ec1e3ad1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Jul 2018 22:34:18 +0200
Subject: [PATCH]  sygusComp2018: minor changes to repair constant utility
 (#2110)

---
 src/options/quantifiers_options.toml                 |  9 +++++++++
 .../quantifiers/sygus/ce_guided_conjecture.cpp       | 12 +++++++++++-
 src/theory/quantifiers/sygus/cegis.cpp               |  2 +-
 src/theory/quantifiers/sygus/sygus_repair_const.cpp  |  9 +++++++--
 src/theory/quantifiers/sygus/sygus_repair_const.h    |  6 ++++++
 5 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index fa8f07dac..8e954ddc0 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -969,6 +969,15 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "abort if synthesis conjecture is not single invocation"
 
+[[option]]
+  name       = "sygusConstRepairAbort"
+  category   = "regular"
+  long       = "sygus-crepair-abort"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "abort if constant repair techniques are not applicable"
+
 [[option]]
   name       = "sygusUnif"
   category   = "regular"
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index bf973bd97..b2b00a31c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -121,7 +121,17 @@ void CegConjecture::assign( Node q ) {
   // initialize the sygus constant repair utility
   if (options::sygusRepairConst())
   {
-    d_sygus_rconst->initialize(d_base_inst, d_candidates);
+    d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
+    if (options::sygusConstRepairAbort())
+    {
+      if (!d_sygus_rconst->isActive())
+      {
+        // no constant repair is possible: abort
+        std::stringstream ss;
+        ss << "Grammar does not allow repair constants." << std::endl;
+        throw LogicException(ss.str());
+      }
+    }
   }
 
   // register this term with sygus database and other utilities that impact
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index a678f1e79..37ee01370 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -397,7 +397,7 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
   lems.push_back(rlem);
 }
 
-bool Cegis::usingRepairConst() { return d_using_gr_repair; }
+bool Cegis::usingRepairConst() { return true; }
 
 void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
                                     const std::vector<Node>& ms,
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 4aaccc71e..71449029b 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -92,6 +92,11 @@ void SygusRepairConst::registerSygusType(TypeNode tn,
   }
 }
 
+bool SygusRepairConst::isActive() const
+{
+  return !d_base_inst.isNull() && d_allow_constant_grammar;
+}
+
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
                                       std::vector<Node>& repair_cv,
@@ -100,7 +105,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   Assert(candidates.size() == candidate_values.size());
 
   // if no grammar type allows constants, no repair is possible
-  if (d_base_inst.isNull() || !d_allow_constant_grammar)
+  if (!isActive())
   {
     return false;
   }
@@ -415,7 +420,7 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
                                   const std::vector<Node>& sk_vars)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node body = d_base_inst.negate();
+  Node body = d_base_inst;
   Trace("sygus-repair-const") << "  Substitute skeletons..." << std::endl;
   body = body.substitute(candidates.begin(),
                          candidates.end(),
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index ba1295988..3e45f9210 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -77,6 +77,12 @@ class SygusRepairConst
                       const std::vector<Node>& candidate_values,
                       std::vector<Node>& repair_cv,
                       bool useConstantsAsHoles = false);
+  /**
+   * Return whether this module has the possibility to repair solutions. This is
+   * true if this module has been initialized, and at least one candidate has
+   * an "any constant" constructor.
+   */
+  bool isActive() const;
   /** must repair?
    *
    * This returns true if n must be repaired for it to be a valid solution.
-- 
2.30.2