GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver_simple.cpp Lines: 33 62 53.2 %
Date: 2021-03-23 Branches: 62 208 29.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_simple.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Gereon Kremer, Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
35320
bool isBVAtom(TNode n)
32
{
33
71208
  return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
34
34752
         || n.getKind() == kind::BITVECTOR_ULT
35
34728
         || n.getKind() == kind::BITVECTOR_ULE
36
34728
         || n.getKind() == kind::BITVECTOR_SLT
37
140688
         || 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
10
BVSolverSimple::BVSolverSimple(TheoryState* s,
70
                               TheoryInferenceManager& inferMgr,
71
10
                               ProofNodeManager* pnm)
72
    : BVSolver(*s, inferMgr),
73
10
      d_bitblaster(new BBProof(s)),
74
2
      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
75
22
                : nullptr)
76
{
77
10
  if (pnm != nullptr)
78
  {
79
1
    d_bvProofChecker.registerTo(pnm->getChecker());
80
  }
81
10
}
82
83
592
void BVSolverSimple::addBBLemma(TNode fact)
84
{
85
592
  if (!d_bitblaster->hasBBAtom(fact))
86
  {
87
120
    d_bitblaster->bbAtom(fact);
88
  }
89
592
  NodeManager* nm = NodeManager::currentNM();
90
91
1184
  Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
92
1184
  Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
93
94
592
  if (d_epg == nullptr)
95
  {
96
592
    d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
97
  }
98
  else
99
  {
100
    TrustNode tlem = d_epg->mkTrustNode(lemma, PfRule::BV_BITBLAST, {}, {fact});
101
    d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
102
  }
103
592
}
104
105
35320
bool BVSolverSimple::preNotifyFact(
106
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
107
{
108
35320
  if (fact.getKind() == kind::NOT)
109
  {
110
33778
    fact = fact[0];
111
  }
112
113
35320
  if (isBVAtom(fact))
114
  {
115
592
    addBBLemma(fact);
116
  }
117
34728
  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::BV_SIMPLE_LEMMA);
127
    }
128
    else
129
    {
130
      TrustNode tlem =
131
          d_epg->mkTrustNode(lemma, PfRule::BV_EAGER_ATOM, {}, {fact});
132
      d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
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
35320
  return true;
144
}
145
146
6
bool BVSolverSimple::collectModelValues(TheoryModel* m,
147
                                        const std::set<Node>& termSet)
148
{
149
6
  return d_bitblaster->collectModelValues(m, termSet);
150
}
151
152
}  // namespace bv
153
}  // namespace theory
154
26685
}  // namespace CVC4