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 a3442e4c61329a2eb5fddecd6a6f42da638aec5a..354b5837633041013bd6a7386b53222126127879 100644 (file)
--- 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<TNode> 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 b9467c1687ee43a8560af3215e0625a5bdecb536..61bbf667d437d1cde122e45eae38d8a07afbb4ff 100644 (file)
--- 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<TNode> 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<TNode> 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<TNode> 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<TNode> 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<TNode> 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 ef56a30ccb7c52e9040b5e9173eb659bfb3cd6ac..d458bc3a6866f19a477565b4c58edc8178b7292a 100644 (file)
--- 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<TNode>& 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<TNode>& queue)
 {
   TNodeSet nodes;

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index e1a37cf769b9377139552f19666cf59586406a31..5c10809015e713457ec2765bd7529e4b682f9c9d 100644 (file)
--- 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<NodeTemplate<ref_count>>& 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.  */