Sygus repair constants (#1812)

16 files changed, 906 insertions, 33 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 28333d905..17deeba81 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -493,6 +493,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus/sygus_module.h \
 	theory/quantifiers/sygus/sygus_process_conj.cpp \
 	theory/quantifiers/sygus/sygus_process_conj.h \
+	theory/quantifiers/sygus/sygus_repair_const.cpp \
+	theory/quantifiers/sygus/sygus_repair_const.h \
 	theory/quantifiers/sygus/sygus_unif.cpp \
 	theory/quantifiers/sygus/sygus_unif.h \
 	theory/quantifiers/sygus/sygus_unif_io.cpp \
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 4c771c143..10000bbb1 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -977,6 +977,14 @@ header = "options/quantifiers_options.h"
   help       = "use quantifier elimination as a preprocessing step for sygus"
 
 [[option]]
+  name       = "sygusRepairConst"
+  category   = "regular"
+  long       = "sygus-repair-const"
+  type       = "bool"
+  default    = "false"
+  help       = "use approach to repair constants in sygus candidate solutions"
+
+[[option]]
   name       = "sygusMinGrammar"
   category   = "regular"
   long       = "sygus-min-grammar"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ac5563fb3..c40096e3f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1318,6 +1318,11 @@ void SmtEngine::setDefaults() {
       options::cbqiMidpoint.set(true);
     }
   }
+  else
+  {
+    // cannot use sygus repair constants
+    options::sygusRepairConst.set(false);
+  }
 
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());
@@ -1485,7 +1490,8 @@ void SmtEngine::setDefaults() {
 
   // cases where we need produce models
   if (!options::produceModels()
-      && (options::produceAssignments() || options::sygusRewSynthCheck()))
+      && (options::produceAssignments() || options::sygusRewSynthCheck()
+          || options::sygusRepairConst()))
   {
     Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));
@@ -5378,6 +5384,11 @@ void SmtEngine::checkSynthSolution()
   map<Node, Node> sol_map;
   /* Get solutions and build auxiliary vectors for substituting */
   d_theoryEngine->getSynthSolutions(sol_map);
+  if (sol_map.empty())
+  {
+    Trace("check-synth-sol") << "No solution to check!\n";
+    return;
+  }
   Trace("check-synth-sol") << "Got solution map:\n";
   std::vector<Node> function_vars, function_sols;
   for (const auto& pair : sol_map)
@@ -5462,8 +5473,8 @@ void SmtEngine::checkSynthSolution()
     else if (r.asSatisfiabilityResult().isSat())
     {
       InternalError(
-          "SmtEngine::checkSynhtSol(): produced solution allows satisfiable "
-          "negated conjecture.");
+          "SmtEngine::checkSynthSolution(): produced solution leads to "
+          "satisfiable negated conjecture.");
     }
     solChecker.resetAssertions();
   }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 757f4d040..15c071431 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1122,7 +1122,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl;
   
   if( Trace.isOn("cegqi-engine") ){
-    if( lemmas.empty() ){
+    if (lemmas.empty() && !d_szinfo.empty())
+    {
       Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
       for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
         SearchSizeInfo * s = it->second;
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index c52d22cdb..98a493423 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -771,8 +771,14 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
         if (lit[1].getType() == lit.getType())
         {
           // t != s ---> ~t = s
-          Assert(lit[1].getKind() != notk);
-          eq = nm->mkNode(EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
+          if (lit[1].getKind() == notk && lit[0].getKind() != notk)
+          {
+            eq = nm->mkNode(EQUAL, lit[0], TermUtil::mkNegate(notk, lit[1]));
+          }
+          else
+          {
+            eq = nm->mkNode(EQUAL, TermUtil::mkNegate(notk, lit[0]), lit[1]);
+          }
         }
       }
       else
@@ -1070,8 +1076,6 @@ bool ExtendedRewriter::inferSubstitution(Node n,
     {
       n = slv_eq;
     }
-    NodeManager* nm = NodeManager::currentNM();
-
     Node v[2];
     for (unsigned i = 0; i < 2; i++)
     {
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 69cf7f73b..cc12fdf17 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -41,10 +41,12 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
       d_ceg_si(new CegConjectureSingleInv(qe, this)),
       d_ceg_proc(new CegConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
+      d_sygus_rconst(new SygusRepairConst(qe)),
       d_ceg_pbe(new CegConjecturePbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
       d_ceg_cegisUnif(new CegisUnif(qe, this)),
       d_master(nullptr),
+      d_repair_index(0),
       d_refine_count(0),
       d_syntax_guided(false)
 {
@@ -116,6 +118,12 @@ void CegConjecture::assign( Node q ) {
       d_embed_quant, vars, d_candidates));
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
 
+  // initialize the sygus constant repair utility
+  if (options::sygusRepairConst())
+  {
+    d_sygus_rconst->initialize(d_base_inst, d_candidates);
+  }
+
   // register this term with sygus database and other utilities that impact
   // the enumerative sygus search
   std::vector< Node > guarded_lemmas;
@@ -243,14 +251,45 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> terms;
   d_master->getTermList(d_candidates, terms);
 
-  // get their model value
+  Assert(!d_candidates.empty());
+
+  Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
+                       << std::endl;
+  std::vector<Node> candidate_values;
+  bool constructed_cand = false;
+
+  if (options::sygusRepairConst())
+  {
+    // 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);
 
-  std::vector<Node> candidate_values;
-  Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
-  bool constructed_cand = d_master->constructCandidates(
-      terms, enum_values, d_candidates, candidate_values, lems);
+  if (!constructed_cand)
+  {
+    Assert(candidate_values.empty());
+    constructed_cand = d_master->constructCandidates(
+        terms, enum_values, d_candidates, candidate_values, lems);
+  }
 
   NodeManager* nm = NodeManager::currentNM();
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 97cc9df1e..231f9f14e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -27,6 +27,8 @@
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #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/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -118,10 +120,12 @@ public:
   /** get model value for term n */
   Node getModelValue( Node n );
 
-  /** get program by examples utility */
-  CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
   /** get utility for static preprocessing and analysis of conjectures */
   CegConjectureProcess* getProcess() { return d_ceg_proc.get(); }
+  /** get constant repair utility */
+  SygusRepairConst* getRepairConst() { return d_sygus_rconst.get(); }
+  /** get program by examples module */
+  CegConjecturePbe* getPbe() { return d_ceg_pbe.get(); }
   /** get the symmetry breaking predicate for type */
   Node getSymmetryBreakingPredicate(
       Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
@@ -136,6 +140,8 @@ private:
   std::unique_ptr<CegConjectureProcess> d_ceg_proc;
   /** grammar utility */
   std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
+  /** repair constant utility */
+  std::unique_ptr<SygusRepairConst> d_sygus_rconst;
 
   //------------------------modules
   /** program by examples module */
@@ -160,7 +166,8 @@ private:
   std::vector< Node > d_candidates;
   /** base instantiation
   * If d_embed_quant is forall d. exists y. P( d, y ), then
-  * this is the formula  exists y. P( d_candidates, y ).
+  * this is the formula  exists y. P( d_candidates, y ). Notice that
+  * (exists y. F) is shorthand above for ~( forall y. ~F ).
   */
   Node d_base_inst;
   /** list of variables on inner quantification */
@@ -185,7 +192,12 @@ private:
     /** list of terms we have instantiated candidates with */
     std::vector< Node > d_inst;
   };
-  std::map< Node, CandidateInfo > d_cinfo;  
+  std::map<Node, CandidateInfo> d_cinfo;
+  /**
+   * The first index of an instantiation in CandidateInfo::d_inst that we have
+   * not yet tried to repair.
+   */
+  unsigned d_repair_index;
   /** number of times we have called doRefine */
   unsigned d_refine_count;
   /** get candidadate */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 86f5abf61..0aebbe11a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -201,10 +201,6 @@ void CegInstantiation::getSynthSolutions(std::map<Node, Node>& sol_map)
   {
     d_conj->getSynthSolutions(sol_map, d_last_inst_si);
   }
-  else
-  {
-    Assert(false);
-  }
 }
 
 void CegInstantiation::preregisterAssertion( Node n ) {
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 c37c0a57a..24b57d025 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -1220,10 +1220,7 @@ Node CegConjectureSingleInvSol::builtinToSygusConst(Node c,
   // them, return a proxy
   if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
   {
-    Node k = nm->mkSkolem("sy", tn, "sygus proxy");
-    SygusPrintProxyAttribute spa;
-    k.setAttribute(spa, c);
-    sc = k;
+    sc = tds->getProxyVariable(tn, c);
   }
   else
   {
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index f48955c9f..92fea9586 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -134,6 +134,13 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
 {
   if (addEvalLemmas(enums, enum_values))
   {
+    // it may be repairable
+    SygusRepairConst* src = d_parent->getRepairConst();
+    std::vector<Node> fail_cvs = enum_values;
+    if (src->repairSolution(candidates, fail_cvs, candidate_values))
+    {
+      return true;
+    }
     return false;
   }
   candidate_values.insert(
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
new file mode 100644
index 000000000..1ca1902a1
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -0,0 +1,543 @@
+/*********************                                                        */
+/*! \file sygus_repair_const.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_repair_const
+ **/
+
+#include "theory/quantifiers/sygus/sygus_repair_const.h"
+
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe)
+    : d_qe(qe), d_allow_constant_grammar(false)
+{
+  d_tds = d_qe->getTermDatabaseSygus();
+}
+
+void SygusRepairConst::initialize(Node base_inst,
+                                  const std::vector<Node>& candidates)
+{
+  Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
+  Trace("sygus-repair-const") << "  conjecture : " << base_inst << std::endl;
+  d_base_inst = base_inst;
+
+  // compute whether there are "allow all constant" types in the variables of q
+  std::map<TypeNode, bool> tprocessed;
+  for (const Node& v : candidates)
+  {
+    TypeNode tn = v.getType();
+    // do the type traversal of the sygus type
+    registerSygusType(tn, tprocessed);
+  }
+  Trace("sygus-repair-const")
+      << "  allow constants : " << d_allow_constant_grammar << std::endl;
+}
+
+// recursion depth bounded by number of types in grammar (small)
+void SygusRepairConst::registerSygusType(TypeNode tn,
+                                         std::map<TypeNode, bool>& tprocessed)
+{
+  if (tprocessed.find(tn) == tprocessed.end())
+  {
+    tprocessed[tn] = true;
+    Assert(tn.isDatatype());
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    Assert(dt.isSygus());
+    // check if this datatype allows all constants
+    if (dt.getSygusAllowConst())
+    {
+      d_allow_constant_grammar = true;
+    }
+    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+    {
+      const DatatypeConstructor& dtc = dt[i];
+      // recurse on all subfields
+      for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
+      {
+        TypeNode tnc = d_tds->getArgType(dtc, j);
+        registerSygusType(tnc, tprocessed);
+      }
+    }
+  }
+}
+
+bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
+                                      const std::vector<Node>& candidate_values,
+                                      std::vector<Node>& repair_cv)
+{
+  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)
+  {
+    return false;
+  }
+  if (Trace.isOn("sygus-repair-const"))
+  {
+    Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
+    Printer* p = Printer::getPrinter(options::outputLanguage());
+    for (unsigned i = 0, size = candidates.size(); i < size; i++)
+    {
+      std::stringstream ss;
+      p->toStreamSygus(ss, candidate_values[i]);
+      Trace("sygus-repair-const")
+          << "  " << candidates[i] << " -> " << ss.str() << std::endl;
+    }
+    Trace("sygus-repair-const")
+        << "Getting candidate skeletons : " << std::endl;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> candidate_skeletons;
+  std::map<TypeNode, int> free_var_count;
+  std::vector<Node> sk_vars;
+  std::map<Node, Node> sk_vars_to_subs;
+  for (unsigned i = 0, size = candidates.size(); i < size; i++)
+  {
+    Node cv = candidate_values[i];
+    Node skeleton = getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs);
+    if (Trace.isOn("sygus-repair-const"))
+    {
+      Printer* p = Printer::getPrinter(options::outputLanguage());
+      std::stringstream ss;
+      p->toStreamSygus(ss, cv);
+      Trace("sygus-repair-const")
+          << "Solution #" << i << " : " << ss.str() << std::endl;
+      if (skeleton == cv)
+      {
+        Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
+      }
+      else
+      {
+        std::stringstream sss;
+        p->toStreamSygus(sss, skeleton);
+        Trace("sygus-repair-const")
+            << "...inferred skeleton : " << sss.str() << std::endl;
+      }
+    }
+    candidate_skeletons.push_back(skeleton);
+  }
+
+  if (sk_vars.empty())
+  {
+    Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
+    return false;
+  }
+
+  Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
+  Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars);
+
+  Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
+
+  if (d_queries.find(fo_body) != d_queries.end())
+  {
+    Trace("sygus-repair-const") << "...duplicate query." << std::endl;
+    return false;
+  }
+  d_queries.insert(fo_body);
+
+  // check whether it is not in the current logic, e.g. non-linear arithmetic.
+  // if so, undo replacements until it is in the current logic.
+  LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
+  if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
+  {
+    fo_body = fitToLogic(logic,
+                         fo_body,
+                         candidates,
+                         candidate_skeletons,
+                         sk_vars,
+                         sk_vars_to_subs);
+  }
+
+  if (fo_body.isNull() || sk_vars.empty())
+  {
+    Trace("sygus-repair-const")
+        << "...all skeleton variables lead to bad logic." << std::endl;
+    return false;
+  }
+
+  Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
+  if (fo_body.getKind() == FORALL)
+  {
+    // must be a CBQI quantifier
+    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe);
+    if (hstatus < CEG_HANDLED)
+    {
+      // abort if less than fully handled
+      Trace("sygus-repair-const") << "...first-order query is not handlable by "
+                                     "counterexample-guided instantiation."
+                                  << std::endl;
+      return false;
+    }
+
+    // do miniscoping explicitly
+    if (fo_body[1].getKind() == AND)
+    {
+      Node bvl = fo_body[0];
+      std::vector<Node> children;
+      for (const Node& conj : fo_body[1])
+      {
+        children.push_back(nm->mkNode(FORALL, bvl, conj));
+      }
+      fo_body = nm->mkNode(AND, children);
+    }
+  }
+
+  Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
+  // make the satisfiability query
+  SmtEngine repcChecker(nm->toExprManager());
+  repcChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
+  repcChecker.assertFormula(fo_body.toExpr());
+  Result r = repcChecker.checkSat();
+  Trace("sygus-repair-const") << "...got : " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat()
+      && !r.asSatisfiabilityResult().isUnknown())
+  {
+    std::vector<Node> sk_sygus_m;
+    for (const Node& v : sk_vars)
+    {
+      Node fov = d_sk_to_fo[v];
+      Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr()));
+      Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
+      // convert to sygus
+      Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
+      sk_sygus_m.push_back(fov_m_to_sygus);
+    }
+    std::stringstream ss;
+    // convert back to sygus
+    for (unsigned i = 0, size = candidates.size(); i < size; i++)
+    {
+      Node csk = candidate_skeletons[i];
+      Node scsk = csk.substitute(
+          sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
+      repair_cv.push_back(scsk);
+      if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
+      {
+        std::stringstream sss;
+        Printer::getPrinter(options::outputLanguage())
+            ->toStreamSygus(sss, repair_cv[i]);
+        ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
+      }
+    }
+    Trace("cegqi-engine") << "...success:" << std::endl;
+    Trace("cegqi-engine") << ss.str();
+    Trace("sygus-repair-const")
+        << "Repaired constants in solution : " << std::endl;
+    Trace("sygus-repair-const") << ss.str();
+    return true;
+  }
+
+  Trace("cegqi-engine") << "...failed" << std::endl;
+
+  return false;
+}
+
+bool SygusRepairConst::isRepairableConstant(Node n)
+{
+  if (n.getKind() != APPLY_CONSTRUCTOR)
+  {
+    return false;
+  }
+  TypeNode tn = n.getType();
+  Assert(tn.isDatatype());
+  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+  Assert(dt.isSygus());
+  if (dt.getSygusAllowConst())
+  {
+    Node op = n.getOperator();
+    unsigned cindex = Datatype::indexOf(op.toExpr());
+    if (dt[cindex].getNumArgs() == 0)
+    {
+      Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+      if (sygusOp.isConst())
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+Node SygusRepairConst::getSkeleton(Node n,
+                                   std::map<TypeNode, int>& free_var_count,
+                                   std::vector<Node>& sk_vars,
+                                   std::map<Node, Node>& sk_vars_to_subs)
+{
+  if (isRepairableConstant(n))
+  {
+    Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
+    sk_vars.push_back(sk_var);
+    sk_vars_to_subs[sk_var] = n;
+    Trace("sygus-repair-const-debug")
+        << "Var to subs : " << sk_var << " -> " << n << std::endl;
+    return sk_var;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  // get the most general candidate skeleton of n
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited[cur] = Node::null();
+      visit.push_back(cur);
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        Node child;
+        // if it is a constant over a type that allows all constants
+        if (isRepairableConstant(cn))
+        {
+          // replace it by the next free variable
+          child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
+          sk_vars.push_back(child);
+          sk_vars_to_subs[child] = cn;
+          Trace("sygus-repair-const-debug")
+              << "Var to subs : " << child << " -> " << cn << std::endl;
+        }
+        else
+        {
+          it = visited.find(cn);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          child = it->second;
+        }
+        childChanged = childChanged || cn != child;
+        children.push_back(child);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
+Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
+                                  const std::vector<Node>& candidate_skeletons,
+                                  const std::vector<Node>& sk_vars)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node body = d_base_inst.negate();
+  Trace("sygus-repair-const") << "  Substitute skeletons..." << std::endl;
+  body = body.substitute(candidates.begin(),
+                         candidates.end(),
+                         candidate_skeletons.begin(),
+                         candidate_skeletons.end());
+  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
+
+  Trace("sygus-repair-const") << "  Unfold the specification..." << std::endl;
+  body = d_tds->evaluateWithUnfolding(body);
+  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
+
+  Trace("sygus-repair-const") << "  Introduce first-order vars..." << std::endl;
+  // now, we must replace all terms of the form eval( z_i, t1...tn ) with
+  // a fresh first-order variable w_i, where z_i is a variable introduced in
+  // the skeleton inference step (z_i is a variable in sk_vars).
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(body);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited[cur] = Node::null();
+      if (cur.getKind() == APPLY_UF && cur.getNumChildren() > 0)
+      {
+        Node v = cur[0];
+        if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
+        {
+          std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
+          if (itf == d_sk_to_fo.end())
+          {
+            Node sk_fov = nm->mkSkolem("k", cur.getType());
+            d_sk_to_fo[v] = sk_fov;
+            d_fo_to_sk[sk_fov] = v;
+            visited[cur] = sk_fov;
+            Trace("sygus-repair-const-debug")
+                << "Map " << v << " -> " << sk_fov << std::endl;
+          }
+          else
+          {
+            visited[cur] = itf->second;
+          }
+        }
+      }
+      if (visited[cur].isNull())
+      {
+        visit.push_back(cur);
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(body) != visited.end());
+  Assert(!visited.find(body)->second.isNull());
+  Node fo_body = visited[body];
+  Trace("sygus-repair-const-debug") << "  ...got : " << fo_body << std::endl;
+  return fo_body;
+}
+
+Node SygusRepairConst::fitToLogic(LogicInfo& logic,
+                                  Node n,
+                                  const std::vector<Node>& candidates,
+                                  std::vector<Node>& candidate_skeletons,
+                                  std::vector<Node>& sk_vars,
+                                  std::map<Node, Node>& sk_vars_to_subs)
+{
+  std::vector<Node> rm_var;
+  Node exc_var;
+  while (getFitToLogicExcludeVar(logic, n, exc_var))
+  {
+    if (exc_var.isNull())
+    {
+      return n;
+    }
+    Trace("sygus-repair-const") << "...exclude " << exc_var
+                                << " due to logic restrictions." << std::endl;
+    TNode tvar = exc_var;
+    Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
+    TNode tsubs = sk_vars_to_subs[exc_var];
+    // revert the substitution
+    for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
+    {
+      candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
+    }
+    // remove the variable
+    sk_vars_to_subs.erase(exc_var);
+    std::vector<Node>::iterator it =
+        std::find(sk_vars.begin(), sk_vars.end(), exc_var);
+    Assert(it != sk_vars.end());
+    sk_vars.erase(it);
+    // reconstruct the query
+    n = getFoQuery(candidates, candidate_skeletons, sk_vars);
+    // reset the exclusion variable
+    exc_var = Node::null();
+  }
+  return Node::null();
+}
+
+bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
+                                               Node n,
+                                               Node& exvar)
+{
+  bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
+
+  // should have at least one restriction
+  Assert(restrictLA);
+
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (restrictLA && cur.getKind() == NONLINEAR_MULT)
+      {
+        for (const Node& ccur : cur)
+        {
+          std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
+          if (itf != d_fo_to_sk.end())
+          {
+            exvar = itf->second;
+            return true;
+          }
+        }
+        return false;
+      }
+      for (const Node& ccur : cur)
+      {
+        visit.push_back(ccur);
+      }
+    }
+  } while (!visit.empty());
+
+  return true;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
new file mode 100644
index 000000000..b2a0d888d
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -0,0 +1,176 @@
+/*********************                                                        */
+/*! \file sygus_repair_const.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_repair_const
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+
+#include <unordered_set>
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegConjecture;
+
+/** SygusRepairConst
+ *
+ * This module is used to repair portions of candidate solutions. In particular,
+ * given a synthesis conjecture:
+ *   exists f. forall x. P( f, x )
+ * and a candidate solution f = \x. t[x,c] where c are constants, this function
+ * checks whether there exists a term of the form \x. t[x,c'] for some constants
+ * c' such that:
+ *   forall x. P( (\x. t[x,c']), x )  [***]
+ * is satisfiable, where notice that the above formula after beta-reduction may
+ * be one in pure first-order logic in a decidable theory (say linear
+ * arithmetic). To check this, we invoke a separate instance of the SmtEngine
+ * within repairSolution(...) below, which if satisfiable gives us the
+ * valuation for c'.
+ */
+class SygusRepairConst
+{
+ public:
+  SygusRepairConst(QuantifiersEngine* qe);
+  ~SygusRepairConst() {}
+  /** initialize
+   *
+   * Initialize this class with the base instantiation of the sygus conjecture
+   * (see CegConjecture::d_base_inst) and its candidate variables (see
+   * CegConjecture::d_candidates).
+   */
+  void initialize(Node base_inst, const std::vector<Node>& candidates);
+  /** repair solution
+   *
+   * This function is called when candidates -> candidate_values is a (failed)
+   * candidate solution for the synthesis conjecture.
+   *
+   * If this function returns true, then this class adds to repair_cv the
+   * repaired version of the solution candidate_values for each candidate,
+   * where for each index i, repair_cv[i] is obtained by replacing constant
+   * subterms in candidate_values[i] with others, and
+   *    candidates -> repair_cv
+   * is a solution for the synthesis conjecture associated with this class.
+   * Moreover, it is the case that
+   *    repair_cv[j] != candidate_values[j], for at least one j.
+   */
+  bool repairSolution(const std::vector<Node>& candidates,
+                      const std::vector<Node>& candidate_values,
+                      std::vector<Node>& repair_cv);
+
+ private:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** pointer to the sygus term database of d_qe */
+  TermDbSygus* d_tds;
+  /**
+   * The "base instantiation" of the deep embedding form of the synthesis
+   * conjecture associated with this class, see CegConjecture::d_base_inst.
+   */
+  Node d_base_inst;
+  /**
+   * whether any sygus type for the candidate variables of d_base_inst (the
+   * syntactic restrictions) allows all constants. If this flag is false, then
+   * this class is a no-op.
+   */
+  bool d_allow_constant_grammar;
+  /** map from skeleton variables to first-order variables */
+  std::map<Node, Node> d_sk_to_fo;
+  /** reverse map of d_sk_to_fo */
+  std::map<Node, Node> d_fo_to_sk;
+  /** a cache of satisfiability queries of the form [***] above we have tried */
+  std::unordered_set<Node, NodeHashFunction> d_queries;
+  /**
+   * Register information for sygus type tn, tprocessed stores the set of
+   * already registered types.
+   */
+  void registerSygusType(TypeNode tn, std::map<TypeNode, bool>& tprocessed);
+  /**
+   * Returns true if n is a term of a sygus datatype type that allows all
+   * constants, and n encodes a constant. The term n must have a sygus datatype
+   * type.
+   */
+  bool isRepairableConstant(Node n);
+  /** get skeleton
+   *
+   * Returns a skeleton for n, where the subterms of n that are repairable
+   * constants are replaced by free variables. Since we are interested in
+   * returning canonical skeletons, the free variables we use in this
+   * replacement are taken from TermDbSygus, where we track indices
+   * in free_var_count. Variables we introduce in this way are added to sk_vars.
+   * The mapping sk_vars_to_subs contains entries v -> c, where v is a
+   * variable in sk_vars, and c is the term in n that it replaced.
+   */
+  Node getSkeleton(Node n,
+                   std::map<TypeNode, int>& free_var_count,
+                   std::vector<Node>& sk_vars,
+                   std::map<Node, Node>& sk_vars_to_subs);
+  /** get first-order query
+   *
+   * This function returns a formula that is equivalent to the negation of the
+   * synthesis conjecture, where candidates are replaced by candidate_skeletons,
+   * whose free variables are in the set sk_vars. The returned formula
+   * is a first-order (quantified) formula in the background logic, without UF,
+   * of the form [***] above.
+   */
+  Node getFoQuery(const std::vector<Node>& candidates,
+                  const std::vector<Node>& candidate_skeletons,
+                  const std::vector<Node>& sk_vars);
+  /** fit to logic
+   *
+   * This function ensures that a query of the form [***] above fits the given
+   * logic. In our approach for constant repair, replacing constants by
+   * variables may introduce e.g. non-linearity. If non-linear arithmetic is
+   * not enabled, we must undo some of the variables we introduced when
+   * inferring candidate skeletons.
+   *
+   * This function may remove variables from sk_vars and the map
+   * sk_vars_to_subs. The skeletons candidate_skeletons are obtained by
+   * getSkeleton(...) on the resulting vectors. If this function returns a
+   * non-null node n', then n' is getFoQuery(...) on the resulting vectors, and
+   * n' is in the given logic. The function may return null if it is not
+   * possible to find a n' of this form.
+   *
+   * It uses the function below to choose which variables to remove from
+   * sk_vars.
+   */
+  Node fitToLogic(LogicInfo& logic,
+                  Node n,
+                  const std::vector<Node>& candidates,
+                  std::vector<Node>& candidate_skeletons,
+                  std::vector<Node>& sk_vars,
+                  std::map<Node, Node>& sk_vars_to_subs);
+  /** get fit to logic exclusion variable
+   *
+   * If n is not in the given logic, then this method either returns false,
+   * or returns true and sets exvar to some variable in the domain of
+   * d_fo_to_sk, that must be replaced by a constant for n to be in the given
+   * logic. For example, for logic linear arithemic, for input:
+   *    x * y = 5
+   * where x is in the domain of d_fo_to_sk, this function returns true and sets
+   * exvar to x.
+   * If n is in the given logic, this method returns true.
+   */
+  bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index c8d7bf04d..3121a4253 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -104,7 +104,28 @@ bool TermDbSygus::hasFreeVar( Node n ) {
   std::map< Node, bool > visited;
   return hasFreeVar( n, visited );
 }
-  
+
+Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
+{
+  Assert(tn.isDatatype());
+  Assert(static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus());
+  Assert(
+      TypeNode::fromType(
+          static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
+      == c.getType());
+
+  std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
+  if (it == d_proxy_vars[tn].end())
+  {
+    Node k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
+    SygusPrintProxyAttribute spa;
+    k.setAttribute(spa, c);
+    d_proxy_vars[tn][c] = k;
+    return k;
+  }
+  return it->second;
+}
+
 TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
   return d_fv_stype[v];
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 57a127d8d..f108dfb8e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -128,6 +128,14 @@ class TermDbSygus {
   int getVarNum(Node n) { return d_fv_num[n]; }
   /** returns true if n has a cached free variable (in d_fv). */
   bool hasFreeVar(Node n);
+  /** get sygus proxy variable
+   *
+   * Returns a fresh variable of type tn with the SygusPrintProxyAttribute set
+   * to constant c. The type tn should be a sygus datatype type, and the type of
+   * c should be the analog type of tn. The semantics of the returned node
+   * is "the variable of sygus datatype tn that encodes constant c".
+   */
+  Node getProxyVariable(TypeNode tn, Node c);
   /** make generic
    *
    * This function returns a builtin term f( t1, ..., tn ) where f is the
@@ -152,6 +160,29 @@ class TermDbSygus {
   Node sygusToBuiltin(Node n, TypeNode tn);
   /** same as above, but without tn */
   Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
+  /** evaluate builtin
+   *
+   * bn is a term of some sygus datatype tn. This function returns the rewritten
+   * form of bn [ args / vars(tn) ], where vars(tn) is the sygus variable
+   * list for type tn (see Datatype::getSygusVarList).
+   */
+  Node evaluateBuiltin(TypeNode tn, Node bn, std::vector<Node>& args);
+  /** evaluate with unfolding
+   *
+   * n is any term that may involve sygus evaluation functions. This function
+   * returns the result of unfolding the evaluation functions within n and
+   * rewriting the result. For example, if eval_A is the evaluation function
+   * for the datatype:
+   *   A -> C_0 | C_1 | C_x | C_+( C_A, C_A )
+   * corresponding to grammar:
+   *   A -> 0 | 1 | x | A + A
+   * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y.
+   * The node returned by this function is in (extended) rewritten form.
+   */
+  Node evaluateWithUnfolding(Node n);
+  /** same as above, but with a cache of visited nodes */
+  Node evaluateWithUnfolding(
+      Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
   //-----------------------------end conversion from sygus to builtin
 
  private:
@@ -201,6 +232,8 @@ class TermDbSygus {
   std::map<Node, int> d_fv_num;
   /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
   bool hasFreeVar(Node n, std::map<Node, bool>& visited);
+  /** cache of getProxyVariable */
+  std::map<TypeNode, std::map<Node, Node> > d_proxy_vars;
   //-----------------------------end conversion from sygus to builtin
 
   // TODO :issue #1235 : below here needs refactor
@@ -316,13 +349,6 @@ public:
     return unfold( en, vtm, exp, false );
   }
   Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
-
-  // builtin evaluation, returns rewrite( bn [ args / vars(tn) ] )
-  Node evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& args );
-  // evaluate with unfolding
-  Node evaluateWithUnfolding(
-      Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
-  Node evaluateWithUnfolding( Node n );
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c3de09de2..52eb63789 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1474,6 +1474,7 @@ REG1_TESTS = \
 	regress1/sygus/clock-inc-tuple.sy \
 	regress1/sygus/commutative.sy \
 	regress1/sygus/constant.sy \
+	regress1/sygus/constant-ite-bv.sy \
 	regress1/sygus/dt-test-ns.sy \
 	regress1/sygus/dup-op.sy \
 	regress1/sygus/fg_polynomial3.sy \
diff --git a/test/regress/regress1/sygus/constant-ite-bv.sy b/test/regress/regress1/sygus/constant-ite-bv.sy
new file mode 100644
index 000000000..330ef026e
--- /dev/null
+++ b/test/regress/regress1/sygus/constant-ite-bv.sy
@@ -0,0 +1,29 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --sygus-repair-const
+(set-logic BV)
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+(Start (BitVec 64) (
+        #x0000000000000000 
+        #x0000000000000001 
+        x 
+        (bvnot Start)
+		    (bvadd Start Start)
+		    (ite StartBool Start Start)
+		    (Constant (BitVec 64))
+ ))
+(StartBool Bool ((bvule Start Start)))
+)
+)
+(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57))
+(constraint (= (f #xFDA75AD598A27135) #xC8E366559002AA57))
+(constraint (= (f #x58682C0FA4F8DB6D) #xC8E366559002AA57))
+(constraint (= (f #x58FDC0941A7E079F) #xC8E366559002AA57))
+(constraint (= (f #xBDC9B88103ECB0C9) #xC8E366559002AA57))
+(constraint (= (f #x000000000001502F) #x0000000000000000))
+(constraint (= (f #x0000000000010999) #x0000000000000000))
+(constraint (= (f #x0000000000013169) #x0000000000000000))
+(constraint (= (f #x000000000001B1A9) #x0000000000000000))
+(constraint (= (f #x0000000000016D77) #x0000000000000000))
+(constraint (= (f #x0000000000000001) #x0000000000000000))
+(check-synth)