From 672d1347c2daeddb8c434ea996f95ba555d22589 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 26 Sep 2018 18:13:29 -0500 Subject: [PATCH] Makes SyGuS parsing more robust in invariant problems (#2509) --- src/parser/smt2/Smt2.g | 54 +++++++++------- src/parser/smt2/smt2.cpp | 62 +++++++++++++------ src/parser/smt2/smt2.h | 28 ++++++--- test/regress/CMakeLists.txt | 1 + test/regress/Makefile.tests | 1 + .../regress0/sygus/inv-different-var-order.sy | 22 +++++++ 6 files changed, 115 insertions(+), 53 deletions(-) create mode 100644 test/regress/regress0/sygus/inv-different-var-order.sy diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 40166a641..ebf50283d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -724,31 +724,39 @@ sygusCommand [std::unique_ptr* cmd] PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 " "arguments."); } - //get primed variables - std::vector< Expr > primed[2]; - std::vector< Expr > all; - for( unsigned i=0; i<2; i++ ){ - PARSER_STATE->getSygusPrimedVars( primed[i], i==1 ); - all.insert( all.end(), primed[i].begin(), primed[i].end() ); - } - //make relevant terms - for( unsigned i=0; i<4; i++ ){ + // get variables (regular and their respective primed versions) + std::vector vars, primed_vars; + PARSER_STATE->getSygusInvVars(terms[0].getType(), vars, primed_vars); + // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post + for (unsigned i = 0; i < 4; ++i) + { Expr op = terms[i]; - Debug("parser-sygus") << "Make inv-constraint term #" << i << " : " << op << "..." << std::endl; - std::vector< Expr > children; - children.push_back( op ); - if( i==2 ){ - children.insert( children.end(), all.begin(), all.end() ); - }else{ - children.insert( children.end(), primed[0].begin(), primed[0].end() ); + Debug("parser-sygus") + << "Make inv-constraint term #" << i << " : " << op << " with type " + << op.getType() << "..." << std::endl; + std::vector children; + children.push_back(op); + // transition relation applied over both variable lists + if (i == 2) + { + children.insert(children.end(), vars.begin(), vars.end()); + children.insert( + children.end(), primed_vars.begin(), primed_vars.end()); } - terms[i] = EXPR_MANAGER->mkExpr( i==0 ? kind::APPLY_UF : kind::APPLY,children); - if( i==0 ){ - std::vector< Expr > children2; - children2.push_back( op ); - children2.insert(children2.end(), primed[1].begin(), - primed[1].end()); - terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY_UF,children2) ); + else + { + children.insert(children.end(), vars.begin(), vars.end()); + } + terms[i] = EXPR_MANAGER->mkExpr(i == 0 ? kind::APPLY_UF : kind::APPLY, + children); + // make application of Inv on primed variables + if (i == 0) + { + children.clear(); + children.push_back(op); + children.insert( + children.end(), primed_vars.begin(), primed_vars.end()); + terms.push_back(EXPR_MANAGER->mkExpr(kind::APPLY_UF, children)); } } //make constraints diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index dfeaca62b..c3a107bdf 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -629,20 +629,18 @@ void Smt2::includeFile(const std::string& filename) { } } -Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) { - Expr e = mkBoundVar(name, type); - d_sygusVars.push_back(e); - d_sygusVarPrimed[e] = false; - if( isPrimed ){ - d_sygusInvVars.push_back(e); - std::stringstream ss; - ss << name << "'"; - Expr ep = mkBoundVar(ss.str(), type); - d_sygusVars.push_back(ep); - d_sygusInvVars.push_back(ep); - d_sygusVarPrimed[ep] = true; +void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) +{ + if (!isPrimed) + { + d_sygusVars.push_back(mkBoundVar(name, type)); } - return e; +#ifdef CVC4_ASSERTIONS + else + { + d_sygusVarPrimed.push_back(mkBoundVar(name, type)); + } +#endif } void Smt2::mkSygusConstantsForType( const Type& type, std::vector& ops ) { @@ -1235,16 +1233,40 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt, return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); } -const void Smt2::getSygusPrimedVars( std::vector& vars, bool isPrimed ) { - for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++) +const void Smt2::getSygusInvVars(FunctionType t, + std::vector& vars, + std::vector& primed_vars) +{ + std::vector argTypes = t.getArgTypes(); + ExprManager* em = getExprManager(); + for (const Type& ti : argTypes) { - Expr v = d_sygusInvVars[i]; - std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v ); - if( it!=d_sygusVarPrimed.end() ){ - if( it->second==isPrimed ){ - vars.push_back( v ); + vars.push_back(em->mkBoundVar(ti)); + d_sygusVars.push_back(vars.back()); + std::stringstream ss; + ss << vars.back() << "'"; + primed_vars.push_back(em->mkBoundVar(ss.str(), ti)); + d_sygusVars.push_back(primed_vars.back()); +#ifdef CVC4_ASSERTIONS + bool find_new_declared_var = false; + for (const Expr& e : d_sygusVarPrimed) + { + if (e.getType() == ti) + { + d_sygusVarPrimed.erase( + std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e)); + find_new_declared_var = true; + break; } } + if (!find_new_declared_var) + { + ss.str(""); + ss << "warning: decleared primed variables do not match invariant's " + "type\n"; + warning(ss.str()); + } +#endif } } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 64a957402..80bd8df83 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -68,17 +68,16 @@ private: std::unordered_map operatorKindMap; std::pair d_lastNamedTerm; // for sygus - std::vector d_sygusVars, d_sygusInvVars, d_sygusConstraints, + std::vector d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, d_sygusFunSymbols; - std::map< Expr, bool > d_sygusVarPrimed; -protected: - Smt2(api::Solver* solver, - Input* input, - bool strictMode = false, - bool parseOnly = false); + protected: + Smt2(api::Solver* solver, + Input* input, + bool strictMode = false, + bool parseOnly = false); -public: + public: /** * Add theory symbols to the parser state. * @@ -228,7 +227,9 @@ public: return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); } - Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false); + void mkSygusVar(const std::string& name, + const Type& type, + bool isPrimed = false); void mkSygusConstantsForType( const Type& type, std::vector& ops ); @@ -287,7 +288,14 @@ public: const std::vector& getSygusVars() { return d_sygusVars; } - const void getSygusPrimedVars( std::vector& vars, bool isPrimed ); + /** retrieves the invariant variables (both regular and primed) + * + * To ensure that the variable list represent the correct argument type order + * the type of the invariant predicate is used during the variable retrieval + */ + const void getSygusInvVars(FunctionType t, + std::vector& vars, + std::vector& primed_vars); const void addSygusFunSymbol( Type t, Expr synth_fun ); const std::vector& getSygusFunSymbols() { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 35672d77a..5252954dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -826,6 +826,7 @@ set(regress_0_tests regress0/sygus/check-generic-red.sy regress0/sygus/const-var-test.sy regress0/sygus/dt-no-syntax.sy + regress0/sygus/inv-different-var-order.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-syntax-test-bool.sy diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c79f42078..08d0ca5bb 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -839,6 +839,7 @@ REG0_TESTS = \ regress0/sygus/const-var-test.sy \ regress0/sygus/dt-no-syntax.sy \ regress0/sygus/hd-05-d1-prog-nogrammar.sy \ + regress0/sygus/inv-different-var-order.sy \ regress0/sygus/let-ringer.sy \ regress0/sygus/let-simp.sy \ regress0/sygus/no-syntax-test-bool.sy \ diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy new file mode 100644 index 000000000..c3f43fc07 --- /dev/null +++ b/test/regress/regress0/sygus/inv-different-var-order.sy @@ -0,0 +1,22 @@ +; COMMAND-LINE: --sygus-out=status +;EXPECT: unsat +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var b Bool) +(declare-primed-var x Int) +(declare-primed-var y Int) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool +(and +(and (>= x 5) (<= x 9)) +(and (>= y 1) (<= y 3)) +) +) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool +(and +(and (= b! b) (= y! x)) +(ite b (= x! (+ x 10)) (= x! (+ x 12))) +) +) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool true) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth) \ No newline at end of file -- 2.30.2