diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-09-15 09:47:15 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 20:47:15 -0500 |
commit | 51be2e14c632d45e63a40659dea2177133251dfa (patch) | |
tree | d47380a72d05dc3ede4d61f4c04f9e4034b791fc /src/theory/quantifiers/sygus | |
parent | 9e2a36f53007b932412a98c8e7ff1556a53f37c5 (diff) |
Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)
Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.cpp | 57 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_interpol.h | 10 |
2 files changed, 30 insertions, 37 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index c2ca83e41..4d18c850b 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/rewriter.h" +#include "theory/smt_engine_subsolver.h" namespace CVC4 { namespace theory { @@ -30,8 +31,6 @@ namespace quantifiers { SygusInterpol::SygusInterpol() {} -SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {} - void SygusInterpol::collectSymbols(const std::vector<Node>& axioms, const Node& conj) { @@ -75,6 +74,9 @@ void SygusInterpol::createVariables(bool needsShared) Node var = nm->mkBoundVar(tn); d_vars.push_back(var); Node vlv = nm->mkBoundVar(ss.str(), tn); + // set that this variable encodes the term s + SygusVarToTermAttribute sta; + vlv.setAttribute(sta, s); d_vlvs.push_back(vlv); if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end()) { @@ -266,7 +268,7 @@ void SygusInterpol::mkSygusConjecture(Node itp, Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; } -bool SygusInterpol::findInterpol(Expr& interpol, Node itp) +bool SygusInterpol::findInterpol(Node& interpol, Node itp) { // get the synthesis solution std::map<Node, Node> sols; @@ -283,31 +285,31 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp) } Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " << its->second << std::endl; - Node interpoln = its->second; + interpol = its->second; // replace back the created variables to original symbols. - Node interpoln_reduced; - if (interpoln.getKind() == kind::LAMBDA) + if (interpol.getKind() == kind::LAMBDA) { - interpoln_reduced = interpoln[1]; + interpol = interpol[1]; } - else + + // get the grammar type for the interpolant + Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute()); + Assert(!igdtbv.isNull()); + Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST); + // convert back to original + // must replace formal arguments of itp with the free variables in the + // input problem that they correspond to. + std::vector<Node> vars; + std::vector<Node> syms; + SygusVarToTermAttribute sta; + for (const Node& bv : igdtbv) { - interpoln_reduced = interpoln; + vars.push_back(bv); + syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv); } - if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0) - { - std::vector<Node> formals; - for (const Node& n : interpoln[0]) - { - formals.push_back(n); - } - interpoln_reduced = interpoln_reduced.substitute(formals.begin(), - formals.end(), - d_symSetShared.begin(), - d_symSetShared.end()); - } - // convert to expression - interpol = interpoln_reduced.toExpr(); + interpol = + interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end()); + return true; } @@ -315,14 +317,11 @@ bool SygusInterpol::SolveInterpolation(const std::string& name, const std::vector<Node>& axioms, const Node& conj, const TypeNode& itpGType, - Expr& interpol) + Node& interpol) { - NodeManager* nm = NodeManager::currentNM(); - // we generate a new smt engine to do the interpolation query - d_subSolver.reset(new SmtEngine(nm->toExprManager())); - d_subSolver->setIsInternalSubsolver(); + initializeSubsolver(d_subSolver); // get the logic - LogicInfo l = d_logic.getUnlockedCopy(); + LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus l.enableSygus(); d_subSolver->setLogic(l); diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 0fe66694f..4abe94f15 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -46,8 +46,6 @@ class SygusInterpol public: SygusInterpol(); - SygusInterpol(LogicInfo logic); - /** * Returns the sygus conjecture in interpol corresponding to the interpolation * problem for input problem (F above) given by axioms (Fa above), and conj @@ -65,7 +63,7 @@ class SygusInterpol const std::vector<Node>& axioms, const Node& conj, const TypeNode& itpGType, - Expr& interpol); + Node& interpol); private: /** @@ -158,7 +156,7 @@ class SygusInterpol * @param interpol the solution to the sygus conjecture. * @param itp the interpolation predicate. */ - bool findInterpol(Expr& interpol, Node itp); + bool findInterpol(Node& interpol, Node itp); /** The SMT engine subSolver * @@ -179,10 +177,6 @@ class SygusInterpol std::unique_ptr<SmtEngine> d_subSolver; /** - * The logic for the local copy of SMT engine (d_subSolver). - */ - LogicInfo d_logic; - /** * symbols from axioms and conjecture. */ std::vector<Node> d_syms; |