From 31a2135f4650a63fa772f001fcf191f2f7093a8d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 10 May 2018 11:25:19 -0700 Subject: [PATCH] Refactored BVAckermann preprocessing pass. (#1889) --- src/Makefile.am | 2 + src/preprocessing/passes/bv_ackermann.cpp | 173 ++++++++++++++++++++++ src/preprocessing/passes/bv_ackermann.h | 68 +++++++++ src/smt/smt_engine.cpp | 10 +- src/theory/bv/kinds | 8 +- src/theory/bv/theory_bv.cpp | 108 +------------- src/theory/bv/theory_bv.h | 9 -- src/theory/theory_engine.cpp | 5 - src/theory/theory_engine.h | 1 - src/theory/theory_model.cpp | 12 +- 10 files changed, 267 insertions(+), 129 deletions(-) create mode 100644 src/preprocessing/passes/bv_ackermann.cpp create mode 100644 src/preprocessing/passes/bv_ackermann.h diff --git a/src/Makefile.am b/src/Makefile.am index 22e7daad9..28333d905 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -64,6 +64,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp new file mode 100644 index 000000000..850136f9d --- /dev/null +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -0,0 +1,173 @@ +/********************* */ +/*! \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 + +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& 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 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 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 diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h new file mode 100644 index 000000000..dbac79d21 --- /dev/null +++ b/src/preprocessing/passes/bv_ackermann.h @@ -0,0 +1,68 @@ +/********************* */ +/*! \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 + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +typedef std::unordered_map 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index aeec5298a..ac5563fb3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,6 +70,7 @@ #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" @@ -2590,6 +2591,8 @@ void SmtEnginePrivate::finishInit() { // actually assembling preprocessing pipelines). std::unique_ptr boolToBv( new BoolToBV(d_preprocessingPassContext.get())); + std::unique_ptr bvAckermann( + new BVAckermann(d_preprocessingPassContext.get())); std::unique_ptr bvAbstract( new BvAbstraction(d_preprocessingPassContext.get())); std::unique_ptr bvGauss( @@ -2609,6 +2612,8 @@ void SmtEnginePrivate::finishInit() { 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)); @@ -4029,8 +4034,9 @@ void SmtEnginePrivate::processAssertions() { "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()) diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index da2833ca0..66ee02c63 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -79,8 +79,8 @@ operator BITVECTOR_REDOR 1 "bit-vector redor" 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 \ @@ -187,8 +187,8 @@ typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule 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 diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 1b1e83ae3..2041b0805 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -55,8 +55,6 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, d_staticLearnCache(), d_BVDivByZero(), d_BVRemByZero(), - d_funcToArgs(), - d_funcToSkolem(u), d_lemmasAdded(c, false), d_conflict(c, false), d_invalidateModelCache(c, true), @@ -189,94 +187,6 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { 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& 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 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; @@ -301,19 +211,11 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { 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; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 90bd6275c..13469d562 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -68,8 +68,6 @@ public: Node expandDefinition(LogicRequest& logicRequest, Node node) override; - void mkAckermanizationAssertions(std::vector& assertions); - void preRegisterTerm(TNode n) override; void check(Effort e) override; @@ -136,8 +134,6 @@ private: Node getBVDivByZero(Kind k, unsigned width); typedef std::unordered_set TNodeSet; - void collectFunctionSymbols(TNode term, TNodeSet& seen); - void storeFunction(TNode func, TNode term); typedef std::unordered_set NodeSet; NodeSet d_staticLearnCache; @@ -148,12 +144,7 @@ private: std::unordered_map d_BVDivByZero; std::unordered_map d_BVRemByZero; - - typedef std::unordered_map FunctionToArgs; typedef std::unordered_map NodeToNode; - // for ackermanization - FunctionToArgs d_funcToArgs; - CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO d_lemmasAdded; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 74b73d718..08d33fe6c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1992,11 +1992,6 @@ void TheoryEngine::staticInitializeBVOptions( } } -void TheoryEngine::mkAckermanizationAssertions(std::vector& 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)) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3ae0a9ea9..fb33b45de 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -852,7 +852,6 @@ private: /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: void staticInitializeBVOptions(const std::vector& assertions); - void mkAckermanizationAssertions(std::vector& assertions); Node ppSimpITE(TNode assertion); /** Returns false if an assertion simplified to false. */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4b603d02a..35ada798c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -184,7 +184,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c 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); @@ -198,10 +199,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c 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 children; if (n.getKind() == APPLY_UF) { -- 2.30.2