diff options
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 118 |
1 files changed, 71 insertions, 47 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 33342dc2e..cc4f52d8d 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -2,9 +2,9 @@ /*! \file lazy_bitblaster.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Liana Hadarean, Aina Niemetz, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** 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 @@ -89,62 +89,76 @@ TLazyBitblaster::~TLazyBitblaster() * @param node the atom to be bitblasted * */ -void TLazyBitblaster::bbAtom(TNode node) { - node = node.getKind() == kind::NOT? node[0] : node; +void TLazyBitblaster::bbAtom(TNode node) +{ + NodeManager* nm = NodeManager::currentNM(); + node = node.getKind() == kind::NOT ? node[0] : node; - if (hasBBAtom(node)) { + if (hasBBAtom(node)) + { return; } - + // make sure it is marked as an atom addAtom(node); - Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; + Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; ++d_statistics.d_numAtoms; - - /// if we are using bit-vector abstraction bit-blast the original interpretation - if (options::bvAbstraction() && - d_abstraction != NULL && - d_abstraction->isAbstraction(node)) { + /// if we are using bit-vector abstraction bit-blast the original + /// interpretation + if (options::bvAbstraction() && d_abstraction != NULL + && d_abstraction->isAbstraction(node)) + { // node must be of the form P(args) = bv1 Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node)); Node atom_bb; - if (expansion.getKind() == kind::CONST_BOOLEAN) { + if (expansion.getKind() == kind::CONST_BOOLEAN) + { atom_bb = expansion; - } else { - Assert (expansion.getKind() == kind::AND); + } + else + { + Assert(expansion.getKind() == kind::AND); std::vector<Node> atoms; - for (unsigned i = 0; i < expansion.getNumChildren(); ++i) { + for (unsigned i = 0; i < expansion.getNumChildren(); ++i) + { Node normalized_i = Rewriter::rewrite(expansion[i]); - Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ? - Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](normalized_i, this)) : - normalized_i; + Node atom_i = + normalized_i.getKind() != kind::CONST_BOOLEAN + ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()]( + normalized_i, this)) + : normalized_i; atoms.push_back(atom_i); } atom_bb = utils::mkAnd(atoms); } - Assert (!atom_bb.isNull()); - Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); + Assert(!atom_bb.isNull()); + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); return; } // the bitblasted definition of the atom Node normalized = Rewriter::rewrite(node); - Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? - d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized; + Node atom_bb = + normalized.getKind() != kind::CONST_BOOLEAN + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; - if (!options::proof()) { + if (!options::proof()) + { atom_bb = Rewriter::rewrite(atom_bb); } // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); } void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { @@ -307,19 +321,24 @@ prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { return d_satSolver->solve(budget); } - -void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) { +void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) +{ + NodeManager* nm = NodeManager::currentNM(); prop::SatClause conflictClause; d_satSolver->getUnsatCore(conflictClause); - for (unsigned i = 0; i < conflictClause.size(); i++) { + for (unsigned i = 0; i < conflictClause.size(); i++) + { prop::SatLiteral lit = conflictClause[i]; TNode atom = d_cnfStream->getNode(lit); - Node not_atom; - if (atom.getKind() == kind::NOT) { + Node not_atom; + if (atom.getKind() == kind::NOT) + { not_atom = atom[0]; - } else { - not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); + } + else + { + not_atom = nm->mkNode(kind::NOT, atom); } conflict.push_back(not_atom); } @@ -394,24 +413,30 @@ void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) d_bv->d_out->safePoint(amount); } - -EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { +EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) +{ int numAssertions = d_bv->numAssertions(); - Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n"; - Debug("bv-equality-status")<< "BVSatSolver has full model? " << (d_fullModelAssertionLevel.get() == numAssertions) <<"\n"; + Debug("bv-equality-status") + << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n"; + Debug("bv-equality-status") + << "BVSatSolver has full model? " + << (d_fullModelAssertionLevel.get() == numAssertions) << "\n"; // First check if it trivially rewrites to false/true - Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b)); + Node a_eq_b = + Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b)); if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - if (d_fullModelAssertionLevel.get() != numAssertions) { + if (d_fullModelAssertionLevel.get() != numAssertions) + { return theory::EQUALITY_UNKNOWN; } // Check if cache is valid (invalidated in check and pops) - if (d_bv->d_invalidateModelCache.get()) { + if (d_bv->d_invalidateModelCache.get()) + { invalidateModelCache(); } d_bv->d_invalidateModelCache.set(false); @@ -419,18 +444,17 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { Node a_value = getTermModel(a, true); Node b_value = getTermModel(b, true); - Assert (a_value.isConst() && - b_value.isConst()); + Assert(a_value.isConst() && b_value.isConst()); - if (a_value == b_value) { - Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n"; + if (a_value == b_value) + { + Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n"; return theory::EQUALITY_TRUE_IN_MODEL; } - Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n"; + Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n"; return theory::EQUALITY_FALSE_IN_MODEL; } - bool TLazyBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } |