diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-10 11:25:19 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-10 11:25:19 -0700 |
commit | 31a2135f4650a63fa772f001fcf191f2f7093a8d (patch) | |
tree | 1d01c094b7df9b010f748905aeaace44f17d904a /src/theory | |
parent | aef0e5ed90b1b8913b5c8c743cbcd012d5916ba7 (diff) |
Refactored BVAckermann preprocessing pass. (#1889)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/kinds | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 108 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 1 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 12 |
6 files changed, 16 insertions, 127 deletions
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<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; @@ -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<Node>& 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<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; @@ -148,12 +144,7 @@ private: 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; 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<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)) 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<Node>& assertions); - void mkAckermanizationAssertions(std::vector<Node>& 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<Node> children; if (n.getKind() == APPLY_UF) { |