decision/justification_heuristic.h \
preprocessing/passes/bv_abstraction.cpp \
preprocessing/passes/bv_abstraction.h \
+ preprocessing/passes/bv_ackermann.cpp \
+ preprocessing/passes/bv_ackermann.h \
preprocessing/passes/bv_gauss.cpp \
preprocessing/passes/bv_gauss.h \
preprocessing/passes/bv_intro_pow2.cpp \
--- /dev/null
+/********************* */
+/*! \file bv_ackermann.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Ackermannization preprocessing pass.
+ **
+ ** This implements the Ackermannization preprocessing pass, which enables
+ ** very limited theory combination support for eager bit-blasting via
+ ** Ackermannization. It reduces constraints over the combination of the
+ ** theories of fixed-size bit-vectors and uninterpreted functions as
+ ** described in
+ ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for
+ ** Bit-vectors in Satisfiability Modulo Theories.
+** https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **/
+
+#include "preprocessing/passes/bv_ackermann.h"
+
+#include "expr/node.h"
+#include "options/bv_options.h"
+#include "theory/bv/theory_bv_utils.h"
+
+#include <unordered_set>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/* -------------------------------------------------------------------------- */
+
+namespace
+{
+
+void storeFunction(
+ TNode func,
+ TNode term,
+ FunctionToArgsMap& fun_to_args,
+ SubstitutionMap& fun_to_skolem)
+{
+ if (fun_to_args.find(func) == fun_to_args.end())
+ {
+ fun_to_args.insert(make_pair(func, NodeSet()));
+ }
+ NodeSet& set = fun_to_args[func];
+ if (set.find(term) == set.end())
+ {
+ set.insert(term);
+ Node skolem = bv::utils::mkVar(bv::utils::getSize(term));
+ fun_to_skolem.addSubstitution(term, skolem);
+ }
+}
+
+void collectFunctionSymbols(
+ TNode term,
+ FunctionToArgsMap& fun_to_args,
+ SubstitutionMap& fun_to_skolem,
+ std::unordered_set<TNode, TNodeHashFunction>& seen)
+{
+ if (seen.find(term) != seen.end()) return;
+ if (term.getKind() == kind::APPLY_UF)
+ {
+ storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem);
+ }
+ else if (term.getKind() == kind::SELECT)
+ {
+ storeFunction(term[0], term, fun_to_args, fun_to_skolem);
+ }
+ else
+ {
+ AlwaysAssert(term.getKind() != kind::STORE,
+ "Cannot use eager bitblasting on QF_ABV formula with stores");
+ }
+ for (const TNode& n : term)
+ {
+ collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen);
+ }
+ seen.insert(term);
+}
+
+} // namespace
+
+/* -------------------------------------------------------------------------- */
+
+BVAckermann::BVAckermann(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "bv-ackermann"),
+ d_funcToSkolem(preprocContext->getUserContext())
+{
+}
+
+PreprocessingPassResult BVAckermann::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
+ AlwaysAssert(!options::incrementalSolving());
+
+ std::unordered_set<TNode, TNodeHashFunction> seen;
+
+ for (const Node& a : assertionsToPreprocess->ref())
+ {
+ collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen);
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+ for (const auto& p : d_funcToArgs)
+ {
+ TNode func = p.first;
+ const NodeSet& args = p.second;
+ NodeSet::const_iterator it1 = args.begin();
+ for (; it1 != args.end(); ++it1)
+ {
+ for (NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2)
+ {
+ TNode args1 = *it1;
+ TNode args2 = *it2;
+ Node args_eq;
+
+ if (args1.getKind() == kind::APPLY_UF)
+ {
+ AlwaysAssert(args1.getKind() == kind::APPLY_UF
+ && args1.getOperator() == func);
+ AlwaysAssert(args2.getKind() == kind::APPLY_UF
+ && args2.getOperator() == func);
+ AlwaysAssert(args1.getNumChildren() == args2.getNumChildren());
+
+ std::vector<Node> eqs(args1.getNumChildren());
+
+ for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
+ {
+ eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
+ }
+ args_eq = bv::utils::mkAnd(eqs);
+ }
+ else
+ {
+ AlwaysAssert(args1.getKind() == kind::SELECT && args1[0] == func);
+ AlwaysAssert(args2.getKind() == kind::SELECT && args2[0] == func);
+ AlwaysAssert(args1.getNumChildren() == 2);
+ AlwaysAssert(args2.getNumChildren() == 2);
+ args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
+ }
+ Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
+ Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
+ assertionsToPreprocess->push_back(lemma);
+ }
+ }
+ }
+
+ /* replace applications of UF by skolems */
+ // FIXME for model building, github issue #1118)
+ for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ assertionsToPreprocess->replace(
+ i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
+ }
+
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+/* -------------------------------------------------------------------------- */
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file bv_ackermann.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Ackermannization preprocessing pass.
+ **
+ ** This implements the Ackermannization preprocessing pass, which enables
+ ** very limited theory combination support for eager bit-blasting via
+ ** Ackermannization. It reduces constraints over the combination of the
+ ** theories of fixed-size bit-vectors and uninterpreted functions as
+ ** described in
+ ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for
+ ** Bit-vectors in Satisfiability Modulo Theories.
+** https://cs.nyu.edu/media/publications/hadarean_liana.pdf
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+#include <unordered_map>
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap;
+
+class BVAckermann : public PreprocessingPass
+{
+ public:
+ BVAckermann(PreprocessingPassContext* preprocContext);
+
+ protected:
+ /**
+ * Apply Ackermannization as follows:
+ *
+ * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh
+ * variable f_X and use it to replace all occurrences of f(X).
+ *
+ * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn)
+ * occurring in the input formula, add the following lemma:
+ * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
+ */
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ FunctionToArgsMap d_funcToArgs;
+ theory::SubstitutionMap d_funcToSkolem;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif
#include "options/uf_options.h"
#include "preprocessing/passes/bool_to_bv.h"
#include "preprocessing/passes/bv_abstraction.h"
+#include "preprocessing/passes/bv_ackermann.h"
#include "preprocessing/passes/bv_gauss.h"
#include "preprocessing/passes/bv_intro_pow2.h"
#include "preprocessing/passes/bv_to_bool.h"
// actually assembling preprocessing pipelines).
std::unique_ptr<BoolToBV> boolToBv(
new BoolToBV(d_preprocessingPassContext.get()));
+ std::unique_ptr<BVAckermann> bvAckermann(
+ new BVAckermann(d_preprocessingPassContext.get()));
std::unique_ptr<BvAbstraction> bvAbstract(
new BvAbstraction(d_preprocessingPassContext.get()));
std::unique_ptr<BVGauss> bvGauss(
d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
d_preprocessingPassRegistry.registerPass("bv-abstraction",
std::move(bvAbstract));
+ d_preprocessingPassRegistry.registerPass("bv-ackermann",
+ std::move(bvAckermann));
d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
std::move(bvIntroPow2));
"Try --bv-div-zero-const to interpret division by zero as a constant.");
}
- if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref());
+ if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+ {
+ d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions);
}
if (options::bvAbstraction() && !options::incrementalSolving())
operator BITVECTOR_REDAND 1 "bit-vector redand"
operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
-operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
-operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
+operator BITVECTOR_ACKERMANNIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
+operator BITVECTOR_ACKERMANNIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
constant BITVECTOR_BITOF_OP \
::CVC4::BitVectorBitOf \
typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
-typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
-typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
d_staticLearnCache(),
d_BVDivByZero(),
d_BVRemByZero(),
- d_funcToArgs(),
- d_funcToSkolem(u),
d_lemmasAdded(c, false),
d_conflict(c, false),
d_invalidateModelCache(c, true),
Unreachable();
}
-
-void TheoryBV::collectFunctionSymbols(TNode term, TNodeSet& seen) {
- if (seen.find(term) != seen.end())
- return;
- if (term.getKind() == kind::APPLY_UF) {
- TNode func = term.getOperator();
- storeFunction(func, term);
- } else if (term.getKind() == kind::SELECT) {
- TNode func = term[0];
- storeFunction(func, term);
- } else if (term.getKind() == kind::STORE) {
- AlwaysAssert(false, "Cannot use eager bitblasting on QF_ABV formula with stores");
- }
- for (unsigned i = 0; i < term.getNumChildren(); ++i) {
- collectFunctionSymbols(term[i], seen);
- }
- seen.insert(term);
-}
-
-void TheoryBV::storeFunction(TNode func, TNode term) {
- if (d_funcToArgs.find(func) == d_funcToArgs.end()) {
- d_funcToArgs.insert(make_pair(func, NodeSet()));
- }
- NodeSet& set = d_funcToArgs[func];
- if (set.find(term) == set.end()) {
- set.insert(term);
- Node skolem = utils::mkVar(utils::getSize(term));
- d_funcToSkolem.addSubstitution(term, skolem);
- }
-}
-
-void TheoryBV::mkAckermanizationAssertions(std::vector<Node>& assertions) {
- Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAssertions\n";
-
- Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
- AlwaysAssert(!options::incrementalSolving());
- TNodeSet seen;
- for (unsigned i = 0; i < assertions.size(); ++i) {
- collectFunctionSymbols(assertions[i], seen);
- }
-
- FunctionToArgs::const_iterator it = d_funcToArgs.begin();
- NodeManager* nm = NodeManager::currentNM();
- for (; it!= d_funcToArgs.end(); ++it) {
- TNode func = it->first;
- const NodeSet& args = it->second;
- NodeSet::const_iterator it1 = args.begin();
- for ( ; it1 != args.end(); ++it1) {
- for(NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2) {
- TNode args1 = *it1;
- TNode args2 = *it2;
- Node args_eq;
-
- if (args1.getKind() == kind::APPLY_UF) {
- AlwaysAssert (args1.getKind() == kind::APPLY_UF &&
- args1.getOperator() == func);
- AlwaysAssert (args2.getKind() == kind::APPLY_UF &&
- args2.getOperator() == func);
- AlwaysAssert (args1.getNumChildren() == args2.getNumChildren());
-
- std::vector<Node> eqs(args1.getNumChildren());
-
- for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
- eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
- }
- args_eq = utils::mkAnd(eqs);
- } else {
- AlwaysAssert (args1.getKind() == kind::SELECT &&
- args1[0] == func);
- AlwaysAssert (args2.getKind() == kind::SELECT &&
- args2[0] == func);
- AlwaysAssert (args1.getNumChildren() == 2);
- AlwaysAssert (args2.getNumChildren() == 2);
- args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
- }
- Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
- Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
- assertions.push_back(lemma);
- }
- }
- }
-
- // replace applications of UF by skolems (FIXME for model building)
- for(unsigned i = 0; i < assertions.size(); ++i) {
- assertions[i] = d_funcToSkolem.apply(assertions[i]);
- }
-}
-
Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width));
Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
kind::BITVECTOR_UREM_TOTAL, num, den);
-
- // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- // // Ackermanize UF if using eager bit-blasting
- // Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
- // node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
- // return node;
- // } else {
- Node divByZero = getBVDivByZero(node.getKind(), width);
- Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
- node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
- logicRequest.widenLogic(THEORY_UF);
- return node;
- //}
+ Node divByZero = getBVDivByZero(node.getKind(), width);
+ Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+ node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+ logicRequest.widenLogic(THEORY_UF);
+ return node;
}
break;
Node expandDefinition(LogicRequest& logicRequest, Node node) override;
- void mkAckermanizationAssertions(std::vector<Node>& assertions);
-
void preRegisterTerm(TNode n) override;
void check(Effort e) override;
Node getBVDivByZero(Kind k, unsigned width);
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- void collectFunctionSymbols(TNode term, TNodeSet& seen);
- void storeFunction(TNode func, TNode term);
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
NodeSet d_staticLearnCache;
std::unordered_map<unsigned, Node> d_BVDivByZero;
std::unordered_map<unsigned, Node> d_BVRemByZero;
-
- typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs;
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
- // for ackermanization
- FunctionToArgs d_funcToArgs;
- CVC4::theory::SubstitutionMap d_funcToSkolem;
context::CDO<bool> d_lemmasAdded;
}
}
-void TheoryEngine::mkAckermanizationAssertions(std::vector<Node>& assertions) {
- bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
- bv_theory->mkAckermanizationAssertions(assertions);
-}
-
Node TheoryEngine::ppSimpITE(TNode assertion)
{
if (!d_iteUtilities->containsTermITE(assertion))
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
public:
void staticInitializeBVOptions(const std::vector<Node>& assertions);
- void mkAckermanizationAssertions(std::vector<Node>& assertions);
Node ppSimpITE(TNode assertion);
/** Returns false if an assertion simplified to false. */
ret = nr;
}
} else {
- // FIXME : special case not necessary? (also address BV_ACKERMANIZE functions below), github issue #1116
+ // FIXME : special case not necessary? (also address BV_ACKERMANNIZE
+ // functions below), github issue #1116
if(n.getKind() == kind::LAMBDA) {
NodeManager* nm = NodeManager::currentNM();
Node body = getModelValue(n[1], true);
d_modelCache[n] = ret;
return ret;
}
-
- if (n.getNumChildren() > 0 &&
- n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV &&
- n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) {
+
+ if (n.getNumChildren() > 0
+ && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UDIV
+ && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UREM)
+ {
Debug("model-getvalue-debug") << "Get model value children " << n << std::endl;
std::vector<Node> children;
if (n.getKind() == APPLY_UF) {
projects / cvc5.git / commitdiff