New algorithm for interpolation and abduction based on unsat cores (#3255)

12 files changed, 1328 insertions, 2 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4f64760e0..5b6c3aeca 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -558,6 +558,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/ce_guided_single_inv_sol.h
   theory/quantifiers/sygus/cegis.cpp
   theory/quantifiers/sygus/cegis.h
+  theory/quantifiers/sygus/cegis_core_connective.cpp
+  theory/quantifiers/sygus/cegis_core_connective.h
   theory/quantifiers/sygus/cegis_unif.cpp
   theory/quantifiers/sygus/cegis_unif.h
   theory/quantifiers/sygus/enum_stream_substitution.cpp
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index e7a24cf3e..d37c9db83 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1002,6 +1002,14 @@ header = "options/quantifiers_options.h"
   help       = "use approach to repair constants in sygus candidate solutions"
 
 [[option]]
+  name       = "sygusCoreConnective"
+  category   = "regular"
+  long       = "sygus-core-connective"
+  type       = "bool"
+  default    = "false"
+  help       = "use unsat core analysis to construct Boolean connective to sygus conjectures"
+
+[[option]]
   name       = "sygusRepairConstTimeout"
   category   = "regular"
   long       = "sygus-repair-const-timeout=N"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 571094618..39d09c4ea 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -192,7 +192,6 @@ header = "options/smt_options.h"
   type       = "bool"
   predicates = ["proofEnabledBuild"]
   notifies   = ["notifyBeforeSearch"]
-  read_only  = true
   help       = "turn on unsat core generation"
 
 [[option]]
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 075c8fa00..7e18e5a6f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1303,6 +1303,12 @@ void SmtEngine::setDefaults() {
     }
   }
 
+  // sygus core connective requires unsat cores
+  if (options::sygusCoreConnective())
+  {
+    options::unsatCores.set(true);
+  }
+
   if ((options::checkModels() || options::checkSynthSol()
        || options::produceAbducts()
        || options::modelCoresMode() != MODEL_CORES_NONE
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
new file mode 100644
index 000000000..0b9dd3b48
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -0,0 +1,874 @@
+/*********************                                                        */
+/*! \file cegis_core_connective.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 cegis core connective module.
+ **/
+
+#include "theory/quantifiers/sygus/cegis_core_connective.h"
+
+#include "expr/datatype.h"
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "proof/unsat_core.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "util/random.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+bool VariadicTrie::add(Node n, const std::vector<Node>& i)
+{
+  VariadicTrie* curr = this;
+  for (const Node& ic : i)
+  {
+    curr = &(curr->d_children[ic]);
+  }
+  if (curr->d_data.isNull())
+  {
+    curr->d_data = n;
+    return true;
+  }
+  return false;
+}
+
+bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
+{
+  if (!d_data.isNull())
+  {
+    return true;
+  }
+  for (const std::pair<const Node, VariadicTrie>& p : d_children)
+  {
+    Node n = p.first;
+    if (std::find(is.begin(), is.end(), n) != is.end())
+    {
+      if (p.second.hasSubset(is))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
+                                         SynthConjecture* p)
+    : Cegis(qe, p)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool CegisCoreConnective::processInitialize(Node conj,
+                                            Node n,
+                                            const std::vector<Node>& candidates,
+                                            std::vector<Node>& lemmas)
+{
+  Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl;
+  Trace("sygus-ccore-init") << "  conjecture : " << conj << std::endl;
+  Trace("sygus-ccore-init") << "  candidates : " << candidates << std::endl;
+  if (candidates.size() != 1)
+  {
+    Trace("sygus-ccore-init")
+        << "...only applies to single candidate conjectures." << std::endl;
+    return false;
+  }
+  d_candidate = candidates[0];
+  Assert(conj.getKind() == FORALL);
+  Assert(conj[0].getNumChildren() == 1);
+  Node body = conj[1];
+  if (body.getKind() == NOT && body[0].getKind() == FORALL)
+  {
+    body = body[0][1];
+  }
+  else
+  {
+    body = TermUtil::simpleNegate(body);
+  }
+  Trace("sygus-ccore-init") << "  body : " << body << std::endl;
+
+  TransitionInference ti;
+  ti.process(body, conj[0][0]);
+
+  if (!ti.isComplete())
+  {
+    Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl;
+    return false;
+  }
+  Node trans = ti.getTransitionRelation();
+  Trace("sygus-ccore-init") << "  transition relation: " << trans << std::endl;
+  if (!trans.isConst() || trans.getConst<bool>())
+  {
+    Trace("sygus-ccore-init")
+        << "...does not apply conjectures with transition relations."
+        << std::endl;
+    return false;
+  }
+
+  // the grammar must allow AND / OR when applicable
+  TypeNode gt = d_candidate.getType();
+
+  Node f = ti.getFunction();
+  Assert(!f.isNull());
+  Trace("sygus-ccore-init") << "  predicate: " << f << std::endl;
+  ti.getVariables(d_vars);
+  Trace("sygus-ccore-init") << "  variables: " << d_vars << std::endl;
+  // make the evaluation function
+  std::vector<Node> echildren;
+  echildren.push_back(d_candidate);
+  echildren.insert(echildren.end(), d_vars.begin(), d_vars.end());
+  d_eterm = NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, echildren);
+  Trace("sygus-ccore-init") << "  evaluation term: " << d_eterm << std::endl;
+
+  Node prePost[2];
+  prePost[0] = ti.getPreCondition();
+  // negate the post condition
+  prePost[1] = TermUtil::simpleNegate(ti.getPostCondition());
+  Trace("sygus-ccore-init") << "  precondition: " << prePost[0] << std::endl;
+  Trace("sygus-ccore-init") << "  postcondition: " << prePost[1] << std::endl;
+
+  // side condition?
+  QAttributes qa;
+  QuantAttributes::computeQuantAttributes(conj, qa);
+  Node sc = qa.d_sygusSideCondition;
+  if (!sc.isNull())
+  {
+    Trace("sygus-ccore-init") << "  side condition: " << sc << std::endl;
+    if (sc.getKind() == EXISTS)
+    {
+      sc = sc[1];
+    }
+    Node scb = TermUtil::simpleNegate(sc);
+    TransitionInference tisc;
+    tisc.process(scb, conj[0][0]);
+    Node scTrans = ti.getTransitionRelation();
+    Trace("sygus-ccore-init")
+        << "  transition relation of SC: " << scTrans << std::endl;
+    if (tisc.isComplete() && scTrans.isConst() && !scTrans.getConst<bool>())
+    {
+      std::vector<Node> scVars;
+      tisc.getVariables(scVars);
+      Node scPre = tisc.getPreCondition();
+      scPre = scPre.substitute(
+          scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end());
+      Node scPost = TermUtil::simpleNegate(tisc.getPostCondition());
+      scPost = scPost.substitute(
+          scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end());
+      Trace("sygus-ccore-init")
+          << "  precondition of SC: " << scPre << std::endl;
+      Trace("sygus-ccore-init")
+          << "  postcondition of SC: " << scPost << std::endl;
+      // We are extracting the side condition to be used by this algorithm
+      // from the side condition ascribed to the synthesis conjecture.
+      // A sygus conjecture of the form, for predicate-to-synthesize I:
+      //   exists I. forall x. P[I,x]
+      // whose ascribed side condition is C[I], has the semantics:
+      //   exists I. C[I] ^ forall x. P[I,x].
+      // Notice that this side condition C may be an arbitrary formula over the
+      // function to synthesize. However, the algorithm implemented by this
+      // class is restricted to side conditions of the form:
+      //   exists k. A[k] ^ I(k)
+      // The above condition guards for this case, and runs this block of code,
+      // where we use the TransitionInference utility to extract A[k] from
+      // A[k] ^ I(k). In the end, we set d_sc to A[d_vars]; notice the variables
+      // d_vars are those introduced by the TransitionInference utility
+      // for normalization.
+      d_sc = scPost;
+    }
+  }
+
+  // We use the postcondition if it non-trivial and the grammar gt for our
+  // candidate has the production rule gt -> AND( gt, gt ). Similarly for
+  // precondition and OR.
+  Assert(gt.isDatatype());
+  const Datatype& gdt = gt.getDatatype();
+  SygusTypeInfo& gti = d_tds->getTypeInfo(gt);
+  for (unsigned r = 0; r < 2; r++)
+  {
+    Node f = prePost[r];
+    if (f.isConst())
+    {
+      // this direction is trivial, ignore
+      continue;
+    }
+    Component& c = r == 0 ? d_pre : d_post;
+    Kind rk = r == 0 ? OR : AND;
+    int i = gti.getKindConsNum(rk);
+    if (i != -1 && gdt[i].getNumArgs() == 2
+        && TypeNode::fromType(gdt[i].getArgType(0)) == gt
+        && TypeNode::fromType(gdt[i].getArgType(1)) == gt)
+    {
+      Trace("sygus-ccore-init") << "  will do " << (r == 0 ? "pre" : "post")
+                                << "condition." << std::endl;
+      Node cons = Node::fromExpr(gdt[i].getConstructor());
+      c.initialize(f, cons);
+      // Register the symmetry breaking lemma: do not do top-level solutions
+      // with this constructor (e.g. we want to enumerate literals, not
+      // conjunctions).
+      Node tst = datatypes::utils::mkTester(d_candidate, i, gdt);
+      Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl;
+      lemmas.push_back(tst.negate());
+    }
+  }
+  if (!isActive())
+  {
+    return false;
+  }
+  // initialize the enumerator
+  return Cegis::processInitialize(conj, n, candidates, lemmas);
+}
+
+bool CegisCoreConnective::processConstructCandidates(
+    const std::vector<Node>& enums,
+    const std::vector<Node>& enum_values,
+    const std::vector<Node>& candidates,
+    std::vector<Node>& candidate_values,
+    bool satisfiedRl,
+    std::vector<Node>& lems)
+{
+  Assert(isActive());
+  bool ret = constructSolution(enums, enum_values, candidate_values);
+
+  // exclude in the basic way if passive
+  Assert(enums.size() == 1);
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0, esize = enums.size(); i < esize; i++)
+  {
+    Node e = enums[i];
+    if (!d_tds->isPassiveEnumerator(e))
+    {
+      continue;
+    }
+    Node v = enum_values[i];
+    Node lem = d_tds->getExplain()->getExplanationForEquality(e, v).negate();
+    Node g = d_tds->getActiveGuardForEnumerator(e);
+    if (!g.isNull())
+    {
+      lem = nm->mkNode(OR, g.negate(), lem);
+    }
+    lems.push_back(lem);
+  }
+  return ret;
+}
+
+bool CegisCoreConnective::isActive() const
+{
+  return d_pre.isActive() || d_post.isActive();
+}
+
+bool CegisCoreConnective::constructSolution(
+    const std::vector<Node>& candidates,
+    const std::vector<Node>& candidate_values,
+    std::vector<Node>& solv)
+{
+  // if the conjecture is not the right shape, no repair is possible
+  if (!isActive())
+  {
+    return false;
+  }
+  Assert(candidates.size() == candidate_values.size());
+  Trace("sygus-ccore-summary")
+      << "CegisCoreConnective: construct solution..." << std::endl;
+  if (Trace.isOn("sygus-ccore"))
+  {
+    Trace("sygus-ccore")
+        << "CegisCoreConnective: Construct 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-ccore") << "  " << candidates[i] << " -> " << ss.str()
+                           << std::endl;
+    }
+  }
+  Assert(candidates.size() == 1 && candidates[0] == d_candidate);
+  TNode cval = candidate_values[0];
+  Node ets = d_eterm.substitute(d_candidate, cval);
+  Node etsr = Rewriter::rewrite(ets);
+  Trace("sygus-ccore-debug") << "...predicate is: " << etsr << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned d = 0; d < 2; d++)
+  {
+    Component& ccheck = d == 0 ? d_pre : d_post;
+    if (!ccheck.isActive())
+    {
+      // not trying this direction
+      continue;
+    }
+    Component& cfilter = d == 0 ? d_post : d_pre;
+    // In terms of the algorithm described in the h file, this gets the formula
+    // A (or B, depending on the direction d).
+    Node fpred = cfilter.getFormula();
+    if (!fpred.isNull() && !fpred.isConst())
+    {
+      // check refinement points
+      Node etsrn = d == 0 ? etsr : etsr.negate();
+      std::unordered_set<Node, NodeHashFunction> visited;
+      std::vector<Node> pt;
+      Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt);
+      if (!rid.isNull())
+      {
+        // failed a refinement point
+        continue;
+      }
+      Node fassert = nm->mkNode(AND, fpred, etsrn);
+      Trace("sygus-ccore-debug")
+          << "...check filter " << fassert << "..." << std::endl;
+      std::vector<Node> mvs;
+      Result r = checkSat(fassert, mvs);
+      Trace("sygus-ccore-debug") << "...got " << r << std::endl;
+      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+      {
+        // failed the filter, remember the refinement point
+        if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+        {
+          cfilter.addRefinementPt(fassert, mvs);
+        }
+        continue;
+      }
+    }
+    Trace("sygus-ccore-debug")
+        << "...add to pool in direction " << d << std::endl;
+    // implements e.g. pool(B) += e_i.
+    ccheck.addToPool(etsr, cval);
+
+    // ----- get the pool of assertions and randomize it
+    std::vector<Node> passerts;
+    ccheck.getTermPool(passerts);
+    std::shuffle(passerts.begin(), passerts.end(), Random::getRandom());
+
+    // ----- check for entailment, adding based on models of failed points
+    std::vector<Node> asserts;
+    Node sol = constructSolutionFromPool(ccheck, asserts, passerts);
+    if (!sol.isNull())
+    {
+      solv.push_back(sol);
+      Trace("sygus-ccore-summary") << "...success" << std::endl;
+      return true;
+    }
+    if (Trace.isOn("sygus-ccore-summary"))
+    {
+      std::stringstream ss;
+      ccheck.debugPrintSummary(ss);
+      Trace("sygus-ccore-summary")
+          << "C[d=" << d << "] " << ss.str() << std::endl;
+    }
+  }
+  Trace("sygus-ccore") << "CegisCoreConnective: failed to generate candidate"
+                       << std::endl;
+  Trace("sygus-ccore-summary") << "...failed" << std::endl;
+  return false;
+}
+
+void CegisCoreConnective::Component::initialize(Node n, Node c)
+{
+  d_this = n;
+  d_scons = c;
+}
+
+void CegisCoreConnective::Component::addToPool(Node n, Node s)
+{
+  d_cpool.push_back(n);
+  d_cpoolToSol[n] = s;
+}
+
+Node CegisCoreConnective::Component::getSygusSolution(
+    std::vector<Node>& conjs) const
+{
+  std::sort(conjs.begin(), conjs.end());
+  Node sol;
+  std::map<Node, Node>::const_iterator itu;
+  NodeManager* nm = NodeManager::currentNM();
+  for (const Node& u : conjs)
+  {
+    itu = d_cpoolToSol.find(u);
+    Assert(itu != d_cpoolToSol.end());
+    Node s = itu->second;
+    Trace("sygus-ccore-debug-sy") << "  uc-s " << s << std::endl;
+    if (sol.isNull())
+    {
+      sol = s;
+    }
+    else
+    {
+      sol = nm->mkNode(APPLY_CONSTRUCTOR, d_scons, s, sol);
+    }
+  }
+  return sol;
+}
+void CegisCoreConnective::Component::debugPrintSummary(std::ostream& os) const
+{
+  os << "size(pool/pts/cores): " << d_cpool.size() << "/" << d_numRefPoints
+     << "/" << d_numFalseCores;
+}
+
+void CegisCoreConnective::Component::addRefinementPt(
+    Node id, const std::vector<Node>& pt)
+{
+  d_numRefPoints++;
+  bool res = d_refinementPt.addTerm(id, pt);
+  // this should always be a new point
+  AlwaysAssert(res);
+}
+void CegisCoreConnective::Component::addFalseCore(Node id,
+                                                  const std::vector<Node>& u)
+{
+  d_numFalseCores++;
+  d_falseCores.add(id, u);
+}
+
+Node CegisCoreConnective::Component::getRefinementPt(
+    CegisCoreConnective* p,
+    Node n,
+    std::unordered_set<Node, NodeHashFunction>& visited,
+    std::vector<Node>& ss)
+{
+  std::vector<Node> ctx;
+
+  unsigned depth = p->d_vars.size();
+  std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator> vt;
+  std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator>::iterator itvt;
+  std::map<Node, NodeTrie>::iterator itv;
+  std::vector<NodeTrie*> visit;
+  NodeTrie* cur;
+  visit.push_back(&d_refinementPt);
+  do
+  {
+    cur = visit.back();
+    Trace("sygus-ccore-ref") << "process trie " << cur << std::endl;
+    if (ctx.size() == depth)
+    {
+      Trace("sygus-ccore-ref") << "...at depth " << std::endl;
+      // at leaf
+      Node id = cur->getData();
+      Trace("sygus-ccore-ref") << "...data is " << id << std::endl;
+      Assert(!id.isNull());
+      AlwaysAssert(id.getType().isBoolean());
+      if (visited.find(id) == visited.end())
+      {
+        visited.insert(id);
+        Trace("sygus-ccore-ref") << "...eval " << std::endl;
+        // check if it is true
+        Node en = p->evaluate(n, id, ctx);
+        if (en.isConst() && en.getConst<bool>())
+        {
+          ss = ctx;
+          return id;
+        }
+      }
+      visit.pop_back();
+      ctx.pop_back();
+    }
+    else
+    {
+      // get the current child iterator for this node
+      itvt = vt.find(cur);
+      if (itvt == vt.end())
+      {
+        Trace("sygus-ccore-ref") << "...initialize iterator " << std::endl;
+        // initialize the iterator
+        itv = cur->d_data.begin();
+        vt[cur] = itv;
+        Trace("sygus-ccore-ref") << "...finished init" << std::endl;
+      }
+      else
+      {
+        Trace("sygus-ccore-ref") << "...continue iterator " << std::endl;
+        itv = itvt->second;
+      }
+      Trace("sygus-ccore-ref") << "...now check status" << std::endl;
+      // are we done iterating children?
+      if (itv == cur->d_data.end())
+      {
+        Trace("sygus-ccore-ref") << "...finished iterating " << std::endl;
+        // yes, pop back
+        if (!ctx.empty())
+        {
+          ctx.pop_back();
+        }
+        visit.pop_back();
+        vt.erase(cur);
+      }
+      else
+      {
+        Trace("sygus-ccore-ref") << "...recurse " << itv->first << std::endl;
+        // recurse
+        ctx.push_back(itv->first);
+        visit.push_back(&(itv->second));
+        ++vt[cur];
+      }
+    }
+
+  } while (!visit.empty());
+  return Node::null();
+}
+
+void CegisCoreConnective::Component::getTermPool(
+    std::vector<Node>& passerts) const
+{
+  passerts.insert(passerts.end(), d_cpool.begin(), d_cpool.end());
+}
+
+bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
+                                                  std::vector<Node>& passerts,
+                                                  const std::vector<Node>& mvs,
+                                                  Node mvId,
+                                                  std::vector<Node>& asserts,
+                                                  Node& an)
+{
+  // point should be valid
+  Assert(!mvId.isNull());
+  Node n;
+  unsigned currIndex = 0;
+  do
+  {
+    // select condition from passerts that evaluates to false on mvs
+    for (unsigned i = currIndex, psize = passerts.size(); i < psize; i++)
+    {
+      Node cn = passerts[i];
+      Node cne = p->evaluate(cn, mvId, mvs);
+      if (cne.isConst() && !cne.getConst<bool>())
+      {
+        n = cn;
+        // remove n from the pool
+        passerts.erase(passerts.begin() + i, passerts.begin() + i + 1);
+        currIndex = i;
+        break;
+      }
+    }
+    if (n.isNull())
+    {
+      // could not find any
+      return false;
+    }
+    Trace("sygus-ccore-debug") << "...try adding " << n << "..." << std::endl;
+    asserts.push_back(n);
+    // is it already part of a false core?
+    if (d_falseCores.hasSubset(asserts))
+    {
+      Trace("sygus-ccore-debug")
+          << "..." << n << " was rejected due to previous false core"
+          << std::endl;
+      asserts.pop_back();
+      n = Node::null();
+    }
+  } while (n.isNull());
+  Trace("sygus-ccore") << "--- Insert " << n << " to falsify " << mvs
+                       << std::endl;
+  // success
+  if (an.isConst())
+  {
+    Assert(an.getConst<bool>());
+    an = n;
+  }
+  else
+  {
+    an = NodeManager::currentNM()->mkNode(AND, n, an);
+  }
+  return true;
+}
+
+void CegisCoreConnective::getModel(SmtEngine& smt,
+                                   std::vector<Node>& vals) const
+{
+  for (const Node& v : d_vars)
+  {
+    Node mv = Node::fromExpr(smt.getValue(v.toExpr()));
+    Trace("sygus-ccore-model") << v << " -> " << mv << " ";
+    vals.push_back(mv);
+  }
+}
+
+bool CegisCoreConnective::getUnsatCore(SmtEngine& smt,
+                                       Node query,
+                                       std::vector<Node>& uasserts) const
+{
+  UnsatCore uc = smt.getUnsatCore();
+  bool hasQuery = false;
+  for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
+  {
+    Node uassert = Node::fromExpr(*i);
+    Trace("sygus-ccore-debug") << "  uc " << uassert << std::endl;
+    if (uassert == query)
+    {
+      hasQuery = true;
+      continue;
+    }
+    uasserts.push_back(uassert);
+  }
+  return hasQuery;
+}
+
+Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
+{
+  Assert(mvs.empty());
+  Assert(n.getType().isBoolean());
+  Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
+  n = Rewriter::rewrite(n);
+  if (n.isConst())
+  {
+    if (n.getConst<bool>())
+    {
+      // default model
+      for (const Node& v : d_vars)
+      {
+        mvs.push_back(v.getType().mkGroundTerm());
+      }
+      return Result(Result::SAT);
+    }
+    else
+    {
+      return Result(Result::UNSAT);
+    }
+  }
+  SmtEngine smt(NodeManager::currentNM()->toExprManager());
+  smt.setIsInternalSubsolver();
+  smt.setLogic(smt::currentSmtEngine()->getLogicInfo());
+  smt.assertFormula(n.toExpr());
+  Result r = smt.checkSat();
+  Trace("sygus-ccore-debug") << "...got " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+  {
+    getModel(smt, mvs);
+  }
+  return r;
+}
+
+Node CegisCoreConnective::evaluate(Node n,
+                                   Node id,
+                                   const std::vector<Node>& mvs)
+{
+  Kind nk = n.getKind();
+  if (nk == AND || nk == OR)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    bool expRes = nk == OR;
+    // split AND/OR
+    for (const Node& nc : n)
+    {
+      Node enc = evaluate(nc, id, mvs);
+      Assert(enc.isConst());
+      if (enc.getConst<bool>() == expRes)
+      {
+        return nm->mkConst(expRes);
+      }
+    }
+    return nm->mkConst(!expRes);
+  }
+  std::unordered_map<Node, Node, NodeHashFunction>& ec = d_eval_cache[n];
+  if (!id.isNull())
+  {
+    std::unordered_map<Node, Node, NodeHashFunction>::iterator it = ec.find(id);
+    if (it != ec.end())
+    {
+      return it->second;
+    }
+  }
+  // use evaluator
+  Node cn = d_eval.eval(n, d_vars, mvs);
+  if (cn.isNull())
+  {
+    Node cn =
+        n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end());
+    cn = Rewriter::rewrite(cn);
+  }
+  if (!id.isNull())
+  {
+    ec[id] = cn;
+  }
+  return cn;
+}
+
+Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
+                                                    std::vector<Node>& asserts,
+                                                    std::vector<Node>& passerts)
+{
+  // In terms of Variant #2 from the header file, the set D is represented by
+  // asserts. The available set of prediates pool(B) is represented by passerts.
+  NodeManager* nm = NodeManager::currentNM();
+  Trace("sygus-ccore") << "------ Get initial candidate..." << std::endl;
+  Node an = asserts.empty()
+                ? d_true
+                : (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts));
+  std::vector<Node> mvs;
+  std::unordered_set<Node, NodeHashFunction> visited;
+  bool addSuccess = true;
+  // Ensure that the current conjunction evaluates to false on all refinement
+  // points. We get refinement points until we have exhausted.
+  // In terms of Variant #2, this is inner while loop that adds points to D
+  // while there exists a point in pts(B) such that D is true.
+  Node mvId;
+  do
+  {
+    mvs.clear();
+    Trace("sygus-ccore-debug") << "...get refinement pt..." << std::endl;
+    // In terms of Variant #2, this implements the line:
+    //   "D[v] is true for some v in pts(B)",
+    // where v is stored in mvs.
+    mvId = ccheck.getRefinementPt(this, an, visited, mvs);
+    if (!mvId.isNull())
+    {
+      Trace("sygus-ccore-debug") << "...got " << mvs << std::endl;
+      // In terms of Variant #2, this checks the conditions:
+      //   "d'[v] is false for some d' in pool(B)" and
+      //   "no element of cores(B) is a subset of D ++ { d' }"
+      // and adds d' to D (asserts) if possible.
+      addSuccess = ccheck.addToAsserts(this, passerts, mvs, mvId, asserts, an);
+      Trace("sygus-ccore-debug")
+          << "...add success is " << addSuccess << std::endl;
+    }
+    else
+    {
+      Trace("sygus-ccore-debug") << "...failed" << std::endl;
+    }
+  } while (!mvId.isNull() && addSuccess);
+  if (!addSuccess)
+  {
+    Trace("sygus-ccore") << ">>> Failed to generate initial candidate"
+                         << std::endl;
+    return Node::null();
+  }
+  Trace("sygus-ccore") << "----- Initial candidate is " << an << std::endl;
+
+  // We now have constructed an initial candidate for D. In terms of Variant #2,
+  // we now enter the block code within "if D is false for all v in pts(B)".
+  // Further refinements to D are made as the following do-while loop proceeds.
+  do
+  {
+    addSuccess = false;
+    // try a new core
+    SmtEngine checkSol(nm->toExprManager());
+    checkSol.setIsInternalSubsolver();
+    checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo());
+    Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
+    std::vector<Node> rasserts = asserts;
+    rasserts.push_back(ccheck.getFormula());
+    std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom());
+    Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
+    for (const Node& a : rasserts)
+    {
+      checkSol.assertFormula(a.toExpr());
+    }
+    Result r = checkSol.checkSat();
+    Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
+    // In terms of Variant #2, this is the check "if D => B"
+    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      // it entails the postcondition, now get the unsat core
+      // In terms of Variant #2, this is the line
+      //   "Let U be a subset of D such that U ^ ~B is unsat."
+      // and uasserts is set to U.
+      std::vector<Node> uasserts;
+      bool hasQuery = getUnsatCore(checkSol, ccheck.getFormula(), uasserts);
+      // now, check the side condition
+      bool falseCore = false;
+      if (!d_sc.isNull())
+      {
+        if (!hasQuery)
+        {
+          // Already know it trivially rewrites to false, don't need
+          // to use unsat cores.
+          falseCore = true;
+        }
+        else
+        {
+          // In terms of Variant #2, this is the check "if S ^ U is unsat"
+          Trace("sygus-ccore") << "----- Check side condition" << std::endl;
+          SmtEngine checkSc(nm->toExprManager());
+          checkSc.setIsInternalSubsolver();
+          checkSc.setLogic(smt::currentSmtEngine()->getLogicInfo());
+          std::vector<Node> scasserts;
+          scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
+          scasserts.push_back(d_sc);
+          std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
+          Result rsc = checkSc.checkSat();
+          Trace("sygus-ccore")
+              << "----- check-sat returned " << rsc << std::endl;
+          if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT)
+          {
+            // In terms of Variant #2, this is the line
+            //   "Let W be a subset of D such that S ^ W is unsat."
+            // and uasserts is set to W.
+            uasserts.clear();
+            getUnsatCore(checkSc, d_sc, uasserts);
+            falseCore = true;
+          }
+        }
+      }
+
+      if (!falseCore)
+      {
+        // In terms of Variant #2, this is the line:
+        //   "return u_1 AND ... AND u_m where U = { u_1, ..., u_m }".
+        Trace("sygus-ccore") << ">>> Solution : " << uasserts << std::endl;
+        // We convert the builtin solution to a sygus datatype to
+        // communicate with the sygus solver.
+        Node sol = ccheck.getSygusSolution(uasserts);
+        Trace("sygus-ccore-sy") << "Sygus solution : " << sol << std::endl;
+        return sol;
+      }
+      else
+      {
+        Assert(!uasserts.empty());
+        Node xu = uasserts[0];
+        Trace("sygus-ccore")
+            << "--- Add false core : " << uasserts << std::endl;
+        // notice that a singleton false core could be removed from pool
+        // in the case that (uasserts.size() == 1).
+        std::sort(uasserts.begin(), uasserts.end());
+        // In terms of Variant #2, this is "cores(B) += W".
+        ccheck.addFalseCore(query, uasserts);
+        // remove and continue
+        // In terms of Variant #2, this is "remove some d'' in W from D".
+        std::vector<Node>::iterator ita =
+            std::find(asserts.begin(), asserts.end(), xu);
+        Assert(ita != asserts.end());
+        asserts.erase(ita);
+        // Start over, since now we don't know which points are required to
+        // falsify.
+        return constructSolutionFromPool(ccheck, asserts, passerts);
+      }
+    }
+    else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+    {
+      // it does not entail the postcondition, add an assertion that blocks
+      // the current point
+      mvs.clear();
+      getModel(checkSol, mvs);
+      // should evaluate to true
+      Node ean = evaluate(an, Node::null(), mvs);
+      Assert(ean.isConst() && ean.getConst<bool>());
+      Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl;
+      // In terms of Variant #2, this is the line:
+      //   "pts(B) += { v } where { x -> v } is a model for D ^ ~B".
+      ccheck.addRefinementPt(query, mvs);
+      Trace("sygus-ccore-debug") << "...get new assertion..." << std::endl;
+      // In terms of Variant #2, this rechecks the condition of the inner while
+      // loop and attempts to add a new assertion to D.
+      addSuccess = ccheck.addToAsserts(this, passerts, mvs, query, asserts, an);
+      Trace("sygus-ccore-debug") << "...success is " << addSuccess << std::endl;
+    }
+  } while (addSuccess);
+  return Node::null();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
new file mode 100644
index 000000000..3589d97e5
--- /dev/null
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -0,0 +1,396 @@
+/*********************                                                        */
+/*! \file cegis_core_connective.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Cegis core connective module.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+
+#include <unordered_set>
+#include "expr/node.h"
+#include "expr/node_trie.h"
+
+#include "theory/evaluator.h"
+#include "theory/quantifiers/sygus/cegis.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * A trie that stores data at undetermined depth. Storing data at
+ * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
+ * assumes all data is stored at a fixed depth.
+ *
+ * Since data can be stored at any depth, we require both a d_children field
+ * and a d_data field.
+ */
+class VariadicTrie
+{
+ public:
+  /** the children of this node */
+  std::map<Node, VariadicTrie> d_children;
+  /** the data at this node */
+  Node d_data;
+  /**
+   * Add data with identifier n indexed by i, return true if data is not already
+   * stored at the node indexed by i.
+   */
+  bool add(Node n, const std::vector<Node>& i);
+  /** Is there any data in this trie that is indexed by any subset of is? */
+  bool hasSubset(const std::vector<Node>& is) const;
+};
+
+/** CegisCoreConnective
+ *
+ * A sygus module that is specialized in handling conjectures of the form:
+ * exists P. forall x. (A[x] => C(x)) ^ (C(x) => B(x))
+ * That is, conjectures with a pre/post condition but no inductive relation
+ * or other constraints. Additionally, we may have that the above conjecture
+ * has a side condition SC, which requires that exists x. SC[x]^C(x) is
+ * satisfiable.
+ *
+ * Two examples of this kind of sygus conjecture are abduction and
+ * interpolation.
+ *
+ * This module implements a specific algorithm for constructing solutions
+ * to this conjecture based on Boolean connectives and unsat cores, described
+ * in following. We give two variants of the algorithm, both implemented as
+ * special cases of this class. Below, let:
+ *
+ * pool(A) be a set of literals { c_1, ..., c_n } s.t. c_i => B for i=1,...,n,
+ * pts(A) : a set of points { v | A[v] is true },
+ * pool(B) : a set of literals { d_1, ..., d_m } s.t. A => d_i for i=1,...,m,
+ * pts(B) : a set of points { v | ~B[v] is true },
+ * cores(B) : a set of sets of literals { U_1, ..., U_p } s.t. for i=1,...,p:
+ * - U_i is a subset of pool(B),
+ * - A ^ U_i is unsat.
+ * We construct pool(A)/pool(B) using enumerative SyGuS, discarding the literals
+ * that do not match the criteria.
+ *
+ * Variant #1 (Interpolation)
+ *
+ * Let the synthesis conjecture be of the form
+ *   exists C. forall x. A[x] => C[x] ^ C[x] => B[x]
+ *
+ * The high level idea is we construct solutions for C of the form
+ *   c_1 OR ... OR c_n where c_i => B for each i=1,...,n, or
+ *   d_1 AND ... AND d_m where A => d_i for each i=1,...,m.
+ *
+ * while(true){
+ *   Let e_i = next_sygus_enum();
+ *   // check if e_i should be added to pool(B)
+ *   if e_i[v] is true for all v in pts(A)
+ *     if A => e_i
+ *       pool(B) += e_i;
+ *     else
+ *       pts(A) += { v } where { x -> v } is a model for A ^ ~e_i;
+ *   // try to construct a solution based on the pool
+ *   Let D = {}.
+ *   while
+ *     D[v] is true for some v in pts(B), and
+ *     d'[v] is false for some d' in pool(B)
+ *   {
+ *     D += { d' }
+ *     if D is false for all v in pts(B)
+ *       if D => B
+ *         return AND_{d in D}( d )
+ *       else
+ *         pts(B) += { v } where { x -> v } is a model for D ^ ~B
+ *   }
+ *
+ *   // analogous for the other direction
+ * }
+ *
+ *
+ * Variant #2 (Abduction)
+ *
+ * Let the synthesis conjecture be of the form exists C. forall x. C[x] => B[x]
+ * such that S[x] ^ C[x] is satisfiable. We refer to S as the side condition
+ * for this conjecture. Notice that A in this variant is false, hence the
+ * algorithm below is modified accordingly.
+ *
+ * The high level idea is we construct solutions for C of the form
+ *   d_1 AND ... AND d_n
+ * where the above conjunction is weakened based on only including conjuncts
+ * that are in the unsat core of d_1 AND ... AND d_n => B.
+ *
+ * while(true){
+ *   Let e_i = next_sygus_enum();
+ *   // add e_i to the pool
+ *   pool(B) += e_i;
+ *   // try to construct a solution based on the pool
+ *   Let D = {}.
+ *   while
+ *     D[v] is true for some v in pts(B), and
+ *     d'[v] is false for some d' in pool(B) and
+ *     no element of cores(B) is a subset of D ++ { d' }
+ *   {
+ *     D += { d' }
+ *     if D is false for all v in pts(B)
+ *       if D => B
+ *         Let U be a subset of D such that U ^ ~B is unsat.
+ *         if S ^ U is unsat
+ *           Let W be a subset of D such that S ^ W is unsat.
+ *             cores(B) += W
+ *             remove some d'' in W from D
+ *         else
+ *           return u_1 AND ... AND u_m where U = { u_1, ..., u_m }
+ *       else
+ *         pts(B) += { v } where { x -> v } is a model for D ^ ~B
+ *   }
+ * }
+ */
+class CegisCoreConnective : public Cegis
+{
+ public:
+  CegisCoreConnective(QuantifiersEngine* qe, SynthConjecture* p);
+  ~CegisCoreConnective() {}
+  /**
+   * Return whether this module has the possibility to construct solutions. This
+   * is true if this module has been initialized, and the shape of the
+   * conjecture allows us to use the core connective algorithm.
+   */
+  bool isActive() const;
+
+ protected:
+  /** do cegis-implementation-specific initialization for this class */
+  bool processInitialize(Node conj,
+                         Node n,
+                         const std::vector<Node>& candidates,
+                         std::vector<Node>& lemmas) override;
+  /** do cegis-implementation-specific post-processing for construct candidate
+   *
+   * satisfiedRl is whether all refinement lemmas are satisfied under the
+   * substitution { enums -> enum_values }.
+   */
+  bool processConstructCandidates(const std::vector<Node>& enums,
+                                  const std::vector<Node>& enum_values,
+                                  const std::vector<Node>& candidates,
+                                  std::vector<Node>& candidate_values,
+                                  bool satisfiedRl,
+                                  std::vector<Node>& lems) override;
+
+  /** construct solution
+   *
+   * This function is called when candidates -> candidate_values is the current
+   * candidate solution for the synthesis conjecture.
+   *
+   * If this function returns true, then this class adds to solv the
+   * a candidate solution for candidates.
+   */
+  bool constructSolution(const std::vector<Node>& candidates,
+                         const std::vector<Node>& candidate_values,
+                         std::vector<Node>& solv);
+
+ private:
+  /** common constants */
+  Node d_true;
+  Node d_false;
+  /** The first-order datatype variable for the function-to-synthesize */
+  TNode d_candidate;
+  /**
+   * Information about the pre and post conditions of the synthesis conjecture.
+   * This maintains all information needed for producing solutions relative to
+   * one direction of the synthesis conjecture. In other words, this component
+   * may be focused on finding a C1 ... Cn such that A => C1 V ... V Cn
+   * or alteratively C1 ^ ... ^ Cn such that C1 ^ ... ^ Cn => B.
+   */
+  class Component
+  {
+   public:
+    Component() : d_numFalseCores(0), d_numRefPoints(0) {}
+    /** initialize
+     *
+     * This initializes this component with pre/post condition given by n
+     * and sygus constructor c.
+     */
+    void initialize(Node n, Node c);
+    /** get the formula n that we initialized this with */
+    Node getFormula() const { return d_this; }
+    /** Is this component active? */
+    bool isActive() const { return !d_scons.isNull(); }
+    /** Add term n to pool whose sygus analog is s */
+    void addToPool(Node n, Node s);
+    /** Add a refinement point to this component */
+    void addRefinementPt(Node id, const std::vector<Node>& pt);
+    /** Add a false case to this component */
+    void addFalseCore(Node id, const std::vector<Node>& u);
+    /**
+     * Selects a node from passerts that evaluates to false on point mv if one
+     * exists, or otherwise returns false.
+     * The argument mvId is an identifier used for indexing the point mv.
+     * The argument asserts stores the current candidate solution (set D in
+     * Variant #2 described above). If the method returns true, it updates
+     * an (the node version of asserts) to be the conjunction of the nodes
+     * in asserts.
+     *
+     * If true is returned, it is removed from passerts.
+     */
+    bool addToAsserts(CegisCoreConnective* p,
+                      std::vector<Node>& passerts,
+                      const std::vector<Node>& mvs,
+                      Node mvId,
+                      std::vector<Node>& asserts,
+                      Node& an);
+
+    /**
+     * Get a refinement point that n evalutes to true on, taken from the
+     * d_refinementPt trie, and store it in ss. The set visited is the set
+     * of leaf nodes (reference by their data) that we have already processed
+     * and should be ignored.
+     */
+    Node getRefinementPt(CegisCoreConnective* p,
+                         Node n,
+                         std::unordered_set<Node, NodeHashFunction>& visited,
+                         std::vector<Node>& ss);
+    /** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */
+    void getTermPool(std::vector<Node>& passerts) const;
+    /**
+     * Get the sygus solution corresponding to the Boolean connective for
+     * this component applied to conj. In particular, this returns a
+     * right-associative chain of applications of sygus constructor d_scons
+     * to the sygus analog of formulas in conj.
+     */
+    Node getSygusSolution(std::vector<Node>& conjs) const;
+    /** debug print summary (for debugging) */
+    void debugPrintSummary(std::ostream& os) const;
+
+   private:
+    /** The original formula for the pre/post condition A/B. */
+    Node d_this;
+    /**
+     * The sygus constructor for constructing solutions based on the core
+     * connective algorithm. This is a sygus datatype constructor that
+     * encodes applications of AND or OR.
+     */
+    Node d_scons;
+    /** This is pool(A)/pool(B) in the algorithms above */
+    std::vector<Node> d_cpool;
+    /**
+     * A map from the formulas in the above vector to their sygus analog.
+     */
+    std::map<Node, Node> d_cpoolToSol;
+    /**
+     * An index of list of predicates such that each list ( P1, ..., Pn )
+     * indexed by this trie is such that P1 ^ ... ^ Pn ^ S is unsatisfiable,
+     * where S is the side condition of our synthesis conjecture. We call this
+     * a "false core". This set is "cores(B)" in Variant #2 above.
+     */
+    VariadicTrie d_falseCores;
+    /**
+     * The number of points that have been added to the above trie, for
+     * debugging.
+     */
+    unsigned d_numFalseCores;
+    /**
+     * An index of the points that satisfy d_this.
+     */
+    NodeTrie d_refinementPt;
+    /**
+     * The number of points that have been added to the above trie, for
+     * debugging.
+     */
+    unsigned d_numRefPoints;
+  };
+  /** Above information for the precondition of the synthesis conjecture */
+  Component d_pre;
+  /** Above information for the postcondition of the synthesis conjecture */
+  Component d_post;
+  /**
+   * The free variables that may appear in the pre/post condition, and our
+   * pools of predicates.
+   */
+  std::vector<Node> d_vars;
+  /**
+   * The evaluation term of the form:
+   *   (DT_SYGUS_EVAL d_candidate d_vars[0]...d_vars[n])
+   * This is used to convert enumerated sygus terms t to their builtin
+   * equivalent via rewriting d_eterm * { d_candidate -> t }.
+   */
+  Node d_eterm;
+  /**
+   * The side condition of the conjecture. If this is non-null, then
+   * this node is a formula such that (builtin) solutions t' are such that
+   * t' ^ d_sc is satisfiable. Notice that the free variables of d_sc are
+   * a subset of d_vars.
+   */
+  Node d_sc;
+  //-----------------------------------for SMT engine calls
+  /**
+   * Assuming smt has just been called to check-sat and returned "SAT", this
+   * method adds the model for d_vars to mvs.
+   */
+  void getModel(SmtEngine& smt, std::vector<Node>& mvs) const;
+  /**
+   * Assuming smt has just been called to check-sat and returned "UNSAT", this
+   * method get the unsat core and adds it to uasserts.
+   *
+   * If query is non-null, then it is excluded from uasserts. If query was
+   * in the unsat core, then this method returns true. Otherwise, this method
+   * returns false. It also returns false if query was null.
+   */
+  bool getUnsatCore(SmtEngine& smt,
+                    Node query,
+                    std::vector<Node>& uasserts) const;
+  /**
+   * Return the result of checking satisfiability of formula n.
+   * If n was satisfiable, then we store the model for d_vars in mvs.
+   */
+  Result checkSat(Node n, std::vector<Node>& mvs) const;
+  //-----------------------------------end for SMT engine calls
+  //-----------------------------------for evaluation
+  /**
+   * Return the evaluation of n under the substitution { d_vars -> mvs }.
+   * If id is non-null, then id is a unique identifier for mvs, and we cache
+   * the result of n for this point.
+   */
+  Node evaluate(Node n, Node id, const std::vector<Node>& mvs);
+  /** A cache of the above function */
+  std::unordered_map<Node,
+                     std::unordered_map<Node, Node, NodeHashFunction>,
+                     NodeHashFunction>
+      d_eval_cache;
+  /** The evaluator utility used for the above function */
+  Evaluator d_eval;
+  //-----------------------------------end for evaluation
+
+  /** Construct solution from pool
+   *
+   * This is the main body of the core connective algorithm, which attempts
+   * to build a solution based on one direction (pre/post) of the synthesis
+   * conjecture.
+   *
+   * It takes as input:
+   * - a component ccheck that maintains information regarding the direction
+   * we are trying to build a solution for,
+   * - the current set of assertions asserts that comprise the current solution
+   * we are building,
+   * - the current pool passerts of available assertions that we may add to
+   * asserts.
+   *
+   * This implements the while loop in the algorithms above. If this method
+   * returns a non-null node, then this is a solution for the given synthesis
+   * conjecture.
+   */
+  Node constructSolutionFromPool(Component& ccheck,
+                                 std::vector<Node>& asserts,
+                                 std::vector<Node>& passerts);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index c980e5413..ca4feda32 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -52,6 +52,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
+      d_sygus_ccore(new CegisCoreConnective(qe, this)),
       d_ceg_pbe(new SygusPbe(qe, this)),
       d_ceg_cegis(new Cegis(qe, this)),
       d_ceg_cegisUnif(new CegisUnif(qe, this)),
@@ -69,6 +70,10 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }
+  if (options::sygusCoreConnective())
+  {
+    d_modules.push_back(d_sygus_ccore.get());
+  }
   d_modules.push_back(d_ceg_cegis.get());
 }
 
@@ -438,7 +443,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
 
   NodeManager* nm = NodeManager::currentNM();
 
-  // check the side condition
+  // check the side condition if we constructed a candidate
   if (constructed_cand)
   {
     if (!checkSideCondition(candidate_values))
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 344f8b460..db9872ec3 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/expr_miner_manager.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/cegis.h"
+#include "theory/quantifiers/sygus/cegis_core_connective.h"
 #include "theory/quantifiers/sygus/cegis_unif.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
@@ -192,6 +193,8 @@ class SynthConjecture
   std::unique_ptr<CegGrammarConstructor> d_ceg_gc;
   /** repair constant utility */
   std::unique_ptr<SygusRepairConst> d_sygus_rconst;
+  /** connective core utility */
+  std::unique_ptr<CegisCoreConnective> d_sygus_ccore;
 
   //------------------------modules
   /** program by examples module */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0bcaa049a..787633178 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1682,8 +1682,10 @@ set(regress_1_tests
   regress1/strings/username_checker_min.smt2
   regress1/sygus-abduct-ex1-grammar.smt2
   regress1/sygus-abduct-test.smt2
+  regress1/sygus-abduct-test-ccore.smt2
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
+  regress1/sygus/abd-simple-conj-4.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array_search_5-Q-easy.sy
   regress1/sygus/bvudiv-by-2.sy
diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
new file mode 100644
index 000000000..86f5fe133
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(get-abduct A (not (< x y)))
diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index 4b7870c78..bb02ebce2 100644
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --produce-abducts
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic QF_UFLIRA)
@@ -19,6 +20,8 @@
 (get-abduct A (not (< x y))
 
 ; the grammar for the abduct-to-synthesize
+; notice it does not permit the sygus-core-connective algorithm; this regression
+; tests that we ignore this option properly.
 ((Start Bool) (StartInt Int))
 (
 (Start Bool ((< StartInt StartInt)))
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
new file mode 100644
index 000000000..98bf70fd7
--- /dev/null
+++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+(assert (>= x 0))
+(get-abduct A (>= (+ x y z w u v) 2))