From 6d82ee2d1f84065ff4a86f688a3b671b85728f80 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 20 Jul 2017 10:35:38 +0200 Subject: [PATCH] Fix a few bugs related to sygus. --- src/parser/smt2/Smt2.g | 62 ++++++++++++------- .../quantifiers/ce_guided_instantiation.cpp | 4 +- .../quantifiers/ce_guided_single_inv.cpp | 2 + .../quantifiers/ce_guided_single_inv_sol.cpp | 6 +- test/regress/regress0/sygus/Makefile.am | 3 +- test/regress/regress0/sygus/parse-bv-let.sy | 20 ++++++ 6 files changed, 69 insertions(+), 28 deletions(-) create mode 100644 test/regress/regress0/sygus/parse-bv-let.sy diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88709c29a..a2c859055 100644 --- 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 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 >::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 a635568fe..cb8e6f200 100644 --- 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 a8dcd5887..f25d42284 100644 --- 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 9e65be202..1eafe1a93 100644 --- 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 0786c3f31..c22f64b93 100644 --- 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 index 000000000..88ddcf139 --- /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) -- 2.30.2