cprover
aig_prop.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_PROP_AIG_PROP_H
11 #define CPROVER_SOLVERS_PROP_AIG_PROP_H
12 
13 #include <cassert>
14 
15 #include <util/threeval.h>
16 #include <solvers/prop/prop.h>
17 
18 #include "aig.h"
19 
20 class aig_prop_baset:public propt
21 {
22 public:
23  explicit aig_prop_baset(aigt &_dest):dest(_dest)
24  {
25  }
26 
27  bool has_set_to() const override { return false; }
28  bool cnf_handled_well() const override { return false; }
29 
30  literalt land(literalt a, literalt b) override;
31  literalt lor(literalt a, literalt b) override;
32  literalt land(const bvt &bv) override;
33  literalt lor(const bvt &bv) override;
34  void lcnf(const bvt &clause) override { assert(false); }
35  literalt lxor(literalt a, literalt b) override;
36  literalt lxor(const bvt &bv) override;
37  literalt lnand(literalt a, literalt b) override;
38  literalt lnor(literalt a, literalt b) override;
39  literalt lequal(literalt a, literalt b) override;
40  literalt limplies(literalt a, literalt b) override;
41  literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
42  void set_equal(literalt a, literalt b) override;
43 
44  void l_set_to(literalt a, bool value) override { assert(false); }
45 
47  {
48  return dest.new_node();
49  }
50 
51  size_t no_variables() const override
52  { return dest.number_of_nodes(); }
53 
54  const std::string solver_text() override
55  { return "conversion into and-inverter graph"; }
56 
57  tvt l_get(literalt a) const override
58  { assert(0); return tvt::unknown(); }
59 
60  resultt prop_solve() override
61  { assert(0); return resultt::P_ERROR; }
62 
63 protected:
65 };
66 
68 {
69 public:
71  aig_prop_baset(_dest),
72  dest(_dest)
73  {
74  }
75 
77  bool has_set_to() const override { return true; }
78 
79  void lcnf(const bvt &clause) override
80  {
81  l_set_to_true(lor(clause));
82  }
83 
84  void l_set_to(literalt a, bool value) override
85  {
86  dest.constraints.push_back(a^!value);
87  }
88 };
89 
91 {
92 public:
93  explicit aig_prop_solvert(propt &_solver):
95  solver(_solver)
96  {
97  }
98 
100 
101  const std::string solver_text() override
102  {
103  return
104  "conversion into and-inverter graph followed by "+
105  solver.solver_text();
106  }
107 
108  tvt l_get(literalt a) const override;
109  resultt prop_solve() override;
110 
112  {
114  solver.set_message_handler(m);
115  }
116 
117 protected:
119 
120  void convert_aig();
121  void usage_count(
122  std::vector<unsigned> &p_usage_count, std::vector<unsigned> &n_usage_count);
123  void compute_phase(std::vector<bool> &n_pos, std::vector<bool> &n_neg);
124  void convert_node(
125  unsigned n,
126  const aigt::nodet &node,
127  bool n_pos,
128  bool n_neg,
129  std::vector<unsigned> &p_usage_count,
130  std::vector<unsigned> &n_usage_count);
131 };
132 
133 #endif // CPROVER_SOLVERS_PROP_AIG_PROP_H
bool has_set_to() const override
Definition: aig_prop.h:27
literalt land(literalt a, literalt b) override
Definition: aig_prop.cpp:56
literalt lnor(literalt a, literalt b) override
Definition: aig_prop.cpp:102
tvt l_get(literalt a) const override
Definition: aig_prop.h:57
resultt prop_solve() override
Definition: aig_prop.h:60
void l_set_to(literalt a, bool value) override
Definition: aig_prop.h:44
aig_prop_solvert(propt &_solver)
Definition: aig_prop.h:93
Definition: aig.h:52
aig_prop_constraintt(aig_plus_constraintst &_dest)
Definition: aig_prop.h:70
literalt lxor(literalt a, literalt b) override
Definition: aig_prop.cpp:76
static tvt unknown()
Definition: threeval.h:33
const std::string solver_text() override
Definition: aig_prop.h:54
void set_equal(literalt a, literalt b) override
asserts a==b in the propositional formula
Definition: aig_prop.cpp:132
void set_message_handler(message_handlert &m) override
Definition: aig_prop.h:111
void l_set_to(literalt a, bool value) override
Definition: aig_prop.h:84
void l_set_to_true(literalt a)
Definition: prop.h:47
propt & solver
Definition: aig_prop.h:118
aig_prop_baset(aigt &_dest)
Definition: aig_prop.h:23
nodest::size_type number_of_nodes() const
Definition: aig.h:89
literalt lnand(literalt a, literalt b) override
Definition: aig_prop.cpp:97
AND-Inverter Graph.
bool cnf_handled_well() const override
Definition: aig_prop.h:28
size_t no_variables() const override
Definition: aig_prop.h:51
Definition: aig.h:21
Definition: threeval.h:19
void lcnf(const bvt &clause) override
Definition: aig_prop.h:34
literalt lselect(literalt a, literalt b, literalt c) override
Definition: aig_prop.cpp:117
resultt
Definition: prop.h:94
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
aig_plus_constraintst & dest
Definition: aig_prop.h:76
TO_BE_DOCUMENTED.
Definition: prop.h:22
void lcnf(const bvt &clause) override
Definition: aig_prop.h:79
literalt lequal(literalt a, literalt b) override
Definition: aig_prop.cpp:107
bool has_set_to() const override
Definition: aig_prop.h:77
literalt new_node()
Definition: aig.h:99
literalt new_variable() override
Definition: aig_prop.h:46
const std::string solver_text() override
Definition: aig_prop.h:101
aigt & dest
Definition: aig_prop.h:64
literalt limplies(literalt a, literalt b) override
Definition: aig_prop.cpp:112
literalt lor(literalt a, literalt b) override
Definition: aig_prop.cpp:71
aig_plus_constraintst aig
Definition: aig_prop.h:99
constraintst constraints
Definition: aig.h:148
std::vector< literalt > bvt
Definition: literal.h:197