From: Andrew Reynolds Date: Fri, 6 Dec 2019 18:03:40 +0000 (-0600) Subject: New algorithm for interpolation and abduction based on unsat cores (#3255) X-Git-Tag: cvc5-1.0.0~3789 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30e5875e066e917b69d01189233aec26ce226cd6;p=cvc5.git New algorithm for interpolation and abduction based on unsat cores (#3255) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4f64760e0..5b6c3aeca 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -558,6 +558,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/ce_guided_single_inv_sol.h theory/quantifiers/sygus/cegis.cpp theory/quantifiers/sygus/cegis.h + theory/quantifiers/sygus/cegis_core_connective.cpp + theory/quantifiers/sygus/cegis_core_connective.h theory/quantifiers/sygus/cegis_unif.cpp theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index e7a24cf3e..d37c9db83 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1001,6 +1001,14 @@ header = "options/quantifiers_options.h" default = "false" help = "use approach to repair constants in sygus candidate solutions" +[[option]] + name = "sygusCoreConnective" + category = "regular" + long = "sygus-core-connective" + type = "bool" + default = "false" + help = "use unsat core analysis to construct Boolean connective to sygus conjectures" + [[option]] name = "sygusRepairConstTimeout" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 571094618..39d09c4ea 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -192,7 +192,6 @@ header = "options/smt_options.h" type = "bool" predicates = ["proofEnabledBuild"] notifies = ["notifyBeforeSearch"] - read_only = true help = "turn on unsat core generation" [[option]] diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 075c8fa00..7e18e5a6f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1303,6 +1303,12 @@ void SmtEngine::setDefaults() { } } + // sygus core connective requires unsat cores + if (options::sygusCoreConnective()) + { + options::unsatCores.set(true); + } + if ((options::checkModels() || options::checkSynthSol() || options::produceAbducts() || options::modelCoresMode() != MODEL_CORES_NONE diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp new file mode 100644 index 000000000..0b9dd3b48 --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -0,0 +1,874 @@ +/********************* */ +/*! \file cegis_core_connective.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of cegis core connective module. + **/ + +#include "theory/quantifiers/sygus/cegis_core_connective.h" + +#include "expr/datatype.h" +#include "options/base_options.h" +#include "printer/printer.h" +#include "proof/unsat_core.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "util/random.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +bool VariadicTrie::add(Node n, const std::vector& i) +{ + VariadicTrie* curr = this; + for (const Node& ic : i) + { + curr = &(curr->d_children[ic]); + } + if (curr->d_data.isNull()) + { + curr->d_data = n; + return true; + } + return false; +} + +bool VariadicTrie::hasSubset(const std::vector& is) const +{ + if (!d_data.isNull()) + { + return true; + } + for (const std::pair& p : d_children) + { + Node n = p.first; + if (std::find(is.begin(), is.end(), n) != is.end()) + { + if (p.second.hasSubset(is)) + { + return true; + } + } + } + return false; +} + +CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe, + SynthConjecture* p) + : Cegis(qe, p) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +bool CegisCoreConnective::processInitialize(Node conj, + Node n, + const std::vector& candidates, + std::vector& lemmas) +{ + Trace("sygus-ccore-init") << "CegisCoreConnective::initialize" << std::endl; + Trace("sygus-ccore-init") << " conjecture : " << conj << std::endl; + Trace("sygus-ccore-init") << " candidates : " << candidates << std::endl; + if (candidates.size() != 1) + { + Trace("sygus-ccore-init") + << "...only applies to single candidate conjectures." << std::endl; + return false; + } + d_candidate = candidates[0]; + Assert(conj.getKind() == FORALL); + Assert(conj[0].getNumChildren() == 1); + Node body = conj[1]; + if (body.getKind() == NOT && body[0].getKind() == FORALL) + { + body = body[0][1]; + } + else + { + body = TermUtil::simpleNegate(body); + } + Trace("sygus-ccore-init") << " body : " << body << std::endl; + + TransitionInference ti; + ti.process(body, conj[0][0]); + + if (!ti.isComplete()) + { + Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl; + return false; + } + Node trans = ti.getTransitionRelation(); + Trace("sygus-ccore-init") << " transition relation: " << trans << std::endl; + if (!trans.isConst() || trans.getConst()) + { + Trace("sygus-ccore-init") + << "...does not apply conjectures with transition relations." + << std::endl; + return false; + } + + // the grammar must allow AND / OR when applicable + TypeNode gt = d_candidate.getType(); + + Node f = ti.getFunction(); + Assert(!f.isNull()); + Trace("sygus-ccore-init") << " predicate: " << f << std::endl; + ti.getVariables(d_vars); + Trace("sygus-ccore-init") << " variables: " << d_vars << std::endl; + // make the evaluation function + std::vector echildren; + echildren.push_back(d_candidate); + echildren.insert(echildren.end(), d_vars.begin(), d_vars.end()); + d_eterm = NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, echildren); + Trace("sygus-ccore-init") << " evaluation term: " << d_eterm << std::endl; + + Node prePost[2]; + prePost[0] = ti.getPreCondition(); + // negate the post condition + prePost[1] = TermUtil::simpleNegate(ti.getPostCondition()); + Trace("sygus-ccore-init") << " precondition: " << prePost[0] << std::endl; + Trace("sygus-ccore-init") << " postcondition: " << prePost[1] << std::endl; + + // side condition? + QAttributes qa; + QuantAttributes::computeQuantAttributes(conj, qa); + Node sc = qa.d_sygusSideCondition; + if (!sc.isNull()) + { + Trace("sygus-ccore-init") << " side condition: " << sc << std::endl; + if (sc.getKind() == EXISTS) + { + sc = sc[1]; + } + Node scb = TermUtil::simpleNegate(sc); + TransitionInference tisc; + tisc.process(scb, conj[0][0]); + Node scTrans = ti.getTransitionRelation(); + Trace("sygus-ccore-init") + << " transition relation of SC: " << scTrans << std::endl; + if (tisc.isComplete() && scTrans.isConst() && !scTrans.getConst()) + { + std::vector scVars; + tisc.getVariables(scVars); + Node scPre = tisc.getPreCondition(); + scPre = scPre.substitute( + scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); + Node scPost = TermUtil::simpleNegate(tisc.getPostCondition()); + scPost = scPost.substitute( + scVars.begin(), scVars.end(), d_vars.begin(), d_vars.end()); + Trace("sygus-ccore-init") + << " precondition of SC: " << scPre << std::endl; + Trace("sygus-ccore-init") + << " postcondition of SC: " << scPost << std::endl; + // We are extracting the side condition to be used by this algorithm + // from the side condition ascribed to the synthesis conjecture. + // A sygus conjecture of the form, for predicate-to-synthesize I: + // exists I. forall x. P[I,x] + // whose ascribed side condition is C[I], has the semantics: + // exists I. C[I] ^ forall x. P[I,x]. + // Notice that this side condition C may be an arbitrary formula over the + // function to synthesize. However, the algorithm implemented by this + // class is restricted to side conditions of the form: + // exists k. A[k] ^ I(k) + // The above condition guards for this case, and runs this block of code, + // where we use the TransitionInference utility to extract A[k] from + // A[k] ^ I(k). In the end, we set d_sc to A[d_vars]; notice the variables + // d_vars are those introduced by the TransitionInference utility + // for normalization. + d_sc = scPost; + } + } + + // We use the postcondition if it non-trivial and the grammar gt for our + // candidate has the production rule gt -> AND( gt, gt ). Similarly for + // precondition and OR. + Assert(gt.isDatatype()); + const Datatype& gdt = gt.getDatatype(); + SygusTypeInfo& gti = d_tds->getTypeInfo(gt); + for (unsigned r = 0; r < 2; r++) + { + Node f = prePost[r]; + if (f.isConst()) + { + // this direction is trivial, ignore + continue; + } + Component& c = r == 0 ? d_pre : d_post; + Kind rk = r == 0 ? OR : AND; + int i = gti.getKindConsNum(rk); + if (i != -1 && gdt[i].getNumArgs() == 2 + && TypeNode::fromType(gdt[i].getArgType(0)) == gt + && TypeNode::fromType(gdt[i].getArgType(1)) == gt) + { + Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post") + << "condition." << std::endl; + Node cons = Node::fromExpr(gdt[i].getConstructor()); + c.initialize(f, cons); + // Register the symmetry breaking lemma: do not do top-level solutions + // with this constructor (e.g. we want to enumerate literals, not + // conjunctions). + Node tst = datatypes::utils::mkTester(d_candidate, i, gdt); + Trace("sygus-ccore-init") << "Sym break lemma " << tst << std::endl; + lemmas.push_back(tst.negate()); + } + } + if (!isActive()) + { + return false; + } + // initialize the enumerator + return Cegis::processInitialize(conj, n, candidates, lemmas); +} + +bool CegisCoreConnective::processConstructCandidates( + const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& lems) +{ + Assert(isActive()); + bool ret = constructSolution(enums, enum_values, candidate_values); + + // exclude in the basic way if passive + Assert(enums.size() == 1); + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, esize = enums.size(); i < esize; i++) + { + Node e = enums[i]; + if (!d_tds->isPassiveEnumerator(e)) + { + continue; + } + Node v = enum_values[i]; + Node lem = d_tds->getExplain()->getExplanationForEquality(e, v).negate(); + Node g = d_tds->getActiveGuardForEnumerator(e); + if (!g.isNull()) + { + lem = nm->mkNode(OR, g.negate(), lem); + } + lems.push_back(lem); + } + return ret; +} + +bool CegisCoreConnective::isActive() const +{ + return d_pre.isActive() || d_post.isActive(); +} + +bool CegisCoreConnective::constructSolution( + const std::vector& candidates, + const std::vector& candidate_values, + std::vector& solv) +{ + // if the conjecture is not the right shape, no repair is possible + if (!isActive()) + { + return false; + } + Assert(candidates.size() == candidate_values.size()); + Trace("sygus-ccore-summary") + << "CegisCoreConnective: construct solution..." << std::endl; + if (Trace.isOn("sygus-ccore")) + { + Trace("sygus-ccore") + << "CegisCoreConnective: Construct candidate solutions..." << std::endl; + Printer* p = Printer::getPrinter(options::outputLanguage()); + for (unsigned i = 0, size = candidates.size(); i < size; i++) + { + std::stringstream ss; + p->toStreamSygus(ss, candidate_values[i]); + Trace("sygus-ccore") << " " << candidates[i] << " -> " << ss.str() + << std::endl; + } + } + Assert(candidates.size() == 1 && candidates[0] == d_candidate); + TNode cval = candidate_values[0]; + Node ets = d_eterm.substitute(d_candidate, cval); + Node etsr = Rewriter::rewrite(ets); + Trace("sygus-ccore-debug") << "...predicate is: " << etsr << std::endl; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned d = 0; d < 2; d++) + { + Component& ccheck = d == 0 ? d_pre : d_post; + if (!ccheck.isActive()) + { + // not trying this direction + continue; + } + Component& cfilter = d == 0 ? d_post : d_pre; + // In terms of the algorithm described in the h file, this gets the formula + // A (or B, depending on the direction d). + Node fpred = cfilter.getFormula(); + if (!fpred.isNull() && !fpred.isConst()) + { + // check refinement points + Node etsrn = d == 0 ? etsr : etsr.negate(); + std::unordered_set visited; + std::vector pt; + Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt); + if (!rid.isNull()) + { + // failed a refinement point + continue; + } + Node fassert = nm->mkNode(AND, fpred, etsrn); + Trace("sygus-ccore-debug") + << "...check filter " << fassert << "..." << std::endl; + std::vector mvs; + Result r = checkSat(fassert, mvs); + Trace("sygus-ccore-debug") << "...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + // failed the filter, remember the refinement point + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + cfilter.addRefinementPt(fassert, mvs); + } + continue; + } + } + Trace("sygus-ccore-debug") + << "...add to pool in direction " << d << std::endl; + // implements e.g. pool(B) += e_i. + ccheck.addToPool(etsr, cval); + + // ----- get the pool of assertions and randomize it + std::vector passerts; + ccheck.getTermPool(passerts); + std::shuffle(passerts.begin(), passerts.end(), Random::getRandom()); + + // ----- check for entailment, adding based on models of failed points + std::vector asserts; + Node sol = constructSolutionFromPool(ccheck, asserts, passerts); + if (!sol.isNull()) + { + solv.push_back(sol); + Trace("sygus-ccore-summary") << "...success" << std::endl; + return true; + } + if (Trace.isOn("sygus-ccore-summary")) + { + std::stringstream ss; + ccheck.debugPrintSummary(ss); + Trace("sygus-ccore-summary") + << "C[d=" << d << "] " << ss.str() << std::endl; + } + } + Trace("sygus-ccore") << "CegisCoreConnective: failed to generate candidate" + << std::endl; + Trace("sygus-ccore-summary") << "...failed" << std::endl; + return false; +} + +void CegisCoreConnective::Component::initialize(Node n, Node c) +{ + d_this = n; + d_scons = c; +} + +void CegisCoreConnective::Component::addToPool(Node n, Node s) +{ + d_cpool.push_back(n); + d_cpoolToSol[n] = s; +} + +Node CegisCoreConnective::Component::getSygusSolution( + std::vector& conjs) const +{ + std::sort(conjs.begin(), conjs.end()); + Node sol; + std::map::const_iterator itu; + NodeManager* nm = NodeManager::currentNM(); + for (const Node& u : conjs) + { + itu = d_cpoolToSol.find(u); + Assert(itu != d_cpoolToSol.end()); + Node s = itu->second; + Trace("sygus-ccore-debug-sy") << " uc-s " << s << std::endl; + if (sol.isNull()) + { + sol = s; + } + else + { + sol = nm->mkNode(APPLY_CONSTRUCTOR, d_scons, s, sol); + } + } + return sol; +} +void CegisCoreConnective::Component::debugPrintSummary(std::ostream& os) const +{ + os << "size(pool/pts/cores): " << d_cpool.size() << "/" << d_numRefPoints + << "/" << d_numFalseCores; +} + +void CegisCoreConnective::Component::addRefinementPt( + Node id, const std::vector& pt) +{ + d_numRefPoints++; + bool res = d_refinementPt.addTerm(id, pt); + // this should always be a new point + AlwaysAssert(res); +} +void CegisCoreConnective::Component::addFalseCore(Node id, + const std::vector& u) +{ + d_numFalseCores++; + d_falseCores.add(id, u); +} + +Node CegisCoreConnective::Component::getRefinementPt( + CegisCoreConnective* p, + Node n, + std::unordered_set& visited, + std::vector& ss) +{ + std::vector ctx; + + unsigned depth = p->d_vars.size(); + std::map::iterator> vt; + std::map::iterator>::iterator itvt; + std::map::iterator itv; + std::vector visit; + NodeTrie* cur; + visit.push_back(&d_refinementPt); + do + { + cur = visit.back(); + Trace("sygus-ccore-ref") << "process trie " << cur << std::endl; + if (ctx.size() == depth) + { + Trace("sygus-ccore-ref") << "...at depth " << std::endl; + // at leaf + Node id = cur->getData(); + Trace("sygus-ccore-ref") << "...data is " << id << std::endl; + Assert(!id.isNull()); + AlwaysAssert(id.getType().isBoolean()); + if (visited.find(id) == visited.end()) + { + visited.insert(id); + Trace("sygus-ccore-ref") << "...eval " << std::endl; + // check if it is true + Node en = p->evaluate(n, id, ctx); + if (en.isConst() && en.getConst()) + { + ss = ctx; + return id; + } + } + visit.pop_back(); + ctx.pop_back(); + } + else + { + // get the current child iterator for this node + itvt = vt.find(cur); + if (itvt == vt.end()) + { + Trace("sygus-ccore-ref") << "...initialize iterator " << std::endl; + // initialize the iterator + itv = cur->d_data.begin(); + vt[cur] = itv; + Trace("sygus-ccore-ref") << "...finished init" << std::endl; + } + else + { + Trace("sygus-ccore-ref") << "...continue iterator " << std::endl; + itv = itvt->second; + } + Trace("sygus-ccore-ref") << "...now check status" << std::endl; + // are we done iterating children? + if (itv == cur->d_data.end()) + { + Trace("sygus-ccore-ref") << "...finished iterating " << std::endl; + // yes, pop back + if (!ctx.empty()) + { + ctx.pop_back(); + } + visit.pop_back(); + vt.erase(cur); + } + else + { + Trace("sygus-ccore-ref") << "...recurse " << itv->first << std::endl; + // recurse + ctx.push_back(itv->first); + visit.push_back(&(itv->second)); + ++vt[cur]; + } + } + + } while (!visit.empty()); + return Node::null(); +} + +void CegisCoreConnective::Component::getTermPool( + std::vector& passerts) const +{ + passerts.insert(passerts.end(), d_cpool.begin(), d_cpool.end()); +} + +bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, + std::vector& passerts, + const std::vector& mvs, + Node mvId, + std::vector& asserts, + Node& an) +{ + // point should be valid + Assert(!mvId.isNull()); + Node n; + unsigned currIndex = 0; + do + { + // select condition from passerts that evaluates to false on mvs + for (unsigned i = currIndex, psize = passerts.size(); i < psize; i++) + { + Node cn = passerts[i]; + Node cne = p->evaluate(cn, mvId, mvs); + if (cne.isConst() && !cne.getConst()) + { + n = cn; + // remove n from the pool + passerts.erase(passerts.begin() + i, passerts.begin() + i + 1); + currIndex = i; + break; + } + } + if (n.isNull()) + { + // could not find any + return false; + } + Trace("sygus-ccore-debug") << "...try adding " << n << "..." << std::endl; + asserts.push_back(n); + // is it already part of a false core? + if (d_falseCores.hasSubset(asserts)) + { + Trace("sygus-ccore-debug") + << "..." << n << " was rejected due to previous false core" + << std::endl; + asserts.pop_back(); + n = Node::null(); + } + } while (n.isNull()); + Trace("sygus-ccore") << "--- Insert " << n << " to falsify " << mvs + << std::endl; + // success + if (an.isConst()) + { + Assert(an.getConst()); + an = n; + } + else + { + an = NodeManager::currentNM()->mkNode(AND, n, an); + } + return true; +} + +void CegisCoreConnective::getModel(SmtEngine& smt, + std::vector& vals) const +{ + for (const Node& v : d_vars) + { + Node mv = Node::fromExpr(smt.getValue(v.toExpr())); + Trace("sygus-ccore-model") << v << " -> " << mv << " "; + vals.push_back(mv); + } +} + +bool CegisCoreConnective::getUnsatCore(SmtEngine& smt, + Node query, + std::vector& uasserts) const +{ + UnsatCore uc = smt.getUnsatCore(); + bool hasQuery = false; + for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) + { + Node uassert = Node::fromExpr(*i); + Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; + if (uassert == query) + { + hasQuery = true; + continue; + } + uasserts.push_back(uassert); + } + return hasQuery; +} + +Result CegisCoreConnective::checkSat(Node n, std::vector& mvs) const +{ + Assert(mvs.empty()); + Assert(n.getType().isBoolean()); + Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; + n = Rewriter::rewrite(n); + if (n.isConst()) + { + if (n.getConst()) + { + // default model + for (const Node& v : d_vars) + { + mvs.push_back(v.getType().mkGroundTerm()); + } + return Result(Result::SAT); + } + else + { + return Result(Result::UNSAT); + } + } + SmtEngine smt(NodeManager::currentNM()->toExprManager()); + smt.setIsInternalSubsolver(); + smt.setLogic(smt::currentSmtEngine()->getLogicInfo()); + smt.assertFormula(n.toExpr()); + Result r = smt.checkSat(); + Trace("sygus-ccore-debug") << "...got " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + getModel(smt, mvs); + } + return r; +} + +Node CegisCoreConnective::evaluate(Node n, + Node id, + const std::vector& mvs) +{ + Kind nk = n.getKind(); + if (nk == AND || nk == OR) + { + NodeManager* nm = NodeManager::currentNM(); + bool expRes = nk == OR; + // split AND/OR + for (const Node& nc : n) + { + Node enc = evaluate(nc, id, mvs); + Assert(enc.isConst()); + if (enc.getConst() == expRes) + { + return nm->mkConst(expRes); + } + } + return nm->mkConst(!expRes); + } + std::unordered_map& ec = d_eval_cache[n]; + if (!id.isNull()) + { + std::unordered_map::iterator it = ec.find(id); + if (it != ec.end()) + { + return it->second; + } + } + // use evaluator + Node cn = d_eval.eval(n, d_vars, mvs); + if (cn.isNull()) + { + Node cn = + n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); + cn = Rewriter::rewrite(cn); + } + if (!id.isNull()) + { + ec[id] = cn; + } + return cn; +} + +Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, + std::vector& asserts, + std::vector& passerts) +{ + // In terms of Variant #2 from the header file, the set D is represented by + // asserts. The available set of prediates pool(B) is represented by passerts. + NodeManager* nm = NodeManager::currentNM(); + Trace("sygus-ccore") << "------ Get initial candidate..." << std::endl; + Node an = asserts.empty() + ? d_true + : (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts)); + std::vector mvs; + std::unordered_set visited; + bool addSuccess = true; + // Ensure that the current conjunction evaluates to false on all refinement + // points. We get refinement points until we have exhausted. + // In terms of Variant #2, this is inner while loop that adds points to D + // while there exists a point in pts(B) such that D is true. + Node mvId; + do + { + mvs.clear(); + Trace("sygus-ccore-debug") << "...get refinement pt..." << std::endl; + // In terms of Variant #2, this implements the line: + // "D[v] is true for some v in pts(B)", + // where v is stored in mvs. + mvId = ccheck.getRefinementPt(this, an, visited, mvs); + if (!mvId.isNull()) + { + Trace("sygus-ccore-debug") << "...got " << mvs << std::endl; + // In terms of Variant #2, this checks the conditions: + // "d'[v] is false for some d' in pool(B)" and + // "no element of cores(B) is a subset of D ++ { d' }" + // and adds d' to D (asserts) if possible. + addSuccess = ccheck.addToAsserts(this, passerts, mvs, mvId, asserts, an); + Trace("sygus-ccore-debug") + << "...add success is " << addSuccess << std::endl; + } + else + { + Trace("sygus-ccore-debug") << "...failed" << std::endl; + } + } while (!mvId.isNull() && addSuccess); + if (!addSuccess) + { + Trace("sygus-ccore") << ">>> Failed to generate initial candidate" + << std::endl; + return Node::null(); + } + Trace("sygus-ccore") << "----- Initial candidate is " << an << std::endl; + + // We now have constructed an initial candidate for D. In terms of Variant #2, + // we now enter the block code within "if D is false for all v in pts(B)". + // Further refinements to D are made as the following do-while loop proceeds. + do + { + addSuccess = false; + // try a new core + SmtEngine checkSol(nm->toExprManager()); + checkSol.setIsInternalSubsolver(); + checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo()); + Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; + std::vector rasserts = asserts; + rasserts.push_back(ccheck.getFormula()); + std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom()); + Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts); + for (const Node& a : rasserts) + { + checkSol.assertFormula(a.toExpr()); + } + Result r = checkSol.checkSat(); + Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl; + // In terms of Variant #2, this is the check "if D => B" + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // it entails the postcondition, now get the unsat core + // In terms of Variant #2, this is the line + // "Let U be a subset of D such that U ^ ~B is unsat." + // and uasserts is set to U. + std::vector uasserts; + bool hasQuery = getUnsatCore(checkSol, ccheck.getFormula(), uasserts); + // now, check the side condition + bool falseCore = false; + if (!d_sc.isNull()) + { + if (!hasQuery) + { + // Already know it trivially rewrites to false, don't need + // to use unsat cores. + falseCore = true; + } + else + { + // In terms of Variant #2, this is the check "if S ^ U is unsat" + Trace("sygus-ccore") << "----- Check side condition" << std::endl; + SmtEngine checkSc(nm->toExprManager()); + checkSc.setIsInternalSubsolver(); + checkSc.setLogic(smt::currentSmtEngine()->getLogicInfo()); + std::vector scasserts; + scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); + scasserts.push_back(d_sc); + std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom()); + Result rsc = checkSc.checkSat(); + Trace("sygus-ccore") + << "----- check-sat returned " << rsc << std::endl; + if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // In terms of Variant #2, this is the line + // "Let W be a subset of D such that S ^ W is unsat." + // and uasserts is set to W. + uasserts.clear(); + getUnsatCore(checkSc, d_sc, uasserts); + falseCore = true; + } + } + } + + if (!falseCore) + { + // In terms of Variant #2, this is the line: + // "return u_1 AND ... AND u_m where U = { u_1, ..., u_m }". + Trace("sygus-ccore") << ">>> Solution : " << uasserts << std::endl; + // We convert the builtin solution to a sygus datatype to + // communicate with the sygus solver. + Node sol = ccheck.getSygusSolution(uasserts); + Trace("sygus-ccore-sy") << "Sygus solution : " << sol << std::endl; + return sol; + } + else + { + Assert(!uasserts.empty()); + Node xu = uasserts[0]; + Trace("sygus-ccore") + << "--- Add false core : " << uasserts << std::endl; + // notice that a singleton false core could be removed from pool + // in the case that (uasserts.size() == 1). + std::sort(uasserts.begin(), uasserts.end()); + // In terms of Variant #2, this is "cores(B) += W". + ccheck.addFalseCore(query, uasserts); + // remove and continue + // In terms of Variant #2, this is "remove some d'' in W from D". + std::vector::iterator ita = + std::find(asserts.begin(), asserts.end(), xu); + Assert(ita != asserts.end()); + asserts.erase(ita); + // Start over, since now we don't know which points are required to + // falsify. + return constructSolutionFromPool(ccheck, asserts, passerts); + } + } + else if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + // it does not entail the postcondition, add an assertion that blocks + // the current point + mvs.clear(); + getModel(checkSol, mvs); + // should evaluate to true + Node ean = evaluate(an, Node::null(), mvs); + Assert(ean.isConst() && ean.getConst()); + Trace("sygus-ccore") << "--- Add refinement point " << mvs << std::endl; + // In terms of Variant #2, this is the line: + // "pts(B) += { v } where { x -> v } is a model for D ^ ~B". + ccheck.addRefinementPt(query, mvs); + Trace("sygus-ccore-debug") << "...get new assertion..." << std::endl; + // In terms of Variant #2, this rechecks the condition of the inner while + // loop and attempts to add a new assertion to D. + addSuccess = ccheck.addToAsserts(this, passerts, mvs, query, asserts, an); + Trace("sygus-ccore-debug") << "...success is " << addSuccess << std::endl; + } + } while (addSuccess); + return Node::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h new file mode 100644 index 000000000..3589d97e5 --- /dev/null +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -0,0 +1,396 @@ +/********************* */ +/*! \file cegis_core_connective.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Cegis core connective module. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H +#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H + +#include +#include "expr/node.h" +#include "expr/node_trie.h" + +#include "theory/evaluator.h" +#include "theory/quantifiers/sygus/cegis.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * A trie that stores data at undetermined depth. Storing data at + * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which + * assumes all data is stored at a fixed depth. + * + * Since data can be stored at any depth, we require both a d_children field + * and a d_data field. + */ +class VariadicTrie +{ + public: + /** the children of this node */ + std::map d_children; + /** the data at this node */ + Node d_data; + /** + * Add data with identifier n indexed by i, return true if data is not already + * stored at the node indexed by i. + */ + bool add(Node n, const std::vector& i); + /** Is there any data in this trie that is indexed by any subset of is? */ + bool hasSubset(const std::vector& is) const; +}; + +/** CegisCoreConnective + * + * A sygus module that is specialized in handling conjectures of the form: + * exists P. forall x. (A[x] => C(x)) ^ (C(x) => B(x)) + * That is, conjectures with a pre/post condition but no inductive relation + * or other constraints. Additionally, we may have that the above conjecture + * has a side condition SC, which requires that exists x. SC[x]^C(x) is + * satisfiable. + * + * Two examples of this kind of sygus conjecture are abduction and + * interpolation. + * + * This module implements a specific algorithm for constructing solutions + * to this conjecture based on Boolean connectives and unsat cores, described + * in following. We give two variants of the algorithm, both implemented as + * special cases of this class. Below, let: + * + * pool(A) be a set of literals { c_1, ..., c_n } s.t. c_i => B for i=1,...,n, + * pts(A) : a set of points { v | A[v] is true }, + * pool(B) : a set of literals { d_1, ..., d_m } s.t. A => d_i for i=1,...,m, + * pts(B) : a set of points { v | ~B[v] is true }, + * cores(B) : a set of sets of literals { U_1, ..., U_p } s.t. for i=1,...,p: + * - U_i is a subset of pool(B), + * - A ^ U_i is unsat. + * We construct pool(A)/pool(B) using enumerative SyGuS, discarding the literals + * that do not match the criteria. + * + * Variant #1 (Interpolation) + * + * Let the synthesis conjecture be of the form + * exists C. forall x. A[x] => C[x] ^ C[x] => B[x] + * + * The high level idea is we construct solutions for C of the form + * c_1 OR ... OR c_n where c_i => B for each i=1,...,n, or + * d_1 AND ... AND d_m where A => d_i for each i=1,...,m. + * + * while(true){ + * Let e_i = next_sygus_enum(); + * // check if e_i should be added to pool(B) + * if e_i[v] is true for all v in pts(A) + * if A => e_i + * pool(B) += e_i; + * else + * pts(A) += { v } where { x -> v } is a model for A ^ ~e_i; + * // try to construct a solution based on the pool + * Let D = {}. + * while + * D[v] is true for some v in pts(B), and + * d'[v] is false for some d' in pool(B) + * { + * D += { d' } + * if D is false for all v in pts(B) + * if D => B + * return AND_{d in D}( d ) + * else + * pts(B) += { v } where { x -> v } is a model for D ^ ~B + * } + * + * // analogous for the other direction + * } + * + * + * Variant #2 (Abduction) + * + * Let the synthesis conjecture be of the form exists C. forall x. C[x] => B[x] + * such that S[x] ^ C[x] is satisfiable. We refer to S as the side condition + * for this conjecture. Notice that A in this variant is false, hence the + * algorithm below is modified accordingly. + * + * The high level idea is we construct solutions for C of the form + * d_1 AND ... AND d_n + * where the above conjunction is weakened based on only including conjuncts + * that are in the unsat core of d_1 AND ... AND d_n => B. + * + * while(true){ + * Let e_i = next_sygus_enum(); + * // add e_i to the pool + * pool(B) += e_i; + * // try to construct a solution based on the pool + * Let D = {}. + * while + * D[v] is true for some v in pts(B), and + * d'[v] is false for some d' in pool(B) and + * no element of cores(B) is a subset of D ++ { d' } + * { + * D += { d' } + * if D is false for all v in pts(B) + * if D => B + * Let U be a subset of D such that U ^ ~B is unsat. + * if S ^ U is unsat + * Let W be a subset of D such that S ^ W is unsat. + * cores(B) += W + * remove some d'' in W from D + * else + * return u_1 AND ... AND u_m where U = { u_1, ..., u_m } + * else + * pts(B) += { v } where { x -> v } is a model for D ^ ~B + * } + * } + */ +class CegisCoreConnective : public Cegis +{ + public: + CegisCoreConnective(QuantifiersEngine* qe, SynthConjecture* p); + ~CegisCoreConnective() {} + /** + * Return whether this module has the possibility to construct solutions. This + * is true if this module has been initialized, and the shape of the + * conjecture allows us to use the core connective algorithm. + */ + bool isActive() const; + + protected: + /** do cegis-implementation-specific initialization for this class */ + bool processInitialize(Node conj, + Node n, + const std::vector& candidates, + std::vector& lemmas) override; + /** do cegis-implementation-specific post-processing for construct candidate + * + * satisfiedRl is whether all refinement lemmas are satisfied under the + * substitution { enums -> enum_values }. + */ + bool processConstructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& lems) override; + + /** construct solution + * + * This function is called when candidates -> candidate_values is the current + * candidate solution for the synthesis conjecture. + * + * If this function returns true, then this class adds to solv the + * a candidate solution for candidates. + */ + bool constructSolution(const std::vector& candidates, + const std::vector& candidate_values, + std::vector& solv); + + private: + /** common constants */ + Node d_true; + Node d_false; + /** The first-order datatype variable for the function-to-synthesize */ + TNode d_candidate; + /** + * Information about the pre and post conditions of the synthesis conjecture. + * This maintains all information needed for producing solutions relative to + * one direction of the synthesis conjecture. In other words, this component + * may be focused on finding a C1 ... Cn such that A => C1 V ... V Cn + * or alteratively C1 ^ ... ^ Cn such that C1 ^ ... ^ Cn => B. + */ + class Component + { + public: + Component() : d_numFalseCores(0), d_numRefPoints(0) {} + /** initialize + * + * This initializes this component with pre/post condition given by n + * and sygus constructor c. + */ + void initialize(Node n, Node c); + /** get the formula n that we initialized this with */ + Node getFormula() const { return d_this; } + /** Is this component active? */ + bool isActive() const { return !d_scons.isNull(); } + /** Add term n to pool whose sygus analog is s */ + void addToPool(Node n, Node s); + /** Add a refinement point to this component */ + void addRefinementPt(Node id, const std::vector& pt); + /** Add a false case to this component */ + void addFalseCore(Node id, const std::vector& u); + /** + * Selects a node from passerts that evaluates to false on point mv if one + * exists, or otherwise returns false. + * The argument mvId is an identifier used for indexing the point mv. + * The argument asserts stores the current candidate solution (set D in + * Variant #2 described above). If the method returns true, it updates + * an (the node version of asserts) to be the conjunction of the nodes + * in asserts. + * + * If true is returned, it is removed from passerts. + */ + bool addToAsserts(CegisCoreConnective* p, + std::vector& passerts, + const std::vector& mvs, + Node mvId, + std::vector& asserts, + Node& an); + + /** + * Get a refinement point that n evalutes to true on, taken from the + * d_refinementPt trie, and store it in ss. The set visited is the set + * of leaf nodes (reference by their data) that we have already processed + * and should be ignored. + */ + Node getRefinementPt(CegisCoreConnective* p, + Node n, + std::unordered_set& visited, + std::vector& ss); + /** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */ + void getTermPool(std::vector& passerts) const; + /** + * Get the sygus solution corresponding to the Boolean connective for + * this component applied to conj. In particular, this returns a + * right-associative chain of applications of sygus constructor d_scons + * to the sygus analog of formulas in conj. + */ + Node getSygusSolution(std::vector& conjs) const; + /** debug print summary (for debugging) */ + void debugPrintSummary(std::ostream& os) const; + + private: + /** The original formula for the pre/post condition A/B. */ + Node d_this; + /** + * The sygus constructor for constructing solutions based on the core + * connective algorithm. This is a sygus datatype constructor that + * encodes applications of AND or OR. + */ + Node d_scons; + /** This is pool(A)/pool(B) in the algorithms above */ + std::vector d_cpool; + /** + * A map from the formulas in the above vector to their sygus analog. + */ + std::map d_cpoolToSol; + /** + * An index of list of predicates such that each list ( P1, ..., Pn ) + * indexed by this trie is such that P1 ^ ... ^ Pn ^ S is unsatisfiable, + * where S is the side condition of our synthesis conjecture. We call this + * a "false core". This set is "cores(B)" in Variant #2 above. + */ + VariadicTrie d_falseCores; + /** + * The number of points that have been added to the above trie, for + * debugging. + */ + unsigned d_numFalseCores; + /** + * An index of the points that satisfy d_this. + */ + NodeTrie d_refinementPt; + /** + * The number of points that have been added to the above trie, for + * debugging. + */ + unsigned d_numRefPoints; + }; + /** Above information for the precondition of the synthesis conjecture */ + Component d_pre; + /** Above information for the postcondition of the synthesis conjecture */ + Component d_post; + /** + * The free variables that may appear in the pre/post condition, and our + * pools of predicates. + */ + std::vector d_vars; + /** + * The evaluation term of the form: + * (DT_SYGUS_EVAL d_candidate d_vars[0]...d_vars[n]) + * This is used to convert enumerated sygus terms t to their builtin + * equivalent via rewriting d_eterm * { d_candidate -> t }. + */ + Node d_eterm; + /** + * The side condition of the conjecture. If this is non-null, then + * this node is a formula such that (builtin) solutions t' are such that + * t' ^ d_sc is satisfiable. Notice that the free variables of d_sc are + * a subset of d_vars. + */ + Node d_sc; + //-----------------------------------for SMT engine calls + /** + * Assuming smt has just been called to check-sat and returned "SAT", this + * method adds the model for d_vars to mvs. + */ + void getModel(SmtEngine& smt, std::vector& mvs) const; + /** + * Assuming smt has just been called to check-sat and returned "UNSAT", this + * method get the unsat core and adds it to uasserts. + * + * If query is non-null, then it is excluded from uasserts. If query was + * in the unsat core, then this method returns true. Otherwise, this method + * returns false. It also returns false if query was null. + */ + bool getUnsatCore(SmtEngine& smt, + Node query, + std::vector& uasserts) const; + /** + * Return the result of checking satisfiability of formula n. + * If n was satisfiable, then we store the model for d_vars in mvs. + */ + Result checkSat(Node n, std::vector& mvs) const; + //-----------------------------------end for SMT engine calls + //-----------------------------------for evaluation + /** + * Return the evaluation of n under the substitution { d_vars -> mvs }. + * If id is non-null, then id is a unique identifier for mvs, and we cache + * the result of n for this point. + */ + Node evaluate(Node n, Node id, const std::vector& mvs); + /** A cache of the above function */ + std::unordered_map, + NodeHashFunction> + d_eval_cache; + /** The evaluator utility used for the above function */ + Evaluator d_eval; + //-----------------------------------end for evaluation + + /** Construct solution from pool + * + * This is the main body of the core connective algorithm, which attempts + * to build a solution based on one direction (pre/post) of the synthesis + * conjecture. + * + * It takes as input: + * - a component ccheck that maintains information regarding the direction + * we are trying to build a solution for, + * - the current set of assertions asserts that comprise the current solution + * we are building, + * - the current pool passerts of available assertions that we may add to + * asserts. + * + * This implements the while loop in the algorithms above. If this method + * returns a non-null node, then this is a solution for the given synthesis + * conjecture. + */ + Node constructSolutionFromPool(Component& ccheck, + std::vector& asserts, + std::vector& passerts); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index c980e5413..ca4feda32 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -52,6 +52,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), + d_sygus_ccore(new CegisCoreConnective(qe, this)), d_ceg_pbe(new SygusPbe(qe, this)), d_ceg_cegis(new Cegis(qe, this)), d_ceg_cegisUnif(new CegisUnif(qe, this)), @@ -69,6 +70,10 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) { d_modules.push_back(d_ceg_cegisUnif.get()); } + if (options::sygusCoreConnective()) + { + d_modules.push_back(d_sygus_ccore.get()); + } d_modules.push_back(d_ceg_cegis.get()); } @@ -438,7 +443,7 @@ bool SynthConjecture::doCheck(std::vector& lems) NodeManager* nm = NodeManager::currentNM(); - // check the side condition + // check the side condition if we constructed a candidate if (constructed_cand) { if (!checkSideCondition(candidate_values)) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 344f8b460..db9872ec3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" +#include "theory/quantifiers/sygus/cegis_core_connective.h" #include "theory/quantifiers/sygus/cegis_unif.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_pbe.h" @@ -192,6 +193,8 @@ class SynthConjecture std::unique_ptr d_ceg_gc; /** repair constant utility */ std::unique_ptr d_sygus_rconst; + /** connective core utility */ + std::unique_ptr d_sygus_ccore; //------------------------modules /** program by examples module */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0bcaa049a..787633178 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1682,8 +1682,10 @@ set(regress_1_tests regress1/strings/username_checker_min.smt2 regress1/sygus-abduct-ex1-grammar.smt2 regress1/sygus-abduct-test.smt2 + regress1/sygus-abduct-test-ccore.smt2 regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy + regress1/sygus/abd-simple-conj-4.smt2 regress1/sygus/abv.sy regress1/sygus/array_search_5-Q-easy.sy regress1/sygus/bvudiv-by-2.sy diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2 new file mode 100644 index 000000000..86f5fe133 --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --produce-abducts --sygus-core-connective +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 + +(set-logic QF_UFLIRA) +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (>= n 1)) +(assert (and (<= n x)(<= x (+ n 5)))) +(assert (and (<= 1 y)(<= y m))) + +(get-abduct A (not (< x y))) diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 index 4b7870c78..bb02ebce2 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --produce-abducts +; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic QF_UFLIRA) @@ -19,6 +20,8 @@ (get-abduct A (not (< x y)) ; the grammar for the abduct-to-synthesize +; notice it does not permit the sygus-core-connective algorithm; this regression +; tests that we ignore this option properly. ((Start Bool) (StartInt Int)) ( (Start Bool ((< StartInt StartInt))) diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2 new file mode 100644 index 000000000..98bf70fd7 --- /dev/null +++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --produce-abducts --sygus-core-connective +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic QF_LIA) +(set-option :produce-abducts true) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun z () Int) +(declare-fun w () Int) +(declare-fun u () Int) +(declare-fun v () Int) +(assert (>= x 0)) +(get-abduct A (>= (+ x y z w u v) 2))