Support for default grammar for datatypes in sygus. Support vts for infinity.

5 files changed, 168 insertions, 61 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1ce7c4aff..3dda54a18 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -730,6 +730,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         }
         evalType.push_back(sorts[i]);
         Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType));
+        Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() << std::endl;
         evals.insert(std::make_pair(dtt, eval));
         if(i == 0) {
           PARSER_STATE->addSygusFun(fun, eval);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0500c9316..cc3b09cfe 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -512,13 +512,38 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
   return e;
 }
 
+void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){
+  if( range.isInteger() || range.isBitVector() || range.isDatatype() ){
+    if( std::find( types.begin(), types.end(), range )==types.end() ){
+      Debug("parser-sygus") << "...will make grammar for " << range << std::endl;
+      types.push_back( range );
+      if( range.isDatatype() ){
+        const Datatype& dt = ((DatatypeType)range).getDatatype();
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+            Type crange = ((SelectorType)dt[i][j].getType()).getRangeType();
+            sels[crange].push_back( dt[i][j] );
+            collectSygusGrammarTypesFor( crange, types, sels );
+          }
+        }
+      }
+    }
+  }
+}
+
 void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
                                   std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) {
+
+  if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
+    parseError("No default grammar for type.");
+  }
   startIndex = -1;
   Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
 
   std::vector< Type > types;
+  std::map< Type, std::vector< DatatypeConstructorArg > > sels;
+  //types for each of the variables
   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() ){
@@ -526,9 +551,8 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       types.push_back( t );
     }
   }
-  if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() ){
-    parseError("No default grammar for type.");
-  }
+  //types connected to range
+  collectSygusGrammarTypesFor( range, types, sels );
 
   //name of boolean sort
   std::stringstream ssb;
@@ -537,25 +561,32 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   Type unres_bt = mkUnresolvedType(ssb.str());
 
   std::vector< Type > unres_types;
+  std::map< Type, Type > type_to_unres;
   for( unsigned i=0; i<types.size(); i++ ){
     std::stringstream ss;
     ss << fun << "_" << types[i];
     std::string dname = ss.str();
     datatypes.push_back(Datatype(dname));
     ops.push_back(std::vector<Expr>());
-    std::vector<std::string> cnames;
-    std::vector<std::vector<CVC4::Type> > cargs;
-    std::vector<std::string> unresolved_gterm_sym;
     //make unresolved type
     Type unres_t = mkUnresolvedType(dname);
     unres_types.push_back(unres_t);
+    type_to_unres[types[i]] = unres_t;
+    sygus_to_builtin[unres_t] = types[i];
+  }
+  for( unsigned i=0; i<types.size(); i++ ){
+    Debug("parser-sygus") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
+    std::vector<std::string> cnames;
+    std::vector<std::vector<CVC4::Type> > cargs;
+    std::vector<std::string> unresolved_gterm_sym;
+    Type unres_t = unres_types[i];
     //add variables
     for( unsigned j=0; j<sygus_vars.size(); j++ ){
       if( sygus_vars[j].getType()==types[i] ){
         std::stringstream ss;
         ss << sygus_vars[j];
         Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
-        ops.back().push_back( sygus_vars[j] );
+        ops[i].push_back( sygus_vars[j] );
         cnames.push_back( ss.str() );
         cargs.push_back( std::vector< CVC4::Type >() );
       }
@@ -567,14 +598,14 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       std::stringstream ss;
       ss << consts[j];
       Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
-      ops.back().push_back( consts[j] );
+      ops[i].push_back( consts[j] );
       cnames.push_back( ss.str() );
       cargs.push_back( std::vector< CVC4::Type >() );
     }
     //ITE
     CVC4::Kind k = kind::ITE;
     Debug("parser-sygus") << "...add for " << k << std::endl;
-    ops.back().push_back(getExprManager()->operatorOf(k));
+    ops[i].push_back(getExprManager()->operatorOf(k));
     cnames.push_back( kind::kindToString(k) );
     cargs.push_back( std::vector< CVC4::Type >() );
     cargs.back().push_back(unres_bt);
@@ -585,20 +616,45 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       for( unsigned j=0; j<2; j++ ){
         CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
         Debug("parser-sygus") << "...add for " << k << std::endl;
-        ops.back().push_back(getExprManager()->operatorOf(k));
+        ops[i].push_back(getExprManager()->operatorOf(k));
         cnames.push_back(kind::kindToString(k));
         cargs.push_back( std::vector< CVC4::Type >() );
         cargs.back().push_back(unres_t);
         cargs.back().push_back(unres_t);
       }
+    }else if( types[i].isDatatype() ){
+      Debug("parser-sygus") << "...add for constructors" << std::endl;
+      const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
+      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+        Debug("parser-sygus") << "...for " << dt[k].getName() << std::endl;
+        ops[i].push_back( dt[k].getConstructor() );
+        cnames.push_back( dt[k].getName() );
+        cargs.push_back( std::vector< CVC4::Type >() );
+        for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
+          Type crange = ((SelectorType)dt[k][j].getType()).getRangeType();
+          cargs.back().push_back( type_to_unres[crange] );
+        }
+      }
     }else{
       std::stringstream sserr;
       sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
       warning(sserr.str());
     }
+    //add for all selectors to this type
+    if( !sels[types[i]].empty() ){
+      Debug("parser-sygus") << "...add for selectors" << std::endl;
+      for( unsigned j=0; j<sels[types[i]].size(); j++ ){
+        Debug("parser-sygus") << "...for " << sels[types[i]][j].getName() << std::endl;
+        Type arg_type = ((SelectorType)sels[types[i]][j].getType()).getDomain();
+        ops[i].push_back( sels[types[i]][j].getSelector() );
+        cnames.push_back( sels[types[i]][j].getName() );
+        cargs.push_back( std::vector< CVC4::Type >() );
+        cargs.back().push_back( type_to_unres[arg_type] );
+      }
+    }
     Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
-    datatypes.back().setSygus( types[i], bvl, true, true );
-    mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
+    datatypes[i].setSygus( types[i], bvl, true, true );
+    mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin );
     sorts.push_back( types[i] );
     //set start index if applicable
     if( types[i]==range ){
@@ -613,6 +669,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   std::vector<std::string> cnames;
   std::vector<std::vector<CVC4::Type> > cargs;
   std::vector<std::string> unresolved_gterm_sym;
+  Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
   //add variables
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
     if( sygus_vars[i].getType().isBoolean() ){
@@ -653,6 +710,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   }
   //add predicates for types
   for( unsigned i=0; i<types.size(); i++ ){
+    Debug("parser-sygus") << "...add predicates for " << types[i] << std::endl;
     //add equality per type
     CVC4::Kind k = kind::EQUAL;
     Debug("parser-sygus") << "...add for " << k << std::endl;
@@ -672,6 +730,17 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       cargs.push_back( std::vector< CVC4::Type >() );
       cargs.back().push_back(unres_types[i]);
       cargs.back().push_back(unres_types[i]);
+    }else if( types[i].isDatatype() ){
+      //add for testers
+      Debug("parser-sygus") << "...add for testers" << std::endl;
+      const Datatype& dt = ((DatatypeType)types[i]).getDatatype();
+      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+        Debug("parser-sygus") << "...for " << dt[k].getTesterName() << std::endl;
+        ops.back().push_back(dt[k].getTester());
+        cnames.push_back(dt[k].getTesterName());
+        cargs.push_back( std::vector< CVC4::Type >() );
+        cargs.back().push_back(unres_types[i]);
+      }
     }
   }
   if( range==btype ){
@@ -1312,7 +1381,9 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
     if( !terms[0].isNull() ){
       patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
     }
+    Debug("parser-sygus-debug") << "...add to built apply " << evals[DatatypeType(extraArgs[k].getType())] << " " << extraArgs[k] << " " << extraArgs[k].getType() << std::endl;
     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
+    Debug("parser-sygus-debug") << "...added " << builtApply.back() << std::endl;
   }
   for(size_t k = 0; k < builtApply.size(); ++k) {
   }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 132c55cd9..380ee19fd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1338,51 +1338,73 @@ Node TermDb::getVtsInfinity( bool isFree, bool create ) {
 }
 
 Node TermDb::rewriteVtsSymbols( Node n ) {
-  Assert( !d_vts_delta_free.isNull() );
-  Assert( !d_vts_delta.isNull() );
-  if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && containsTerm( n, d_vts_delta ) ){
+  if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){
     Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
-    if( n.getKind()==EQUAL ){
-      return d_false;
-    }else{
-      std::map< Node, Node > msum;
-      if( QuantArith::getMonomialSumLit( n, msum ) ){
-        if( Trace.isOn("quant-vts-debug") ){
-          Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
-          QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
-        }
-        Node iso_n;
-        int res = QuantArith::isolate( d_vts_delta, msum, iso_n, n.getKind(), true );
-        if( res!=0 ){
-          Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n << ", res = " << res << std::endl;
-          int index = res==1 ? 0 : 1;
-          Node slv = iso_n[res==1 ? 1 : 0];
-          if( iso_n[index]!=d_vts_delta ){
-            if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){
-              slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) );
+    bool rew_inf = false;
+    bool rew_delta = false;
+    if( !d_vts_inf.isNull() && containsTerm( n, d_vts_inf ) ){
+      rew_inf = true;
+    }else if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
+      rew_delta = true;
+    }
+    if( rew_inf || rew_delta ){
+      if( n.getKind()==EQUAL ){
+        return d_false;
+      }else{
+        std::map< Node, Node > msum;
+        if( QuantArith::getMonomialSumLit( n, msum ) ){
+          if( Trace.isOn("quant-vts-debug") ){
+            Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
+            QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
+          }
+          Node vts_sym = rew_inf ? d_vts_inf : d_vts_delta;
+          Node iso_n;
+          int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true );
+          if( res!=0 ){
+            Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n << ", res = " << res << std::endl;
+            int index = res==1 ? 0 : 1;
+            Node slv = iso_n[res==1 ? 1 : 0];
+            if( iso_n[index]!=vts_sym ){
+              if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){
+                slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) );
+              }else{
+                return n;
+              }
+            }
+            Node nlit;
+            if( res==1 ){
+              if( rew_inf ){
+                nlit = d_true;
+              }else{
+                nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
+              }
             }else{
-              return n;
+              if( rew_inf ){
+                nlit = d_false;
+              }else{
+                nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
+              }
             }
+            Trace("quant-vts-debug") << "Return " << nlit << std::endl;
+            return nlit;
           }
-          Node nlit;
-          if( res==1 ){
-            nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
-          }else{
-            nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
-          }
-          Trace("quant-vts-debug") << "Return " << nlit << std::endl;
-          return nlit;
         }
       }
-      return n;
     }
+    return n;
   }else if( n.getKind()==FORALL ){
     //cannot traverse beneath quantifiers
-    std::vector< Node > delta;
-    delta.push_back( d_vts_delta );
-    std::vector< Node > delta_free;
-    delta_free.push_back( d_vts_delta_free );
-    n = n.substitute( delta.begin(), delta.end(), delta_free.begin(), delta_free.end() );
+    std::vector< Node > vars;
+    std::vector< Node > vars_free;
+    if( !d_vts_inf.isNull() ){
+      vars.push_back( d_vts_inf );
+      vars_free.push_back( d_vts_inf_free );
+    }
+    if( !d_vts_delta.isNull() ){
+      vars.push_back( d_vts_delta );
+      vars_free.push_back( d_vts_delta_free );
+    }
+    n = n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
     return n;
   }else{
     bool childChanged = false;
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 82ff67d41..cf0f005b9 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -9,8 +9,8 @@ AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
 if AUTOMAKE_1_11
 # old-style (pre-automake 1.12) test harness
 TESTS_ENVIRONMENT = \
-	$(LOG_COMPILER) \
-	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+  $(LOG_COMPILER) \
+  $(AM_LOG_FLAGS) $(LOG_FLAGS)
 endif
 
 MAKEFLAGS = -k
@@ -22,12 +22,12 @@ TESTS = commutative.sy \
         constant.sy \
         multi-fun-polynomial2.sy \
         unbdd_inv_gen_winf1.sy \
-	max.sy \
-	array_sum_2_5.sy \
-	parity-AIG-d0.sy \
-	twolets1.sy \
-	array_search_2.sy \        
-	hd-01-d1-prog.sy \
+        max.sy \
+        array_sum_2_5.sy \
+        parity-AIG-d0.sy \
+        twolets1.sy \
+        array_search_2.sy \        
+        hd-01-d1-prog.sy \
         icfp_28_10.sy \
         const-var-test.sy \
         no-syntax-test.sy \
@@ -44,23 +44,24 @@ TESTS = commutative.sy \
         no-syntax-test-bool.sy \
         inv-example.sy \
         uminus_one.sy \
-        sygus-dt.sy
+        sygus-dt.sy \
+        dt-no-syntax.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
-	max.smt2 \
-	sygus-uf.sl
+  max.smt2 \
+  sygus-uf.sl
 
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
-#	error.cvc
+# error.cvc
 #endif
 
 # disabled tests, yet distribute
 #EXTRA_DIST += \
-#	setofsets-disequal.smt2
+# setofsets-disequal.smt2
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
new file mode 100644
index 000000000..e0f8112ce
--- /dev/null
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --cegqi --no-dump-synth
+; EXPECT: unsat
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+
+(synth-fun f ((x Int)) List)
+
+(declare-var x Int)
+
+(constraint (= (f x) (cons (+ x 1) nil)))
+(check-synth)