From 20704741e4609055d61e010b6981c6916d28019a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Nov 2017 14:25:59 -0600
Subject: Sygus Lambda Grammars (#1390)

---
 src/theory/quantifiers/term_database_sygus.cpp | 119 ++++---------------------
 1 file changed, 15 insertions(+), 104 deletions(-)

(limited to 'src/theory/quantifiers/term_database_sygus.cpp')

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);
   }
 }
 
-- 
cgit v1.2.3