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

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_quick_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Morgan Deters
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 Sandboxed sat solver for bv quickchecks.
13
 **
14
 ** Sandboxed sat solver for bv quickchecks.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__BV_QUICK_CHECK_H
20
#define CVC4__BV_QUICK_CHECK_H
21
22
#include <unordered_set>
23
#include <vector>
24
25
#include "context/cdo.h"
26
#include "expr/node.h"
27
#include "prop/sat_solver_types.h"
28
#include "theory/bv/theory_bv_utils.h"
29
#include "util/statistics_registry.h"
30
#include "util/stats_timer.h"
31
32
namespace CVC4 {
33
namespace theory {
34
35
class TheoryModel;
36
37
namespace bv {
38
39
class TLazyBitblaster;
40
class BVSolverLazy;
41
42
class BVQuickCheck
43
{
44
  context::Context d_ctx;
45
  std::unique_ptr<TLazyBitblaster> d_bitblaster;
46
  Node d_conflict;
47
  context::CDO<bool> d_inConflict;
48
  void setConflict();
49
50
 public:
51
  BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv);
52
  ~BVQuickCheck();
53
  bool inConflict();
54
  Node getConflict() { return d_conflict; }
55
  /**
56
   * Checks the satisfiability for a given set of assumptions.
57
   *
58
   * @param assumptions literals assumed true
59
   * @param budget max number of conflicts
60
   *
61
   * @return
62
   */
63
  prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
64
  /**
65
   * Checks the satisfiability of given assertions.
66
   *
67
   * @param budget max number of conflicts
68
   *
69
   * @return
70
   */
71
  prop::SatValue checkSat(unsigned long budget);
72
73
  /**
74
   * Convert to CNF and assert the given literal.
75
   *
76
   * @param assumption bv literal
77
   *
78
   * @return false if a conflict has been found via bcp.
79
   */
80
  bool addAssertion(TNode assumption);
81
82
  void push();
83
  void pop();
84
  void popToZero();
85
  /**
86
   * Deletes the SAT solver and CNF stream, but maintains the
87
   * bit-blasting term cache.
88
   *
89
   */
90
  void clearSolver();
91
92
  /**
93
   * Computes the size of the circuit required to bit-blast
94
   * atom, by not recounting the nodes in seen.
95
   *
96
   * @param node
97
   * @param seen
98
   *
99
   * @return
100
   */
101
  uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
102
  bool collectModelValues(theory::TheoryModel* model,
103
                          const std::set<Node>& termSet);
104
105
  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
106
      vars_iterator;
107
  vars_iterator beginVars();
108
  vars_iterator endVars();
109
110
  Node getVarValue(TNode var, bool fullModel);
111
};
112
113
class QuickXPlain
114
{
115
  struct Statistics
116
  {
117
    TimerStat d_xplainTime;
118
    IntStat d_numSolved;
119
    IntStat d_numUnknown;
120
    IntStat d_numUnknownWasUnsat;
121
    IntStat d_numConflictsMinimized;
122
    IntStat d_finalPeriod;
123
    AverageStat d_avgMinimizationRatio;
124
    Statistics(const std::string& name);
125
    ~Statistics();
126
  };
127
  BVQuickCheck* d_solver;
128
  unsigned long d_budget;
129
130
  // crazy heuristic variables
131
  unsigned d_numCalled;  // number of times called
132
  double d_minRatioSum;  // sum of minimization ratio for computing average min
133
                         // ratio
134
  unsigned d_numConflicts;  // number of conflicts (including when minimization
135
                            // not applied)
136
  // unsigned d_period; // after how many conflicts to try minimizing again
137
138
  // double d_thresh; // if minimization ratio is less, increase period
139
  // double d_hardThresh; // decrease period if minimization ratio is greater
140
  // than this
141
142
  Statistics d_statistics;
143
  /**
144
   * Uses solve with assumptions unsat core feature to
145
   * further minimize a conflict. The minimized conflict
146
   * will be between low and the returned value in conflict.
147
   *
148
   * @param low
149
   * @param high
150
   * @param conflict
151
   *
152
   * @return
153
   */
154
  unsigned selectUnsatCore(unsigned low,
155
                           unsigned high,
156
                           std::vector<TNode>& conflict);
157
  /**
158
   * Internal conflict  minimization, attempts to minimize
159
   * literals in conflict between low and high and adds the
160
   * result in new_conflict.
161
   *
162
   * @param low
163
   * @param high
164
   * @param conflict
165
   * @param new_conflict
166
   */
167
  void minimizeConflictInternal(unsigned low,
168
                                unsigned high,
169
                                std::vector<TNode>& conflict,
170
                                std::vector<TNode>& new_conflict);
171
172
  bool useHeuristic();
173
174
 public:
175
  QuickXPlain(const std::string& name,
176
              BVQuickCheck* solver,
177
              unsigned long budged = 10000);
178
  ~QuickXPlain();
179
  Node minimizeConflict(TNode conflict);
180
};
181
182
}  // namespace bv
183
}  // namespace theory
184
}  // namespace CVC4
185
186
#endif /* CVC4__BV_QUICK_CHECK_H */