From: Andrew Reynolds Date: Mon, 29 Jul 2019 18:58:09 +0000 (-0500) Subject: Support get-abduct smt2 command (#3122) X-Git-Tag: cvc5-1.0.0~4071 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;ds=sidebyside;h=90eddb069c3c9abf96719ac20aff45b44af86207;p=cvc5.git Support get-abduct smt2 command (#3122) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9da9bd603..861841633 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -90,8 +90,6 @@ libcvc4_add_sources( preprocessing/passes/sort_infer.h preprocessing/passes/static_learning.cpp preprocessing/passes/static_learning.h - preprocessing/passes/sygus_abduct.cpp - preprocessing/passes/sygus_abduct.h preprocessing/passes/sygus_inference.cpp preprocessing/passes/sygus_inference.h preprocessing/passes/symmetry_breaker.cpp @@ -551,6 +549,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis_unif.h theory/quantifiers/sygus/enum_stream_substitution.cpp theory/quantifiers/sygus/enum_stream_substitution.h + theory/quantifiers/sygus/sygus_abduct.cpp + theory/quantifiers/sygus/sygus_abduct.h theory/quantifiers/sygus/sygus_enumerator.cpp theory/quantifiers/sygus/sygus_enumerator.h theory/quantifiers/sygus/sygus_eval_unfold.cpp diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index a94afc0a0..555ab2d6f 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -111,6 +111,7 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java + ${CMAKE_CURRENT_BINARY_DIR}/GetAbductCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetAssignmentCommand.java ${CMAKE_CURRENT_BINARY_DIR}/GetInfoCommand.java diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 03ffade46..8792fb56b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -885,15 +885,6 @@ header = "options/quantifiers_options.h" read_only = false help = "attempt to preprocess arbitrary inputs to sygus conjectures" -[[option]] - name = "sygusAbduct" - category = "regular" - long = "sygus-abduct" - type = "bool" - default = "false" - read_only = false - help = "compute abductions using sygus" - [[option]] name = "ceGuidedInst" category = "regular" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 72dfdd7f8..ef4e19654 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -614,3 +614,12 @@ header = "options/smt_options.h" default = "false" read_only = true help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" + +[[option]] + name = "produceAbducts" + category = "undocumented" + long = "produce-abducts" + type = "bool" + default = "false" + read_only = true + help = "support the get-abduct command" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d72188c6c..a95689f1c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1529,8 +1529,19 @@ extendedCommand[std::unique_ptr* cmd] | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } - | DECLARE_HEAP LPAREN_TOK - sortSymbol[t,CHECK_DECLARED] + | GET_ABDUCT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + term[e,e2] + ( + sygusGrammar[t, terms, name] + )? + { + cmd->reset(new GetAbductCommand(name,e, t)); + } + | DECLARE_HEAP LPAREN_TOK + sortSymbol[t,CHECK_DECLARED] sortSymbol[t, CHECK_DECLARED] // We currently do nothing with the type information declared for the heap. { cmd->reset(new EmptyCommand()); } @@ -3055,6 +3066,7 @@ SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; GET_QE_TOK : 'get-qe'; GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; +GET_ABDUCT_TOK : 'get-abduct'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 278f2bdfd..752bf58b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -674,11 +674,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } // get unlocked copy, modify, copy and relock LogicInfo log(d_logic.getUnlockedCopy()); - log.enableQuantifiers(); - log.enableTheory(theory::THEORY_UF); - log.enableTheory(theory::THEORY_DATATYPES); - log.enableIntegers(); - log.enableHigherOrder(); + // enable everything needed for sygus + log.enableSygus(); d_logic = log; d_logic.lock(); } diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp deleted file mode 100644 index b2dc872e4..000000000 --- a/src/preprocessing/passes/sygus_abduct.cpp +++ /dev/null @@ -1,360 +0,0 @@ -/********************* */ -/*! \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 preprocessing pass, which - ** transforms an arbitrary input into an abduction problem. - **/ - -#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" -#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 preprocessing { -namespace passes { - -SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "sygus-abduct"){}; - -PreprocessingPassResult SygusAbduct::applyInternal( - AssertionPipeline* assertionsToPreprocess) -{ - Trace("sygus-abduct") << "Run sygus abduct..." << std::endl; - - Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl; - std::vector& asserts = assertionsToPreprocess->ref(); - // do we have any assumptions, e.g. via check-sat-assuming? - bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0); - // The following is our set of "axioms". We construct this set only when the - // usingAssumptions (above) is true. In this case, our input formula is - // partitioned into Fa ^ Fc as described in the header of this class, where: - // - The conjunction of assertions marked as assumptions are the negated - // conjecture Fc, and - // - The conjunction of all other assertions are the axioms Fa. - std::vector axioms; - if (usingAssumptions) - { - 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; - - Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; - std::vector syms; - std::vector vars; - std::vector varlist; - std::vector 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("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); - 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 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 passes -} // namespace preprocessing -} // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h deleted file mode 100644 index db40b9688..000000000 --- a/src/preprocessing/passes/sygus_abduct.h +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \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 preprocessing pass, which transforms an arbitrary - ** input into an abduction problem. - **/ - -#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H -#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H - -#include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" - -namespace CVC4 { -namespace preprocessing { -namespace passes { - -/** SygusAbduct - * - * A preprocessing 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 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 - * above. - */ - PreprocessingPassResult applyInternal( - AssertionPipeline* assertionsToPreprocess) override; -}; - -} // namespace passes -} // namespace preprocessing -} // namespace CVC4 - -#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 15618f575..34bae1224 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -48,7 +48,6 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" -#include "preprocessing/passes/sygus_abduct.h" #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" @@ -127,7 +126,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("synth-rr", callCtor); registerPassInfo("real-to-int", callCtor); registerPassInfo("sygus-infer", callCtor); - registerPassInfo("sygus-abduct", callCtor); registerPassInfo("bv-to-bool", callCtor); registerPassInfo("bv-intro-pow2", callCtor); registerPassInfo("sort-inference", callCtor); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index b1936d8cc..044062f77 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2033,6 +2033,90 @@ std::string GetSynthSolutionCommand::getCommandName() const return "get-instantiations"; } +GetAbductCommand::GetAbductCommand() {} +GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj) + : d_name(name), d_conj(conj), d_resultStatus(false) +{ +} +GetAbductCommand::GetAbductCommand(const std::string& name, + Expr conj, + const Type& gtype) + : d_name(name), + d_conj(conj), + d_sygus_grammar_type(gtype), + d_resultStatus(false) +{ +} + +Expr GetAbductCommand::getConjecture() const { return d_conj; } +Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; } +Expr GetAbductCommand::getResult() const { return d_result; } + +void GetAbductCommand::invoke(SmtEngine* smtEngine) +{ + try + { + if (d_sygus_grammar_type.isNull()) + { + d_resultStatus = smtEngine->getAbduct(d_conj, d_result); + } + else + { + d_resultStatus = + smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result); + } + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const +{ + if (!ok()) + { + this->Command::printResult(out, verbosity); + } + else + { + expr::ExprDag::Scope scope(out, false); + if (d_resultStatus) + { + out << "(define-fun " << d_name << " () Bool " << d_result << ")" + << std::endl; + } + else + { + out << "none" << std::endl; + } + } +} + +Command* GetAbductCommand::exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) +{ + GetAbductCommand* c = + new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap)); + c->d_sygus_grammar_type = + d_sygus_grammar_type.exportTo(exprManager, variableMap); + c->d_result = d_result.exportTo(exprManager, variableMap); + c->d_resultStatus = d_resultStatus; + return c; +} + +Command* GetAbductCommand::clone() const +{ + GetAbductCommand* c = new GetAbductCommand(d_name, d_conj); + c->d_sygus_grammar_type = d_sygus_grammar_type; + c->d_result = d_result; + c->d_resultStatus = d_resultStatus; + return c; +} + +std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } + /* -------------------------------------------------------------------------- */ /* class GetQuantifierEliminationCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 68f9d1881..eb3199944 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1009,6 +1009,56 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command SmtEngine* d_smtEngine; }; /* class GetSynthSolutionCommand */ +/** The command (get-abduct s B (G)?) + * + * This command asks for an abduct from the current set of assertions and + * conjecture (goal) given by the argument B. + * + * The symbol s is the name for the abduction predicate. If we successfully + * find a predicate P, then the output response of this command is: + * (define-fun s () Bool P) + * + * A grammar type G can be optionally provided to indicate the syntactic + * restrictions on the possible solutions returned. + */ +class CVC4_PUBLIC GetAbductCommand : public Command +{ + public: + GetAbductCommand(); + GetAbductCommand(const std::string& name, Expr conj); + GetAbductCommand(const std::string& name, Expr conj, const Type& gtype); + + /** Get the conjecture of the abduction query */ + Expr getConjecture() const; + /** Get the grammar type given for the abduction query */ + Type getGrammarType() const; + /** Get the result of the query, which is the solution to the abduction query. + */ + Expr getResult() const; + + void invoke(SmtEngine* smtEngine) override; + void printResult(std::ostream& out, uint32_t verbosity = 2) const override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const override; + + protected: + /** The name of the abduction predicate */ + std::string d_name; + /** The conjecture of the abduction query */ + Expr d_conj; + /** + * The (optional) grammar of the abduction query, expressed as a sygus + * datatype type. + */ + Type d_sygus_grammar_type; + /** the return status of the command */ + bool d_resultStatus; + /** the return expression of the command */ + Expr d_result; +}; /* class GetAbductCommand */ + class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command { protected: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5e8540348..5db3fc43d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -98,6 +98,7 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" +#include "theory/quantifiers/sygus/sygus_abduct.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -1258,21 +1259,25 @@ void SmtEngine::setDefaults() { // sygus inference may require datatypes if (!d_isInternalSubsolver) { - if (options::sygusInference() || options::sygusRewSynthInput() - || options::sygusAbduct()) + if (options::produceAbducts()) + { + // we may invoke a sygus conjecture, hence we need options related to + // sygus + is_sygus = true; + } + if (options::sygusInference() || options::sygusRewSynthInput()) { - d_logic = d_logic.getUnlockedCopy(); - // sygus requires arithmetic, datatypes and quantifiers - d_logic.enableTheory(THEORY_ARITH); - d_logic.enableTheory(THEORY_DATATYPES); - d_logic.enableTheory(THEORY_QUANTIFIERS); - d_logic.lock(); // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; + // we change the logic to incorporate sygus immediately + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableSygus(); + d_logic.lock(); } } if ((options::checkModels() || options::checkSynthSol() + || options::produceAbducts() || options::modelCoresMode() != MODEL_CORES_NONE) && !options::produceAssertions()) { @@ -1954,16 +1959,24 @@ void SmtEngine::setDefaults() { options::sygusExtRew.set(false); } } - if (options::sygusAbduct()) + // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm + // is one that is specialized for returning a single solution. Non-basic + // sygus algorithms currently include the PBE solver, static template + // inference for invariant synthesis, and single invocation techniques. + bool reqBasicSygus = false; + if (options::produceAbducts()) { // if doing abduction, we should filter strong solutions if (!options::sygusFilterSolMode.wasSetByUser()) { options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG); } + // we must use basic sygus algorithms, since e.g. we require checking + // a sygus side condition for consistency with axioms. + reqBasicSygus = true; } if (options::sygusRewSynth() || options::sygusRewVerify() - || options::sygusQueryGen() || options::sygusAbduct()) + || options::sygusQueryGen()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); @@ -1971,9 +1984,12 @@ void SmtEngine::setDefaults() { if (options::sygusStream()) { // Streaming is incompatible with techniques that focus the search towards - // finding a single solution. This currently includes the PBE solver, - // static template inference for invariant synthesis, and single - // invocation techniques. + // finding a single solution. + reqBasicSygus = true; + } + // Now, disable options for non-basic sygus algorithms, if necessary. + if (reqBasicSygus) + { if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); @@ -2291,11 +2307,11 @@ void SmtEngine::setDefaults() { "--sygus-expr-miner-check-timeout=N requires " "--sygus-expr-miner-check-use-export"); } - if (options::sygusRewSynthInput() || options::sygusAbduct()) + if (options::sygusRewSynthInput() || options::produceAbducts()) { std::stringstream ss; ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input" - : "--sygus-abduct"); + : "--produce-abducts"); ss << "requires --sygus-expr-miner-check-use-export"; throw OptionException(ss.str()); } @@ -3325,10 +3341,6 @@ void SmtEnginePrivate::processAssertions() { { d_passes["sygus-infer"]->apply(&d_assertions); } - else if (options::sygusAbduct()) - { - d_passes["sygus-abduct"]->apply(&d_assertions); - } else if (options::sygusRewSynthInput()) { // do candidate rewrite rule synthesis @@ -4961,6 +4973,96 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) } } +bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) +{ + SmtScope smts(this); + + if (!options::produceAbducts()) + { + const char* msg = "Cannot get abduct when produce-abducts options is off."; + throw ModalException(msg); + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj + << std::endl; + std::vector easserts = getAssertions(); + std::vector axioms; + for (unsigned i = 0, size = easserts.size(); i < size; i++) + { + axioms.push_back(Node::fromExpr(easserts[i])); + } + std::vector asserts(axioms.begin(), axioms.end()); + asserts.push_back(Node::fromExpr(conj)); + d_sssfVarlist.clear(); + d_sssfSyms.clear(); + std::string name("A"); + Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture( + name, + asserts, + axioms, + TypeNode::fromType(grammarType), + d_sssfVarlist, + d_sssfSyms); + // should be a quantified conjecture with one function-to-synthesize + Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1); + // remember the abduct-to-synthesize + d_sssf = aconj[0][0].toExpr(); + Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj + << ", solving for " << d_sssf << std::endl; + // we generate a new smt engine to do the abduction query + d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager())); + d_subsolver->setIsInternalSubsolver(); + // get the logic + LogicInfo l = d_logic.getUnlockedCopy(); + // enable everything needed for sygus + l.enableSygus(); + d_subsolver->setLogic(l); + // assert the abduction query + d_subsolver->assertFormula(aconj.toExpr()); + Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; + Result r = d_subsolver->checkSat(); + Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + // get the synthesis solution + std::map sols; + d_subsolver->getSynthSolutions(sols); + Assert(sols.size() == 1); + std::map::iterator its = sols.find(d_sssf); + if (its != sols.end()) + { + Node abdn = Node::fromExpr(its->second); + Trace("sygus-abduct") + << "SmtEngine::getAbduct: solution is " << abdn << std::endl; + if (abdn.getKind() == kind::LAMBDA) + { + abdn = abdn[1]; + } + // convert back to original + // must replace formal arguments of abd with the free variables in the + // input problem that they correspond to. + abdn = abdn.substitute(d_sssfVarlist.begin(), + d_sssfVarlist.end(), + d_sssfSyms.begin(), + d_sssfSyms.end()); + + // convert to expression + abd = abdn.toExpr(); + + return true; + } + Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" + << std::endl; + throw RecoverableModalException("Could not find solution for get-abduct."); + } + return false; +} + +bool SmtEngine::getAbduct(const Expr& conj, Expr& abd) +{ + Type grammarType; + return getAbduct(conj, grammarType, abd); +} + void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { SmtScope smts(this); if( d_theoryEngine ){ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5913716e6..566777a89 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -147,6 +147,34 @@ class CVC4_PUBLIC SmtEngine { ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** The SMT engine subsolver + * + * This is a separate copy of the SMT engine which is used for making + * calls that cannot be answered by this copy of the SMT engine. An example + * of invoking this subsolver is the get-abduct command, where we wish to + * solve a sygus conjecture based on the current assertions. In particular, + * consider the input: + * (assert A) + * (get-abduct B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. To solve the abduction problem, instead of + * modifying the assertion stack to remove A and add the sygus conjecture + * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the + * assertion stack unchaged. This copy of the SMT engine can be further + * queried for information regarding further solutions. + */ + std::unique_ptr d_subsolver; + /** + * If applicable, the function-to-synthesize that the subsolver is solving + * for. This is used for the get-abduct command. + */ + Expr d_sssf; + /** + * The substitution to apply to the solutions from the subsolver, used for + * the get-abduct command. + */ + std::vector d_sssfVarlist; + std::vector d_sssfSyms; /** recursive function definition abstractions for --fmf-fun */ std::map< Node, TypeNode > d_fmfRecFunctionsAbs; std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; @@ -849,6 +877,21 @@ class CVC4_PUBLIC SmtEngine { Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true) /* throw(Exception) */; + /** + * This method asks this SMT engine to find an abduct with respect to the + * current assertion stack (call it A) and the conjecture (call it B). + * If this method returns true, then abd is set to a formula C such that + * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + /** Same as above, but without user-provided grammar restrictions */ + bool getAbduct(const Expr& conj, Expr& abd); /** * Get list of quantified formulas that were instantiated 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& 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& asserts, + const std::vector& axioms, + TypeNode abdGType, + std::vector& varlist, + std::vector& syms) +{ + 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; + + Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector vars; + std::vector 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 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); + 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 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 +#include +#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& asserts, + const std::vector& axioms, + TypeNode abdGType, + std::vector& varlist, + std::vector& syms); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 62672878e..5ecacd4ab 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1618,6 +1618,7 @@ set(regress_1_tests regress1/strings/type003.smt2 regress1/strings/username_checker_min.smt2 regress1/sygus-abduct-test.smt2 + regress1/sygus-abduct-test-user.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy regress1/sygus/array_search_2.sy diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 new file mode 100644 index 000000000..bdb680613 --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --produce-abducts +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic QF_UFLIRA) +(set-option :produce-abducts true) +(declare-fun n () Int) +(declare-fun m () Int) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (>= n 1)) +(assert (and (<= n x)(<= x (+ n 5)))) +(assert (and (<= 1 y)(<= y m))) + +; Generate a predicate A that is consistent with the above axioms (i.e. +; their conjunction is SAT), and is such that the conjunction of the above +; axioms, A and the conjecture below are UNSAT. +; The signature of A is below grammar. +(get-abduct A (< x y) + +; the grammar for the abduct-to-synthesize +((Start Bool) (StartInt Int)) +( +(Start Bool ((< StartInt StartInt))) +(StartInt Int (n m (+ StartInt StartInt) 0 1)) +) + +) diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 index 4ac90870c..d01f5f5ff 100644 --- a/test/regress/regress1/sygus-abduct-test.smt2 +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-abduct --sygus-abort-size=2 +; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=2 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 1 @@ -13,4 +13,4 @@ (assert (and (<= n x)(<= x (+ n 5)))) (assert (and (<= 1 y)(<= y m))) -(check-sat-assuming ((< x y))) +(get-abduct A (< x y))