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:public messaget
25 {
26 public:
27  propt() { }
28  virtual ~propt() { }
29 
30  // boolean operators
31  virtual literalt land(literalt a, literalt b)=0;
32  virtual literalt lor(literalt a, literalt b)=0;
33  virtual literalt land(const bvt &bv)=0;
34  virtual literalt lor(const bvt &bv)=0;
35  virtual literalt lxor(literalt a, literalt b)=0;
36  virtual literalt lxor(const bvt &bv)=0;
37  virtual literalt lnand(literalt a, literalt b)=0;
38  virtual literalt lnor(literalt a, literalt b)=0;
39  virtual literalt lequal(literalt a, literalt b)=0;
40  virtual literalt limplies(literalt a, literalt b)=0;
41  virtual literalt lselect(literalt a, literalt b, literalt c)=0; // a?b:c
42  virtual void set_equal(literalt a, literalt b);
43 
44  virtual void l_set_to(literalt a, bool value)
45  {
46  set_equal(a, const_literal(value));
47  }
48 
50  { l_set_to(a, true); }
52  { l_set_to(a, false); }
53 
54  // constraints
55  void lcnf(literalt l0, literalt l1)
56  { lcnf_bv.resize(2); lcnf_bv[0]=l0; lcnf_bv[1]=l1; lcnf(lcnf_bv); }
57 
58  void lcnf(literalt l0, literalt l1, literalt l2)
59  {
60  lcnf_bv.resize(3);
61  lcnf_bv[0]=l0;
62  lcnf_bv[1]=l1;
63  lcnf_bv[2]=l2;
64  lcnf(lcnf_bv);
65  }
66 
67  void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
68  {
69  lcnf_bv.resize(4);
70  lcnf_bv[0]=l0;
71  lcnf_bv[1]=l1;
72  lcnf_bv[2]=l2;
73  lcnf_bv[3]=l3;
74  lcnf(lcnf_bv);
75  }
76 
77  virtual void lcnf(const bvt &bv)=0;
78  virtual bool has_set_to() const { return true; }
79 
80  // Some solvers (notably aig) prefer encodings that avoid raw CNF
81  // They overload this to return false and thus avoid some optimisations
82  virtual bool cnf_handled_well() const { return true; }
83 
84  // assumptions
85  virtual void set_assumptions(const bvt &) { }
86  virtual bool has_set_assumptions() const { return false; }
87 
88  // variables
89  virtual literalt new_variable()=0;
90  virtual void set_variable_name(literalt, const irep_idt &) { }
91  virtual size_t no_variables() const=0;
92  bvt new_variables(std::size_t width);
93 
94  // solving
95  virtual const std::string solver_text()=0;
97  virtual resultt prop_solve()=0;
98 
99  // satisfying assignment
100  virtual tvt l_get(literalt a) const=0;
101  virtual void set_assignment(literalt a, bool value) = 0;
102 
107  virtual bool is_in_conflict(literalt l) const = 0;
108  virtual bool has_is_in_conflict() const { return false; }
109 
110  // an incremental solver may remove any variables that aren't frozen
111  virtual void set_frozen(literalt) { }
112 
113  // Resource limits:
114  virtual void set_time_limit_seconds(uint32_t)
115  {
116  warning() << "CPU limit ignored (not implemented)" << eom;
117  }
118 
119 protected:
120  // to avoid a temporary for lcnf(...)
122 };
123 
124 #endif // CPROVER_SOLVERS_PROP_PROP_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
propt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: prop.h:108
propt::set_assumptions
virtual void set_assumptions(const bvt &)
Definition: prop.h:85
propt::solver_text
virtual const std::string solver_text()=0
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:200
threeval.h
propt::resultt::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:58
propt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:114
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:49
propt::l_set_to
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:44
messaget::eom
static eomt eom
Definition: message.h:284
propt::no_variables
virtual size_t no_variables() const =0
propt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop.h:86
propt::land
virtual literalt land(literalt a, literalt b)=0
propt::lcnf
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
Definition: prop.h:67
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
propt::set_assignment
virtual void set_assignment(literalt a, bool value)=0
propt::lnand
virtual literalt lnand(literalt a, literalt b)=0
propt::resultt::P_ERROR
propt::resultt::P_SATISFIABLE
propt::cnf_handled_well
virtual bool cnf_handled_well() const
Definition: prop.h:82
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:111
propt::resultt
resultt
Definition: prop.h:96
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:19
literal.h
propt::set_variable_name
virtual void set_variable_name(literalt, const irep_idt &)
Definition: prop.h:90
propt::l_set_to_false
void l_set_to_false(literalt a)
Definition: prop.h:51
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
propt::~propt
virtual ~propt()
Definition: prop.h:28
propt::l_get
virtual tvt l_get(literalt a) const =0
propt::prop_solve
virtual resultt prop_solve()=0
literalt
Definition: literal.h:24
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:78
propt::lcnf_bv
bvt lcnf_bv
Definition: prop.h:121
message.h
propt::propt
propt()
Definition: prop.h:27
messaget::warning
mstreamt & warning() const
Definition: message.h:391
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:55
propt::lnor
virtual literalt lnor(literalt a, literalt b)=0