Sygus support for inductive datatypes.

7 files changed, 91 insertions, 29 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();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fa145813c..ce8f68c09 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1787,6 +1787,12 @@ void SmtEngine::defineFunction(Expr func,
   d_definedFunctions->insert(funcNode, def);
 }
 
+bool SmtEngine::isDefinedFunction( Expr func ){
+  Node nf = Node::fromExpr( func );
+  Debug("smt") << "isDefined function " << nf << "?" << std::endl;
+  return d_definedFunctions->find(nf) != d_definedFunctions->end();
+}
+
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index de9b8127d..db0809308 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine {
    *A vector of command definitions to be imported in the new
    *SmtEngine when checking unsat-cores.
    */
-#ifdef CVC4_PROOF  
+#ifdef CVC4_PROOF
   std::vector<Command*> d_defineCommands;
-#endif   
+#endif
   /**
    * The logic we're in.
    */
@@ -455,6 +455,9 @@ public:
                       const std::vector<Expr>& formals,
                       Expr formula);
 
+  /** is defined function */
+  bool isDefinedFunction(Expr func);
+
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
@@ -536,7 +539,7 @@ public:
    * Print solution for synthesis conjectures found by ce_guided_instantiation module
    */
   void printSynthSolution( std::ostream& out );
-  
+
   /**
    * Get an unsatisfiable core (only if immediately preceded by an
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
@@ -707,7 +710,7 @@ public:
    * Set print function in model
    */
   void setPrintFuncInModel(Expr f, bool p);
-  
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 37c7a4d57..132c55cd9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1322,7 +1322,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
       d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" );
     }
   }
-  return isFree ? d_vts_delta_free : d_vts_delta;  
+  return isFree ? d_vts_delta_free : d_vts_delta;
 }
 
 Node TermDb::getVtsInfinity( bool isFree, bool create ) {
@@ -1832,10 +1832,12 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
   if( op.getKind()==BUILTIN ){
     ret = NodeManager::currentNM()->mkNode( op, children );
   }else{
-    if( children.size()==1 ){
+    Kind ok = getOperatorKind( op );
+    Trace("sygus-db") << "Operator kind is " << ok << std::endl;
+    if( children.size()==1 && ok==kind::UNDEFINED_KIND ){
       ret = children[0];
     }else{
-      ret = NodeManager::currentNM()->mkNode( APPLY, children );
+      ret = NodeManager::currentNM()->mkNode( ok, children );
       /*
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
@@ -2463,6 +2465,24 @@ 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() ) ){
+    return APPLY;
+  }else{
+    TypeNode tn = op.getType();
+    if( tn.isConstructor() ){
+      return APPLY_CONSTRUCTOR;
+    }else if( tn.isSelector() ){
+      return APPLY_SELECTOR;
+    }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();
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index ad206b470..23594d49a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -518,6 +518,8 @@ public:
   Kind getComparisonKind( TypeNode tn );
   Kind getPlusKind( TypeNode tn, bool is_neg = false );
   bool doCompare( Node a, Node b, Kind k );
+  /** get operator kind */
+  static Kind getOperatorKind( Node op );
   /** print sygus term */
   static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
 };