CBMC
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_PROP_H
11 #define CPROVER_SOLVERS_PROP_PROP_H
12 
13 // decision procedure wrapper for boolean propositional logics
14 
15 #include <util/message.h>
16 #include <util/threeval.h>
17 
18 #include "literal.h"
19 
20 #include <cstdint>
21 
24 class propt
25 {
26 public:
27  explicit propt(message_handlert &message_handler) : log(message_handler)
28  {
29  }
30 
31  virtual ~propt() { }
32 
33  // boolean operators
34  virtual literalt land(literalt a, literalt b)=0;
35  virtual literalt lor(literalt a, literalt b)=0;
36  virtual literalt land(const bvt &bv)=0;
37  virtual literalt lor(const bvt &bv)=0;
38  virtual literalt lxor(literalt a, literalt b)=0;
39  virtual literalt lxor(const bvt &bv)=0;
40  virtual literalt lnand(literalt a, literalt b)=0;
41  virtual literalt lnor(literalt a, literalt b)=0;
42  virtual literalt lequal(literalt a, literalt b)=0;
44  virtual literalt lselect(literalt a, literalt b, literalt c)=0; // a?b:c
45  virtual void set_equal(literalt a, literalt b);
46 
47  virtual void l_set_to(literalt a, bool value)
48  {
49  set_equal(a, const_literal(value));
50  }
51 
53  { l_set_to(a, true); }
55  { l_set_to(a, false); }
56 
57  // constraints
58  void lcnf(literalt l0, literalt l1)
59  { lcnf_bv.resize(2); lcnf_bv[0]=l0; lcnf_bv[1]=l1; lcnf(lcnf_bv); }
60 
61  void lcnf(literalt l0, literalt l1, literalt l2)
62  {
63  lcnf_bv.resize(3);
64  lcnf_bv[0]=l0;
65  lcnf_bv[1]=l1;
66  lcnf_bv[2]=l2;
67  lcnf(lcnf_bv);
68  }
69 
70  void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
71  {
72  lcnf_bv.resize(4);
73  lcnf_bv[0]=l0;
74  lcnf_bv[1]=l1;
75  lcnf_bv[2]=l2;
76  lcnf_bv[3]=l3;
77  lcnf(lcnf_bv);
78  }
79 
80  virtual void lcnf(const bvt &bv)=0;
81  virtual bool has_set_to() const { return true; }
82 
83  // Some solvers (notably aig) prefer encodings that avoid raw CNF
84  // They overload this to return false and thus avoid some optimisations
85  virtual bool cnf_handled_well() const { return true; }
86 
87  // solving with assumptions
88  virtual bool has_assumptions() const
89  {
90  return false;
91  }
92 
93  // variables
94  virtual literalt new_variable()=0;
95  virtual void set_variable_name(literalt, const irep_idt &) { }
96  virtual size_t no_variables() const=0;
97  virtual bvt new_variables(std::size_t width);
98 
99  // solving
100  virtual std::string solver_text() const = 0;
103  resultt prop_solve(const bvt &assumptions);
104 
105  // satisfying assignment
106  virtual tvt l_get(literalt a) const=0;
107  virtual void set_assignment(literalt a, bool value) = 0;
108 
113  virtual bool is_in_conflict(literalt l) const = 0;
114  virtual bool has_is_in_conflict() const { return false; }
115 
116  // an incremental solver may remove any variables that aren't frozen
117  virtual void set_frozen(literalt) { }
118 
119  // Resource limits:
120  virtual void set_time_limit_seconds(uint32_t)
121  {
122  log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
123  }
124 
125  std::size_t get_number_of_solver_calls() const;
126 
127 protected:
128  // solve under the given assumption
129  virtual resultt do_prop_solve(const bvt &assumptions) = 0;
130 
131  // to avoid a temporary for lcnf(...)
133 
135  std::size_t number_of_solver_calls = 0;
136 };
137 
138 #endif // CPROVER_SOLVERS_PROP_PROP_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
TO_BE_DOCUMENTED.
Definition: prop.h:25
propt(message_handlert &message_handler)
Definition: prop.h:27
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
Definition: prop.h:70
void l_set_to_true(literalt a)
Definition: prop.h:52
virtual literalt land(literalt a, literalt b)=0
std::size_t number_of_solver_calls
Definition: prop.h:135
virtual literalt lnand(literalt a, literalt b)=0
std::size_t get_number_of_solver_calls() const
Definition: prop.cpp:52
virtual size_t no_variables() const =0
virtual literalt lnor(literalt a, literalt b)=0
virtual literalt land(const bvt &bv)=0
virtual void set_variable_name(literalt, const irep_idt &)
Definition: prop.h:95
virtual literalt limplies(literalt a, literalt b)=0
bvt lcnf_bv
Definition: prop.h:132
virtual literalt lor(const bvt &bv)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual void set_frozen(literalt)
Definition: prop.h:117
virtual bool cnf_handled_well() const
Definition: prop.h:85
virtual literalt lxor(const bvt &bv)=0
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:47
virtual literalt lxor(literalt a, literalt b)=0
virtual resultt do_prop_solve(const bvt &assumptions)=0
virtual void set_assignment(literalt a, bool value)=0
virtual std::string solver_text() const =0
virtual ~propt()
Definition: prop.h:31
void lcnf(literalt l0, literalt l1, literalt l2)
Definition: prop.h:61
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
resultt prop_solve()
Definition: prop.cpp:39
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:30
virtual bool has_assumptions() const
Definition: prop.h:88
resultt
Definition: prop.h:101
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
void l_set_to_false(literalt a)
Definition: prop.h:54
virtual tvt l_get(literalt a) const =0
virtual bool has_set_to() const
Definition: prop.h:81
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:120
virtual void lcnf(const bvt &bv)=0
virtual bool has_is_in_conflict() const
Definition: prop.h:114
messaget log
Definition: prop.h:134
Definition: threeval.h:20
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
resultt
The result of goto verifying.
Definition: properties.h:45