Add interface in sygus to get synthesis solution Nodes (#1552)

diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 74d5cef472930c8ecbd7f2271189ce8023a41ed2..cc00599d31da65d996973fcda3f3d4e5484c60c6 100644 (file)
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -560,67 +560,22 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
 void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) {
   Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
   Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
-  for( unsigned i=0; i<d_embed_quant[0].getNumChildren(); i++ ){
-    Node prog = d_embed_quant[0][i];
-    Trace("cegqi-debug") << "  print solution for " << prog << std::endl;
-    std::stringstream ss;
-    ss << prog;
-    std::string f(ss.str());
-    f.erase(f.begin());
-    TypeNode tn = prog.getType();
-    Assert( tn.isDatatype() );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    //get the solution
-    Node sol;
-    int status = -1;
-    if( singleInvocation ){
-      Assert( d_ceg_si != NULL );
-      sol = d_ceg_si->getSolution( i, tn, status, true );
-      if( !sol.isNull() ){
-        sol = sol.getKind()==LAMBDA ? sol[1] : sol;
-      }
-    }else{
-      Node cprog = getCandidate( i );
-      if( !d_cinfo[cprog].d_inst.empty() ){
-        // the solution is just the last instantiated term
-        sol = d_cinfo[cprog].d_inst.back();
-        status = 1;
-        
-        //check if there was a template
-        Node sf = d_quant[0][i];
-        Node templ = d_ceg_si->getTemplate( sf );
-        if( !templ.isNull() ){
-          Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl;
-          // if it was not embedded into the grammar
-          if( !options::sygusTemplEmbedGrammar() ){
-            TNode templa = d_ceg_si->getTemplateArg( sf );
-            // make the builtin version of the full solution
-            TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
-            sol = sygusDb->sygusToBuiltin( sol, sol.getType() );               
-            Trace("cegqi-inv") << "Builtin version of solution is : "
-                               << sol << ", type : " << sol.getType()
-                               << std::endl;
-            TNode tsol = sol;
-            sol = templ.substitute( templa, tsol );
-            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
-            sol = Rewriter::rewrite( sol );
-            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
-            // now, reconstruct to the syntax
-            sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
-            sol = sol.getKind()==LAMBDA ? sol[1] : sol;
-            Trace("cegqi-inv-debug") << "Reconstructed to syntax : " << sol << std::endl;
-          }else{
-            Trace("cegqi-inv-debug") << "...was embedding into grammar." << std::endl;
-          }
-        }else{
-          Trace("cegqi-inv-debug") << sf << " did not use template" << std::endl;
-        }
-      }else{
-        Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl;
-      }
-    }
-    if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){
+  std::vector<Node> sols;
+  std::vector<int> statuses;
+  getSynthSolutionsInternal(sols, statuses, singleInvocation);
+  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
+  {
+    Node sol = sols[i];
+    if (!sol.isNull())
+    {
+      Node prog = d_embed_quant[0][i];
+      int status = statuses[i];
+      TypeNode tn = prog.getType();
+      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      std::stringstream ss;
+      ss << prog;
+      std::string f(ss.str());
+      f.erase(f.begin());
       out << "(define-fun " << f << " ";
       if( dt.getSygusVarList().isNull() ){
         out << "() ";
@@ -695,6 +650,122 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
   }
 }
 
+void CegConjecture::getSynthSolutions(std::map<Node, Node>& sol_map,
+                                      bool singleInvocation)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+  std::vector<Node> sols;
+  std::vector<int> statuses;
+  getSynthSolutionsInternal(sols, statuses, singleInvocation);
+  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
+  {
+    Node sol = sols[i];
+    int status = statuses[i];
+    // get the builtin solution
+    Node bsol = sol;
+    if (status != 0)
+    {
+      // convert sygus to builtin here
+      bsol = sygusDb->sygusToBuiltin(sol, sol.getType());
+    }
+    // convert to lambda
+    TypeNode tn = d_embed_quant[0][i].getType();
+    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    Node bvl = Node::fromExpr(dt.getSygusVarList());
+    if (!bvl.isNull())
+    {
+      bsol = nm->mkNode(LAMBDA, bvl, bsol);
+    }
+    // store in map
+    Node fvar = d_quant[0][i];
+    Assert(fvar.getType() == bsol.getType());
+    sol_map[fvar] = bsol;
+  }
+}
+
+void CegConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
+                                              std::vector<int>& statuses,
+                                              bool singleInvocation)
+{
+  for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
+  {
+    Node prog = d_embed_quant[0][i];
+    Trace("cegqi-debug") << "  get solution for " << prog << std::endl;
+    TypeNode tn = prog.getType();
+    Assert(tn.isDatatype());
+    // get the solution
+    Node sol;
+    int status = -1;
+    if (singleInvocation)
+    {
+      Assert(d_ceg_si != NULL);
+      sol = d_ceg_si->getSolution(i, tn, status, true);
+      if (!sol.isNull())
+      {
+        sol = sol.getKind() == LAMBDA ? sol[1] : sol;
+      }
+    }
+    else
+    {
+      Node cprog = getCandidate(i);
+      if (!d_cinfo[cprog].d_inst.empty())
+      {
+        // the solution is just the last instantiated term
+        sol = d_cinfo[cprog].d_inst.back();
+        status = 1;
+
+        // check if there was a template
+        Node sf = d_quant[0][i];
+        Node templ = d_ceg_si->getTemplate(sf);
+        if (!templ.isNull())
+        {
+          Trace("cegqi-inv-debug")
+              << sf << " used template : " << templ << std::endl;
+          // if it was not embedded into the grammar
+          if (!options::sygusTemplEmbedGrammar())
+          {
+            TNode templa = d_ceg_si->getTemplateArg(sf);
+            // make the builtin version of the full solution
+            TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+            sol = sygusDb->sygusToBuiltin(sol, sol.getType());
+            Trace("cegqi-inv") << "Builtin version of solution is : " << sol
+                               << ", type : " << sol.getType() << std::endl;
+            TNode tsol = sol;
+            sol = templ.substitute(templa, tsol);
+            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+            sol = Rewriter::rewrite(sol);
+            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+            // now, reconstruct to the syntax
+            sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
+            sol = sol.getKind() == LAMBDA ? sol[1] : sol;
+            Trace("cegqi-inv-debug")
+                << "Reconstructed to syntax : " << sol << std::endl;
+          }
+          else
+          {
+            Trace("cegqi-inv-debug")
+                << "...was embedding into grammar." << std::endl;
+          }
+        }
+        else
+        {
+          Trace("cegqi-inv-debug")
+              << sf << " did not use template" << std::endl;
+        }
+      }
+      else
+      {
+        Trace("cegqi-warn") << "WARNING : No recorded instantiations for "
+                               "syntax-guided solution!"
+                            << std::endl;
+      }
+    }
+    sols.push_back(sol);
+    statuses.push_back(status);
+  }
+}
+
 Node CegConjecture::getSymmetryBreakingPredicate(
     Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
 {

diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index e57b545e608803ca6cd54e51779b418df4b7495d..011967ca1c22ae746e213250777e386b55965439 100644 (file)
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -79,8 +79,25 @@ public:
    * singleInvocation is whether the solution was found by single invocation techniques.
    */
   //-------------------------------end for counterexample-guided check/refine
-
+  /**
+   * prints the synthesis solution to output stream out.
+   *
+   * singleInvocation : set to true if we should consult the single invocation
+   * module to get synthesis solutions.
+   */
   void printSynthSolution( std::ostream& out, bool singleInvocation );
+  /** get synth solutions
+   *
+   * This returns a map from function-to-synthesize variables to their
+   * builtin solution, which has the same type. For example, for synthesis
+   * conjecture exists f. forall x. f( x )>x, this function may return the map
+   * containing the entry:
+   *   f -> (lambda x. x+1)
+   *
+   * singleInvocation : set to true if we should consult the single invocation
+   * module to get synthesis solutions.
+   */
+  void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
   /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
   Node getGuard();
   /** is ground */
@@ -184,6 +201,27 @@ private:
       d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
     }
   }
+  /** get synth solutions internal
+   *
+   * This function constructs the body of solutions for all
+   * functions-to-synthesize in this conjecture and stores them in sols, in
+   * order. For each solution added to sols, we add an integer indicating what
+   * kind of solution n is, where if sols[i] = n, then
+   *   if status[i] = 0: n is the (builtin term) corresponding to the solution,
+   *   if status[i] = 1: n is the sygus representation of the solution.
+   * We store builtin versions under some conditions (such as when the sygus
+   * grammar is being ignored).
+   *
+   * singleInvocation : set to true if we should consult the single invocation
+   * module to get synthesis solutions.
+   *
+   * For example, for conjecture exists fg. forall x. f(x)>g(x), this function
+   * may set ( sols, status ) to ( { x+1, d_x() }, { 1, 0 } ), where d_x() is
+   * the sygus datatype constructor corresponding to variable x.
+   */
+  void getSynthSolutionsInternal(std::vector<Node>& sols,
+                                 std::vector<int>& status,
+                                 bool singleInvocation);
   //-------------------------------- sygus stream
   /** the streaming guards for sygus streaming mode */
   std::vector< Node > d_stream_guards;

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index b54ce48057980ac79a5017425af76c3c0d745aa4..dc359d252676a2dd7939ce55f674cb56edc3d318 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -310,14 +310,28 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto
 }
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj->isAssigned() ){
-    // print the conjecture
+  if( d_conj->isAssigned() )
+  {
     d_conj->printSynthSolution( out, d_last_inst_si );
-  }else{
+  }
+  else
+  {
     Assert( false );
   }
 }
 
+void CegInstantiation::getSynthSolutions(std::map<Node, Node>& sol_map)
+{
+  if (d_conj->isAssigned())
+  {
+    d_conj->getSynthSolutions(sol_map, d_last_inst_si);
+  }
+  else
+  {
+    Assert(false);
+  }
+}
+
 void CegInstantiation::preregisterAssertion( Node n ) {
   //check if it sygus conjecture
   if( QuantAttributes::checkSygusConjecture( n ) ){

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 86f0c4c9ff478d81016b143220738eee9390472f..6913633118b9e6a646c0d0efa1e68fd34f9b177f 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -55,6 +55,17 @@ public:
   std::string identify() const { return "CegInstantiation"; }
   /** print solution for synthesis conjectures */
   void printSynthSolution( std::ostream& out );
+  /** get synth solutions
+   *
+   * This function adds entries to sol_map that map functions-to-synthesize
+   * with their solutions, for all active conjectures (currently just the one
+   * assigned to d_conj). This should be called immediately after the solver
+   * answers unsat for sygus input.
+   *
+   * For details on what is added to sol_map, see
+   * CegConjecture::getSynthSolutions.
+   */
+  void getSynthSolutions(std::map<Node, Node>& sol_map);
   /** preregister assertion (before rewrite) */
   void preregisterAssertion( Node n );
 public: