diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 85 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/issue4790-dtd.sy | 23 |
3 files changed, 70 insertions, 39 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index ce13b6744..61916ce4c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -47,11 +47,18 @@ bool UnifContextIo::updateContext(SygusUnifIo* sui, Assert(d_vals.size() == vals.size()); bool changed = false; Node poln = pol ? d_true : d_false; - for (unsigned i = 0; i < vals.size(); i++) + for (size_t i = 0, vsize = vals.size(); i < vsize; i++) { - if (vals[i] != poln) + Node v = vals[i]; + if (v.isNull()) + { + // nothing can be inferred if the evaluation is unknown, e.g. if using + // partial functions. + continue; + } + if (v != poln) { - if (d_vals[i] == d_true) + if (v == d_true) { d_vals[i] = d_false; changed = true; @@ -571,8 +578,6 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) eec->evaluateVec(bv, base_results); // get the results for each slave enumerator std::map<Node, std::vector<Node>> srmap; - Evaluator* ev = d_tds->getEvaluator(); - bool tryEval = options::sygusEvalOpt(); for (const Node& xs : ei.d_enum_slave) { Assert(srmap.find(xs) == srmap.end()); @@ -580,34 +585,15 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) Node templ = eiv.d_template; if (!templ.isNull()) { - TNode templ_var = eiv.d_template_arg; - std::vector<Node> args; - args.push_back(templ_var); + // Substitute and evaluate, notice that the template skeleton may + // involve the sygus variables e.g. (>= x _) where x is a sygus + // variable, hence we must compute the substituted template before + // calling the evaluator. + TNode targ = eiv.d_template_arg; + TNode tbv = bv; + Node stempl = templ.substitute(targ, tbv); std::vector<Node> sresults; - for (const Node& res : base_results) - { - TNode tres = res; - Node sres; - // It may not be constant, e.g. if we involve a partial operator - // like datatype selectors. In this case, we avoid using the evaluator, - // which expects a constant substitution. - if (tres.isConst()) - { - std::vector<Node> vals; - vals.push_back(tres); - if (tryEval) - { - sres = ev->eval(templ, args, vals); - } - } - if (sres.isNull()) - { - // fall back on rewriter - sres = templ.substitute(templ_var, tres); - sres = Rewriter::rewrite(sres); - } - sresults.push_back(sres); - } + eec->evaluateVec(stempl, sresults); srmap[xs] = sresults; } else @@ -658,6 +644,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> results; std::map<Node, bool> cond_vals; std::map<Node, std::vector<Node>>::iterator itsr = srmap.find(xs); + Trace("sygus-sui-debug") << " {" << itsr->second << "} "; Assert(itsr != srmap.end()); for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { @@ -1003,6 +990,8 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results) { + Trace("sygus-sui-debug") << "Add enum value " << this << " " << v << " : " + << results << std::endl; // should not have been enumerated before Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end()); d_enum_val_to_index[v] = d_enum_vals.size(); @@ -1080,7 +1069,7 @@ Node SygusUnifIo::constructSol( { ret_dt = constructBestSolvedTerm(e, subsumed_by); indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "return PBE: success : conditionally solved" + Trace("sygus-sui-dt") << "return PBE: success : conditionally solved " << d_tds->sygusToBuiltin(ret_dt) << std::endl; } else @@ -1442,12 +1431,30 @@ Node SygusUnifIo::constructSol( } else { - // TODO (#1250) : degenerate case where children have different - // types? - indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " - "cannot find a distinguishable condition" - << std::endl; + // if the child types are different, it could still make a + // difference to recurse, for instance see issue #4790. + bool childTypesEqual = ce.getType() == etn; + if (!childTypesEqual) + { + if (!ecache_child.d_enum_vals.empty()) + { + // take arbitrary + rec_c = constructBestConditional(ce, ecache_child.d_enum_vals); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") + << "PBE: ITE strategy : choose arbitrary conditional due " + "to disequal child types " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + } + if (rec_c.isNull()) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") + << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition, childTypesEqual=" + << childTypesEqual << std::endl; + } } if (!rec_c.isNull()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0b0da8e93..a21b76b0c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1043,6 +1043,7 @@ set(regress_0_tests regress0/sygus/issue3624.sy regress0/sygus/issue3645-grammar-sets.smt2 regress0/sygus/issue4383-cache-fv-id.sy + regress0/sygus/issue4790-dtd.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy regress0/sygus/no-logic.sy diff --git a/test/regress/regress0/sygus/issue4790-dtd.sy b/test/regress/regress0/sygus/issue4790-dtd.sy new file mode 100644 index 000000000..55f4723ec --- /dev/null +++ b/test/regress/regress0/sygus/issue4790-dtd.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic NIA) +(synth-fun patternGen ((i Int)) Int +((ITE Int) (CONST Int) (I Int) (B Bool)) +( (ITE Int ( + (ite (<= i CONST) I I) + + )) + (CONST Int (0)) + (I Int (i 1 + (+ I I) (- I I) (* I I) + )) + (B Bool ( + (<= I I) + )) +) +) +(declare-var i Int) +(constraint (= (patternGen 0) 1)) +(constraint (= (patternGen 1) 1)) +(constraint (= (patternGen 2) 1)) +(check-synth) |