cprover
prop_conv.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_CONV_H
11 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
12 
13 #include <string>
14 #include <map>
15 
17 #include <util/expr.h>
18 #include <util/std_expr.h>
19 
20 #include "literal.h"
21 #include "literal_expr.h"
22 #include "prop.h"
23 
24 // API that provides a "handle" in the form of a literalt
25 // for expressions.
26 
28 {
29 public:
30  explicit prop_convt(
31  const namespacet &_ns):
32  decision_proceduret(_ns) { }
33  virtual ~prop_convt() { }
34 
35  // conversion to handle
36  virtual literalt convert(const exprt &expr)=0;
37 
38  literalt operator()(const exprt &expr)
39  {
40  return convert(expr);
41  }
42 
43  using decision_proceduret::operator();
44 
45  // specialised variant of get
46  virtual tvt l_get(literalt a) const=0;
47 
48  // incremental solving
49  virtual void set_frozen(literalt a);
50  virtual void set_frozen(const bvt &);
51  virtual void set_assumptions(const bvt &_assumptions);
52  virtual bool has_set_assumptions() const { return false; }
53  virtual void set_all_frozen() {}
54 
55  // returns true if an assumption is in the final conflict
56  virtual bool is_in_conflict(literalt l) const;
57  virtual bool has_is_in_conflict() const { return false; }
58 
59  // Resource limits:
60  virtual void set_time_limit_seconds(uint32_t) {}
61 };
62 
63 //
64 // an instance of the above that converts the
65 // propositional skeleton by passing it to a propt
66 //
67 
71 {
72 public:
73  prop_conv_solvert(const namespacet &_ns, propt &_prop):
74  prop_convt(_ns),
75  prop(_prop) { }
76 
77  virtual ~prop_conv_solvert() = default;
78 
79  // overloading from decision_proceduret
80  void set_to(const exprt &expr, bool value) override;
82  void print_assignment(std::ostream &out) const override;
83  std::string decision_procedure_text() const override
84  { return "propositional reduction"; }
85  exprt get(const exprt &expr) const override;
86 
87  // overloading from prop_convt
89  virtual tvt l_get(literalt a) const override { return prop.l_get(a); }
90  void set_frozen(literalt a) override
91  {
92  prop.set_frozen(a);
93  }
94  void set_assumptions(const bvt &_assumptions) override
95  { prop.set_assumptions(_assumptions); }
96  bool has_set_assumptions() const override
97  { return prop.has_set_assumptions(); }
98  void set_all_frozen() override
99  {
100  freeze_all = true;
101  }
102  literalt convert(const exprt &expr) override;
103  bool is_in_conflict(literalt l) const override
104  { return prop.is_in_conflict(l); }
105  bool has_is_in_conflict() const override
106  { return prop.has_is_in_conflict(); }
107 
108  // get literal for expression, if available
109  bool literal(const symbol_exprt &expr, literalt &literal) const;
110 
111  bool use_cache = true;
112  bool equality_propagation = true;
113  bool freeze_all = false; // freezing variables (for incremental solving)
114 
115  virtual void clear_cache() { cache.clear();}
116 
117  typedef std::map<irep_idt, literalt> symbolst;
118  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
119 
120  const cachet &get_cache() const { return cache; }
121  const symbolst &get_symbols() const { return symbols; }
122 
123  void set_time_limit_seconds(uint32_t lim) override
124  {
126  }
127 
128 protected:
129  virtual void post_process();
130 
131  bool post_processing_done = false;
132 
133  // get a _boolean_ value from counterexample if not valid
134  virtual bool get_bool(const exprt &expr, tvt &value) const;
135 
136  virtual literalt convert_rest(const exprt &expr);
137  virtual literalt convert_bool(const exprt &expr);
138 
139  virtual bool set_equality_to_true(const equal_exprt &expr);
140 
141  // symbols
143 
144  virtual literalt get_literal(const irep_idt &symbol);
145 
146  // cache
148 
149  virtual void ignoring(const exprt &expr);
150 
151  // deliberately protected now to protect lower-level API
153 };
154 
155 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv.h:112
prop_convt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:19
propt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: prop.h:108
prop_convt::set_all_frozen
virtual void set_all_frozen()
Definition: prop_conv.h:53
propt::set_assumptions
virtual void set_assumptions(const bvt &)
Definition: prop.h:85
prop_convt::is_in_conflict
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
Definition: prop_conv.cpp:13
prop_conv_solvert::set_assumptions
void set_assumptions(const bvt &_assumptions) override
Definition: prop_conv.h:94
prop_convt
Definition: prop_conv.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
decision_proceduret
Definition: decision_procedure.h:20
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv.h:142
propt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:114
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv.h:113
exprt
Base class for all expressions.
Definition: expr.h:54
prop_conv_solvert::l_get
virtual tvt l_get(literalt a) const override
Definition: prop_conv.h:89
prop_convt::has_is_in_conflict
virtual bool has_is_in_conflict() const
Definition: prop_conv.h:57
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:190
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
propt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop.h:86
equal_exprt
Equality.
Definition: std_expr.h:1484
decision_procedure.h
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:454
expr.h
prop_conv_solvert::cache
cachet cache
Definition: prop_conv.h:147
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
prop_conv_solvert::literal
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:36
prop_conv_solvert::post_processing_done
bool post_processing_done
Definition: prop_conv.h:131
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv.h:115
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
prop_conv_solvert::get_bool
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
Definition: prop_conv.cpp:69
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv.cpp:461
prop_conv_solvert::get_cache
const cachet & get_cache() const
Definition: prop_conv.h:120
prop.h
prop_conv_solvert::get
exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:485
prop_conv_solvert::has_set_assumptions
bool has_set_assumptions() const override
Definition: prop_conv.h:96
prop_conv_solvert::is_in_conflict
bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
Definition: prop_conv.h:103
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:111
prop_conv_solvert::cachet
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv.h:118
prop_conv_solvert::has_is_in_conflict
bool has_is_in_conflict() const override
Definition: prop_conv.h:105
prop_conv_solvert::get_literal
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv.cpp:51
prop_conv_solvert::prop_conv_solvert
prop_conv_solvert(const namespacet &_ns, propt &_prop)
Definition: prop_conv.h:73
propt::is_in_conflict
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
prop_convt::~prop_convt
virtual ~prop_convt()
Definition: prop_conv.h:33
tvt
Definition: threeval.h:19
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
literal.h
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv.h:111
prop_convt::set_frozen
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:24
prop_conv_solvert::symbolst
std::map< irep_idt, literalt > symbolst
Definition: prop_conv.h:117
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
prop_conv_solvert::~prop_conv_solvert
virtual ~prop_conv_solvert()=default
propt::l_get
virtual tvt l_get(literalt a) const =0
prop_convt::has_set_assumptions
virtual bool has_set_assumptions() const
Definition: prop_conv.h:52
prop_conv_solvert::decision_procedure_text
std::string decision_procedure_text() const override
Definition: prop_conv.h:83
prop_conv_solvert::set_frozen
void set_frozen(literalt a) override
Definition: prop_conv.h:90
prop_conv_solvert::dec_solve
decision_proceduret::resultt dec_solve() override
Definition: prop_conv.cpp:465
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition: prop_conv.h:121
literalt
Definition: literal.h:24
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:509
prop_convt::prop_convt
prop_convt(const namespacet &_ns)
Definition: prop_conv.h:30
prop_conv_solvert::set_all_frozen
void set_all_frozen() override
Definition: prop_conv.h:98
prop_conv_solvert::set_time_limit_seconds
void set_time_limit_seconds(uint32_t lim) override
Definition: prop_conv.h:123
prop_convt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop_conv.h:60
prop_conv_solvert
TO_BE_DOCUMENTED.
Definition: prop_conv.h:70
std_expr.h
prop_convt::operator()
literalt operator()(const exprt &expr)
Definition: prop_conv.h:38
literal_expr.h
prop_conv_solvert::set_to
void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:364
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
prop_conv_solvert::set_equality_to_true
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv.cpp:337