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
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
${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
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"
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"
| 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()); }
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
}
// 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();
}
+++ /dev/null
-/********************* */
-/*! \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<Node>& 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<Node> 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<Node>& asserts,
- const std::vector<Node>& axioms,
- TypeNode abdGType)
-{
- 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> syms;
- std::vector<Node> vars;
- std::vector<Node> varlist;
- 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("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<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 passes
-} // namespace preprocessing
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \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<Node>& asserts,
- const std::vector<Node>& 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_ */
#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"
registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
registerPassInfo("real-to-int", callCtor<RealToInt>);
registerPassInfo("sygus-infer", callCtor<SygusInference>);
- registerPassInfo("sygus-abduct", callCtor<SygusAbduct>);
registerPassInfo("bv-to-bool", callCtor<BVToBool>);
registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
registerPassInfo("sort-inference", callCtor<SortInferencePass>);
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 */
/* -------------------------------------------------------------------------- */
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:
#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"
// 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())
{
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);
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);
"--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());
}
{
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
}
}
+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<Expr> easserts = getAssertions();
+ std::vector<Node> axioms;
+ for (unsigned i = 0, size = easserts.size(); i < size; i++)
+ {
+ axioms.push_back(Node::fromExpr(easserts[i]));
+ }
+ std::vector<Node> 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<Expr, Expr> sols;
+ d_subsolver->getSynthSolutions(sols);
+ Assert(sols.size() == 1);
+ std::map<Expr, Expr>::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 ){
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<SmtEngine> 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<Node> d_sssfVarlist;
+ std::vector<Node> d_sssfSyms;
/** recursive function definition abstractions for --fmf-fun */
std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
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
}
}
+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 = "";
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. */
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);
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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
--- /dev/null
+; 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))
+)
+
+)
-; 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
(assert (and (<= n x)(<= x (+ n 5))))
(assert (and (<= 1 y)(<= y m)))
-(check-sat-assuming ((< x y)))
+(get-abduct A (< x y))
projects / cvc5.git / commitdiff