src/theory/bv/bv_solver_simple.cpp

   1 /*********************                                                        */
   2 /*! \file bv_solver_simple.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Simple bit-blast solver
  13  **
  14  ** Simple bit-blast solver that sends bitblast lemmas directly to MiniSat.
  15  **/
  16
  17 #include "theory/bv/bv_solver_simple.h"
  18
  19 #include "theory/bv/theory_bv.h"
  20 #include "theory/bv/theory_bv_utils.h"
  21 #include "theory/theory_model.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace bv {
  26
  27 /* -------------------------------------------------------------------------- */
  28
  29 namespace {
  30
  31 bool isBVAtom(TNode n)
  32 {
  33   return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
  34          || n.getKind() == kind::BITVECTOR_ULT
  35          || n.getKind() == kind::BITVECTOR_ULE
  36          || n.getKind() == kind::BITVECTOR_SLT
  37          || n.getKind() == kind::BITVECTOR_SLE;
  38 }
  39
  40 /* Traverse Boolean nodes and collect BV atoms. */
  41 void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
  42 {
  43   std::vector<TNode> visit;
  44   std::unordered_set<TNode, TNodeHashFunction> visited;
  45
  46   visit.push_back(n);
  47
  48   do
  49   {
  50     TNode cur = visit.back();
  51     visit.pop_back();
  52
  53     if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
  54       continue;
  55
  56     visited.insert(cur);
  57     if (isBVAtom(cur))
  58     {
  59       atoms.insert(cur);
  60       continue;
  61     }
  62
  63     visit.insert(visit.end(), cur.begin(), cur.end());
  64   } while (!visit.empty());
  65 }
  66
  67 }  // namespace
  68
  69 BVSolverSimple::BVSolverSimple(TheoryState* s,
  70                                TheoryInferenceManager& inferMgr,
  71                                ProofNodeManager* pnm)
  72     : BVSolver(*s, inferMgr),
  73       d_bitblaster(new BBSimple(s)),
  74       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
  75                 : nullptr)
  76 {
  77   if (pnm != nullptr)
  78   {
  79     d_bvProofChecker.registerTo(pnm->getChecker());
  80   }
  81 }
  82
  83 void BVSolverSimple::addBBLemma(TNode fact)
  84 {
  85   if (!d_bitblaster->hasBBAtom(fact))
  86   {
  87     d_bitblaster->bbAtom(fact);
  88   }
  89   NodeManager* nm = NodeManager::currentNM();
  90
  91   Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
  92   Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
  93
  94   if (d_epg == nullptr)
  95   {
  96     d_im.lemma(lemma, InferenceId::UNKNOWN);
  97   }
  98   else
  99   {
 100     TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
 101     d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
 102   }
 103 }
 104
 105 bool BVSolverSimple::preNotifyFact(
 106     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 107 {
 108   if (fact.getKind() == kind::NOT)
 109   {
 110     fact = fact[0];
 111   }
 112
 113   if (isBVAtom(fact))
 114   {
 115     addBBLemma(fact);
 116   }
 117   else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 118   {
 119     TNode n = fact[0];
 120
 121     NodeManager* nm = NodeManager::currentNM();
 122     Node lemma = nm->mkNode(kind::EQUAL, fact, n);
 123
 124     if (d_epg == nullptr)
 125     {
 126       d_im.lemma(lemma, InferenceId::UNKNOWN);
 127     }
 128     else
 129     {
 130       TrustNode tlem =
 131           d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
 132       d_im.trustedLemma(tlem, InferenceId::UNKNOWN);
 133     }
 134
 135     std::unordered_set<Node, NodeHashFunction> bv_atoms;
 136     collectBVAtoms(n, bv_atoms);
 137     for (const Node& nn : bv_atoms)
 138     {
 139       addBBLemma(nn);
 140     }
 141   }
 142
 143   return true;
 144 }
 145
 146 bool BVSolverSimple::collectModelValues(TheoryModel* m,
 147                                         const std::set<Node>& termSet)
 148 {
 149   return d_bitblaster->collectModelValues(m, termSet);
 150 }
 151
 152 }  // namespace bv
 153 }  // namespace theory
 154 }  // namespace CVC4