Infrastructure for sygus side conditions (#2729)

4 files changed, 79 insertions, 2 deletions

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index ff906a95b..e3463df0d 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -267,6 +267,14 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
           qa.d_sygus = true;
         }
+        if (avar.hasAttribute(SygusSideConditionAttribute()))
+        {
+          qa.d_sygusSideCondition =
+              avar.getAttribute(SygusSideConditionAttribute());
+          Trace("quant-attr")
+              << "Attribute : sygus side condition : "
+              << qa.d_sygusSideCondition << " : " << q << std::endl;
+        }
         if (avar.getAttribute(QuantNameAttribute()))
         {
           Trace("quant-attr") << "Attribute : quantifier name : " << avar
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 918269bbe..d3acc9434 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -73,6 +73,17 @@ struct SygusPrintProxyAttributeId
 typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
     SygusPrintProxyAttribute;
 
+/** Attribute for specifying a "side condition" for a sygus conjecture
+ *
+ * A sygus conjecture of the form exists f. forall x. P[f,x] whose side
+ * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x].
+ */
+struct SygusSideConditionAttributeId
+{
+};
+typedef expr::Attribute<SygusSideConditionAttributeId, Node>
+    SygusSideConditionAttribute;
+
 namespace quantifiers {
 
 /** Attribute priority for rewrite rules */
@@ -109,6 +120,8 @@ struct QAttributes
   Node d_fundef_f;
   /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
+  /** side condition for sygus conjectures */
+  Node d_sygusSideCondition;
   /** if a rewrite rule, then this is the priority value for the rewrite rule */
   int d_rr_priority;
   /** stores the maximum instantiation level allowed for this quantified formula
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ff7bb6378..e25e8a225 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -87,10 +87,14 @@ void SynthConjecture::assign(Node q)
   // pre-simplify the quantified formula based on the process utility
   d_simp_quant = d_ceg_proc->preSimplify(d_quant);
 
+  // compute its attributes
+  QAttributes qa;
+  QuantAttributes::computeQuantAttributes(q, qa);
+
   std::map<Node, Node> templates;
   std::map<Node, Node> templates_arg;
   // register with single invocation if applicable
-  if (d_qe->getQuantAttributes()->isSygus(q))
+  if (qa.d_sygus)
   {
     d_ceg_si->initialize(d_simp_quant);
     d_simp_quant = d_ceg_si->getSimplifiedConjecture();
@@ -117,9 +121,18 @@ void SynthConjecture::assign(Node q)
   Trace("cegqi") << "SynthConjecture : converted to embedding : "
                  << d_embed_quant << std::endl;
 
+  Node sc = qa.d_sygusSideCondition;
+  if (!sc.isNull())
+  {
+    // convert to deep embedding
+    d_embedSideCondition = d_ceg_gc->convertToEmbedding(sc);
+    Trace("cegqi") << "SynthConjecture : side condition : "
+                   << d_embedSideCondition << std::endl;
+  }
+
   // we now finalize the single invocation module, based on the syntax
   // restrictions
-  if (d_qe->getQuantAttributes()->isSygus(q))
+  if (qa.d_sygus)
   {
     d_ceg_si->finishInit(d_ceg_gc->isSyntaxRestricted());
   }
@@ -138,6 +151,11 @@ void SynthConjecture::assign(Node q)
   // construct base instantiation
   d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation(
       d_embed_quant, vars, d_candidates));
+  if (!d_embedSideCondition.isNull())
+  {
+    d_embedSideCondition = d_embedSideCondition.substitute(
+        vars.begin(), vars.end(), d_candidates.begin(), d_candidates.end());
+  }
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
 
   // initialize the sygus constant repair utility
@@ -509,6 +527,33 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   // record the instantiation
   // this is used for remembering the solution
   recordInstantiation(candidate_values);
+
+  // check the side condition
+  Node sc;
+  if (!d_embedSideCondition.isNull() && constructed_cand)
+  {
+    sc = d_embedSideCondition.substitute(d_candidates.begin(),
+                                         d_candidates.end(),
+                                         candidate_values.begin(),
+                                         candidate_values.end());
+    sc = Rewriter::rewrite(sc);
+    Trace("cegqi-engine") << "Check side condition..." << std::endl;
+    Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
+    SmtEngine scSmt(nm->toExprManager());
+    scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
+    scSmt.assertFormula(sc.toExpr());
+    Result r = scSmt.checkSat();
+    Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
+    if (r == Result::UNSAT)
+    {
+      // exclude the current solution TODO
+      excludeCurrentSolution();
+      Trace("cegqi-engine") << "...failed side condition" << std::endl;
+      return false;
+    }
+    Trace("cegqi-engine") << "...passed side condition" << std::endl;
+  }
+
   Node query = lem;
   bool success = false;
   if (query.isConst() && !query.getConst<bool>())
@@ -968,7 +1013,11 @@ void SynthConjecture::printAndContinueStream()
   // this output stream should coincide with wherever --dump-synth is output on
   Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
   printSynthSolution(*nodeManagerOptions.getOut());
+  excludeCurrentSolution();
+}
 
+void SynthConjecture::excludeCurrentSolution()
+{
   // We will not refine the current candidate solution since it is a solution
   // thus, we clear information regarding the current refinement
   d_set_ce_sk_vars = false;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 3a43eb83d..cf6178fdb 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -280,6 +280,11 @@ class SynthConjecture
 
   /** the asserted (negated) conjecture */
   Node d_quant;
+  /**
+   * The side condition for solving the conjecture, after conversion to deep
+   * embedding.
+   */
+  Node d_embedSideCondition;
   /** (negated) conjecture after simplification */
   Node d_simp_quant;
   /** (negated) conjecture after simplification, conversion to deep embedding */
@@ -363,6 +368,8 @@ class SynthConjecture
    * output channel, which we refer to as a "stream exclusion lemma".
    */
   void printAndContinueStream();
+  /** exclude the current solution */
+  void excludeCurrentSolution();
   /**
    * Whether we have guarded a stream exclusion lemma when using sygusStream.
    * This is an optimization that allows us to guard only the first stream