--- /dev/null
+/********************* */
+/*! \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<Node>& 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<Node>& is) const
+{
+ if (!d_data.isNull())
+ {
+ return true;
+ }
+ for (const std::pair<const Node, VariadicTrie>& 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<Node>& candidates,
+ std::vector<Node>& 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<bool>())
+ {
+ 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<Node> 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<bool>())
+ {
+ std::vector<Node> 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<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& 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<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& 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<Node, NodeHashFunction> visited;
+ std::vector<Node> 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<Node> 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<Node> passerts;
+ ccheck.getTermPool(passerts);
+ std::shuffle(passerts.begin(), passerts.end(), Random::getRandom());
+
+ // ----- check for entailment, adding based on models of failed points
+ std::vector<Node> 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<Node>& conjs) const
+{
+ std::sort(conjs.begin(), conjs.end());
+ Node sol;
+ std::map<Node, Node>::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<Node>& 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<Node>& u)
+{
+ d_numFalseCores++;
+ d_falseCores.add(id, u);
+}
+
+Node CegisCoreConnective::Component::getRefinementPt(
+ CegisCoreConnective* p,
+ Node n,
+ std::unordered_set<Node, NodeHashFunction>& visited,
+ std::vector<Node>& ss)
+{
+ std::vector<Node> ctx;
+
+ unsigned depth = p->d_vars.size();
+ std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator> vt;
+ std::map<NodeTrie*, std::map<Node, NodeTrie>::iterator>::iterator itvt;
+ std::map<Node, NodeTrie>::iterator itv;
+ std::vector<NodeTrie*> 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<bool>())
+ {
+ 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<Node>& passerts) const
+{
+ passerts.insert(passerts.end(), d_cpool.begin(), d_cpool.end());
+}
+
+bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p,
+ std::vector<Node>& passerts,
+ const std::vector<Node>& mvs,
+ Node mvId,
+ std::vector<Node>& 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<bool>())
+ {
+ 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<bool>());
+ an = n;
+ }
+ else
+ {
+ an = NodeManager::currentNM()->mkNode(AND, n, an);
+ }
+ return true;
+}
+
+void CegisCoreConnective::getModel(SmtEngine& smt,
+ std::vector<Node>& 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<Node>& 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<Node>& 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<bool>())
+ {
+ // 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<Node>& 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<bool>() == expRes)
+ {
+ return nm->mkConst(expRes);
+ }
+ }
+ return nm->mkConst(!expRes);
+ }
+ std::unordered_map<Node, Node, NodeHashFunction>& ec = d_eval_cache[n];
+ if (!id.isNull())
+ {
+ std::unordered_map<Node, Node, NodeHashFunction>::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<Node>& asserts,
+ std::vector<Node>& 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<Node> mvs;
+ std::unordered_set<Node, NodeHashFunction> 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<Node> 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<Node> 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<Node> 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<Node>::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<bool>());
+ 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
--- /dev/null
+/********************* */
+/*! \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 <unordered_set>
+#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<Node, VariadicTrie> 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<Node>& i);
+ /** Is there any data in this trie that is indexed by any subset of is? */
+ bool hasSubset(const std::vector<Node>& 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<Node>& candidates,
+ std::vector<Node>& 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<Node>& enums,
+ const std::vector<Node>& enum_values,
+ const std::vector<Node>& candidates,
+ std::vector<Node>& candidate_values,
+ bool satisfiedRl,
+ std::vector<Node>& 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<Node>& candidates,
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& 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<Node>& pt);
+ /** Add a false case to this component */
+ void addFalseCore(Node id, const std::vector<Node>& 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<Node>& passerts,
+ const std::vector<Node>& mvs,
+ Node mvId,
+ std::vector<Node>& 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<Node, NodeHashFunction>& visited,
+ std::vector<Node>& ss);
+ /** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */
+ void getTermPool(std::vector<Node>& 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<Node>& 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<Node> d_cpool;
+ /**
+ * A map from the formulas in the above vector to their sygus analog.
+ */
+ std::map<Node, Node> 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<Node> 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<Node>& 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<Node>& 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<Node>& 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<Node>& mvs);
+ /** A cache of the above function */
+ std::unordered_map<Node,
+ std::unordered_map<Node, Node, NodeHashFunction>,
+ 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<Node>& asserts,
+ std::vector<Node>& passerts);
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
projects / cvc5.git / commitdiff