cprover
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 <cstdint>
16 
17 #include <util/message.h>
18 #include <util/threeval.h>
19 
20 #include "literal.h"
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  // assumptions
88  virtual void set_assumptions(const bvt &) { }
89  virtual bool has_set_assumptions() const { return false; }
90 
91  // variables
92  virtual literalt new_variable()=0;
93  virtual void set_variable_name(literalt, const irep_idt &) { }
94  virtual size_t no_variables() const=0;
95  bvt new_variables(std::size_t width);
96 
97  // solving
98  virtual const std::string solver_text()=0;
101 
102  // satisfying assignment
103  virtual tvt l_get(literalt a) const=0;
104  virtual void set_assignment(literalt a, bool value) = 0;
105 
110  virtual bool is_in_conflict(literalt l) const = 0;
111  virtual bool has_is_in_conflict() const { return false; }
112 
113  // an incremental solver may remove any variables that aren't frozen
114  virtual void set_frozen(literalt) { }
115 
116  // Resource limits:
117  virtual void set_time_limit_seconds(uint32_t)
118  {
119  log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
120  }
121 
122  std::size_t get_number_of_solver_calls() const;
123 
124 protected:
125  virtual resultt do_prop_solve() = 0;
126 
127  // to avoid a temporary for lcnf(...)
129 
131  std::size_t number_of_solver_calls = 0;
132 };
133 
134 #endif // CPROVER_SOLVERS_PROP_PROP_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: prop.h:111
propt::set_assumptions
virtual void set_assumptions(const bvt &)
Definition: prop.h:88
propt::solver_text
virtual const std::string solver_text()=0
resultt
resultt
The result of goto verifying.
Definition: properties.h:44
propt::new_variables
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
propt::resultt::P_UNSATISFIABLE
@ P_UNSATISFIABLE
propt::set_equal
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
propt::lcnf
void lcnf(literalt l0, literalt l1, literalt l2)
Definition: prop.h:61
propt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:117
propt::new_variable
virtual literalt new_variable()=0
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
propt::l_set_to
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:47
messaget::eom
static eomt eom
Definition: message.h:297
propt::lor
virtual literalt lor(const bvt &bv)=0
propt::no_variables
virtual size_t no_variables() const =0
propt::do_prop_solve
virtual resultt do_prop_solve()=0
propt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop.h:89
propt::land
virtual literalt land(literalt a, literalt b)=0
propt::number_of_solver_calls
std::size_t number_of_solver_calls
Definition: prop.h:131
propt::lcnf
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
Definition: prop.h:70
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
propt::prop_solve
resultt prop_solve()
Definition: prop.cpp:29
propt::land
virtual literalt land(const bvt &bv)=0
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
propt::propt
propt(message_handlert &message_handler)
Definition: prop.h:27
propt::set_assignment
virtual void set_assignment(literalt a, bool value)=0
propt::lnand
virtual literalt lnand(literalt a, literalt b)=0
propt::lcnf
virtual void lcnf(const bvt &bv)=0
propt::resultt::P_ERROR
@ P_ERROR
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
propt::cnf_handled_well
virtual bool cnf_handled_well() const
Definition: prop.h:85
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
message_handlert
Definition: message.h:28
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:114
propt::resultt
resultt
Definition: prop.h:99
propt::get_number_of_solver_calls
std::size_t get_number_of_solver_calls() const
Definition: prop.cpp:35
propt::is_in_conflict
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
tvt
Definition: threeval.h:20
literal.h
propt::set_variable_name
virtual void set_variable_name(literalt, const irep_idt &)
Definition: prop.h:93
propt::l_set_to_false
void l_set_to_false(literalt a)
Definition: prop.h:54
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
propt::~propt
virtual ~propt()
Definition: prop.h:31
propt::l_get
virtual tvt l_get(literalt a) const =0
literalt
Definition: literal.h:26
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
propt::lxor
virtual literalt lxor(const bvt &bv)=0
propt::lcnf_bv
bvt lcnf_bv
Definition: prop.h:128
propt::log
messaget log
Definition: prop.h:130
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
propt::lnor
virtual literalt lnor(literalt a, literalt b)=0