From 8078ed4c404238371a34d2c122e1489d6de9d3a9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 25 Jul 2019 21:24:26 -0500 Subject: [PATCH] Input user grammar in sygus abduct (#3119) --- src/preprocessing/passes/sygus_abduct.cpp | 218 ++++++++++++++++++++-- src/preprocessing/passes/sygus_abduct.h | 12 ++ 2 files changed, 214 insertions(+), 16 deletions(-) diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp index 346915b51..b2dc872e4 100644 --- a/src/preprocessing/passes/sygus_abduct.cpp +++ b/src/preprocessing/passes/sygus_abduct.cpp @@ -15,7 +15,9 @@ #include "preprocessing/passes/sygus_abduct.h" +#include "expr/datatype.h" #include "expr/node_algorithm.h" +#include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" @@ -37,11 +39,9 @@ SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) PreprocessingPassResult SygusAbduct::applyInternal( AssertionPipeline* assertionsToPreprocess) { - NodeManager* nm = NodeManager::currentNM(); Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; - std::unordered_set symset; std::vector& asserts = assertionsToPreprocess->ref(); // do we have any assumptions, e.g. via check-sat-assuming? bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); @@ -52,15 +52,44 @@ PreprocessingPassResult SygusAbduct::applyInternal( // conjecture Fc, and // - The conjunction of all other assertions are the axioms Fa. std::vector axioms; - for (size_t i = 0, size = asserts.size(); i < size; i++) + if (usingAssumptions) { - expr::getSymbols(asserts[i], symset); - // if we are not an assumption, add it to the set of axioms - if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart()) + for (size_t i = 0, astart = assertionsToPreprocess->getAssumptionsStart(); + i < astart; + i++) { + // if we are not an assumption, add it to the set of axioms axioms.push_back(asserts[i]); } } + + // the abduction grammar type we are using (null for now, until a future + // commit) + TypeNode abdGType; + + Node res = mkAbductionConjecture(asserts, axioms, abdGType); + + Node trueNode = NodeManager::currentNM()->mkConst(true); + + assertionsToPreprocess->replace(0, res); + for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, trueNode); + } + + return PreprocessingPassResult::NO_CONFLICT; +} + +Node SygusAbduct::mkAbductionConjecture(const std::vector& asserts, + const std::vector& axioms, + TypeNode abdGType) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_set symset; + for (size_t i = 0, size = asserts.size(); i < size; i++) + { + expr::getSymbols(asserts[i], symset); + } Trace("sygus-abduct-debug") << "...finish, got " << symset.size() << " symbols." << std::endl; @@ -84,6 +113,8 @@ PreprocessingPassResult SygusAbduct::applyInternal( varlistTypes.push_back(tn); } } + // make the sygus variable list + Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); Trace("sygus-abduct-debug") << "...finish" << std::endl; Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl; @@ -93,6 +124,170 @@ PreprocessingPassResult SygusAbduct::applyInternal( Node abd = nm->mkBoundVar("A", abdType); Trace("sygus-abduct-debug") << "...finish" << std::endl; + // if provided, we will associate it with the function-to-synthesize + if (!abdGType.isNull()) + { + Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus()); + // must convert all constructors to version with bound variables in "vars" + std::vector datatypes; + std::set unres; + + Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl; + Trace("sygus-abduct-debug") << abdGType.getDatatype() << std::endl; + + // datatype types we need to process + std::vector dtToProcess; + // datatype types we have processed + std::map dtProcessed; + dtToProcess.push_back(abdGType); + std::stringstream ssutn0; + ssutn0 << abdGType.getDatatype().getName() << "_s"; + TypeNode abdTNew = + nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + unres.insert(abdTNew.toType()); + dtProcessed[abdGType] = abdTNew; + + // We must convert all symbols in the sygus datatype type abdGType to + // apply the substitution { syms -> varlist }, where syms is the free + // variables of the input problem, and varlist is the formal argument list + // of the abduct-to-synthesize. For example, given user-provided sygus + // grammar: + // G -> a | +( b, G ) + // we synthesize a abduct A with two arguments x_a and x_b corresponding to + // a and b, and reconstruct the grammar: + // G' -> x_a | +( x_b, G' ) + // In this way, x_a and x_b are treated as bound variables and handled as + // arguments of the abduct-to-synthesize instead of as free variables with + // no relation to A. We additionally require that x_a, when printed, prints + // "a", which we do with a custom sygus callback below. + + // 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.getDatatype().isSygus()); + const Datatype& dtc = curr.getDatatype(); + std::stringstream ssdtn; + ssdtn << dtc.getName() << "_s"; + datatypes.push_back(Datatype(ssdtn.str())); + Trace("sygus-abduct-debug") + << "Process datatype " << datatypes.back().getName() << "..." + << std::endl; + for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) + { + Node op = Node::fromExpr(dtc[j].getSygusOp()); + // apply the substitution to the argument + Node ops = op.substitute( + syms.begin(), syms.end(), varlist.begin(), varlist.end()); + Trace("sygus-abduct-debug") << " Process constructor " << op << " / " + << ops << "..." << std::endl; + std::vector cargs; + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k)); + std::map::iterator itdp = + dtProcessed.find(argt); + TypeNode argtNew; + if (itdp == dtProcessed.end()) + { + std::stringstream ssutn; + ssutn << argt.getDatatype().getName() << "_s"; + argtNew = + nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + Trace("sygus-abduct-debug") + << " ...unresolved type " << argtNew << " for " << argt + << std::endl; + unres.insert(argtNew.toType()); + dtProcessed[argt] = argtNew; + dtNextToProcess.push_back(argt); + } + else + { + argtNew = itdp->second; + } + Trace("sygus-abduct-debug") + << " Arg #" << k << ": " << argtNew << std::endl; + cargs.push_back(argtNew.toType()); + } + // 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("sygus-abduct-debug") + << "Add constructor : " << ops << std::endl; + datatypes.back().addSygusConstructor( + ops.toExpr(), ss.str(), cargs, spc); + } + Trace("sygus-abduct-debug") + << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; + datatypes.back().setSygus(dtc.getSygusType(), + abvl.toExpr(), + dtc.getSygusAllowConst(), + dtc.getSygusAllowAll()); + } + dtToProcess.clear(); + dtToProcess.insert( + dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); + } + Trace("sygus-abduct-debug") + << "Make " << datatypes.size() << " datatype types..." << std::endl; + // make the datatype types + std::vector datatypeTypes = + nm->toExprManager()->mkMutualDatatypeTypes( + datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + TypeNode abdGTypeS = TypeNode::fromType(datatypeTypes[0]); + if (Trace.isOn("sygus-abduct-debug")) + { + Trace("sygus-abduct-debug") << "Made datatype types:" << std::endl; + for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) + { + const Datatype& dtj = datatypeTypes[j].getDatatype(); + Trace("sygus-abduct-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("sygus-abduct-debug") + << "Argument " << l << " of " << dtj[k] + << " is not datatype : " << dtj[k].getArgType(l) << std::endl; + AlwaysAssert(false); + } + } + } + } + } + + Trace("sygus-abduct-debug") + << "Make sygus grammar attribute..." << std::endl; + Node sym = nm->mkBoundVar("sfproxy_abduct", abdGTypeS); + // Set the sygus grammar attribute to indicate that abdGTypeS encodes the + // grammar for abd. + theory::SygusSynthGrammarAttribute ssg; + abd.setAttribute(ssg, sym); + Trace("sygus-abduct-debug") << "Finished setting up grammar." << std::endl; + } + Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl; std::vector achildren; achildren.push_back(abd); @@ -102,7 +297,6 @@ PreprocessingPassResult SygusAbduct::applyInternal( Trace("sygus-abduct-debug") << "Set attributes..." << std::endl; // set the sygus bound variable list - Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl); Trace("sygus-abduct-debug") << "...finish" << std::endl; @@ -158,15 +352,7 @@ PreprocessingPassResult SygusAbduct::applyInternal( Trace("sygus-abduct") << "Generate: " << res << std::endl; - Node trueNode = nm->mkConst(true); - - assertionsToPreprocess->replace(0, res); - for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i) - { - assertionsToPreprocess->replace(i, trueNode); - } - - return PreprocessingPassResult::NO_CONFLICT; + return res; } } // namespace passes diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h index 0e0868cda..db40b9688 100644 --- a/src/preprocessing/passes/sygus_abduct.h +++ b/src/preprocessing/passes/sygus_abduct.h @@ -56,6 +56,18 @@ class SygusAbduct : public PreprocessingPass public: SygusAbduct(PreprocessingPassContext* preprocContext); + /** + * Returns the sygus conjecture corresponding to the abduction problem for + * input problem (F above) given by asserts, and axioms (Fa above) given by + * axioms. Note that axioms is expected to be a subset of asserts. + * + * The type abdGType (if non-null) is a sygus datatype type that encodes the + * grammar that should be used for solutions of the abduction conjecture. + */ + static Node mkAbductionConjecture(const std::vector& asserts, + const std::vector& axioms, + TypeNode abdGType); + protected: /** * Replaces the set of assertions by an abduction sygus problem described -- 2.30.2