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 
60 //
61 // an instance of the above that converts the
62 // propositional skeleton by passing it to a propt
63 //
64 
68 {
69 public:
70  prop_conv_solvert(const namespacet &_ns, propt &_prop):
71  prop_convt(_ns),
72  use_cache(true),
74  freeze_all(false),
75  post_processing_done(false),
76  prop(_prop) { }
77 
78  virtual ~prop_conv_solvert() { }
79 
80  // overloading from decision_proceduret
81  virtual void set_to(const exprt &expr, bool value) override;
82  virtual decision_proceduret::resultt dec_solve() override;
83  virtual void print_assignment(std::ostream &out) const override;
84  virtual std::string decision_procedure_text() const override
85  { return "propositional reduction"; }
86  virtual exprt get(const exprt &expr) const override;
87 
88  // overloading from prop_convt
90  virtual tvt l_get(literalt a) const override { return prop.l_get(a); }
91  virtual void set_frozen(literalt a) override { prop.set_frozen(a); }
92  virtual void set_assumptions(const bvt &_assumptions) override
93  { prop.set_assumptions(_assumptions); }
94  virtual bool has_set_assumptions() const override
95  { return prop.has_set_assumptions(); }
96  virtual void set_all_frozen() override { freeze_all = true; }
97  virtual literalt convert(const exprt &expr) override;
98  virtual bool is_in_conflict(literalt l) const override
99  { return prop.is_in_conflict(l); }
100  virtual bool has_is_in_conflict() const override
101  { return prop.has_is_in_conflict(); }
102 
103  // get literal for expression, if available
104  virtual bool literal(const exprt &expr, literalt &literal) const;
105 
106  bool use_cache;
108  bool freeze_all; // freezing variables (for incremental solving)
109 
110  virtual void clear_cache() { cache.clear();}
111 
112  typedef std::map<irep_idt, literalt> symbolst;
113  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
114 
115  const cachet &get_cache() const { return cache; }
116  const symbolst &get_symbols() const { return symbols; }
117 
118 protected:
119  virtual void post_process();
120 
122 
123  // get a _boolean_ value from counterexample if not valid
124  virtual bool get_bool(const exprt &expr, tvt &value) const;
125 
126  virtual literalt convert_rest(const exprt &expr);
127  virtual literalt convert_bool(const exprt &expr);
128 
129  virtual bool set_equality_to_true(const equal_exprt &expr);
130 
131  // symbols
133 
134  virtual literalt get_literal(const irep_idt &symbol);
135 
136  // cache
138 
139  virtual void ignoring(const exprt &expr);
140 
141  // deliberately protected now to protect lower-level API
143 };
144 
145 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
virtual void set_all_frozen()
Definition: prop_conv.h:53
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv.cpp:344
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
virtual void set_frozen(literalt a)
Definition: prop.h:109
bool equality_propagation
Definition: prop_conv.h:107
virtual bool has_is_in_conflict() const
Definition: prop.h:106
literalt operator()(const exprt &expr)
Definition: prop_conv.h:38
virtual bool has_is_in_conflict() const
Definition: prop_conv.h:57
virtual ~prop_conv_solvert()
Definition: prop_conv.h:78
Decision Procedure Interface.
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
Definition: prop_conv.cpp:23
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:209
virtual void set_frozen(literalt a) override
Definition: prop_conv.h:91
virtual decision_proceduret::resultt dec_solve() override
Definition: prop_conv.cpp:481
const symbolst & get_symbols() const
Definition: prop_conv.h:116
std::map< irep_idt, literalt > symbolst
Definition: prop_conv.h:112
virtual void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:371
virtual void post_process()
Definition: prop_conv.cpp:477
virtual bool literal(const exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:46
virtual void set_assumptions(const bvt &_assumptions) override
Definition: prop_conv.h:92
symbolst symbols
Definition: prop_conv.h:132
equality
Definition: std_expr.h:1082
virtual bool has_set_assumptions() const
Definition: prop.h:84
virtual void clear_cache()
Definition: prop_conv.h:110
virtual void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:531
const cachet & get_cache() const
Definition: prop_conv.h:115
API to expression classes.
virtual ~prop_convt()
Definition: prop_conv.h:33
Definition: threeval.h:19
virtual bool has_set_assumptions() const override
Definition: prop_conv.h:94
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual bool has_is_in_conflict() const override
Definition: prop_conv.h:100
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv.h:113
virtual literalt convert(const exprt &expr)=0
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop.h:83
virtual std::string decision_procedure_text() const override
Definition: prop_conv.h:84
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual bool has_set_assumptions() const
Definition: prop_conv.h:52
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv.cpp:66
virtual tvt l_get(literalt a) const =0
TO_BE_DOCUMENTED.
Definition: prop_conv.h:67
virtual tvt l_get(literalt a) const override
Definition: prop_conv.h:90
virtual bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
Definition: prop_conv.h:98
Base class for all expressions.
Definition: expr.h:46
virtual tvt l_get(literalt a) const =0
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
Definition: prop_conv.cpp:87
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:337
bool post_processing_done
Definition: prop_conv.h:121
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:34
prop_conv_solvert(const namespacet &_ns, propt &_prop)
Definition: prop_conv.h:70
virtual bool is_in_conflict(literalt l) const
Definition: prop.cpp:31
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:470
std::vector< literalt > bvt
Definition: literal.h:197
prop_convt(const namespacet &_ns)
Definition: prop_conv.h:30
virtual void set_all_frozen() override
Definition: prop_conv.h:96
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:29