summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/sygus_abduct.cpp174
-rw-r--r--src/preprocessing/passes/sygus_abduct.h72
2 files changed, 246 insertions, 0 deletions
diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp
new file mode 100644
index 000000000..a2fe38219
--- /dev/null
+++ b/src/preprocessing/passes/sygus_abduct.cpp
@@ -0,0 +1,174 @@
+/********************* */
+/*! \file sygus_abduct.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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/node_algorithm.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)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Trace("sygus-abduct") << "Run sygus abduct..." << std::endl;
+
+ Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl;
+ std::unordered_set<Node, NodeHashFunction> symset;
+ 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;
+ for (size_t i = 0, size = asserts.size(); i < size; i++)
+ {
+ expr::getSymbols(asserts[i], symset);
+ // if we are not an assumption, add it to the set of axioms
+ if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart())
+ {
+ axioms.push_back(asserts[i]);
+ }
+ }
+ 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);
+ }
+ }
+ 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;
+
+ 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
+ Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
+ 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;
+
+ Node trueNode = nm->mkConst(true);
+
+ assertionsToPreprocess->replace(0, res);
+ for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ assertionsToPreprocess->replace(i, trueNode);
+ }
+
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h
new file mode 100644
index 000000000..8e83bf1d7
--- /dev/null
+++ b/src/preprocessing/passes/sygus_abduct.h
@@ -0,0 +1,72 @@
+/********************* */
+/*! \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);
+
+ 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_ */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback