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