cprover
prop.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
22class propt
23{
24public:
25 explicit propt(message_handlert &message_handler) : log(message_handler)
26 {
27 }
28
29 virtual ~propt() { }
30
31 // boolean operators
32 virtual literalt land(literalt a, literalt b)=0;
33 virtual literalt lor(literalt a, literalt b)=0;
34 virtual literalt land(const bvt &bv)=0;
35 virtual literalt lor(const bvt &bv)=0;
36 virtual literalt lxor(literalt a, literalt b)=0;
37 virtual literalt lxor(const bvt &bv)=0;
39 virtual literalt lnor(literalt a, literalt b)=0;
42 virtual literalt lselect(literalt a, literalt b, literalt c)=0; // a?b:c
43 virtual void set_equal(literalt a, literalt b);
44
45 virtual void l_set_to(literalt a, bool value)
46 {
47 set_equal(a, const_literal(value));
48 }
49
51 { l_set_to(a, true); }
53 { l_set_to(a, false); }
54
55 // constraints
56 void lcnf(literalt l0, literalt l1)
57 { lcnf_bv.resize(2); lcnf_bv[0]=l0; lcnf_bv[1]=l1; lcnf(lcnf_bv); }
58
59 void lcnf(literalt l0, literalt l1, literalt l2)
60 {
61 lcnf_bv.resize(3);
62 lcnf_bv[0]=l0;
63 lcnf_bv[1]=l1;
64 lcnf_bv[2]=l2;
66 }
67
68 void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
69 {
70 lcnf_bv.resize(4);
71 lcnf_bv[0]=l0;
72 lcnf_bv[1]=l1;
73 lcnf_bv[2]=l2;
74 lcnf_bv[3]=l3;
76 }
77
78 virtual void lcnf(const bvt &bv)=0;
79 virtual bool has_set_to() const { return true; }
80
81 // Some solvers (notably aig) prefer encodings that avoid raw CNF
82 // They overload this to return false and thus avoid some optimisations
83 virtual bool cnf_handled_well() const { return true; }
84
85 // assumptions
86 virtual void set_assumptions(const bvt &) { }
87 virtual bool has_set_assumptions() const { return false; }
88
89 // variables
91 virtual void set_variable_name(literalt, const irep_idt &) { }
92 virtual size_t no_variables() const=0;
93 virtual bvt new_variables(std::size_t width);
94
95 // solving
96 virtual const std::string solver_text()=0;
97 enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
99
100 // satisfying assignment
101 virtual tvt l_get(literalt a) const=0;
102 virtual void set_assignment(literalt a, bool value) = 0;
103
108 virtual bool is_in_conflict(literalt l) const = 0;
109 virtual bool has_is_in_conflict() const { return false; }
110
111 // an incremental solver may remove any variables that aren't frozen
112 virtual void set_frozen(literalt) { }
113
114 // Resource limits:
115 virtual void set_time_limit_seconds(uint32_t)
116 {
117 log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
118 }
119
120 std::size_t get_number_of_solver_calls() const;
121
122protected:
123 virtual resultt do_prop_solve() = 0;
124
125 // to avoid a temporary for lcnf(...)
127
129 std::size_t number_of_solver_calls = 0;
130};
131
132#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:37
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:23
propt(message_handlert &message_handler)
Definition: prop.h:25
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
Definition: prop.h:68
void l_set_to_true(literalt a)
Definition: prop.h:50
virtual literalt land(literalt a, literalt b)=0
std::size_t number_of_solver_calls
Definition: prop.h:129
virtual literalt lnand(literalt a, literalt b)=0
std::size_t get_number_of_solver_calls() const
Definition: prop.cpp:35
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:91
virtual bool has_set_assumptions() const
Definition: prop.h:87
virtual literalt limplies(literalt a, literalt b)=0
bvt lcnf_bv
Definition: prop.h:126
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:112
virtual bool cnf_handled_well() const
Definition: prop.h:83
virtual literalt lxor(const bvt &bv)=0
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:45
virtual literalt lxor(literalt a, literalt b)=0
virtual void set_assignment(literalt a, bool value)=0
virtual ~propt()
Definition: prop.h:29
virtual void set_assumptions(const bvt &)
Definition: prop.h:86
void lcnf(literalt l0, literalt l1, literalt l2)
Definition: prop.h:59
void lcnf(literalt l0, literalt l1)
Definition: prop.h:56
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:29
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
resultt
Definition: prop.h:97
virtual resultt do_prop_solve()=0
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:52
virtual tvt l_get(literalt a) const =0
virtual bool has_set_to() const
Definition: prop.h:79
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:115
virtual void lcnf(const bvt &bv)=0
virtual const std::string solver_text()=0
virtual bool has_is_in_conflict() const
Definition: prop.h:109
messaget log
Definition: prop.h:128
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