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 <util/message.h>
16 #include <util/threeval.h>
17 
18 #include "prop_assignment.h"
19 
22 class propt:public messaget, public prop_assignmentt
23 {
24 public:
25  propt() { }
26  virtual ~propt() { }
27 
28  // boolean operators
29  virtual literalt land(literalt a, literalt b)=0;
30  virtual literalt lor(literalt a, literalt b)=0;
31  virtual literalt land(const bvt &bv)=0;
32  virtual literalt lor(const bvt &bv)=0;
33  virtual literalt lxor(literalt a, literalt b)=0;
34  virtual literalt lxor(const bvt &bv)=0;
35  virtual literalt lnand(literalt a, literalt b)=0;
36  virtual literalt lnor(literalt a, literalt b)=0;
37  virtual literalt lequal(literalt a, literalt b)=0;
38  virtual literalt limplies(literalt a, literalt b)=0;
39  virtual literalt lselect(literalt a, literalt b, literalt c)=0; // a?b:c
40  virtual void set_equal(literalt a, literalt b);
41 
42  virtual void l_set_to(literalt a, bool value)
43  {
44  set_equal(a, const_literal(value));
45  }
46 
48  { l_set_to(a, true); }
50  { l_set_to(a, false); }
51 
52  // constraints
53  void lcnf(literalt l0, literalt l1)
54  { lcnf_bv.resize(2); lcnf_bv[0]=l0; lcnf_bv[1]=l1; lcnf(lcnf_bv); }
55 
56  void lcnf(literalt l0, literalt l1, literalt l2)
57  {
58  lcnf_bv.resize(3);
59  lcnf_bv[0]=l0;
60  lcnf_bv[1]=l1;
61  lcnf_bv[2]=l2;
62  lcnf(lcnf_bv);
63  }
64 
65  void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
66  {
67  lcnf_bv.resize(4);
68  lcnf_bv[0]=l0;
69  lcnf_bv[1]=l1;
70  lcnf_bv[2]=l2;
71  lcnf_bv[3]=l3;
72  lcnf(lcnf_bv);
73  }
74 
75  virtual void lcnf(const bvt &bv)=0;
76  virtual bool has_set_to() const { return true; }
77 
78  // Some solvers (notably aig) prefer encodings that avoid raw CNF
79  // They overload this to return false and thus avoid some optimisations
80  virtual bool cnf_handled_well() const { return true; }
81 
82  // assumptions
83  virtual void set_assumptions(const bvt &_assumptions) { }
84  virtual bool has_set_assumptions() const { return false; }
85 
86  // variables
87  virtual literalt new_variable()=0;
88  virtual void set_variable_name(literalt a, const std::string &name) { }
89  virtual size_t no_variables() const=0;
90  bvt new_variables(std::size_t width);
91 
92  // solving
93  virtual const std::string solver_text()=0;
95  virtual resultt prop_solve()=0;
96 
97  // satisfying assignment, from prop_assignmentt
98  virtual tvt l_get(literalt a) const=0;
99  virtual void set_assignment(literalt a, bool value);
100  virtual void copy_assignment_from(const propt &prop);
101 
102  // Returns true if an assumption is in the final conflict.
103  // Note that only literals that are assumptions (see set_assumptions)
104  // may be queried.
105  virtual bool is_in_conflict(literalt l) const;
106  virtual bool has_is_in_conflict() const { return false; }
107 
108  // an incremental solver may remove any variables that aren't frozen
109  virtual void set_frozen(literalt a) { }
110 
111 protected:
112  // to avoid a temporary for lcnf(...)
114 };
115 
116 #endif // CPROVER_SOLVERS_PROP_PROP_H
void lcnf(literalt l0, literalt l1, literalt l2)
Definition: prop.h:56
virtual void set_frozen(literalt a)
Definition: prop.h:109
virtual bool has_is_in_conflict() const
Definition: prop.h:106
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
virtual const std::string solver_text()=0
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
virtual literalt lor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
Definition: prop.h:65
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:14
virtual bool has_set_assumptions() const
Definition: prop.h:84
virtual literalt land(literalt a, literalt b)=0
TO_BE_DOCUMENTED.
virtual literalt new_variable()=0
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:42
virtual void set_variable_name(literalt a, const std::string &name)
Definition: prop.h:88
virtual literalt lxor(literalt a, literalt b)=0
virtual size_t no_variables() const =0
Definition: threeval.h:19
virtual void set_assignment(literalt a, bool value)
Definition: prop.cpp:20
void l_set_to_false(literalt a)
Definition: prop.h:49
resultt
Definition: prop.h:94
virtual bool cnf_handled_well() const
Definition: prop.h:80
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop.h:83
virtual ~propt()
Definition: prop.h:26
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
literalt const_literal(bool value)
Definition: literal.h:187
bvt lcnf_bv
Definition: prop.h:113
virtual bool has_set_to() const
Definition: prop.h:76
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bool is_in_conflict(literalt l) const
Definition: prop.cpp:31
virtual void copy_assignment_from(const propt &prop)
Definition: prop.cpp:25
virtual literalt lnor(literalt a, literalt b)=0
propt()
Definition: prop.h:25
std::vector< literalt > bvt
Definition: literal.h:197