Sygus Lambda Grammars (#1390)

6 files changed, 38 insertions, 131 deletions

diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index e1bc32761..bc6817560 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/ce_guided_conjecture.h"
 
 #include "expr/datatype.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "prop/prop_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -428,8 +430,7 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >&
       TypeNode tn = nv.getType();
       Trace("cegqi-engine") << n[i] << " -> ";
       std::stringstream ss;
-      std::vector< Node > lvs;
-      TermDbSygus::printSygusTerm( ss, nv, lvs );
+      Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
       Trace("cegqi-engine") << ss.str() << " ";
     }
     Assert( !nv.isNull() );
@@ -621,8 +622,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
       if( status==0 ){
         out << sol;
       }else{
-        std::vector< Node > lvs;
-        TermDbSygus::printSygusTerm( out, sol, lvs );
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
     }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 03026069f..b2b4fe18c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -143,22 +143,12 @@ void CegConjectureSingleInv::initialize( Node q ) {
       d_sip->debugPrint( "cegqi-si" );
 
       //map from program to bound variables
-      std::vector< Node > order_vars;
-      std::map< Node, Node > single_inv_app_map;
-      for( unsigned j=0; j<progs.size(); j++ ){
-        Node prog = progs[j];
-        Node pv = d_sip->getFirstOrderVariableForFunction(prog);
-        if (!pv.isNull())
-        {
-          Node inv = d_sip->getFunctionInvocationFor(prog);
-          Assert(!inv.isNull());
-          single_inv_app_map[prog] = inv;
-          Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
-          d_prog_to_sol_index[prog] = order_vars.size();
-          order_vars.push_back( pv );
-        }else{
-          Trace("cegqi-si") << "  " << prog << " has no fo var." << std::endl;
-        }
+      std::vector<Node> funcs;
+      d_sip->getFunctions(funcs);
+      for (unsigned j = 0, size = funcs.size(); j < size; j++)
+      {
+        Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end());
+        d_prog_to_sol_index[funcs[j]] = j;
       }
 
       //check if it is single invocation
@@ -180,7 +170,8 @@ void CegConjectureSingleInv::initialize( Node q ) {
             Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
             std::vector<Node> sivars;
             d_sip->getSingleInvocationVariables(sivars);
-            Node invariant = single_inv_app_map[prog];
+            Node invariant = d_sip->getFunctionInvocationFor(prog);
+            Assert(!invariant.isNull());
             invariant = invariant.substitute(sivars.begin(),
                                              sivars.end(),
                                              prog_templ_vars.begin(),
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index b618fc5d5..9a18d13fb 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -55,6 +55,17 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
 struct SynthesisAttributeId {};
 typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
 
+/** Attribute for setting printing information for sygus variables
+ *
+ * For variable d of sygus datatype type, if
+ * d.getAttribute(SygusPrintProxyAttribute) = t, then printing d will print t.
+ */
+struct SygusPrintProxyAttributeId
+{
+};
+typedef expr::Attribute<SygusPrintProxyAttributeId, Node>
+    SygusPrintProxyAttribute;
+
 namespace quantifiers {
 
 /** Attribute priority for rewrite rules */
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index e212e0dfb..8625d9089 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ce_guided_conjecture.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -277,13 +278,6 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       ret = children[0];
     }else{
       ret = NodeManager::currentNM()->mkNode( ok, children );
-      /*
-      Node n = NodeManager::currentNM()->mkNode( APPLY, children );
-      //must expand definitions
-      Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
-      Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
-      return ne;
-      */
     }
   }
   Trace("sygus-db-debug") << "...returning " << ret << std::endl;
@@ -345,13 +339,12 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) {
     // if we are not interested in reconstructing constants, or the grammar allows them, return a proxy
     if( !options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst() ){
       Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
-      SygusProxyAttribute spa;
+      SygusPrintProxyAttribute spa;
       k.setAttribute(spa,c);
       sc = k;
     }else{
       int carg = getOpConsNum( tn, c );
       if( carg!=-1 ){
-        //sc = Node::fromExpr( dt[carg].getSygusOp() );
         sc = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
       }else{
         //identity functions
@@ -1545,110 +1538,28 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string
 
 Kind TermDbSygus::getOperatorKind( Node op ) {
   Assert( op.getKind()!=BUILTIN );
-  if( smt::currentSmtEngine()->isDefinedFunction( op.toExpr() ) ){
+  Assert(!smt::currentSmtEngine()->isDefinedFunction(op.toExpr()));
+  if (op.getKind() == LAMBDA)
+  {
     return APPLY;
   }else{
     TypeNode tn = op.getType();
     if( tn.isConstructor() ){
       return APPLY_CONSTRUCTOR;
-    }else if( tn.isSelector() ){
+    }
+    else if (tn.isSelector())
+    {
       return APPLY_SELECTOR;
-    }else if( tn.isTester() ){
+    }
+    else if (tn.isTester())
+    {
       return APPLY_TESTER;
-    }else{
-      return NodeManager::operatorToKind( op );
     }
-  }
-}
-
-void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ) {
-  if( n.getKind()==APPLY_CONSTRUCTOR ){
-    TypeNode tn = n.getType();
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    if( dt.isSygus() ){
-      int cIndex = Datatype::indexOf( n.getOperator().toExpr() );
-      Assert( !dt[cIndex].getSygusOp().isNull() );
-      if( dt[cIndex].getSygusLetBody().isNull() ){
-        if( n.getNumChildren()>0 ){
-          out << "(";
-        }
-        Node op = dt[cIndex].getSygusOp();
-        if( op.getType().isBitVector() && op.isConst() ){
-          //print in the style it was given
-          Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
-          std::stringstream ss;
-          ss << dt[cIndex].getName();
-          std::string str = ss.str();
-          std::size_t found = str.find_last_of("_");
-          Assert( found!=std::string::npos );
-          std::string name = std::string( str.begin() + found +1, str.end() );
-          out << name;
-        }else{
-          out << op;
-        }
-        if( n.getNumChildren()>0 ){
-          for( unsigned i=0; i<n.getNumChildren(); i++ ){
-            out << " ";
-            printSygusTerm( out, n[i], lvs );
-          }
-          out << ")";
-        }
-      }else{
-        std::stringstream let_out;
-        //print as let term
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          let_out << "(let (";
-        }
-        std::vector< Node > subs_lvs;
-        std::vector< Node > new_lvs;
-        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
-          Node v = Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
-          subs_lvs.push_back( v );
-          std::stringstream ss;
-          ss << "_l_" << new_lvs.size();
-          Node lv = NodeManager::currentNM()->mkBoundVar( ss.str(), v.getType() );
-          new_lvs.push_back( lv );
-          //map free variables to proper terms
-          if( i<dt[cIndex].getNumSygusLetInputArgs() ){
-            //it should be printed as a let argument
-            let_out << "(";
-            let_out << lv << " " << lv.getType() << " ";
-            printSygusTerm( let_out, n[i], lvs );
-            let_out << ")";
-          }
-        }
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          let_out << ") ";
-        }
-        //print the body
-        Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
-        let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
-        new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
-        printSygusTerm( let_out, let_body, new_lvs );
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          let_out << ")";
-        }
-        //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables
-        std::string lbody = let_out.str();
-        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
-          std::stringstream old_str;
-          old_str << new_lvs[i];
-          std::stringstream new_str;
-          if( i>=dt[cIndex].getNumSygusLetInputArgs() ){
-            printSygusTerm( new_str, n[i], lvs );
-          }else{
-            new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
-          }
-          doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
-        }
-        out << lbody;
-      }
-      return;
+    else if (tn.isFunction())
+    {
+      return APPLY_UF;
     }
-  }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
-    out << n.getAttribute(SygusProxyAttribute());
-  }else{
-    out << n;
+    return NodeManager::operatorToKind(op);
   }
 }
 
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 5ff1612c9..45851c0c8 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -198,8 +198,6 @@ public:
   
   /** get operator kind */
   static Kind getOperatorKind( Node op );
-  /** print sygus term */
-  static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
 
   /** get anchor */
   static Node getAnchor( Node n );
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index d2a8a14f0..5ac21dafb 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -62,10 +62,6 @@ typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 struct LtePartialInstAttributeId {};
 typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
 
-// attribute for sygus proxy variables
-struct SygusProxyAttributeId {};
-typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
-
 // attribute for associating a synthesis function with a first order variable
 struct SygusSynthGrammarAttributeId {};
 typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>