From: Aina Niemetz Date: Fri, 16 Feb 2018 01:51:42 +0000 (-0800) Subject: Removed bv::utils::mkConjunction (redundant). (#1610) X-Git-Tag: cvc5-1.0.0~5281 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=81f8a73120f3237baabad1faa2c467d1759d56d7;p=cvc5.git Removed bv::utils::mkConjunction (redundant). (#1610) --- diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index a3442e4c6..354b58376 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -2,9 +2,9 @@ /*! \file bv_quick_check.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Liana Hadarean, Tim King, Aina Niemetz ** 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 @@ -20,11 +20,12 @@ #include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv_utils.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; using namespace CVC4::prop; +namespace CVC4 { +namespace theory { +namespace bv { + BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv) : d_ctx() , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)) @@ -39,11 +40,12 @@ uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) { return d_bitblaster->computeAtomWeight(node, seen); } -void BVQuickCheck::setConflict() { - Assert (!inConflict()); +void BVQuickCheck::setConflict() +{ + Assert(!inConflict()); std::vector conflict; d_bitblaster->getConflict(conflict); - Node confl = utils::mkConjunction(conflict); + Node confl = utils::mkAnd(conflict); d_inConflict = true; d_conflict = confl; } @@ -377,3 +379,7 @@ QuickXPlain::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_finalPeriod); smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio); } + +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index b9467c168..61bbf667d 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -2,9 +2,9 @@ /*! \file bv_subtheory_bitblast.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Tim King + ** Liana Hadarean, Dejan Jovanovic, Aina Niemetz ** 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 @@ -29,7 +29,6 @@ using namespace std; using namespace CVC4::context; -using namespace CVC4::theory::bv::utils; namespace CVC4 { namespace theory { @@ -118,7 +117,8 @@ void BitblastSolver::bitblastQueue() { } } -bool BitblastSolver::check(Theory::Effort e) { +bool BitblastSolver::check(Theory::Effort e) +{ Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); @@ -130,33 +130,40 @@ bool BitblastSolver::check(Theory::Effort e) { bitblastQueue(); // Processing assertions - while (!done()) { + while (!done()) + { TNode fact = get(); d_validModelCache = false; Debug("bv-bitblast") << " fact " << fact << ")\n"; - if (options::bvAbstraction()) { + if (options::bvAbstraction()) + { // skip atoms that are the result of abstraction lemmas - if (d_abstractionModule->isLemmaAtom(fact)) { + if (d_abstractionModule->isLemmaAtom(fact)) + { d_lemmaAtomsQueue.push_back(fact); continue; } } - //skip facts involving integer equalities (from bv2nat) - if( !utils::isBitblastAtom( fact ) ){ + // skip facts involving integer equalities (from bv2nat) + if (!utils::isBitblastAtom(fact)) + { continue; } - if (!d_bv->inConflict() && - (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { + if (!d_bv->inConflict() + && (!d_bv->wasPropagatedBySubtheory(fact) + || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) + { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); // Assert to sat bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation); - if (!ok) { + if (!ok) + { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); - setConflict(mkConjunction(conflictAtoms)); + setConflict(utils::mkAnd(conflictAtoms)); return false; } } @@ -164,66 +171,73 @@ bool BitblastSolver::check(Theory::Effort e) { Debug("bv-bitblast-debug") << "...do propagation" << std::endl; // We need to ensure we are fully propagated, so propagate now - if (d_useSatPropagation) { + if (d_useSatPropagation) + { d_bv->spendResource(1); bool ok = d_bitblaster->propagate(); - if (!ok) { + if (!ok) + { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); - setConflict(mkConjunction(conflictAtoms)); + setConflict(utils::mkAnd(conflictAtoms)); return false; } } // Solving Debug("bv-bitblast-debug") << "...do solving" << std::endl; - if (e == Theory::EFFORT_FULL) { + if (e == Theory::EFFORT_FULL) + { Assert(!d_bv->inConflict()); - Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; + Debug("bitvector::bitblaster") + << "BitblastSolver::addAssertions solving. \n"; bool ok = d_bitblaster->solve(); - if (!ok) { + if (!ok) + { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); - Node conflict = mkConjunction(conflictAtoms); + Node conflict = utils::mkAnd(conflictAtoms); setConflict(conflict); return false; } } Debug("bv-bitblast-debug") << "...do abs bb" << std::endl; - if (options::bvAbstraction() && - e == Theory::EFFORT_FULL && - d_lemmaAtomsQueue.size()) { - + if (options::bvAbstraction() && e == Theory::EFFORT_FULL + && d_lemmaAtomsQueue.size()) + { // bit-blast lemma atoms - while(!d_lemmaAtomsQueue.empty()) { + while (!d_lemmaAtomsQueue.empty()) + { TNode lemma_atom = d_lemmaAtomsQueue.front(); d_lemmaAtomsQueue.pop(); - if( !utils::isBitblastAtom( lemma_atom ) ){ + if (!utils::isBitblastAtom(lemma_atom)) + { continue; } d_bitblaster->bbAtom(lemma_atom); // Assert to sat and check for conflicts bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation); - if (!ok) { + if (!ok) + { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); - setConflict(mkConjunction(conflictAtoms)); + setConflict(utils::mkAnd(conflictAtoms)); return false; } } Assert(!d_bv->inConflict()); bool ok = d_bitblaster->solve(); - if (!ok) { + if (!ok) + { std::vector conflictAtoms; d_bitblaster->getConflict(conflictAtoms); - Node conflict = mkConjunction(conflictAtoms); + Node conflict = utils::mkAnd(conflictAtoms); setConflict(conflict); ++(d_statistics.d_numBBLemmas); return false; } - } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index ef56a30cc..d458bc3a6 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -2,7 +2,7 @@ /*! \file theory_bv_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Liana Hadarean, Tim King + ** Aina Niemetz, Tim King, Liana Hadarean ** 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. @@ -424,26 +424,6 @@ Node mkUmulo(TNode t1, TNode t2) /* ------------------------------------------------------------------------- */ -Node mkConjunction(const std::vector& nodes) -{ - NodeBuilder<> conjunction(kind::AND); - Node btrue = mkTrue(); - for (const Node& n : nodes) - { - if (n != btrue) - { - Assert(isBVPredicate(n)); - conjunction << n; - } - } - unsigned nchildren = conjunction.getNumChildren(); - if (nchildren == 0) { return btrue; } - if (nchildren == 1) { return conjunction[0]; } - return conjunction; -} - -/* ------------------------------------------------------------------------- */ - Node flattenAnd(std::vector& queue) { TNodeSet nodes; diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index e1a37cf76..5c1080901 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -135,6 +135,9 @@ Node mkAnd(const std::vector>& conjunctions) for (const Node& n : all) { conjunction << n; } return conjunction; } + +/* ------------------------------------------------------------------------- */ + /* Create node of kind OR. */ Node mkOr(TNode node1, TNode node2); /* Create n-ary node of kind OR. */