Avoid naming conflicts in sygus, refactor. Add missing regression. Detect Start...

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ffa2994fcd868c5e5def8c1c7d20990707029cb8..11ddf2a155e6426062e4d96e410ffee26aae5e1f 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -503,6 +503,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   Type sygus_ret;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
   std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
+  int startIndex = -1;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -606,26 +607,34 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     sortSymbol[range,CHECK_DECLARED]
     ( LPAREN_TOK
     ( LPAREN_TOK
-      symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); }
+      symbol[name,CHECK_NONE,SYM_VARIABLE] 
       sortSymbol[t,CHECK_DECLARED]
       { std::stringstream ss;
         ss << fun << "_" << name;
+        if( name=="Start" ){
+          startIndex = datatypes.size();
+        }
         std::string dname = ss.str();
         PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym);
+        Type unres_t;
         if(!PARSER_STATE->isUnresolvedType(dname)) {
           // if not unresolved, must be undeclared
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
+          unres_t = PARSER_STATE->mkUnresolvedType(dname);
+        }else{
+          unres_t = PARSER_STATE->getSort(dname);
         }
-        Type unres_t = PARSER_STATE->mkUnresolvedType(dname);
         sygus_to_builtin[unres_t] = t;
         sygus_dt_index = datatypes.size()-1;
-        Debug("parser-sygus") << "Read sygus grammar " << name << " under function " << fun << "..." << std::endl;
+        Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl;
+        Debug("parser-sygus") << "    type to resolve " << unres_t << std::endl;
+        Debug("parser-sygus") << "    builtin type " << t << std::endl;
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
       LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
                             sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sygus_ret, -1]+ RPAREN_TOK
-      RPAREN_TOK { PARSER_STATE->popScope(); }
+      RPAREN_TOK 
     )+
     RPAREN_TOK { read_syntax = true; }
     )?
@@ -634,10 +643,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         //create the default grammar
         PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars );
       }else{
+        //swap index if necessary
         Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
-        //make unresolved types to recognize 
         for( unsigned i=0; i<datatypes.size(); i++ ){
-          PARSER_STATE->mkUnresolvedType(datatypes[i].getName());
+          Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl;
         }
         for( unsigned i=0; i<datatypes.size(); i++ ){
           Debug("parser-sygus") << "...make " << datatypes[i].getName() << " with builtin sort " << sorts[i] << std::endl;
@@ -647,6 +656,22 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false );
           PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin );
         }
+        //only care about datatypes/sorts/ops past here
+        if( startIndex>0 ){
+         // PARSER_STATE->swapSygusStart( startIndex, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
+          CVC4::Datatype tmp_dt = datatypes[0];
+          Type tmp_sort = sorts[0];
+          std::vector< Expr > tmp_ops;
+          tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
+          datatypes[0] = datatypes[startIndex];
+          sorts[0] = sorts[startIndex];
+          ops[0].clear();
+          ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() );
+          datatypes[startIndex] = tmp_dt;
+          sorts[startIndex] = tmp_sort;
+          ops[startIndex].clear();
+          ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() );
+        }
       }
       PARSER_STATE->popScope();
       Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl;
@@ -798,7 +823,7 @@ sygusGTerm[int index,
           Expr v = PARSER_STATE->mkBoundVar(sname,t); 
           let_vars.push_back( v ); 
           std::stringstream ss;
-          ss << datatypes[index].getName() << "_let_var_" << let_vars.size();
+          ss << datatypes[index].getName() << "_" << ops[index].size() << "_lv_" << let_vars.size();
           sub_dname = ss.str();
           PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
           sub_dt_index = datatypes.size()-1;
@@ -860,7 +885,7 @@ sygusGTerm[int index,
       //add datatype definition for argument
       count++;
       std::stringstream ss;
-      ss << datatypes[index].getName() << "_" << name << "_arg_" << count;
+      ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
       sub_dname = ss.str();
       PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
       sub_dt_index = datatypes.size()-1;
@@ -875,7 +900,7 @@ sygusGTerm[int index,
         //add next datatype definition for argument
         count++;
         std::stringstream ss;
-        ss << datatypes[index].getName() << "_" << name << "_arg_" << count;
+        ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count;
         sub_dname = ss.str();
         PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
         sub_dt_index = datatypes.size()-1;

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 17bedf1154faf7114c3a9b78dd47ede5cd2a6117..47022da3ea0dc18937a605cf80b4610b04f37871 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -653,7 +653,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
   unresolved_gterm_sym.pop_back();
   return true;
 }
-
+  
 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
                                     std::vector< std::vector<CVC4::Expr> >& ops,
@@ -927,6 +927,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
         Expr v = mkBoundVar(ss.str(), bt);
         let_args.push_back( v );
         fsorts.push_back( bt );
+        Debug("parser-sygus") << ": var " << i << " " << v << " with type " << bt << " from " << cargs[i][j] << std::endl;
       }
       //make the let_body
       std::vector< Expr > children;

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 50f755fefb160cd6b3d15c05a8012984049f68af..dbef0494a1329e6c96d55065597527a2be333b8e 100644 (file)
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -37,7 +37,8 @@ TESTS = commutative.sy \
         let-ringer.sy \
         let-simp.sy \
         tl-type.sy \
-        dup-op.sy
+        dup-op.sy \
+        nflat-fwd.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \

diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
new file mode 100644 (file)
index 0000000..dbf4159
--- /dev/null
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ Con Con) (+ Start Start) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) (* 2 x)))
+(check-synth)
+

diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
new file mode 100644 (file)
index 0000000..0f9d462
--- /dev/null
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) (* 2 x)))
+(check-synth)
+