Sygus support for inductive datatypes.

3 files changed, 53 insertions, 22 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1564e6f3e..1ce7c4aff 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -606,6 +606,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
+  | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
+  | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | /* synth-fun */
     ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -912,7 +914,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
           // fail, but we need an operator to continue here..
           Debug("parser-sygus") << "Sygus grammar " << fun;
           Debug("parser-sygus") << " : op (declare=" <<  PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl;
-          if( !PARSER_STATE->isDefinedFunction(name) ){
+          if( !PARSER_STATE->isDeclared(name) && !PARSER_STATE->isDefinedFunction(name) ){
             PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
           }
           sgt.d_name = name;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9ee6d24b4..0500c9316 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -522,9 +522,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
     Type t = sygus_vars[i].getType();
     if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){
+      Debug("parser-sygus") << "...will make grammar for " << t << std::endl;
       types.push_back( t );
     }
   }
+  if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() ){
+    parseError("No default grammar for type.");
+  }
 
   //name of boolean sort
   std::stringstream ssb;
@@ -993,6 +997,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
   std::stringstream ss;
   ss << datatypes[index].getName() << "_let";
   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+  d_sygus_defined_funs.push_back( let_func );
   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
 
   ops[index].pop_back();
@@ -1180,6 +1185,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       //replace operator and name
       ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
       cnames[i] = ss.str();
+      d_sygus_defined_funs.push_back( ops[i] );
       preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) );
       addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 );
     }else{
@@ -1216,6 +1222,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           std::stringstream ssid;
           ssid << unresolved_gterm_sym[i] << "_id";
           Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+          d_sygus_defined_funs.push_back( id_op );
           preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) );
           //make the sygus argument list
           std::vector< Type > id_carg;
@@ -1310,15 +1317,35 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   for(size_t k = 0; k < builtApply.size(); ++k) {
   }
   Expr builtTerm;
-  //if( ops[i][j].getKind() == kind::BUILTIN ){
-  if( !builtApply.empty() ){
-    if( ops[i][j].getKind() != kind::BUILTIN ){
-      builtTerm = getExprManager()->mkExpr(kind::APPLY, ops[i][j], builtApply);
+  Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl;
+  if( ops[i][j].getKind() != kind::BUILTIN ){
+    Kind ok = kind::UNDEFINED_KIND;
+    if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){
+      ok = kind::APPLY;
     }else{
-      builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
+      Type t = ops[i][j].getType();
+      if( t.isConstructor() ){
+        ok = kind::APPLY_CONSTRUCTOR;
+      }else if( t.isSelector() ){
+        ok = kind::APPLY_SELECTOR;
+      }else if( t.isTester() ){
+        ok = kind::APPLY_TESTER;
+      }else{
+        ok = getExprManager()->operatorToKind( ops[i][j] );
+      }
+    }
+    Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl;
+    if( ok!=kind::UNDEFINED_KIND ){
+      builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply);
+    }else{
+      builtTerm = ops[i][j];
     }
   }else{
-    builtTerm = ops[i][j];
+    if( !builtApply.empty() ){
+      builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
+    }else{
+      builtTerm = ops[i][j];
+    }
   }
   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c88f7cd8f..c8b89799c 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -35,7 +35,7 @@ namespace CVC4 {
 class SExpr;
 
 namespace parser {
-  
+
 class Smt2 : public Parser {
   friend class ParserBuilder;
 
@@ -180,7 +180,7 @@ public:
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
 
-  void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,                                
+  void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                           std::vector< CVC4::Datatype >& datatypes,
                           std::vector< CVC4::Type>& sorts,
                           std::vector< std::vector<CVC4::Expr> >& ops,
@@ -188,10 +188,10 @@ public:
                           std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
                           std::vector< bool >& allow_const,
                           std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                          std::vector<CVC4::Expr>& sygus_vars, 
-                          std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, 
+                          std::vector<CVC4::Expr>& sygus_vars,
+                          std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
                           CVC4::Type& ret, bool isNested = false );
-  
+
   static bool pushSygusDatatypeDef( Type t, std::string& dname,
                                     std::vector< CVC4::Datatype >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
@@ -208,12 +208,12 @@ public:
                                    std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
                                    std::vector< bool >& allow_const,
                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym );
-  
-  void setSygusStartIndex( std::string& fun, int startIndex, 
+
+  void setSygusStartIndex( std::string& fun, int startIndex,
                            std::vector< CVC4::Datatype >& datatypes,
                            std::vector< CVC4::Type>& sorts,
                            std::vector< std::vector<CVC4::Expr> >& ops );
-  
+
   void addSygusFun(const std::string& fun, Expr eval) {
     d_sygusFuns.push_back(std::make_pair(fun, eval));
   }
@@ -222,7 +222,7 @@ public:
 
   void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                         std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
-                        std::vector<std::string>& unresolved_gterm_sym, 
+                        std::vector<std::string>& unresolved_gterm_sym,
                         std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
 
   // i is index in datatypes/ops
@@ -230,7 +230,7 @@ public:
   Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops,
                           std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms,
                           Expr eval, const Datatype& dt, size_t i, size_t j );
-  
+
 
 
   void addSygusConstraint(Expr constraint) {
@@ -311,9 +311,11 @@ private:
   std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
   std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;
   std::map< CVC4::Expr, unsigned > d_sygus_let_func_to_num_input_vars;
-  
+  //auxiliary define-fun functions introduced for production rules
+  std::vector< CVC4::Expr > d_sygus_defined_funs;
+
   void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
-  
+
   void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
                                     CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args );
 
@@ -327,16 +329,16 @@ private:
                                 std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                 std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
 
-  void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, 
+  void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index,
                                    std::vector< CVC4::Datatype >& datatypes,
                                    std::vector< CVC4::Type>& sorts,
                                    std::vector< std::vector<CVC4::Expr> >& ops,
                                    std::vector< std::vector<std::string> >& cnames,
                                    std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                   std::vector<CVC4::Expr>& sygus_vars, 
+                                   std::vector<CVC4::Expr>& sygus_vars,
                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                    std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
-  
+
   void addArithmeticOperators();
 
   void addBitvectorOperators();