From: Andrew Reynolds Date: Fri, 18 Dec 2020 16:01:17 +0000 (-0600) Subject: Simplify internal API for sygus (#5687) X-Git-Tag: cvc5-1.0.0~2421 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d4c7be8cbe1ac3b68c3bb5e2b08143f8324b5a1;p=cvc5.git Simplify internal API for sygus (#5687) This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8044508c7..b11a01628 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5615,7 +5615,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const Node res = getNodeManager()->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ - d_smtEngine->declareSygusVar(symbol, res, *sort.d_type); + d_smtEngine->declareSygusVar(res); return Term(this, res); @@ -5740,7 +5740,7 @@ Term Solver::synthFunHelper(const std::string& symbol, std::vector bvns = termVectorToNodes(boundVars); d_smtEngine->declareSynthFun( - symbol, fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); + fun, g == nullptr ? funType : *g->resolve().d_type, isInv, bvns); return Term(this, fun); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 48ed0d5c9..4c47587a6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1063,10 +1063,10 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) -------------------------------------------------------------------------- */ -void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type) +void SmtEngine::declareSygusVar(Node var) { SmtScope smts(this); - d_sygusSolver->declareSygusVar(id, var, type); + d_sygusSolver->declareSygusVar(var); if (Dump.isOn("raw-benchmark")) { getOutputManager().getPrinter().toStreamCmdDeclareVar( @@ -1075,15 +1075,14 @@ void SmtEngine::declareSygusVar(const std::string& id, Node var, TypeNode type) // don't need to set that the conjecture is stale } -void SmtEngine::declareSynthFun(const std::string& id, - Node func, +void SmtEngine::declareSynthFun(Node func, TypeNode sygusType, bool isInv, const std::vector& vars) { SmtScope smts(this); d_state->doPendingPops(); - d_sygusSolver->declareSynthFun(id, func, sygusType, isInv, vars); + d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars); // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we @@ -1095,6 +1094,14 @@ void SmtEngine::declareSynthFun(const std::string& id, getOutputManager().getDumpOut(), func, vars, isInv, sygusType); } } +void SmtEngine::declareSynthFun(Node func, + bool isInv, + const std::vector& vars) +{ + // use a null sygus type + TypeNode sygusType; + declareSynthFun(func, sygusType, isInv, vars); +} void SmtEngine::assertSygusConstraint(Node constraint) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 6f08359b5..091f69642 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -434,13 +434,13 @@ class CVC4_PUBLIC SmtEngine * which a function is being synthesized. Thus declared functions should use * this method as well. */ - void declareSygusVar(const std::string& id, Node var, TypeNode type); + void declareSygusVar(Node var); /** * Add a function-to-synthesize declaration. * - * The given type may not correspond to the actual function type but to a - * datatype encoding the syntax restrictions for the + * The given sygusType may not correspond to the actual function type of func + * but to a datatype encoding the syntax restrictions for the * function-to-synthesize. In this case this information is stored to be used * during solving. * @@ -451,11 +451,14 @@ class CVC4_PUBLIC SmtEngine * invariant. This information is necessary if we are dumping a command * corresponding to this declaration, so that it can be properly printed. */ - void declareSynthFun(const std::string& id, - Node func, - TypeNode type, + void declareSynthFun(Node func, + TypeNode sygusType, bool isInv, const std::vector& vars); + /** + * Same as above, without a sygus type. + */ + void declareSynthFun(Node func, bool isInv, const std::vector& vars); /** Add a regular sygus constraint.*/ void assertSygusConstraint(Node constraint); diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 42dbcd43e..a3a976d4a 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -23,6 +23,7 @@ #include "smt/smt_solver.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" +#include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/smt_engine_subsolver.h" using namespace CVC4::theory; @@ -44,24 +45,20 @@ SygusSolver::SygusSolver(SmtSolver& sms, SygusSolver::~SygusSolver() {} -void SygusSolver::declareSygusVar(const std::string& id, - Node var, - TypeNode type) +void SygusSolver::declareSygusVar(Node var) { - Trace("smt") << "SygusSolver::declareSygusVar: " << id << " " << var << " " - << type << "\n"; - Assert(var.getType() == type); + Trace("smt") << "SygusSolver::declareSygusVar: " << var << " " + << var.getType() << "\n"; d_sygusVars.push_back(var); // don't need to set that the conjecture is stale } -void SygusSolver::declareSynthFun(const std::string& id, - Node fn, +void SygusSolver::declareSynthFun(Node fn, TypeNode sygusType, bool isInv, const std::vector& vars) { - Trace("smt") << "SygusSolver::declareSynthFun: " << id << "\n"; + Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n"; NodeManager* nm = NodeManager::currentNM(); d_sygusFunSymbols.push_back(fn); if (!vars.empty()) @@ -72,7 +69,8 @@ void SygusSolver::declareSynthFun(const std::string& id, fn.setAttribute(ssfvla, bvl); } // whether sygus type encodes syntax restrictions - if (sygusType.isDatatype() && sygusType.getDType().isSygus()) + if (!sygusType.isNull() && sygusType.isDatatype() + && sygusType.getDType().isSygus()) { Node sym = nm->mkBoundVar("sfproxy", sygusType); // use an attribute to mark its grammar @@ -180,9 +178,6 @@ Result SygusSolver::checkSynth(Assertions& as) NodeManager* nm = NodeManager::currentNM(); // build synthesis conjecture from asserted constraints and declared // variables/functions - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - Node inst_attr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - Node sygusAttr = nm->mkNode(INST_PATTERN_LIST, inst_attr); std::vector bodyv; Trace("smt") << "Sygus : Constructing sygus constraint...\n"; size_t nconstraints = d_sygusConstraints.size(); @@ -200,15 +195,11 @@ Result SygusSolver::checkSynth(Assertions& as) } if (!d_sygusFunSymbols.empty()) { - Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusFunSymbols); - body = nm->mkNode(FORALL, boundVars, body, sygusAttr); + body = + quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body); } Trace("smt") << "...constructed forall " << body << std::endl; - // set attribute for synthesis conjecture - SygusAttribute sa; - sygusVar.setAttribute(sa, true); - Trace("smt") << "Check synthesis conjecture: " << body << std::endl; if (Dump.isOn("raw-benchmark")) { diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index c9de7b7e9..b0670ea27 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -62,7 +62,7 @@ class SygusSolver * which a function is being synthesized. Thus declared functions should use * this method as well. */ - void declareSygusVar(const std::string& id, Node var, TypeNode type); + void declareSygusVar(Node var); /** * Add a function-to-synthesize declaration. @@ -79,8 +79,7 @@ class SygusSolver * invariant. This information is necessary if we are dumping a command * corresponding to this declaration, so that it can be properly printed. */ - void declareSynthFun(const std::string& id, - Node func, + void declareSynthFun(Node func, TypeNode type, bool isInv, const std::vector& vars); diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 9fdb33700..3edec96c7 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -233,14 +233,6 @@ void SygusInterpol::mkSygusConjecture(Node itp, // set the sygus bound variable list Trace("sygus-interpol-debug") << "Set attributes..." << std::endl; itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared); - // sygus attribute - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - 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 ) @@ -339,12 +331,12 @@ bool SygusInterpol::solveInterpolation(const std::string& name, l.enableSygus(); subSolver->setLogic(l); - for (Node var : d_vars) + for (const Node& var : d_vars) { - subSolver->declareSygusVar(name, var, var.getType()); + subSolver->declareSygusVar(var); } std::vector vars_empty; - subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty); + subSolver->declareSynthFun(itp, grammarType, false, vars_empty); Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " << d_sygusConj << ", solving for " << d_sygusConj[0][0] << std::endl;