diff options
| -rw-r--r-- | src/options/arith_options.toml | 1 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
| -rw-r--r-- | src/smt/set_defaults.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 65 |
4 files changed, 42 insertions, 38 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index da3a8dc88..fad1b3dcd 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -460,7 +460,6 @@ header = "options/arith_options.h" long = "nl-ext-tplanes" type = "bool" default = "false" - read_only = true help = "use non-terminating tangent plane strategy for non-linear incremental linearization solver" [[option]] diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 724a2ef2b..2a5faf9f7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1311,14 +1311,6 @@ header = "options/quantifiers_options.h" help = "enumerate a stream of solutions instead of terminating after the first one" [[option]] - name = "sygusVerifySubcall" - category = "regular" - long = "sygus-verify-subcall" - type = "bool" - default = "true" - help = "use separate copy of the SMT solver for verification lemmas in sygus" - -[[option]] name = "sygusExtRew" category = "regular" long = "sygus-ext-rew" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 468e246c4..d9123e7f4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1117,6 +1117,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { options::cegqiPreRegInst.set(true); } + // use tangent planes by default, since we want to put effort into + // the verification step for sygus queries with non-linear arithmetic + if (!options::nlExtTangentPlanes.wasSetByUser()) + { + options::nlExtTangentPlanes.set(true); + } // not compatible with proofs if (options::proofNew()) { diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0531d859d..c65ac9e65 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -617,26 +617,25 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) // either this conjecture does not have a solution, or candidate_values // is a solution for this conjecture. lem = nm->mkNode(OR, d_quant.negate(), query); - if (options::sygusVerifySubcall()) - { - Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; + Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - Result r = - checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); - Trace("sygus-engine") << " ...got " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() == Result::SAT) + Result r = + checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); + Trace("sygus-engine") << " ...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + if (Trace.isOn("sygus-engine")) { - if (Trace.isOn("sygus-engine")) + Trace("sygus-engine") << " * Verification lemma failed for:\n "; + for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) { - Trace("sygus-engine") << " * Verification lemma failed for:\n "; - for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) - { - Trace("sygus-engine") - << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; - } - Trace("sygus-engine") << std::endl; + Trace("sygus-engine") + << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " "; } -#ifdef CVC4_ASSERTIONS + Trace("sygus-engine") << std::endl; + } + if (Configuration::isAssertionBuild()) + { // the values for the query should be a complete model Node squery = query.substitute(d_ce_sk_vars.begin(), d_ce_sk_vars.end(), @@ -647,20 +646,28 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; Assert(options::sygusRecFun() || (squery.isConst() && squery.getConst<bool>())); -#endif - return false; } - else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - // if the result in the subcall was unsatisfiable, we avoid - // rechecking, hence we drop "query" from the verification lemma - lem = d_quant.negate(); - // we can short circuit adding the lemma (for sygus stream) - success = true; - } - // In the rare case that the subcall is unknown, we add the verification - // lemma in the main solver. This should only happen if the quantifier - // free logic is undecidable. + return false; + } + else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // if the result in the subcall was unsatisfiable, we avoid + // rechecking, hence we drop "query" from the verification lemma + lem = d_quant.negate(); + // we can short circuit adding the lemma (for sygus stream) + success = true; + } + else + { + // In the rare case that the subcall is unknown, we simply exclude the + // solution, without adding a counterexample point. This should only + // happen if the quantifier free logic is undecidable. + excludeCurrentSolution(terms, candidate_values); + // We should set incomplete, since a "sat" answer should not be + // interpreted as "infeasible", which would make a difference in the rare + // case where e.g. we had a finite grammar and exhausted the grammar. + d_qe->getOutputChannel().setIncomplete(); + return false; } } if (success) |