From d31b7cb6e695d6489134956408858a94d2308178 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Oct 2019 15:01:05 -0500 Subject: [PATCH] Support UF in default sygus grammars (#3319) --- .../sygus/ce_guided_single_inv.cpp | 5 +- src/theory/quantifiers/sygus/sygus_abduct.cpp | 28 +++++----- .../quantifiers/sygus/sygus_grammar_cons.cpp | 56 +++++++++++++++++-- .../sygus/transition_inference.cpp | 24 +++++--- .../quantifiers/sygus/transition_inference.h | 8 ++- test/regress/CMakeLists.txt | 2 + test/regress/regress1/sygus/ho-sygus.sy | 8 +++ test/regress/regress1/sygus/uf-abduct.smt2 | 8 +++ 8 files changed, 107 insertions(+), 32 deletions(-) create mode 100644 test/regress/regress1/sygus/ho-sygus.sy create mode 100644 test/regress/regress1/sygus/uf-abduct.smt2 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 96c79e69d..47a1f6142 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -143,14 +143,15 @@ void CegSingleInv::initialize(Node q) } // if we are doing invariant templates, then construct the template Trace("cegqi-si") << "- Do transition inference..." << std::endl; - d_ti[q].process(qq); + d_ti[q].process(qq, q[0][0]); Trace("cegqi-inv") << std::endl; Node prog = d_ti[q].getFunction(); - if (prog.isNull()) + if (!d_ti[q].isComplete()) { // the invariant could not be inferred return; } + Assert(prog == q[0][0]); NodeManager* nm = NodeManager::currentNM(); // map the program back via non-single invocation map std::vector prog_templ_vars; diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 047a78d11..529ef037f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -55,20 +55,20 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, for (const Node& s : symset) { TypeNode tn = s.getType(); - if (tn.isFirstClass()) - { - std::stringstream ss; - ss << s; - Node var = nm->mkBoundVar(tn); - syms.push_back(s); - vars.push_back(var); - Node vlv = nm->mkBoundVar(ss.str(), tn); - varlist.push_back(vlv); - varlistTypes.push_back(tn); - // set that this variable encodes the term s - SygusVarToTermAttribute sta; - vlv.setAttribute(sta, s); - } + // Notice that we allow for non-first class (e.g. function) variables here. + // This is applicable to the case where we are doing get-abduct in a logic + // with UF. + std::stringstream ss; + ss << s; + Node var = nm->mkBoundVar(tn); + syms.push_back(s); + vars.push_back(var); + Node vlv = nm->mkBoundVar(ss.str(), tn); + varlist.push_back(vlv); + varlistTypes.push_back(tn); + // set that this variable encodes the term s + SygusVarToTermAttribute sta; + vlv.setAttribute(sta, s); } // make the sygus variable list Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index ba55db132..43696bff0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" @@ -428,6 +429,15 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode intType = NodeManager::currentNM()->integerType(); collectSygusGrammarTypesFor(intType,types); } + else if (range.isFunction()) + { + std::vector atypes = range.getArgTypes(); + for (unsigned i = 0, ntypes = atypes.size(); i < ntypes; i++) + { + collectSygusGrammarTypesFor(atypes[i], types); + } + collectSygusGrammarTypesFor(range.getRangeType(), types); + } } } } @@ -533,18 +543,42 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; Type unres_t = unres_types[i]; //add variables - for (unsigned j = 0, size_j = sygus_vars.size(); j < size_j; ++j) + for (const Node& sv : sygus_vars) { - if( sygus_vars[j].getType()==types[i] ){ + TypeNode svt = sv.getType(); + if (svt == types[i]) + { std::stringstream ss; - ss << sygus_vars[j]; - Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl; - ops[i].push_back( sygus_vars[j].toExpr() ); + ss << sv; + Trace("sygus-grammar-def") + << "...add for variable " << ss.str() << std::endl; + ops[i].push_back(sv.toExpr()); cnames[i].push_back(ss.str()); cargs[i].push_back(std::vector()); pcs[i].push_back(nullptr); weights[i].push_back(-1); } + else if (svt.isFunction() && svt.getRangeType() == types[i]) + { + // We add an APPLY_UF for all function whose return type is this type + // whose argument types are the other sygus types we are constructing. + std::vector argTypes = svt.getArgTypes(); + std::vector stypes; + for (unsigned k = 0, ntypes = argTypes.size(); k < ntypes; k++) + { + unsigned index = + std::distance(types.begin(), + std::find(types.begin(), types.end(), argTypes[k])); + stypes.push_back(unres_types[index]); + } + std::stringstream ss; + ss << "apply_" << sv; + ops[i].push_back(sv.toExpr()); + cnames[i].push_back(ss.str()); + cargs[i].push_back(stypes); + pcs[i].push_back(nullptr); + weights[i].push_back(-1); + } } //add constants std::vector< Node > consts; @@ -812,7 +846,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( pcs[i].push_back(nullptr); weights[i].push_back(-1); } - }else{ + } + else if (types[i].isSort() || types[i].isFunction()) + { + // do nothing + } + else + { Warning() << "Warning: No implementation for default Sygus grammar of type " << types[i] << std::endl; @@ -903,6 +943,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // add predicates for types for (unsigned i = 0, size = types.size(); i < size; ++i) { + if (!types[i].isFirstClass()) + { + continue; + } Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; //add equality per type Kind k = EQUAL; diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 88ffe84b2..7db3f50f8 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -186,6 +186,13 @@ void TransitionInference::getConstantSubstitution( } } +void TransitionInference::process(Node n, Node f) +{ + // set the function + d_func = f; + process(n); +} + void TransitionInference::process(Node n) { NodeManager* nm = NodeManager::currentNM(); @@ -404,10 +411,14 @@ bool TransitionInference::processDisjunct( // if another part mentions UF or a free variable, then fail bool lit_pol = n.getKind() != NOT; Node lit = n.getKind() == NOT ? n[0] : n; - if (lit.getKind() == APPLY_UF) + // is it an application of the function-to-synthesize? Yes if we haven't + // encountered a function or if it matches the existing d_func. + if (lit.getKind() == APPLY_UF + && (d_func.isNull() || lit.getOperator() == d_func)) { Node op = lit.getOperator(); - if (d_func.isNull()) + // initialize the variables + if (d_vars.empty()) { d_func = op; Trace("cegqi-inv-debug") << "Use " << op << " with args "; @@ -420,13 +431,8 @@ bool TransitionInference::processDisjunct( } Trace("cegqi-inv-debug") << std::endl; } - if (op != d_func) - { - Trace("cegqi-inv-debug") - << "...failed, free function : " << n << std::endl; - return false; - } - else if (topLevel) + Assert(!d_func.isNull()); + if (topLevel) { if (terms.find(lit_pol) == terms.end()) { diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h index b4fb220db..8939cf6da 100644 --- a/src/theory/quantifiers/sygus/transition_inference.h +++ b/src/theory/quantifiers/sygus/transition_inference.h @@ -123,7 +123,13 @@ class TransitionInference * The node n should be the inner body of the negated synthesis conjecture, * prior to generating the deep embedding. That is, given: * forall f. ~forall x. P( f, x ), - * this method expects n to be P( f, x ). + * this method expects n to be P( f, x ), and the argument f to be the + * function f above. + */ + void process(Node n, Node f); + /** + * Same as above, without specifying f. This will try to infer a function f + * based on the body of n. */ void process(Node n); /** diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8dba70f91..25637acdc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1690,6 +1690,7 @@ set(regress_1_tests regress1/sygus/hd-01-d1-prog.sy regress1/sygus/hd-19-d1-prog-dup-op.sy regress1/sygus/hd-sdiv.sy + regress1/sygus/ho-sygus.sy regress1/sygus/icfp_14.12-flip-args.sy regress1/sygus/icfp_14.12.sy regress1/sygus/icfp_14_12_diff_types.sy @@ -1753,6 +1754,7 @@ set(regress_1_tests regress1/sygus/trivial-stream.sy regress1/sygus/twolets1.sy regress1/sygus/twolets2-orig.sy + regress1/sygus/uf-abduct.smt2 regress1/sygus/unbdd_inv_gen_ex7.sy regress1/sygus/unbdd_inv_gen_winf1.sy regress1/sygus/univ_2-long-repeat.sy diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy new file mode 100644 index 000000000..c66485817 --- /dev/null +++ b/test/regress/regress1/sygus/ho-sygus.sy @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --uf-ho +(set-logic ALL) +(synth-fun f ((y (-> Int Int)) (z Int)) Int) +(declare-var z (-> Int Int)) +(constraint (= (f z 0) (z 1))) +(constraint (= (f z 1) (z 2))) +(check-synth) diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2 new file mode 100644 index 000000000..690e57290 --- /dev/null +++ b/test/regress/regress1/sygus/uf-abduct.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --produce-abducts --uf-ho +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic UFLIA) +(declare-fun f (Int) Int) +(declare-fun a () Int) +(assert (and (<= 0 a) (< a 4))) +(get-abduct ensureF (or (> (f 0) 0) (> (f 1) 0) (> (f 2) 0) (> (f 3) 0))) -- 2.30.2