cprover
prop_conv_solver.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
10 #define CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
11 
12 #include <map>
13 #include <string>
14 
15 #include <util/expr.h>
16 #include <util/message.h>
17 
20 
21 #include "prop.h"
22 #include "prop_conv.h"
23 #include "solver_resource_limits.h"
24 
26  public prop_convt,
28  public hardness_collectort
29 {
30 public:
31  prop_conv_solvert(propt &_prop, message_handlert &message_handler)
32  : prop(_prop), log(message_handler)
33  {
34  }
35 
36  virtual ~prop_conv_solvert() = default;
37 
38  // overloading from decision_proceduret
40  void print_assignment(std::ostream &out) const override;
41  std::string decision_procedure_text() const override;
42  exprt get(const exprt &expr) const override;
43 
44  tvt l_get(literalt a) const override
45  {
46  return prop.l_get(a);
47  }
48 
49  exprt handle(const exprt &expr) override;
50 
51  void set_frozen(literalt);
52  void set_frozen(const bvt &);
53  void set_all_frozen();
54 
55  literalt convert(const exprt &expr) override;
56  bool is_in_conflict(const exprt &expr) const override;
57 
61  void set_to(const exprt &expr, bool value) override;
62 
63  void push() override;
64 
66  void push(const std::vector<exprt> &assumptions) override;
67 
68  void pop() override;
69 
70  bool use_cache = true;
71  bool equality_propagation = true;
72  bool freeze_all = false; // freezing variables (for incremental solving)
73 
74  virtual void clear_cache()
75  {
76  cache.clear();
77  }
78 
79  typedef std::map<irep_idt, literalt> symbolst;
80  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
81 
82  const cachet &get_cache() const
83  {
84  return cache;
85  }
86  const symbolst &get_symbols() const
87  {
88  return symbols;
89  }
90 
91  void set_time_limit_seconds(uint32_t lim) override
92  {
94  }
95 
96  std::size_t get_number_of_solver_calls() const override;
97 
98  void with_solver_hardness(handlert handler) override;
99  void enable_hardness_collection() override;
100 
101 protected:
102  virtual void post_process();
103 
104  bool post_processing_done = false;
105 
109  virtual optionalt<bool> get_bool(const exprt &expr) const;
110 
111  virtual literalt convert_rest(const exprt &expr);
112  virtual literalt convert_bool(const exprt &expr);
113 
114  virtual bool set_equality_to_true(const equal_exprt &expr);
115 
116  // symbols
118 
119  virtual literalt get_literal(const irep_idt &symbol);
120 
121  // cache
123 
124  virtual void ignoring(const exprt &expr);
125 
127 
129 
130  static const char *context_prefix;
131 
134 
136  std::size_t context_literal_counter = 0;
137 
140  std::vector<size_t> context_size_stack;
141 
142 private:
145  void add_constraints_to_prop(const exprt &expr, bool value);
146 };
147 
148 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::function< void(solver_hardnesst &)> handlert
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
void pop() override
Pop whatever is on top of the stack.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
virtual bool set_equality_to_true(const equal_exprt &expr)
virtual literalt convert_bool(const exprt &expr)
virtual void post_process()
void set_frozen(literalt)
std::vector< size_t > context_size_stack
assumption_stack is segmented in contexts; Number of assumptions in each context on the stack
std::size_t context_literal_counter
To generate unique literal names for contexts.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
virtual optionalt< bool > get_bool(const exprt &expr) const
Get a boolean value from the model if the formula is satisfiable.
virtual void clear_cache()
prop_conv_solvert(propt &_prop, message_handlert &message_handler)
std::map< irep_idt, literalt > symbolst
virtual literalt get_literal(const irep_idt &symbol)
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
virtual void ignoring(const exprt &expr)
const symbolst & get_symbols() const
virtual ~prop_conv_solvert()=default
const cachet & get_cache() const
void set_time_limit_seconds(uint32_t lim) override
Set the limit for the solver to time out in seconds.
void with_solver_hardness(handlert handler) override
tvt l_get(literalt a) const override
Return value of literal l from satisfying assignment.
void add_constraints_to_prop(const exprt &expr, bool value)
Helper method used by set_to for adding the constraints to prop.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
bvt assumption_stack
Assumptions on the stack.
virtual literalt convert_rest(const exprt &expr)
std::unordered_map< exprt, literalt, irep_hash > cachet
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
static const char * context_prefix
bool is_in_conflict(const exprt &expr) const override
Returns true if an expression is in the final conflict leading to UNSAT.
void enable_hardness_collection() override
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
TO_BE_DOCUMENTED.
Definition: prop.h:23
virtual tvt l_get(literalt a) const =0
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:115
Definition: threeval.h:20
Capability to check whether an expression is a reason for the solver returning UNSAT.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition: literal.h:201
nonstd::optional< T > optionalt
Definition: optional.h:35
Solver capability to set resource limits.