cprover
satcheck_smvsat.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H
12 
13 #include <vector>
14 #include <set>
15 
16 #include <util/expr.h>
17 
18 #include "cnf.h"
19 
21 {
22 public:
24  virtual ~satcheck_smvsatt();
25 
26  virtual const std::string solver_text();
27  virtual resultt prop_solve();
28  virtual tvt l_get(literalt a) const;
29  virtual void lcnf(const bvt &bv);
30 
31 protected:
32  // NOLINTNEXTLINE(readability/identifiers)
33  struct sat_instance *satsolver;
34 };
35 
37 {
38 public:
40 
41  virtual resultt prop_solve();
42 
43  bool is_in_core(literalt l) const
44  {
45  assert(l.var_no()<in_core.size());
46  return in_core[l.var_no()];
47  }
48 
49 protected:
50  std::vector<bool> in_core;
51 };
52 
54 {
55 public:
57  {
58  }
59 
60  void set_partition_no(short p)
61  {
62  partition_no=p;
63  }
64 
65  void interpolate(exprt &dest);
66 
67 protected:
68  virtual void lcnf(const bvt &bv);
69  short partition_no;
70 
71  std::vector<short> partition_numbers;
72 
73  void build_aig(
74  // NOLINTNEXTLINE(readability/identifiers)
75  struct interpolator &interpolator_satsolver,
76  int output,
77  exprt &dest);
78 
79  struct entryt
80  {
81  int g;
82  exprt *e;
83 
84  entryt(int _g, exprt *_e):g(_g), e(_e)
85  {
86  }
87  };
88 };
89 
90 #endif // CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H
CNF Generation, via Tseitin.
std::vector< short > partition_numbers
virtual resultt prop_solve()
virtual ~satcheck_smvsatt()
virtual const std::string solver_text()
Definition: threeval.h:19
virtual void lcnf(const bvt &bv)
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
std::vector< bool > in_core
Base class for all expressions.
Definition: expr.h:46
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
bool is_in_core(literalt l) const
struct sat_instance * satsolver
void build_aig(struct interpolator &interpolator_satsolver, int output, exprt &dest)
std::vector< literalt > bvt
Definition: literal.h:197
virtual void lcnf(const bvt &bv)