GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_solver_simple.h Lines: 4 5 80.0 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_simple.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Andrew Reynolds, 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 bit-blast lemmas directly to MiniSat.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
20
#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
21
22
#include "theory/bv/bitblast/proof_bitblaster.h"
23
#include "theory/bv/bv_solver.h"
24
#include "theory/bv/proof_checker.h"
25
#include "theory/eager_proof_generator.h"
26
27
namespace CVC4 {
28
29
namespace theory {
30
namespace bv {
31
32
/**
33
 * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
34
 * internal MiniSat. It is also ablo to handle atoms of kind
35
 * BITVECTOR_EAGER_ATOM.
36
 *
37
 * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
38
 */
39
class BVSolverSimple : public BVSolver
40
{
41
 public:
42
  BVSolverSimple(TheoryState* state,
43
                 TheoryInferenceManager& inferMgr,
44
                 ProofNodeManager* pnm);
45
20
  ~BVSolverSimple() = default;
46
47
1030
  void preRegisterTerm(TNode n) override {}
48
49
  bool preNotifyFact(TNode atom,
50
                     bool pol,
51
                     TNode fact,
52
                     bool isPrereg,
53
                     bool isInternal) override;
54
55
  std::string identify() const override { return "BVSolverSimple"; };
56
57
30
  Theory::PPAssertStatus ppAssert(
58
      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
59
  {
60
30
    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
61
  }
62
63
  bool collectModelValues(TheoryModel* m,
64
                          const std::set<Node>& termSet) override;
65
66
 private:
67
  /**
68
   * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
69
   * inference manager.
70
   */
71
  void addBBLemma(TNode fact);
72
73
  /** Bit-blaster used to bit-blast atoms/terms. */
74
  std::unique_ptr<BBProof> d_bitblaster;
75
76
  /** Proof generator that manages proofs for lemmas generated by this class. */
77
  std::unique_ptr<EagerProofGenerator> d_epg;
78
79
  BVProofRuleChecker d_bvProofChecker;
80
};
81
82
}  // namespace bv
83
}  // namespace theory
84
}  // namespace CVC4
85
86
#endif