From: Ying Sheng Date: Mon, 3 Aug 2020 23:26:08 +0000 (-0700) Subject: Add implementation for SyGuS interpolation module (step4) (#4811) X-Git-Tag: cvc5-1.0.0~3048 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dad390f4216a9d279197a52b40b8e93696d4019;p=cvc5.git Add implementation for SyGuS interpolation module (step4) (#4811) This is the 4th step of adding interface for SyGuS Interpolation module. The whole change will be 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. The 4th step finished the implementation of the interpolation module. --- diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index cc97bb974..0d08140d3 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -204,7 +204,15 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType, Node SygusInterpol::mkPredicate(const std::string& name) { - Node itp; + NodeManager* nm = NodeManager::currentNM(); + // make the interpolation predicate to synthesize + Trace("sygus-interpol-debug") + << "Make interpolation predicate..." << std::endl; + TypeNode itpType = d_varTypesShared.empty() + ? nm->booleanType() + : nm->mkPredicateType(d_varTypesShared); + Node itp = nm->mkBoundVar(name.c_str(), itpType); + Trace("sygus-interpol-debug") << "...finish" << std::endl; return itp; } @@ -212,11 +220,100 @@ void SygusInterpol::mkSygusConjecture(Node itp, const std::vector& axioms, const Node& conj) { + NodeManager* nm = NodeManager::currentNM(); + // make the interpolation application to synthesize + Trace("sygus-interpol-debug") + << "Make interpolation predicate app..." << std::endl; + std::vector ichildren; + ichildren.push_back(itp); + ichildren.insert(ichildren.end(), d_varsShared.begin(), d_varsShared.end()); + Node itpApp = + d_varsShared.empty() ? itp : nm->mkNode(kind::APPLY_UF, ichildren); + Trace("sygus-interpol-debug") << "itpApp: " << itpApp << std::endl + << std::endl; + Trace("sygus-interpol-debug") << "...finish" << std::endl; + + // set the sygus bound variable list + Trace("sygus-interpol-debug") << "Set attributes..." << std::endl; + itp.setAttribute(theory::SygusSynthFunVarListAttribute(), d_ibvlShared); + // sygus attribute + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + theory::SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(kind::INST_ATTRIBUTE, sygusVar); + std::vector iplc; + iplc.push_back(instAttr); + Node instAttrList = nm->mkNode(kind::INST_PATTERN_LIST, iplc); + Trace("sygus-interpol-debug") << "...finish" << std::endl; + + // Fa( x ) + Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl; + Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms); + // Fa( x ) => A( x ) + Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp); + Trace("sygus-interpol-debug") + << "first implication: " << firstImplication << std::endl + << std::endl; + // A( x ) => Fc( x ) + Node Fc = conj; + Node secondImplication = nm->mkNode(kind::IMPLIES, itpApp, Fc); + Trace("sygus-interpol-debug") + << "second implication: " << secondImplication << std::endl + << std::endl; + // Fa( x ) => A( x ) ^ A( x ) => Fc( x ) + Node constraint = nm->mkNode(kind::AND, firstImplication, secondImplication); + constraint = constraint.substitute( + d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end()); + Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl; + constraint = theory::Rewriter::rewrite(constraint); + + d_sygusConj = constraint; + Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; } bool SygusInterpol::findInterpol(Expr& interpol, Node itp) { - return false; + // get the synthesis solution + std::map sols; + d_subSolver->getSynthSolutions(sols); + Assert(sols.size() == 1); + std::map::iterator its = sols.find(itp.toExpr()); + if (its == sols.end()) + { + Trace("sygus-interpol") + << "SmtEngine::getInterpol: could not find solution!" << std::endl; + throw RecoverableModalException( + "Could not find solution for get-interpol."); + return false; + } + Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is " + << its->second << std::endl; + Node interpoln = Node::fromExpr(its->second); + // replace back the created variables to original symbols. + Node interpoln_reduced; + if (interpoln.getKind() == kind::LAMBDA) + { + interpoln_reduced = interpoln[1]; + } + else + { + interpoln_reduced = interpoln; + } + if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0) + { + std::vector 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(); + return true; } bool SygusInterpol::SolveInterpolation(const std::string& name, @@ -225,6 +322,42 @@ bool SygusInterpol::SolveInterpolation(const std::string& name, const TypeNode& itpGType, Expr& 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(); + // get the logic + LogicInfo l = d_logic.getUnlockedCopy(); + // enable everything needed for sygus + l.enableSygus(); + d_subSolver->setLogic(l); + + collectSymbols(axioms, conj); + createVariables(itpGType.isNull()); + for (Node var : d_vars) + { + d_subSolver->declareSygusVar(name, var.toExpr(), var.getType().toType()); + } + std::vector vars_empty; + TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); + Node itp = mkPredicate(name); + d_subSolver->declareSynthFun( + name, itp.toExpr(), grammarType.toType(), false, vars_empty); + mkSygusConjecture(itp, axioms, conj); + Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " + << d_sygusConj << ", solving for " + << d_sygusConj[0][0].toExpr() << std::endl; + d_subSolver->assertSygusConstraint(d_sygusConj.toExpr()); + + Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..." + << std::endl; + Result r = d_subSolver->checkSynth(); + Trace("sygus-interpol") << " SmtEngine::getInterpol result: " << r + << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + return findInterpol(interpol, itp); + } return false; } diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index a79d583cd..0fe66694f 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -34,7 +34,7 @@ namespace quantifiers { * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc * then the sygus conjecture we construct is: * - * exists A. forall x. ( (Fa( x ) => A( x )) ^ (A( x ) => Fc( x )) ) + * (Fa( x ) => A( x )) ^ (A( x ) => Fc( x )) * * where A( x ) is a predicate over the free symbols of our input that are * shared between Fa and Fc. In other words, A( x ) must be implied by our @@ -141,6 +141,8 @@ class SygusInterpol /** * Make the sygus conjecture to be synthesis. + * The conjecture body is Fa( x ) => A( x ) ^ A( x ) => Fc( x ) as described + * above. * * @param itp the interpolation predicate. * @param axioms the assertions (Fa above)