Sygus support for inductive datatypes.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1564e6f3eb5cb9533428cddce10967456d1b05ad..1ce7c4affe094ce203f6054b85c2c71517d4a54b 100644 (file)
--- 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 9ee6d24b476398015ac1985e552f815f8e9a6db7..0500c93163ed7db27f861e85ef2940c7fdcebb88 100644 (file)
--- 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 c88f7cd8fce9451ab68beb1a7c5c1527cabff01c..c8b89799c05f19d0b1a025d6d3450ebf703318a1 100644 (file)
--- 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 fa145813cca7f0c5612d0e9e0b1a6fd2712a67ac..ce8f68c09c5b1b99f597d3ec0d1c30fe3e5b79fa 100644 (file)
--- 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 de9b8127de73b03e16d4e7755a24642ddb9cce03..db0809308270b24edb8d217b0442faee0732cf09 100644 (file)
--- 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 37c7a4d57febf1ff3e67b4e1f80006889dbf8107..132c55cd99dca2463a734c73a194c4ef98c11059 100644 (file)
--- 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 ad206b470b6d1900b5c0fac8a11ae404b73186d8..23594d49ae747605d59527f66bd199f8ea874af6 100644 (file)
--- 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 );
 };

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 9d7155f78159a2a52d9f073c5609cd9f8b67a448..82ff67d415cabf463c571dba117bff4f81e01af0 100644 (file)
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -43,7 +43,8 @@ TESTS = commutative.sy \
         enum-test.sy \
         no-syntax-test-bool.sy \
         inv-example.sy \
-        uminus_one.sy
+        uminus_one.sy \
+        sygus-dt.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \

diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
new file mode 100755 (executable)
index 0000000..e842477
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-dump-synth
+
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+(define-fun g ((x Int)) List (cons (+ x 1) nil))
+(define-fun i () List (cons 3 nil))
+
+(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start)))
+                             (StartInt Int (x 0 1 (+ StartInt StartInt)))))
+
+(declare-var x Int)
+
+(constraint (= (f x) (cons x nil)))
+(check-synth)
\ No newline at end of file