Fix a few bugs related to sygus.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 88709c29a7782a226e2adb5e859b261af0c6ed44..a2c859055319407abe3068d2fadaa2c4ce3d9e24 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -898,7 +898,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
         sgt.d_gterm_type = SygusGTerm::gterm_op;
         sgt.d_expr = EXPR_MANAGER->operatorOf(k);
       }
-     | LET_TOK LPAREN_TOK { 
+     | SYGUS_LET_TOK LPAREN_TOK { 
          sgt.d_name = std::string("let");
          sgt.d_gterm_type = SygusGTerm::gterm_let;
          PARSER_STATE->pushScope(true);
@@ -1803,7 +1803,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Type type;
   std::string s;
   bool isBuiltinOperator = false;
-  bool readLetSort = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
 }
@@ -2005,27 +2004,41 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
       }
     )
-  | /* a let binding */
-    LPAREN_TOK LET_TOK LPAREN_TOK
-    { PARSER_STATE->pushScope(true); }
-    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-      (term[expr, f2] | sortSymbol[type,CHECK_DECLARED]
-       { readLetSort = true; } term[expr, f2]
-      )
-      RPAREN_TOK
-      // this is a parallel let, so we have to save up all the contributions
-      // of the let and define them only later on
-      { if( !PARSER_STATE->sygus() && readLetSort ){
-          PARSER_STATE->parseError("Bad syntax for let term.");
-        }else if(names.count(name) == 1) {
-          std::stringstream ss;
-          ss << "warning: symbol `" << name << "' bound multiple times by let;"
-             << " the last binding will be used, shadowing earlier ones";
-          PARSER_STATE->warning(ss.str());
-        } else {
-          names.insert(name);
-        }
-        binders.push_back(std::make_pair(name, expr)); } )+
+  | /* a let or sygus let binding */
+    LPAREN_TOK ( 
+      LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ |
+      SYGUS_LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        sortSymbol[type,CHECK_DECLARED]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ )
     { // now implement these bindings
       for(std::vector< std::pair<std::string, Expr> >::iterator
             i = binders.begin(); i != binders.end(); ++i) {
@@ -3004,7 +3017,8 @@ EXIT_TOK : 'exit';
 RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
-LET_TOK : 'let';
+LET_TOK : { !PARSER_STATE->sygus() }? 'let';
+SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let';
 ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index a635568fe1cc7022f3cf2d77e68666d80a55e5ff..cb8e6f200775c6a0e21e53aa3c61c01ac31e67e3 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -924,7 +924,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       if( d_last_inst_si ){
         Assert( d_conj->getCegConjectureSingleInv() != NULL );
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
-        sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+        if( !sol.isNull() ){
+          sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+        }
       }else{
         Node cprog = d_conj->getCandidate( i );
         if( !d_conj->d_cinfo[cprog].d_inst.empty() ){

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index a8dcd588791f00732e8073b9b9e07a05b80795ca..f25d4228482669b6eda58aeaf8142ed4cf4eddef 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -888,6 +888,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   Node sol;
   if( reconstructed==1 ){
     sol = d_sygus_solution;
+  }else if( reconstructed==-1 ){
+    return Node::null();
   }else{
     sol = d_solution;
   }

diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 9e65be20242f3600e856713a1f561bfb1408225d..1eafe1a9316a7e7b9a4d9f660c4c144785c2f2d7 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -714,8 +714,10 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
       }
     }while( !active.empty() );
 
-    //if solution is null, we ran out of elements, return the original solution
-    return sol;
+    // we ran out of elements, return null
+    reconstructed = -1;
+    Warning() << CommandFailure("Cannot get synth function: reconstruction to syntax failed.");
+    return Node::null(); // return sol;
   }
 }
 

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 0786c3f31f41b24d4ae263c1b9f00b68ceb43a4d..c22f64b93cc9149ab176d11e64c29fd3f07a8102 100644 (file)
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -61,7 +61,8 @@ TESTS = commutative.sy \
         strings-trivial.sy \
         General_plus10.sy \
         qe.sy \
-        cggmp.sy
+        cggmp.sy \
+        parse-bv-let.sy
 
 
 # sygus tests currently taking too long for make regress

diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy
new file mode 100644 (file)
index 0000000..88ddcf1
--- /dev/null
+++ b/test/regress/regress0/sygus/parse-bv-let.sy
@@ -0,0 +1,20 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth
+(set-logic BV)
+
+(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
+  (let ((modulo-shift (BitVec 32) (bvand bit #x0000001f)))
+        (bvand modulo-shift x)))
+
+(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
+    ((Start (BitVec 32) (
+                         (Constant (BitVec 32))
+                         (Variable (BitVec 32))
+                        (bvneg  Start) (bvnot  Start) (bvadd  Start Start) (bvand  Start Start) (bvlshr Start Start) (bvmul  Start Start) (bvor   Start Start) (bvshl  Start Start)
+                         ))))
+
+(declare-var x   (BitVec 32))
+(declare-var bit (BitVec 32))
+(constraint (= (btr x bit) #b00000000000000000000000000000000))
+
+(check-synth)