GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_subtheory_bitblast.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_subtheory_bitblast.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Dejan Jovanovic
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 Algebraic solver.
13
 **
14
 ** Algebraic solver.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#pragma once
20
21
#include <unordered_map>
22
23
#include "theory/bv/bv_subtheory.h"
24
25
namespace CVC4 {
26
27
namespace theory {
28
namespace bv {
29
30
class TLazyBitblaster;
31
class AbstractionModule;
32
class BVQuickCheck;
33
class QuickXPlain;
34
35
/**
36
 * BitblastSolver
37
 */
38
class BitblastSolver : public SubtheorySolver
39
{
40
  struct Statistics
41
  {
42
    IntStat d_numCallstoCheck;
43
    IntStat d_numBBLemmas;
44
    Statistics();
45
    ~Statistics();
46
  };
47
  /** Bitblaster */
48
  std::unique_ptr<TLazyBitblaster> d_bitblaster;
49
50
  /** Nodes that still need to be bit-blasted */
51
  context::CDQueue<TNode> d_bitblastQueue;
52
  Statistics d_statistics;
53
54
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
55
  NodeMap d_modelCache;
56
  context::CDO<bool> d_validModelCache;
57
58
  /** Queue for bit-blasting lemma atoms only in full check if we are sat */
59
  context::CDQueue<TNode> d_lemmaAtomsQueue;
60
  bool d_useSatPropagation;
61
  AbstractionModule* d_abstractionModule;
62
  std::unique_ptr<BVQuickCheck> d_quickCheck;
63
  std::unique_ptr<QuickXPlain> d_quickXplain;
64
  //  Node getModelValueRec(TNode node);
65
  void setConflict(TNode conflict);
66
67
 public:
68
  BitblastSolver(context::Context* c, BVSolverLazy* bv);
69
  ~BitblastSolver();
70
71
  void preRegister(TNode node) override;
72
  bool check(Theory::Effort e) override;
73
  void explain(TNode literal, std::vector<TNode>& assumptions) override;
74
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
75
  bool collectModelValues(TheoryModel* m,
76
                          const std::set<Node>& termSet) override;
77
  Node getModelValue(TNode node) override;
78
182243
  bool isComplete() override { return true; }
79
  void bitblastQueue();
80
  void setAbstraction(AbstractionModule* module);
81
  uint64_t computeAtomWeight(TNode atom);
82
};
83
84
}  // namespace bv
85
}  // namespace theory
86
} /* namespace CVC4 */