From 78373c7f5fe93b7e8bbea10e3924f24d25a618ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Oct 2017 14:52:31 -0500 Subject: [PATCH] Make Sygus conjectures higher-order (#1244) * Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks. * Minor fix * Fix bug in Node::hasBoundVar for non-ground operators. * Add regression. * Address review. * Apply clang format. --- src/expr/node.cpp | 3 + src/parser/smt2/Smt2.g | 1 + src/parser/smt2/smt2.cpp | 14 +- src/smt/smt_engine.cpp | 7 +- .../quantifiers/ce_guided_conjecture.cpp | 9 +- .../quantifiers/ce_guided_single_inv.cpp | 5 +- .../quantifiers/quantifiers_attributes.cpp | 9 +- src/theory/quantifiers/sygus_grammar_cons.cpp | 8 +- src/theory/quantifiers/term_util.h | 5 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- test/regress/regress1/sygus/MPwL_d1s3.sy | 151 ++++++++++++++++++ test/regress/regress1/sygus/Makefile.am | 3 +- 12 files changed, 187 insertions(+), 30 deletions(-) create mode 100644 test/regress/regress1/sygus/MPwL_d1s3.sy diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 75e37151a..126feadd8 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -111,6 +111,9 @@ bool NodeTemplate::hasBoundVar() { hasBv = (*i).hasBoundVar(); } } + if (!hasBv && hasOperator()) { + hasBv = getOperator().hasBoundVar(); + } setAttribute(HasBoundVarAttr(), hasBv); setAttribute(HasBoundVarComputedAttr(), true); Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 05faf040e..4d39c7635 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -626,6 +626,7 @@ sygusCommand [std::unique_ptr* cmd] synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); // we add a declare function command here // this is the single unmuted command in the sequence generated by this smt2 command + // TODO (as part of #1170) : make this a standard command. seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bc9f2a06f..0fc3678c7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1081,13 +1081,17 @@ const void Smt2::getSygusPrimedVars( std::vector& vars, bool isPrimed ) { } const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ - //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute + // When constructing the synthesis conjecture, we quantify on the + // (higher-order) bound variable synth_fun. + d_sygusFunSymbols.push_back(synth_fun); + + // Variable "sfproxy" carries the type, which may be a SyGuS datatype + // that corresponds to syntactic restrictions. Expr sym = mkBoundVar("sfproxy", t); - d_sygusFunSymbols.push_back(sym); - std::vector< Expr > attr_value; - attr_value.push_back( synth_fun ); - Command* cattr = new SetUserAttributeCommand("sygus-synth-fun", sym, attr_value); + attr_value.push_back(sym); + Command* cattr = + new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value); cattr->setMuted(true); preemptCommand(cattr); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4bcb78867..e32d8913d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4574,12 +4574,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; quantifiers::SingleInvocationPartition sip; std::vector< Node > funcs; - for( unsigned i=0; igetTemplate(sf); + Node templ = d_ceg_si->getTemplate(v); if( !templ.isNull() ){ - templates[sf] = templ; - templates_arg[sf] = d_ceg_si->getTemplateArg(sf); + templates[v] = templ; + templates_arg[v] = d_ceg_si->getTemplateArg(v); } } } @@ -562,7 +561,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation status = 1; //check if there was a template - Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute()); + Node sf = d_quant[0][i]; Node templ = d_ceg_si->getTemplate( sf ); if( !templ.isNull() ){ Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index bf09c83f7..3349492a2 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -126,8 +126,7 @@ void CegConjectureSingleInv::initialize( Node q ) { std::vector< Node > progs; std::map< Node, std::vector< Node > > prog_vars; for( unsigned i=0; i vars; Node s; if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index ac3fb85d1..c9a7f07ab 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -51,11 +51,12 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set sygus " << n << std::endl; SygusAttribute ca; n.setAttribute( ca, true ); - }else if( attr=="sygus-synth-fun" ){ + } else if (attr == "sygus-synth-grammar") { Assert( node_values.size()==1 ); - Trace("quant-attr-debug") << "Set sygus synth fun " << n << " to " << node_values[0] << std::endl; - SygusSynthFunAttribute ssfa; - n.setAttribute( ssfa, node_values[0] ); + Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to " + << node_values[0] << std::endl; + SygusSynthGrammarAttribute ssg; + n.setAttribute(ssg, node_values[0]); }else if( attr=="sygus-synth-fun-var-list" ){ Assert( node_values.size()==1 ); Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to " << node_values[0] << std::endl; diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index 2eb541e66..6152417a5 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -83,9 +83,11 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::vector< Node > ebvl; Node qbody_subs = q[1]; for( unsigned i=0; i SygusProxyAttribute; // attribute for associating a synthesis function with a first order variable -struct SygusSynthFunAttributeId {}; -typedef expr::Attribute SygusSynthFunAttribute; +struct SygusSynthGrammarAttributeId {}; +typedef expr::Attribute + SygusSynthGrammarAttribute; // attribute for associating a variable list with a synth fun struct SygusSynthFunVarListAttributeId {}; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 855cdb911..66e05b1cd 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -44,7 +44,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); - out.handleUserAttribute( "sygus-synth-fun", this ); + out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy new file mode 100644 index 000000000..b5b848848 --- /dev/null +++ b/test/regress/regress1/sygus/MPwL_d1s3.sy @@ -0,0 +1,151 @@ +; EXPECT: unsat +; COMMAND-LINE: --no-dump-synth +(set-logic LIA) + +(define-fun get-y ((currPoint Int)) Int +(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9)))))))))) + +(define-fun get-x ((currPoint Int)) Int + (- currPoint (* (get-y currPoint) 10))) +(define-fun interpret-move (( currPoint Int ) ( move Int)) Int +(ite (= move 0) currPoint +(ite (= move 1) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 2) (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10)) currPoint (+ currPoint 1)) +(ite (= move 3) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +(ite (= move 4) (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10)) currPoint (+ currPoint -1)) +currPoint)))))) + +(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int +(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 1) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +currPoint))) + +(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int +(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10)) +(ite (= move 1) currPoint +(ite (= move 2) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10)) +currPoint)))) + +(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool + (or (= (interpret-move-obstacle-0 start 0) end) + (or (= (interpret-move-obstacle-0 start 1) end) false))) + +(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool + (or (= (interpret-move-obstacle-1 start 0) end) + (or (= (interpret-move-obstacle-1 start 1) end) + (or (= (interpret-move-obstacle-1 start 2) end) false)))) + +(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int + (ite (= (interpret-move-obstacle-0 start 0) end) 0 + (ite (= (interpret-move-obstacle-0 start 1) end) 1 -1))) + +(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int + (ite (= (interpret-move-obstacle-1 start 0) end) 0 + (ite (= (interpret-move-obstacle-1 start 1) end) 1 + (ite (= (interpret-move-obstacle-1 start 2) end) 2 -1)))) + +(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool + (and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true))))) + +(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool + (= 1 + (ite (= move 0) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 1) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 2) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 3) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) + (ite (= move 4) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0))))))) + +(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool + (= 1 + (ite (= move 0) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 1) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 2) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 3) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) + (ite (= move 4) + (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0) + (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0) + (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0))))))) + +(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool + (and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true))) + +(define-fun no-overlaps-one-step ((currPoint Int) (move Int) (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool + (no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1))) + + + +(declare-var o0-1 Int) +(declare-var o0-2 Int) +(declare-var o0-3 Int) +(declare-var o1-1 Int) +(declare-var o1-2 Int) +(declare-var o1-3 Int) + +(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int + ((Start Int ( + MoveId + (ite StartBool Start Start))) + (MoveId Int (0 + 1 + 2 + 3 + 4 + )) + (CondInt Int ( + (get-y currPoint) ;y coord + (get-x currPoint) ;x coord + (get-y o0) + (get-x o0) + (get-y o1) + (get-x o1) + (+ CondInt CondInt) + (- CondInt CondInt) + -1 + 0 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 + )) + (StartBool Bool ((and StartBool StartBool) + (or StartBool StartBool) + (not StartBool) + (<= CondInt CondInt) + (= CondInt CondInt) + (>= CondInt CondInt))))) + + (constraint (let ((pos0 Int 0)) (let ((mov0 Int (move pos0 99 98))) (let ((pos1 Int (interpret-move pos0 mov0))) (let ((mov1 Int (move pos1 o0-1 o1-1))) (let ((pos2 Int (interpret-move pos1 mov1))) (let ((mov2 Int (move pos2 o0-2 o1-2))) (let ((pos3 Int (interpret-move pos2 mov2))) + (or + (and + (= pos3 30) + (and (no-overlaps-one-step pos0 mov0 99 o0-1 98 o1-1) (and (no-overlaps-one-step pos1 mov1 o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step pos2 mov2 o0-2 o0-3 o1-2 o1-3) true)))) + (not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true)))))))))))))))) + +(check-synth) diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am index ed8755236..17b8e8872 100644 --- a/test/regress/regress1/sygus/Makefile.am +++ b/test/regress/regress1/sygus/Makefile.am @@ -26,7 +26,8 @@ TESTS = \ unbdd_inv_gen_ex7.sy \ icfp_easy_mt_ite.sy \ three.sy \ - nia-max-square.sy + nia-max-square.sy \ + MPwL_d1s3.sy EXTRA_DIST = $(TESTS) -- 2.30.2