Remove support for prototype (non-sygus) synthesis (#2338)

7 files changed, 66 insertions, 118 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6491856a5..5e068948f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2435,8 +2435,9 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
         PARSER_STATE->warning(ss.str());
       }
       // do nothing
-    } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" ||
-              attr==":sygus" || attr==":synthesis") {
+    }
+    else if (attr==":axiom" || attr==":conjecture" || attr==":fun-def")
+    {
       if(hasValue) {
         std::stringstream ss;
         ss << "warning: Attribute " << attr
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index e8e93dc0f..dde6dc4a9 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -74,10 +74,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
     SygusSynthFunVarListAttribute ssfvla;
     n.setAttribute( ssfvla, node_values[0] );
-  }else if( attr=="synthesis" ){
-    Trace("quant-attr-debug") << "Set synthesis " << n << std::endl;
-    SynthesisAttribute ca;
-    n.setAttribute( ca, true );
   }else if( attr=="quant-inst-max-level" ){
     Assert( node_values.size()==1 );
     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
@@ -238,12 +234,6 @@ void QuantAttributes::computeAttributes( Node q ) {
     }
     d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
   }
-  if( d_qattr[q].d_synthesis ){
-    if( d_quantEngine->getCegInstantiation()==NULL ){
-      Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
-    }
-    d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
-  }
 }
 
 void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
@@ -282,10 +272,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
                               << " for " << q << std::endl;
           qa.d_name = avar;
         }
-        if( avar.getAttribute(SynthesisAttribute()) ){
-          Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
-          qa.d_synthesis = true;
-        }
         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
           qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
           Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
@@ -355,15 +341,6 @@ bool QuantAttributes::isSygus( Node q ) {
   }
 }
 
-bool QuantAttributes::isSynthesis( Node q ) {
-  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
-  if( it==d_qattr.end() ){
-    return false;
-  }else{
-    return it->second.d_synthesis;
-  }
-}
-
 int QuantAttributes::getQuantInstLevel( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 16de5fd2e..918269bbe 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -57,10 +57,6 @@ struct QuantNameAttributeId
 };
 typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
 
-/** Attribute true for quantifiers that are synthesis conjectures */
-struct SynthesisAttributeId {};
-typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-
 struct InstLevelAttributeId
 {
 };
@@ -87,8 +83,17 @@ namespace quantifiers {
 struct QAttributes
 {
  public:
-  QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
-                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
+  QAttributes()
+      : d_hasPattern(false),
+        d_conjecture(false),
+        d_axiom(false),
+        d_sygus(false),
+        d_rr_priority(-1),
+        d_qinstLevel(-1),
+        d_quant_elim(false),
+        d_quant_elim_partial(false)
+  {
+  }
   ~QAttributes(){}
   /** does the quantified formula have a pattern? */
   bool d_hasPattern;
@@ -104,8 +109,6 @@ struct QAttributes
   Node d_fundef_f;
   /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
-  /** is this formula marked as a synthesis (non-sygus) conjecture? */
-  bool d_synthesis;
   /** 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
@@ -192,8 +195,6 @@ public:
   bool isFunDef( Node q );
   /** is sygus conjecture */
   bool isSygus( Node q );
-  /** is synthesis conjecture */
-  bool isSynthesis( Node q );
   /** get instantiation level */
   int getQuantInstLevel( Node q );
   /** get rewrite rule priority */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 31a76d933..e3057da29 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -50,8 +50,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
-      d_refine_count(0),
-      d_syntax_guided(false)
+      d_refine_count(0)
 {
   if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
   {
@@ -153,36 +152,19 @@ void CegConjecture::assign( Node q ) {
     Assert(d_master != nullptr);
   }
 
-  if (d_qe->getQuantAttributes()->isSygus(q))
+  Assert(d_qe->getQuantAttributes()->isSygus(q));
+  // if the base instantiation is an existential, store its variables
+  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
   {
-    // if the base instantiation is an existential, store its variables
-    if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
+    for (const Node& v : d_base_inst[0][0])
     {
-      for (const Node& v : d_base_inst[0][0])
-      {
-        d_inner_vars.push_back(v);
-      }
+      d_inner_vars.push_back(v);
     }
-    d_syntax_guided = true;
-  }
-  else if (d_qe->getQuantAttributes()->isSynthesis(q))
-  {
-    d_syntax_guided = false;
-  }else{
-    Assert( false );
   }
   
   // initialize the guard
-  if( !d_syntax_guided ){
-    if( d_nsg_guard.isNull() ){
-      d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-      d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
-      AlwaysAssert( !d_nsg_guard.isNull() );
-      d_qe->getOutputChannel().requirePhase( d_nsg_guard, true );
-      // negated base as a guarded lemma
-      guarded_lemmas.push_back( d_base_inst.negate() );
-    }
-  }else if( d_ceg_si->getGuard().isNull() ){
+  if (d_ceg_si->getGuard().isNull())
+  {
     std::vector< Node > lems;
     d_ceg_si->getInitialSingleInvLemma( lems );
     for( unsigned i=0; i<lems.size(); i++ ){
@@ -205,9 +187,7 @@ void CegConjecture::assign( Node q ) {
   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
 }
 
-Node CegConjecture::getGuard() {
-  return !d_syntax_guided ? d_nsg_guard : d_ceg_si->getGuard();
-}
+Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); }
 
 bool CegConjecture::isSingleInvocation() const {
   return d_ceg_si->isSingleInvocation();
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 0b6f0e1a8..25f063e06 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -101,8 +101,6 @@ public:
   Node getGuard();
   /** is ground */
   bool isGround() { return d_inner_vars.empty(); }
-  /** does this conjecture correspond to a syntax-guided synthesis input */
-  bool isSyntaxGuided() const { return d_syntax_guided; }
   /** are we using single invocation techniques */
   bool isSingleInvocation() const;
   /** preregister conjecture 
@@ -259,14 +257,6 @@ private:
    */
   void printAndContinueStream();
   //-------------------------------- end sygus stream
-  //-------------------------------- non-syntax guided (deprecated)
-  /** Whether we are syntax-guided (e.g. was the input in SyGuS format).
-   * This includes SyGuS inputs where no syntactic restrictions are provided.
-   */
-  bool d_syntax_guided;
-  /** the guard for non-syntax-guided synthesis */
-  Node d_nsg_guard;
-  //-------------------------------- end non-syntax guided (deprecated)
   /** candidate rewrite objects for each program variable
    *
    * This is used for the sygusRewSynth() option to synthesize new candidate
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 378c2f1d7..b3cb98bc5 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -267,52 +267,52 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
   if( !conj->needsRefinement() ){
     Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
-    if( conj->isSyntaxGuided() ){
-      std::vector< Node > clems;
-      conj->doSingleInvCheck( clems );
-      if( !clems.empty() ){
-        d_last_inst_si = true;
-        for( unsigned j=0; j<clems.size(); j++ ){
-          Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << clems[j] << std::endl;
-          d_quantEngine->addLemma( clems[j] );
-        }
-        d_statistics.d_cegqi_si_lemmas += clems.size();
-        Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
-        return;
-      }
-      
-      Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
-      std::vector< Node > cclems;
-      conj->doCheck(cclems);
-      bool addedLemma = false;
-      for( unsigned i=0; i<cclems.size(); i++ ){
-        Node lem = cclems[i];
-        d_last_inst_si = false;
-        Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
-        if( d_quantEngine->addLemma( lem ) ){
-          ++(d_statistics.d_cegqi_lemmas_ce);
-          addedLemma = true;
-        }else{
-          //this may happen if we eagerly unfold, simplify to true
-          Trace("cegqi-engine-debug")
-              << "  ...FAILED to add candidate!" << std::endl;
-        }
+    std::vector<Node> clems;
+    conj->doSingleInvCheck(clems);
+    if (!clems.empty())
+    {
+      d_last_inst_si = true;
+      for (const Node& lem : clems)
+      {
+        Trace("cegqi-lemma")
+            << "Cegqi::Lemma : single invocation instantiation : " << lem
+            << std::endl;
+        d_quantEngine->addLemma(lem);
       }
-      if( addedLemma ){
-        Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
+      d_statistics.d_cegqi_si_lemmas += clems.size();
+      Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
+      return;
+    }
+
+    Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+    std::vector<Node> cclems;
+    conj->doCheck(cclems);
+    bool addedLemma = false;
+    for (const Node& lem : cclems)
+    {
+      d_last_inst_si = false;
+      Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
+                           << std::endl;
+      if (d_quantEngine->addLemma(lem))
+      {
+        ++(d_statistics.d_cegqi_lemmas_ce);
+        addedLemma = true;
       }else{
-        if( conj->needsRefinement() ){
-          //immediately go to refine candidate
-          checkCegConjecture( conj );
-          return;
-        }
-      } 
+        // this may happen if we eagerly unfold, simplify to true
+        Trace("cegqi-engine-debug")
+            << "  ...FAILED to add candidate!" << std::endl;
+      }
+    }
+    if (addedLemma)
+    {
+      Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
     }else{
-      Assert( aq==q );
-      Trace("cegqi-engine") << "  *** Check candidate phase (non-SyGuS)." << std::endl;
-      std::vector< Node > lems;
-      conj->doBasicCheck(lems);
-      Assert(lems.empty());
+      if (conj->needsRefinement())
+      {
+        // immediately go to refine candidate
+        checkCegConjecture(conj);
+        return;
+      }
     }
   }else{
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 842671a5e..2ab45aa96 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -47,7 +47,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute("quant-name", this);
   out.handleUserAttribute("sygus-synth-grammar", this);
   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
-  out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );
   out.handleUserAttribute( "rr-priority", this );
   out.handleUserAttribute( "quant-elim", this );