From: Andrew Reynolds Date: Sat, 13 Jun 2020 00:18:42 +0000 (-0500) Subject: Move sygus datatype utility functions to their own file (#4595) X-Git-Tag: cvc5-1.0.0~3219 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60ed666d657bfcd69f48821c78a34696796df5fb;p=cvc5.git Move sygus datatype utility functions to their own file (#4595) Separates them from the core datatype utilities. Code move only. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 08725409b..a5160d2fe 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -417,6 +417,8 @@ libcvc4_add_sources( theory/care_graph.h theory/datatypes/datatypes_rewriter.cpp theory/datatypes/datatypes_rewriter.h + theory/datatypes/sygus_datatype_utils.cpp + theory/datatypes/sygus_datatype_utils.h theory/datatypes/sygus_extension.cpp theory/datatypes/sygus_extension.h theory/datatypes/sygus_simple_sym.cpp diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 77cb45f36..6918132d3 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -20,6 +20,7 @@ #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "options/datatypes_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" using namespace CVC4; diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp new file mode 100644 index 000000000..78cd0fc94 --- /dev/null +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -0,0 +1,741 @@ +/********************* */ +/*! \file sygus_datatype_utils.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 rewriter for the theory of (co)inductive datatypes. + ** + ** Implementation of rewriter for the theory of (co)inductive datatypes. + **/ + +#include "theory/datatypes/sygus_datatype_utils.h" + +#include "expr/dtype.h" +#include "expr/node_algorithm.h" +#include "expr/sygus_datatype.h" +#include "printer/sygus_print_callback.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/evaluator.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace datatypes { +namespace utils { + +Node applySygusArgs(const DType& dt, + Node op, + Node n, + const std::vector& args) +{ + if (n.getKind() == BOUND_VARIABLE) + { + Assert(n.hasAttribute(SygusVarNumAttribute())); + int vn = n.getAttribute(SygusVarNumAttribute()); + Assert(dt.getSygusVarList()[vn] == n); + return args[vn]; + } + // n is an application of operator op. + // We must compute the free variables in op to determine if there are + // any substitutions we need to make to n. + TNode val; + if (!op.hasAttribute(SygusVarFreeAttribute())) + { + std::unordered_set fvs; + if (expr::getFreeVariables(op, fvs)) + { + if (fvs.size() == 1) + { + for (const Node& v : fvs) + { + val = v; + } + } + else + { + val = op; + } + } + Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl; + op.setAttribute(SygusVarFreeAttribute(), val); + } + else + { + val = op.getAttribute(SygusVarFreeAttribute()); + } + if (val.isNull()) + { + return n; + } + if (val.getKind() == BOUND_VARIABLE) + { + // single substitution case + int vn = val.getAttribute(SygusVarNumAttribute()); + TNode sub = args[vn]; + return n.substitute(val, sub); + } + // do the full substitution + std::vector vars; + Node bvl = dt.getSygusVarList(); + for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++) + { + vars.push_back(bvl[i]); + } + return n.substitute(vars.begin(), vars.end(), args.begin(), args.end()); +} + +Kind getOperatorKindForSygusBuiltin(Node op) +{ + Assert(op.getKind() != BUILTIN); + if (op.getKind() == LAMBDA) + { + return APPLY_UF; + } + return NodeManager::getKindForFunction(op); +} + +struct SygusOpRewrittenAttributeId +{ +}; +typedef expr::Attribute + SygusOpRewrittenAttribute; + +Kind getEliminateKind(Kind ok) +{ + Kind nk = ok; + // We also must ensure that builtin operators which are eliminated + // during expand definitions are replaced by the proper operator. + if (ok == BITVECTOR_UDIV) + { + nk = BITVECTOR_UDIV_TOTAL; + } + else if (ok == BITVECTOR_UREM) + { + nk = BITVECTOR_UREM_TOTAL; + } + else if (ok == DIVISION) + { + nk = DIVISION_TOTAL; + } + else if (ok == INTS_DIVISION) + { + nk = INTS_DIVISION_TOTAL; + } + else if (ok == INTS_MODULUS) + { + nk = INTS_MODULUS_TOTAL; + } + return nk; +} + +Node eliminatePartialOperators(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + Kind ok = cur.getKind(); + Kind nk = getEliminateKind(ok); + if (nk != ok || childChanged) + { + ret = nm->mkNode(nk, children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +Node mkSygusTerm(const DType& dt, + unsigned i, + const std::vector& children, + bool doBetaReduction, + bool isExternal) +{ + Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i + << "] with children: " << children << std::endl; + Assert(i < dt.getNumConstructors()); + Assert(dt.isSygus()); + Assert(!dt[i].getSygusOp().isNull()); + Node op = dt[i].getSygusOp(); + Node opn = op; + if (!isExternal) + { + // Get the normalized version of the sygus operator. We do this by + // expanding definitions, rewriting it, and eliminating partial operators. + if (!op.hasAttribute(SygusOpRewrittenAttribute())) + { + if (op.isConst()) + { + // If it is a builtin operator, convert to total version if necessary. + // First, get the kind for the operator. + Kind ok = NodeManager::operatorToKind(op); + Trace("sygus-grammar-normalize-debug") + << "...builtin kind is " << ok << std::endl; + Kind nk = getEliminateKind(ok); + if (nk != ok) + { + Trace("sygus-grammar-normalize-debug") + << "...replace by builtin operator " << nk << std::endl; + opn = NodeManager::currentNM()->operatorOf(nk); + } + } + else + { + // Only expand definitions if the operator is not constant, since + // calling expandDefinitions on them should be a no-op. This check + // ensures we don't try to expand e.g. bitvector extract operators, + // whose type is undefined, and thus should not be passed to + // expandDefinitions. + opn = Node::fromExpr( + smt::currentSmtEngine()->expandDefinitions(op.toExpr())); + opn = Rewriter::rewrite(opn); + opn = eliminatePartialOperators(opn); + SygusOpRewrittenAttribute sora; + op.setAttribute(sora, opn); + } + } + else + { + opn = op.getAttribute(SygusOpRewrittenAttribute()); + } + } + return mkSygusTerm(opn, children, doBetaReduction); +} + +Node mkSygusTerm(Node op, + const std::vector& children, + bool doBetaReduction) +{ + Trace("dt-sygus-util") << "Operator is " << op << std::endl; + if (children.empty()) + { + // no children, return immediately + Trace("dt-sygus-util") << "...return direct op" << std::endl; + return op; + } + // if it is the any constant, we simply return the child + if (op.getAttribute(SygusAnyConstAttribute())) + { + Assert(children.size() == 1); + return children[0]; + } + std::vector schildren; + // get the kind of the operator + Kind ok = op.getKind(); + if (ok != BUILTIN) + { + if (ok == LAMBDA && doBetaReduction) + { + // Do immediate beta reduction. It suffices to use a normal substitution + // since neither op nor children have quantifiers, since they are + // generated by sygus grammars. + std::vector vars{op[0].begin(), op[0].end()}; + Assert(vars.size() == children.size()); + Node ret = op[1].substitute( + vars.begin(), vars.end(), children.begin(), children.end()); + Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl; + return ret; + } + else + { + schildren.push_back(op); + } + } + schildren.insert(schildren.end(), children.begin(), children.end()); + Node ret; + if (ok == BUILTIN) + { + ret = NodeManager::currentNM()->mkNode(op, schildren); + Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; + return ret; + } + // get the kind used for applying op + Kind otk = NodeManager::operatorToKind(op); + Trace("dt-sygus-util") << "operator kind is " << otk << std::endl; + if (otk != UNDEFINED_KIND) + { + // If it is an APPLY_UF operator, we should have at least an operator and + // a child. + Assert(otk != APPLY_UF || schildren.size() != 1); + ret = NodeManager::currentNM()->mkNode(otk, schildren); + Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; + return ret; + } + Kind tok = getOperatorKindForSygusBuiltin(op); + if (schildren.size() == 1 && tok == UNDEFINED_KIND) + { + ret = schildren[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(tok, schildren); + } + Trace("dt-sygus-util") << "...return " << ret << std::endl; + return ret; +} + +struct SygusToBuiltinTermAttributeId +{ +}; +typedef expr::Attribute + SygusToBuiltinTermAttribute; + +Node sygusToBuiltin(Node n, bool isExternal) +{ + Assert(n.isConst()); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + unsigned index; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + if (cur.getKind() == APPLY_CONSTRUCTOR) + { + if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute())) + { + visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute()); + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else + { + // non-datatypes are themselves + visited[cur] = cur; + } + } + else if (it->second.isNull()) + { + Node ret = cur; + Assert(cur.getKind() == APPLY_CONSTRUCTOR); + const DType& dt = cur.getType().getDType(); + // Non sygus-datatype terms are also themselves. Notice we treat the + // case of non-sygus datatypes this way since it avoids computing + // the type / datatype of the node in the pre-traversal above. The + // case of non-sygus datatypes is very rare, so the extra addition to + // visited is justified performance-wise. + if (dt.isSygus()) + { + std::vector children; + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + children.push_back(it->second); + } + index = indexOf(cur.getOperator()); + ret = mkSygusTerm(dt, index, children, true, isExternal); + } + visited[cur] = ret; + // cache + if (!isExternal) + { + SygusToBuiltinTermAttribute stbt; + cur.setAttribute(stbt, ret); + } + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +Node sygusToBuiltinEval(Node n, const std::vector& args) +{ + NodeManager* nm = NodeManager::currentNM(); + Evaluator eval; + // constant arguments? + bool constArgs = true; + for (const Node& a : args) + { + if (!a.isConst()) + { + constArgs = false; + break; + } + } + std::vector eargs; + bool svarsInit = false; + std::vector svars; + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + unsigned index; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + TypeNode tn = cur.getType(); + if (!tn.isDatatype() || !tn.getDType().isSygus()) + { + visited[cur] = cur; + } + else if (cur.isConst()) + { + // convert to builtin term + Node bt = sygusToBuiltin(cur); + // run the evaluator if possible + if (!svarsInit) + { + svarsInit = true; + TypeNode type = cur.getType(); + Node varList = type.getDType().getSygusVarList(); + for (const Node& v : varList) + { + svars.push_back(v); + } + } + Assert(args.size() == svars.size()); + // try evaluation if we have constant arguments + Node ret = constArgs ? eval.eval(bt, svars, args) : Node::null(); + if (ret.isNull()) + { + // if evaluation was not available, use a substitution + ret = bt.substitute( + svars.begin(), svars.end(), args.begin(), args.end()); + } + visited[cur] = ret; + } + else + { + if (cur.getKind() == APPLY_CONSTRUCTOR) + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + else + { + // it is the evaluation of this term on the arguments + if (eargs.empty()) + { + eargs.push_back(cur); + eargs.insert(eargs.end(), args.begin(), args.end()); + } + else + { + eargs[0] = cur; + } + visited[cur] = nm->mkNode(DT_SYGUS_EVAL, eargs); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + Assert(cur.getKind() == APPLY_CONSTRUCTOR); + const DType& dt = cur.getType().getDType(); + // non sygus-datatype terms are also themselves + if (dt.isSygus()) + { + std::vector children; + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + children.push_back(it->second); + } + index = indexOf(cur.getOperator()); + // apply to arguments + ret = mkSygusTerm(dt, index, children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +void getFreeSymbolsSygusType(TypeNode sdt, + std::unordered_set& syms) +{ + // datatype types we need to process + std::vector typeToProcess; + // datatype types we have processed + std::map typesProcessed; + typeToProcess.push_back(sdt); + while (!typeToProcess.empty()) + { + std::vector typeNextToProcess; + for (const TypeNode& curr : typeToProcess) + { + Assert(curr.isDatatype() && curr.getDType().isSygus()); + const DType& dtc = curr.getDType(); + for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) + { + // collect the symbols from the operator + Node op = dtc[j].getSygusOp(); + expr::getSymbols(op, syms); + // traverse the argument types + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = dtc[j].getArgType(k); + if (!argt.isDatatype() || !argt.getDType().isSygus()) + { + // not a sygus datatype + continue; + } + if (typesProcessed.find(argt) == typesProcessed.end()) + { + typeNextToProcess.push_back(argt); + } + } + } + } + typeToProcess.clear(); + typeToProcess.insert(typeToProcess.end(), + typeNextToProcess.begin(), + typeNextToProcess.end()); + } +} + +TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, + const std::vector& syms, + const std::vector& vars) +{ + NodeManager* nm = NodeManager::currentNM(); + const DType& sdtd = sdt.getDType(); + // compute the new formal argument list + std::vector formalVars; + Node prevVarList = sdtd.getSygusVarList(); + if (!prevVarList.isNull()) + { + for (const Node& v : prevVarList) + { + // if it is not being replaced + if (std::find(syms.begin(), syms.end(), v) != syms.end()) + { + formalVars.push_back(v); + } + } + } + for (const Node& v : vars) + { + if (v.getKind() == BOUND_VARIABLE) + { + formalVars.push_back(v); + } + } + // make the sygus variable list for the formal argument list + Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + // must convert all constructors to version with variables in "vars" + std::vector sdts; + std::set unres; + + Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; + Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; + + // datatype types we need to process + std::vector dtToProcess; + // datatype types we have processed + std::map dtProcessed; + dtToProcess.push_back(sdt); + std::stringstream ssutn0; + ssutn0 << sdtd.getName() << "_s"; + TypeNode abdTNew = + nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + unres.insert(abdTNew.toType()); + dtProcessed[sdt] = abdTNew; + + // We must convert all symbols in the sygus datatype type sdt to + // apply the substitution { syms -> vars }, where syms is the free + // variables of the input problem, and vars is the formal argument list + // of the function-to-synthesize. + + // We are traversing over the subfield types of the datatype to convert + // them into the form described above. + while (!dtToProcess.empty()) + { + std::vector dtNextToProcess; + for (const TypeNode& curr : dtToProcess) + { + Assert(curr.isDatatype() && curr.getDType().isSygus()); + const DType& dtc = curr.getDType(); + std::stringstream ssdtn; + ssdtn << dtc.getName() << "_s"; + sdts.push_back(SygusDatatype(ssdtn.str())); + Trace("dtsygus-gen-debug") + << "Process datatype " << sdts.back().getName() << "..." << std::endl; + for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) + { + Node op = dtc[j].getSygusOp(); + // apply the substitution to the argument + Node ops = + op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("dtsygus-gen-debug") << " Process constructor " << op << " / " + << ops << "..." << std::endl; + std::vector cargs; + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = dtc[j].getArgType(k); + std::map::iterator itdp = dtProcessed.find(argt); + TypeNode argtNew; + if (itdp == dtProcessed.end()) + { + std::stringstream ssutn; + ssutn << argt.getDType().getName() << "_s"; + argtNew = + nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew + << " for " << argt << std::endl; + unres.insert(argtNew.toType()); + dtProcessed[argt] = argtNew; + dtNextToProcess.push_back(argt); + } + else + { + argtNew = itdp->second; + } + Trace("dtsygus-gen-debug") + << " Arg #" << k << ": " << argtNew << std::endl; + cargs.push_back(argtNew); + } + // callback prints as the expression + std::shared_ptr spc; + std::vector args; + if (op.getKind() == LAMBDA) + { + Node opBody = op[1]; + for (const Node& v : op[0]) + { + args.push_back(v.toExpr()); + } + spc = std::make_shared( + opBody.toExpr(), args); + } + else if (cargs.empty()) + { + spc = std::make_shared(op.toExpr(), + args); + } + std::stringstream ss; + ss << ops.getKind(); + Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; + sdts.back().addConstructor(ops, ss.str(), cargs, spc); + } + Trace("dtsygus-gen-debug") + << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; + TypeNode stn = dtc.getSygusType(); + sdts.back().initializeDatatype( + stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); + } + dtToProcess.clear(); + dtToProcess.insert( + dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); + } + Trace("dtsygus-gen-debug") + << "Make " << sdts.size() << " datatype types..." << std::endl; + // extract the datatypes + std::vector datatypes; + for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) + { + datatypes.push_back(sdts[i].getDatatype()); + } + // make the datatype types + std::vector datatypeTypes = + nm->toExprManager()->mkMutualDatatypeTypes( + datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]); + if (Trace.isOn("dtsygus-gen-debug")) + { + Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; + for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) + { + const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType(); + Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; + for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) + { + for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) + { + if (!dtj[k].getArgType(l).isDatatype()) + { + Trace("dtsygus-gen-debug") + << "Argument " << l << " of " << dtj[k] + << " is not datatype : " << dtj[k].getArgType(l) << std::endl; + AlwaysAssert(false); + } + } + } + } + } + return sdtS; +} + +} // namespace utils +} // namespace datatypes +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h new file mode 100644 index 000000000..242f3ebc1 --- /dev/null +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -0,0 +1,229 @@ +/********************* */ +/*! \file sygus_datatype_utils.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 Util functions for sygus datatypes + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H +#define CVC4__THEORY__STRINGS__SYGUS_DATATYPE_UTILS_H + +#include + +#include "expr/dtype.h" +#include "expr/node.h" +#include "expr/node_manager_attributes.h" +#include "theory/datatypes/theory_datatypes_utils.h" + +namespace CVC4 { +namespace theory { + +// ----------------------- sygus datatype attributes +/** sygus var num */ +struct SygusVarNumAttributeId +{ +}; +typedef expr::Attribute SygusVarNumAttribute; + +/** + * Attribute true for enumerators whose current model values were registered by + * the datatypes sygus solver, and were not excluded by sygus symmetry breaking. + * This is set by the datatypes sygus solver during LAST_CALL effort checks for + * each active sygus enumerator. + */ +struct SygusSymBreakOkAttributeId +{ +}; +typedef expr::Attribute + SygusSymBreakOkAttribute; + +/** sygus var free + * + * This attribute is used to mark whether sygus operators have free occurrences + * of variables from the formal argument list of the function-to-synthesize. + * + * We store three possible cases for sygus operators op: + * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null() + * In this case, op has no free variables from the formal argument list of the + * function-to-synthesize. + * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable. + * In this case, op has exactly one free variable, v. + * (3) op.getAttribute(SygusVarFreeAttribute())==op + * In this case, op has an arbitrary set (cardinality >1) of free variables from + * the formal argument list of the function to synthesize. + * + * This attribute is used to compute applySygusArgs below. + */ +struct SygusVarFreeAttributeId +{ +}; +typedef expr::Attribute SygusVarFreeAttribute; +// ----------------------- end sygus datatype attributes + +namespace datatypes { +namespace utils { + + +/** get operator kind for sygus builtin + * + * This returns the Kind corresponding to applications of the operator op + * when building the builtin version of sygus terms. This is used by the + * function mkSygusTerm. + */ +Kind getOperatorKindForSygusBuiltin(Node op); +/** + * Returns the total version of Kind k if it is a partial operator, or + * otherwise k itself. + */ +Kind getEliminateKind(Kind k); +/** + * Returns a version of n where all partial functions such as bvudiv + * have been replaced by their total versions like bvudiv_total. + */ +Node eliminatePartialOperators(Node n); +/** make sygus term + * + * This function returns a builtin term f( children[0], ..., children[n] ) + * where f is the builtin op that the i^th constructor of sygus datatype dt + * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated + * via beta reduction. + * + * If isExternal is true, then the returned term respects the original grammar + * that was provided. This includes the use of defined functions. + */ +Node mkSygusTerm(const DType& dt, + unsigned i, + const std::vector& children, + bool doBetaReduction = true, + bool isExternal = false); +/** + * Same as above, but we already have the sygus operator op. The above method + * is syntax sugar for calling this method on dt[i].getSygusOp(). + */ +Node mkSygusTerm(Node op, + const std::vector& children, + bool doBetaReduction = true); +/** + * n is a builtin term that is an application of operator op. + * + * This returns an n' such that (eval n args) is n', where n' is a instance of + * n for the appropriate substitution. + * + * For example, given a function-to-synthesize with formal argument list (x,y), + * say we have grammar: + * A -> A+A | A+x | A+(x+y) | y + * These lead to constructors with sygus ops: + * C1 / (lambda w1 w2. w1+w2) + * C2 / (lambda w1. w1+x) + * C3 / (lambda w1. w1+(x+y)) + * C4 / y + * Examples of calling this function: + * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2). + * applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1. w1+3) t1). + * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1). + * applySygusArgs( dt, C4, y, { 3, 5 } ) + * ... returns 5. + * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4, + * to cache the results of whether the evaluation of this constructor needs + * a substitution over the formal argument list of the function-to-synthesize. + */ +Node applySygusArgs(const DType& dt, + Node op, + Node n, + const std::vector& args); +/** Sygus to builtin + * + * This method converts a constant term of SyGuS datatype type to its builtin + * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns + * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y + * respectively. + * + * If isExternal is true, then the returned term respects the original grammar + * that was provided. This includes the use of defined functions. This argument + * should typically be false, unless we are e.g. exporting the value of the + * term as a final solution. + */ +Node sygusToBuiltin(Node c, bool isExternal = false); +/** Sygus to builtin eval + * + * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that + * n does not necessarily need to be a constant. + * + * It does so by (1) converting constant subterms of n to builtin terms and + * evaluating them on the arguments args, (2) unfolding non-constant + * applications of sygus constructors in n with respect to args and (3) + * converting all other non-constant subterms of n to applications of + * DT_SYGUS_EVAL. + * + * For example, if + * n = C_+( C_*( C_x(), C_y() ), n' ), and args = { 3, 4 } + * where n' is a variable, then this method returns: + * 12 + (DT_SYGUS_EVAL n' 3 4) + * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin + * equivalent x*y and evaluated under the substition { x -> 3, x -> 4 } giving + * 12. The subterm n' is non-constant and thus we return its evaluation under + * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor + * is C_+, these terms are added together to give the result. + */ +Node sygusToBuiltinEval(Node n, const std::vector& args); + +/** Get free symbols in a sygus datatype type + * + * Add the free symbols (expr::getSymbols) in terms that can be generated by + * sygus datatype sdt to the set syms. For example, given sdt encodes the + * grammar: + * G -> a | +( b, G ) | c | e + * We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols + * excludes variables whose kind is BOUND_VARIABLE. + */ +void getFreeSymbolsSygusType(TypeNode sdt, + std::unordered_set& syms); + +/** Substitute and generalize a sygus datatype type + * + * This transforms a sygus datatype sdt into another one sdt' that generates + * terms t such that t * { vars -> syms } is generated by sdt. + * + * The arguments syms and vars should be vectors of the same size and types. + * It is recommended that the arguments in syms and vars should be variables + * (return true for .isVar()) but this is not required. + * + * The variables in vars of type BOUND_VARIABLE are added to the + * formal argument list of t. Other symbols are not. + * + * For example, given sdt encodes the grammar: + * G -> a | +( b, G ) | c | e + * Let syms = { a, b, c } and vars = { x_a, x_b, d }, where x_a and x_b have + * type BOUND_VARIABLE and d does not. + * The returned type encodes the grammar: + * G' -> x_a | +( x_b, G' ) | d | e + * Additionally, x_a and x_b are treated as formal arguments of a function + * to synthesize whose syntax restrictions are specified by G'. + * + * This method traverses the type definition of the datatype corresponding to + * the argument sdt. + */ +TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, + const std::vector& syms, + const std::vector& vars); + +// ------------------------ end sygus utils + +} // namespace utils +} // namespace datatypes +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index f22e0e6d5..f4b618427 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -21,6 +21,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_explain.h" diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index ea67ab79d..0c30280af 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -17,13 +17,6 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "expr/dtype.h" -#include "expr/node_algorithm.h" -#include "expr/sygus_datatype.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/evaluator.h" -#include "theory/rewriter.h" -#include "printer/sygus_print_callback.h" using namespace CVC4; using namespace CVC4::kind; @@ -33,311 +26,6 @@ namespace theory { namespace datatypes { namespace utils { -Node applySygusArgs(const DType& dt, - Node op, - Node n, - const std::vector& args) -{ - if (n.getKind() == BOUND_VARIABLE) - { - Assert(n.hasAttribute(SygusVarNumAttribute())); - int vn = n.getAttribute(SygusVarNumAttribute()); - Assert(dt.getSygusVarList()[vn] == n); - return args[vn]; - } - // n is an application of operator op. - // We must compute the free variables in op to determine if there are - // any substitutions we need to make to n. - TNode val; - if (!op.hasAttribute(SygusVarFreeAttribute())) - { - std::unordered_set fvs; - if (expr::getFreeVariables(op, fvs)) - { - if (fvs.size() == 1) - { - for (const Node& v : fvs) - { - val = v; - } - } - else - { - val = op; - } - } - Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl; - op.setAttribute(SygusVarFreeAttribute(), val); - } - else - { - val = op.getAttribute(SygusVarFreeAttribute()); - } - if (val.isNull()) - { - return n; - } - if (val.getKind() == BOUND_VARIABLE) - { - // single substitution case - int vn = val.getAttribute(SygusVarNumAttribute()); - TNode sub = args[vn]; - return n.substitute(val, sub); - } - // do the full substitution - std::vector vars; - Node bvl = dt.getSygusVarList(); - for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++) - { - vars.push_back(bvl[i]); - } - return n.substitute(vars.begin(), vars.end(), args.begin(), args.end()); -} - -Kind getOperatorKindForSygusBuiltin(Node op) -{ - Assert(op.getKind() != BUILTIN); - if (op.getKind() == LAMBDA) - { - return APPLY_UF; - } - TypeNode tn = op.getType(); - if (tn.isConstructor()) - { - return APPLY_CONSTRUCTOR; - } - else if (tn.isSelector()) - { - return APPLY_SELECTOR; - } - else if (tn.isTester()) - { - return APPLY_TESTER; - } - else if (tn.isFunction()) - { - return APPLY_UF; - } - return UNDEFINED_KIND; -} - -struct SygusOpRewrittenAttributeId -{ -}; -typedef expr::Attribute - SygusOpRewrittenAttribute; - -Kind getEliminateKind(Kind ok) -{ - Kind nk = ok; - // We also must ensure that builtin operators which are eliminated - // during expand definitions are replaced by the proper operator. - if (ok == BITVECTOR_UDIV) - { - nk = BITVECTOR_UDIV_TOTAL; - } - else if (ok == BITVECTOR_UREM) - { - nk = BITVECTOR_UREM_TOTAL; - } - else if (ok == DIVISION) - { - nk = DIVISION_TOTAL; - } - else if (ok == INTS_DIVISION) - { - nk = INTS_DIVISION_TOTAL; - } - else if (ok == INTS_MODULUS) - { - nk = INTS_MODULUS_TOTAL; - } - return nk; -} - -Node eliminatePartialOperators(Node n) -{ - NodeManager* nm = NodeManager::currentNM(); - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - TNode cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - - if (it == visited.end()) - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else if (it->second.isNull()) - { - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - Kind ok = cur.getKind(); - Kind nk = getEliminateKind(ok); - if (nk != ok || childChanged) - { - ret = nm->mkNode(nk, children); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - -Node mkSygusTerm(const DType& dt, - unsigned i, - const std::vector& children, - bool doBetaReduction, - bool isExternal) -{ - Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i - << "] with children: " << children << std::endl; - Assert(i < dt.getNumConstructors()); - Assert(dt.isSygus()); - Assert(!dt[i].getSygusOp().isNull()); - Node op = dt[i].getSygusOp(); - Node opn = op; - if (!isExternal) - { - // Get the normalized version of the sygus operator. We do this by - // expanding definitions, rewriting it, and eliminating partial operators. - if (!op.hasAttribute(SygusOpRewrittenAttribute())) - { - if (op.isConst()) - { - // If it is a builtin operator, convert to total version if necessary. - // First, get the kind for the operator. - Kind ok = NodeManager::operatorToKind(op); - Trace("sygus-grammar-normalize-debug") - << "...builtin kind is " << ok << std::endl; - Kind nk = getEliminateKind(ok); - if (nk != ok) - { - Trace("sygus-grammar-normalize-debug") - << "...replace by builtin operator " << nk << std::endl; - opn = NodeManager::currentNM()->operatorOf(nk); - } - } - else - { - // Only expand definitions if the operator is not constant, since - // calling expandDefinitions on them should be a no-op. This check - // ensures we don't try to expand e.g. bitvector extract operators, - // whose type is undefined, and thus should not be passed to - // expandDefinitions. - opn = Node::fromExpr( - smt::currentSmtEngine()->expandDefinitions(op.toExpr())); - opn = Rewriter::rewrite(opn); - opn = eliminatePartialOperators(opn); - SygusOpRewrittenAttribute sora; - op.setAttribute(sora, opn); - } - } - else - { - opn = op.getAttribute(SygusOpRewrittenAttribute()); - } - } - return mkSygusTerm(opn, children, doBetaReduction); -} - -Node mkSygusTerm(Node op, - const std::vector& children, - bool doBetaReduction) -{ - Trace("dt-sygus-util") << "Operator is " << op << std::endl; - if (children.empty()) - { - // no children, return immediately - Trace("dt-sygus-util") << "...return direct op" << std::endl; - return op; - } - // if it is the any constant, we simply return the child - if (op.getAttribute(SygusAnyConstAttribute())) - { - Assert(children.size() == 1); - return children[0]; - } - std::vector schildren; - // get the kind of the operator - Kind ok = op.getKind(); - if (ok != BUILTIN) - { - if (ok == LAMBDA && doBetaReduction) - { - // Do immediate beta reduction. It suffices to use a normal substitution - // since neither op nor children have quantifiers, since they are - // generated by sygus grammars. - std::vector vars{op[0].begin(), op[0].end()}; - Assert(vars.size() == children.size()); - Node ret = op[1].substitute( - vars.begin(), vars.end(), children.begin(), children.end()); - Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl; - return ret; - } - else - { - schildren.push_back(op); - } - } - schildren.insert(schildren.end(), children.begin(), children.end()); - Node ret; - if (ok == BUILTIN) - { - ret = NodeManager::currentNM()->mkNode(op, schildren); - Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; - return ret; - } - // get the kind used for applying op - Kind otk = NodeManager::operatorToKind(op); - Trace("dt-sygus-util") << "operator kind is " << otk << std::endl; - if (otk != UNDEFINED_KIND) - { - // If it is an APPLY_UF operator, we should have at least an operator and - // a child. - Assert(otk != APPLY_UF || schildren.size() != 1); - ret = NodeManager::currentNM()->mkNode(otk, schildren); - Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; - return ret; - } - Kind tok = getOperatorKindForSygusBuiltin(op); - if (schildren.size() == 1 && tok == UNDEFINED_KIND) - { - ret = schildren[0]; - } - else - { - ret = NodeManager::currentNM()->mkNode(tok, schildren); - } - Trace("dt-sygus-util") << "...return " << ret << std::endl; - return ret; -} - /** get instantiate cons */ Node getInstCons(Node n, const DType& dt, int index) { @@ -515,420 +203,6 @@ bool checkClash(Node n1, Node n2, std::vector& rew) return false; } -struct SygusToBuiltinTermAttributeId -{ -}; -typedef expr::Attribute - SygusToBuiltinTermAttribute; - -Node sygusToBuiltin(Node n, bool isExternal) -{ - Assert(n.isConst()); - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - TNode cur; - unsigned index; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - if (it == visited.end()) - { - if (cur.getKind() == APPLY_CONSTRUCTOR) - { - if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute())) - { - visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute()); - } - else - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - } - else - { - // non-datatypes are themselves - visited[cur] = cur; - } - } - else if (it->second.isNull()) - { - Node ret = cur; - Assert(cur.getKind() == APPLY_CONSTRUCTOR); - const DType& dt = cur.getType().getDType(); - // Non sygus-datatype terms are also themselves. Notice we treat the - // case of non-sygus datatypes this way since it avoids computing - // the type / datatype of the node in the pre-traversal above. The - // case of non-sygus datatypes is very rare, so the extra addition to - // visited is justified performance-wise. - if (dt.isSygus()) - { - std::vector children; - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - children.push_back(it->second); - } - index = indexOf(cur.getOperator()); - ret = mkSygusTerm(dt, index, children, true, isExternal); - } - visited[cur] = ret; - // cache - if (!isExternal) - { - SygusToBuiltinTermAttribute stbt; - cur.setAttribute(stbt, ret); - } - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - -Node sygusToBuiltinEval(Node n, const std::vector& args) -{ - NodeManager* nm = NodeManager::currentNM(); - Evaluator eval; - // constant arguments? - bool constArgs = true; - for (const Node& a : args) - { - if (!a.isConst()) - { - constArgs = false; - break; - } - } - std::vector eargs; - bool svarsInit = false; - std::vector svars; - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - TNode cur; - unsigned index; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - if (it == visited.end()) - { - TypeNode tn = cur.getType(); - if (!tn.isDatatype() || !tn.getDType().isSygus()) - { - visited[cur] = cur; - } - else if (cur.isConst()) - { - // convert to builtin term - Node bt = sygusToBuiltin(cur); - // run the evaluator if possible - if (!svarsInit) - { - svarsInit = true; - TypeNode type = cur.getType(); - Node varList = type.getDType().getSygusVarList(); - for (const Node& v : varList) - { - svars.push_back(v); - } - } - Assert(args.size() == svars.size()); - // try evaluation if we have constant arguments - Node ret = constArgs ? eval.eval(bt, svars, args) : Node::null(); - if (ret.isNull()) - { - // if evaluation was not available, use a substitution - ret = bt.substitute( - svars.begin(), svars.end(), args.begin(), args.end()); - } - visited[cur] = ret; - } - else - { - if (cur.getKind() == APPLY_CONSTRUCTOR) - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else - { - // it is the evaluation of this term on the arguments - if (eargs.empty()) - { - eargs.push_back(cur); - eargs.insert(eargs.end(), args.begin(), args.end()); - } - else - { - eargs[0] = cur; - } - visited[cur] = nm->mkNode(DT_SYGUS_EVAL, eargs); - } - } - } - else if (it->second.isNull()) - { - Node ret = cur; - Assert(cur.getKind() == APPLY_CONSTRUCTOR); - const DType& dt = cur.getType().getDType(); - // non sygus-datatype terms are also themselves - if (dt.isSygus()) - { - std::vector children; - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - children.push_back(it->second); - } - index = indexOf(cur.getOperator()); - // apply to arguments - ret = mkSygusTerm(dt, index, children); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - -void getFreeSymbolsSygusType(TypeNode sdt, - std::unordered_set& syms) -{ - // datatype types we need to process - std::vector typeToProcess; - // datatype types we have processed - std::map typesProcessed; - typeToProcess.push_back(sdt); - while (!typeToProcess.empty()) - { - std::vector typeNextToProcess; - for (const TypeNode& curr : typeToProcess) - { - Assert(curr.isDatatype() && curr.getDType().isSygus()); - const DType& dtc = curr.getDType(); - for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) - { - // collect the symbols from the operator - Node op = dtc[j].getSygusOp(); - expr::getSymbols(op, syms); - // traverse the argument types - for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) - { - TypeNode argt = dtc[j].getArgType(k); - if (!argt.isDatatype() || !argt.getDType().isSygus()) - { - // not a sygus datatype - continue; - } - if (typesProcessed.find(argt) == typesProcessed.end()) - { - typeNextToProcess.push_back(argt); - } - } - } - } - typeToProcess.clear(); - typeToProcess.insert(typeToProcess.end(), - typeNextToProcess.begin(), - typeNextToProcess.end()); - } -} - -TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, - const std::vector& syms, - const std::vector& vars) -{ - NodeManager* nm = NodeManager::currentNM(); - const DType& sdtd = sdt.getDType(); - // compute the new formal argument list - std::vector formalVars; - Node prevVarList = sdtd.getSygusVarList(); - if (!prevVarList.isNull()) - { - for (const Node& v : prevVarList) - { - // if it is not being replaced - if (std::find(syms.begin(), syms.end(), v) != syms.end()) - { - formalVars.push_back(v); - } - } - } - for (const Node& v : vars) - { - if (v.getKind() == BOUND_VARIABLE) - { - formalVars.push_back(v); - } - } - // make the sygus variable list for the formal argument list - Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars); - Trace("sygus-abduct-debug") << "...finish" << std::endl; - - // must convert all constructors to version with variables in "vars" - std::vector sdts; - std::set unres; - - Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; - Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; - - // datatype types we need to process - std::vector dtToProcess; - // datatype types we have processed - std::map dtProcessed; - dtToProcess.push_back(sdt); - std::stringstream ssutn0; - ssutn0 << sdtd.getName() << "_s"; - TypeNode abdTNew = - nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); - unres.insert(abdTNew.toType()); - dtProcessed[sdt] = abdTNew; - - // We must convert all symbols in the sygus datatype type sdt to - // apply the substitution { syms -> vars }, where syms is the free - // variables of the input problem, and vars is the formal argument list - // of the function-to-synthesize. - - // We are traversing over the subfield types of the datatype to convert - // them into the form described above. - while (!dtToProcess.empty()) - { - std::vector dtNextToProcess; - for (const TypeNode& curr : dtToProcess) - { - Assert(curr.isDatatype() && curr.getDType().isSygus()); - const DType& dtc = curr.getDType(); - std::stringstream ssdtn; - ssdtn << dtc.getName() << "_s"; - sdts.push_back(SygusDatatype(ssdtn.str())); - Trace("dtsygus-gen-debug") - << "Process datatype " << sdts.back().getName() << "..." << std::endl; - for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) - { - Node op = dtc[j].getSygusOp(); - // apply the substitution to the argument - Node ops = - op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); - Trace("dtsygus-gen-debug") << " Process constructor " << op << " / " - << ops << "..." << std::endl; - std::vector cargs; - for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) - { - TypeNode argt = dtc[j].getArgType(k); - std::map::iterator itdp = dtProcessed.find(argt); - TypeNode argtNew; - if (itdp == dtProcessed.end()) - { - std::stringstream ssutn; - ssutn << argt.getDType().getName() << "_s"; - argtNew = - nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); - Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew - << " for " << argt << std::endl; - unres.insert(argtNew.toType()); - dtProcessed[argt] = argtNew; - dtNextToProcess.push_back(argt); - } - else - { - argtNew = itdp->second; - } - Trace("dtsygus-gen-debug") - << " Arg #" << k << ": " << argtNew << std::endl; - cargs.push_back(argtNew); - } - // callback prints as the expression - std::shared_ptr spc; - std::vector args; - if (op.getKind() == LAMBDA) - { - Node opBody = op[1]; - for (const Node& v : op[0]) - { - args.push_back(v.toExpr()); - } - spc = std::make_shared( - opBody.toExpr(), args); - } - else if (cargs.empty()) - { - spc = std::make_shared(op.toExpr(), - args); - } - std::stringstream ss; - ss << ops.getKind(); - Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; - sdts.back().addConstructor(ops, ss.str(), cargs, spc); - } - Trace("dtsygus-gen-debug") - << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; - TypeNode stn = dtc.getSygusType(); - sdts.back().initializeDatatype( - stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); - } - dtToProcess.clear(); - dtToProcess.insert( - dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); - } - Trace("dtsygus-gen-debug") - << "Make " << sdts.size() << " datatype types..." << std::endl; - // extract the datatypes - std::vector datatypes; - for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) - { - datatypes.push_back(sdts[i].getDatatype()); - } - // make the datatype types - std::vector datatypeTypes = - nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]); - if (Trace.isOn("dtsygus-gen-debug")) - { - Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; - for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) - { - const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType(); - Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; - for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) - { - for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) - { - if (!dtj[k].getArgType(l).isDatatype()) - { - Trace("dtsygus-gen-debug") - << "Argument " << l << " of " << dtj[k] - << " is not datatype : " << dtj[k].getArgType(l) << std::endl; - AlwaysAssert(false); - } - } - } - } - } - return sdtS; -} - } // namespace utils } // namespace datatypes } // namespace theory diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 038922f37..590250df5 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -27,49 +27,6 @@ namespace CVC4 { namespace theory { - -// ----------------------- sygus datatype attributes -/** sygus var num */ -struct SygusVarNumAttributeId -{ -}; -typedef expr::Attribute SygusVarNumAttribute; - -/** - * Attribute true for enumerators whose current model values were registered by - * the datatypes sygus solver, and were not excluded by sygus symmetry breaking. - * This is set by the datatypes sygus solver during LAST_CALL effort checks for - * each active sygus enumerator. - */ -struct SygusSymBreakOkAttributeId -{ -}; -typedef expr::Attribute - SygusSymBreakOkAttribute; - -/** sygus var free - * - * This attribute is used to mark whether sygus operators have free occurrences - * of variables from the formal argument list of the function-to-synthesize. - * - * We store three possible cases for sygus operators op: - * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null() - * In this case, op has no free variables from the formal argument list of the - * function-to-synthesize. - * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable. - * In this case, op has exactly one free variable, v. - * (3) op.getAttribute(SygusVarFreeAttribute())==op - * In this case, op has an arbitrary set (cardinality >1) of free variables from - * the formal argument list of the function to synthesize. - * - * This attribute is used to compute applySygusArgs below. - */ -struct SygusVarFreeAttributeId -{ -}; -typedef expr::Attribute SygusVarFreeAttribute; -// ----------------------- end sygus datatype attributes - namespace datatypes { namespace utils { @@ -137,156 +94,6 @@ bool isNullaryConstructor(const DTypeConstructor& c); */ bool checkClash(Node n1, Node n2, std::vector& rew); -// ------------------------ sygus utils - -/** get operator kind for sygus builtin - * - * This returns the Kind corresponding to applications of the operator op - * when building the builtin version of sygus terms. This is used by the - * function mkSygusTerm. - */ -Kind getOperatorKindForSygusBuiltin(Node op); -/** - * Returns the total version of Kind k if it is a partial operator, or - * otherwise k itself. - */ -Kind getEliminateKind(Kind k); -/** - * Returns a version of n where all partial functions such as bvudiv - * have been replaced by their total versions like bvudiv_total. - */ -Node eliminatePartialOperators(Node n); -/** make sygus term - * - * This function returns a builtin term f( children[0], ..., children[n] ) - * where f is the builtin op that the i^th constructor of sygus datatype dt - * encodes. If doBetaReduction is true, then lambdas are eagerly eliminated - * via beta reduction. - * - * If isExternal is true, then the returned term respects the original grammar - * that was provided. This includes the use of defined functions. - */ -Node mkSygusTerm(const DType& dt, - unsigned i, - const std::vector& children, - bool doBetaReduction = true, - bool isExternal = false); -/** - * Same as above, but we already have the sygus operator op. The above method - * is syntax sugar for calling this method on dt[i].getSygusOp(). - */ -Node mkSygusTerm(Node op, - const std::vector& children, - bool doBetaReduction = true); -/** - * n is a builtin term that is an application of operator op. - * - * This returns an n' such that (eval n args) is n', where n' is a instance of - * n for the appropriate substitution. - * - * For example, given a function-to-synthesize with formal argument list (x,y), - * say we have grammar: - * A -> A+A | A+x | A+(x+y) | y - * These lead to constructors with sygus ops: - * C1 / (lambda w1 w2. w1+w2) - * C2 / (lambda w1. w1+x) - * C3 / (lambda w1. w1+(x+y)) - * C4 / y - * Examples of calling this function: - * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } ) - * ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2). - * applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } ) - * ... returns (APPLY_UF (lambda w1. w1+3) t1). - * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } ) - * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1). - * applySygusArgs( dt, C4, y, { 3, 5 } ) - * ... returns 5. - * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4, - * to cache the results of whether the evaluation of this constructor needs - * a substitution over the formal argument list of the function-to-synthesize. - */ -Node applySygusArgs(const DType& dt, - Node op, - Node n, - const std::vector& args); -/** Sygus to builtin - * - * This method converts a constant term of SyGuS datatype type to its builtin - * equivalent. For example, given input C_*( C_x(), C_y() ), this method returns - * x*y, assuming C_+, C_x, and C_y have sygus operators *, x, and y - * respectively. - * - * If isExternal is true, then the returned term respects the original grammar - * that was provided. This includes the use of defined functions. This argument - * should typically be false, unless we are e.g. exporting the value of the - * term as a final solution. - */ -Node sygusToBuiltin(Node c, bool isExternal = false); -/** Sygus to builtin eval - * - * This method returns the rewritten form of (DT_SYGUS_EVAL n args). Notice that - * n does not necessarily need to be a constant. - * - * It does so by (1) converting constant subterms of n to builtin terms and - * evaluating them on the arguments args, (2) unfolding non-constant - * applications of sygus constructors in n with respect to args and (3) - * converting all other non-constant subterms of n to applications of - * DT_SYGUS_EVAL. - * - * For example, if - * n = C_+( C_*( C_x(), C_y() ), n' ), and args = { 3, 4 } - * where n' is a variable, then this method returns: - * 12 + (DT_SYGUS_EVAL n' 3 4) - * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin - * equivalent x*y and evaluated under the substition { x -> 3, x -> 4 } giving - * 12. The subterm n' is non-constant and thus we return its evaluation under - * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor - * is C_+, these terms are added together to give the result. - */ -Node sygusToBuiltinEval(Node n, const std::vector& args); - -/** Get free symbols in a sygus datatype type - * - * Add the free symbols (expr::getSymbols) in terms that can be generated by - * sygus datatype sdt to the set syms. For example, given sdt encodes the - * grammar: - * G -> a | +( b, G ) | c | e - * We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols - * excludes variables whose kind is BOUND_VARIABLE. - */ -void getFreeSymbolsSygusType(TypeNode sdt, - std::unordered_set& syms); - -/** Substitute and generalize a sygus datatype type - * - * This transforms a sygus datatype sdt into another one sdt' that generates - * terms t such that t * { vars -> syms } is generated by sdt. - * - * The arguments syms and vars should be vectors of the same size and types. - * It is recommended that the arguments in syms and vars should be variables - * (return true for .isVar()) but this is not required. - * - * The variables in vars of type BOUND_VARIABLE are added to the - * formal argument list of t. Other symbols are not. - * - * For example, given sdt encodes the grammar: - * G -> a | +( b, G ) | c | e - * Let syms = { a, b, c } and vars = { x_a, x_b, d }, where x_a and x_b have - * type BOUND_VARIABLE and d does not. - * The returned type encodes the grammar: - * G' -> x_a | +( x_b, G' ) | d | e - * Additionally, x_a and x_b are treated as formal arguments of a function - * to synthesize whose syntax restrictions are specified by G'. - * - * This method traverses the type definition of the datatype corresponding to - * the argument sdt. - */ -TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, - const std::vector& syms, - const std::vector& vars); - -// ------------------------ end sygus utils - } // namespace utils } // namespace datatypes } // namespace theory diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index ef2e7e445..1508267c3 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,7 +19,8 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "printer/sygus_print_callback.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 9d327bfe1..b8c867934 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -16,7 +16,7 @@ #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index f15b6780c..ea129803b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,7 +20,7 @@ #include "options/quantifiers_options.h" #include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index bb5307c79..91911e1f0 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -21,7 +21,7 @@ #include "printer/printer.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index f53637ebb..293048e8c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -21,7 +21,7 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/arith/arith_msum.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 7235fd65c..f5a708c8e 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -17,7 +17,7 @@ #include "base/check.h" #include "expr/dtype.h" #include "expr/sygus_datatype.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 696860302..e927ac249 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -18,7 +18,7 @@ #include #include "expr/node_algorithm.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h"