diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /src/theory | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/logic_info.cpp | 9 | ||||
-rw-r--r-- | src/theory/logic_info.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 313 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.h | 90 |
5 files changed, 418 insertions, 1 deletions
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index e21d1f630..37b25163a 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -579,6 +579,15 @@ void LogicInfo::disableTheory(theory::TheoryId theory) { } } +void LogicInfo::enableSygus() +{ + enableQuantifiers(); + enableTheory(THEORY_UF); + enableTheory(THEORY_DATATYPES); + enableIntegers(); + enableHigherOrder(); +} + void LogicInfo::enableIntegers() { PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); d_logicString = ""; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a765472dd..969810a6f 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -201,6 +201,12 @@ public: disableTheory(theory::THEORY_QUANTIFIERS); } + /** + * Enable everything that is needed for sygus with respect to this logic info. + * This means enabling quantifiers, datatypes, UF, integers, and higher order. + */ + void enableSygus(); + // these are for arithmetic /** Enable the use of integers in this logic. */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 98d07fdea..6b042e294 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -91,7 +91,6 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); - checker->setOption("sygus-abduct", false); checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp new file mode 100644 index 000000000..52fb60c06 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -0,0 +1,313 @@ +/********************* */ +/*! \file sygus_abduct.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 sygus abduction utility, which + ** transforms an arbitrary input into an abduction problem. + **/ + +#include "theory/quantifiers/sygus/sygus_abduct.h" + +#include "expr/datatype.h" +#include "expr/node_algorithm.h" +#include "printer/sygus_print_callback.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusAbduct::SygusAbduct() {} + +Node SygusAbduct::mkAbductionConjecture(const std::string& name, + const std::vector<Node>& asserts, + const std::vector<Node>& axioms, + TypeNode abdGType, + std::vector<Node>& varlist, + std::vector<Node>& syms) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_set<Node, NodeHashFunction> 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; + + Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector<Node> vars; + std::vector<TypeNode> varlistTypes; + for (const Node& s : symset) + { + TypeNode tn = s.getType(); + if (tn.isFirstClass()) + { + std::stringstream ss; + ss << s; + Node var = nm->mkBoundVar(tn); + syms.push_back(s); + vars.push_back(var); + Node vlv = nm->mkBoundVar(ss.str(), tn); + varlist.push_back(vlv); + 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; + // make the abduction predicate to synthesize + TypeNode abdType = varlistTypes.empty() ? nm->booleanType() + : nm->mkPredicateType(varlistTypes); + Node abd = nm->mkBoundVar(name.c_str(), 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<Datatype> datatypes; + std::set<Type> 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<TypeNode> dtToProcess; + // datatype types we have processed + std::map<TypeNode, TypeNode> 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<TypeNode> 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<Type> cargs; + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k)); + std::map<TypeNode, TypeNode>::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<SygusPrintCallback> spc; + std::vector<Expr> args; + if (op.getKind() == LAMBDA) + { + Node opBody = op[1]; + for (const Node& v : op[0]) + { + args.push_back(v.toExpr()); + } + spc = std::make_shared<printer::SygusExprPrintCallback>( + opBody.toExpr(), args); + } + else if (cargs.empty()) + { + spc = std::make_shared<printer::SygusExprPrintCallback>(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<DatatypeType> 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<Node> achildren; + achildren.push_back(abd); + achildren.insert(achildren.end(), vars.begin(), vars.end()); + Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Set attributes..." << std::endl; + // set the sygus bound variable list + abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl; + Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts); + input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + // A(x) => ~input( x ) + input = nm->mkNode(OR, abdApp.negate(), input.negate()); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl; + Node res = input.negate(); + if (!vars.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); + // exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(EXISTS, bvl, res); + } + // sygus attribute + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + theory::SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); + std::vector<Node> iplc; + iplc.push_back(instAttr); + if (!axioms.empty()) + { + Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms); + aconj = + aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; + Node sc = nm->mkNode(AND, aconj, abdApp); + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); + sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); + instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); + // build in the side condition + // exists x. A( x ) ^ input_axioms( x ) + // as an additional annotation on the sygus conjecture. In other words, + // the abducts A we procedure must be consistent with our axioms. + iplc.push_back(instAttr); + } + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); + + Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); + + // forall A. exists x. ~( A( x ) => ~input( x ) ) + res = nm->mkNode(FORALL, fbvl, res, instAttrList); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + res = theory::Rewriter::rewrite(res); + + Trace("sygus-abduct") << "Generate: " << res << std::endl; + + return res; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h new file mode 100644 index 000000000..d6bbd0e3f --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file sygus_abduct.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 Sygus abduction utility, which transforms an arbitrary input into an + ** abduction problem. + **/ + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H + +#include <string> +#include <vector> +#include "expr/node.h" +#include "expr/type.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** SygusAbduct + * + * A utility that turns a set of quantifier-free assertions into + * a sygus conjecture that encodes an abduction problem. In detail, if our + * input formula is F( x ) for free symbols x, then we construct the sygus + * conjecture: + * + * exists A. forall x. ( A( x ) => ~F( x ) ) + * + * where A( x ) is a predicate over the free symbols of our input. In other + * words, A( x ) is a sufficient condition for showing ~F( x ). + * + * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x ) + * is unsatisfiable. + * + * A common use case is to find the weakest such A that meets the above + * specification. We do this by streaming solutions (sygus-stream) for A + * while filtering stronger solutions (sygus-filter-sol=strong). These options + * are enabled by default when this preprocessing class is used (sygus-abduct). + * + * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc + * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is: + * + * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) ) + * + * In other words, A( y ) must be consistent with our axioms Fa and imply + * ~F( x ). We encode this conjecture using SygusSideConditionAttribute. + */ +class SygusAbduct +{ + public: + SygusAbduct(); + + /** + * 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 argument name is the name for the abduct-to-synthesize. + * + * 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. + * + * The arguments varlist and syms specify the relationship between the free + * variables of asserts and the formal argument list of the + * abduct-to-synthesize. In particular, solutions to the synthesis conjecture + * will be in the form of a closed term (lambda varlist. t). The intended + * solution, which is a term whose free variables are a subset of asserts, + * is the term t { varlist -> syms }. + */ + static Node mkAbductionConjecture(const std::string& name, + const std::vector<Node>& asserts, + const std::vector<Node>& axioms, + TypeNode abdGType, + std::vector<Node>& varlist, + std::vector<Node>& syms); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ |