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 #include <util/std_expr.h>
18 
20 
21 #include "literal.h"
22 #include "literal_expr.h"
23 #include "prop.h"
24 #include "prop_conv.h"
25 #include "solver_resource_limits.h"
26 
28  public prop_convt,
30 {
31 public:
32  prop_conv_solvert(propt &_prop, message_handlert &message_handler)
33  : prop(_prop), log(message_handler)
34  {
35  }
36 
37  virtual ~prop_conv_solvert() = default;
38 
39  // overloading from decision_proceduret
41  void print_assignment(std::ostream &out) const override;
42  std::string decision_procedure_text() const override;
43  exprt get(const exprt &expr) const override;
44 
45  tvt l_get(literalt a) const override
46  {
47  return prop.l_get(a);
48  }
49 
50  exprt handle(const exprt &expr) override;
51 
52  void set_frozen(literalt);
53  void set_frozen(const bvt &);
54  void set_all_frozen();
55 
56  literalt convert(const exprt &expr) override;
57  bool is_in_conflict(const exprt &expr) const override;
58 
62  void set_to(const exprt &expr, bool value) override;
63 
64  void push() override;
65 
67  void push(const std::vector<exprt> &assumptions) override;
68 
69  void pop() override;
70 
71  // get literal for expression, if available
72  bool literal(const symbol_exprt &expr, literalt &literal) const;
73 
74  bool use_cache = true;
75  bool equality_propagation = true;
76  bool freeze_all = false; // freezing variables (for incremental solving)
77 
78  virtual void clear_cache()
79  {
80  cache.clear();
81  }
82 
83  typedef std::map<irep_idt, literalt> symbolst;
84  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
85 
86  const cachet &get_cache() const
87  {
88  return cache;
89  }
90  const symbolst &get_symbols() const
91  {
92  return symbols;
93  }
94 
95  void set_time_limit_seconds(uint32_t lim) override
96  {
98  }
99 
100  std::size_t get_number_of_solver_calls() const override;
101 
102 protected:
103  virtual void post_process();
104 
105  bool post_processing_done = false;
106 
110  virtual optionalt<bool> get_bool(const exprt &expr) const;
111 
112  virtual literalt convert_rest(const exprt &expr);
113  virtual literalt convert_bool(const exprt &expr);
114 
115  virtual bool set_equality_to_true(const equal_exprt &expr);
116 
117  // symbols
119 
120  virtual literalt get_literal(const irep_idt &symbol);
121 
122  // cache
124 
125  virtual void ignoring(const exprt &expr);
126 
128 
130 
131  static const char *context_prefix;
132 
135 
137  std::size_t context_literal_counter = 0;
138 
141  std::vector<size_t> context_size_stack;
142 
143 private:
146  void add_constraints_to_prop(const exprt &expr, bool value);
147 };
148 
149 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_SOLVER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
prop_conv_solvert::l_get
tvt l_get(literalt a) const override
Return value of literal l from satisfying assignment.
Definition: prop_conv_solver.h:45
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv_solver.h:75
prop_conv_solvert::assumption_stack
bvt assumption_stack
Assumptions on the stack.
Definition: prop_conv_solver.h:134
prop_conv_solvert::context_size_stack
std::vector< size_t > context_size_stack
assumption_stack is segmented in contexts; Number of assumptions in each context on the stack
Definition: prop_conv_solver.h:141
prop_conv_solvert::prop_conv_solvert
prop_conv_solvert(propt &_prop, message_handlert &message_handler)
Definition: prop_conv_solver.h:32
prop_convt
Definition: prop_conv.h:22
bvt
std::vector< literalt > bvt
Definition: literal.h:201
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv_solver.h:118
propt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:117
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv_solver.h:76
prop_conv_solvert::context_literal_counter
std::size_t context_literal_counter
To generate unique literal names for contexts.
Definition: prop_conv_solver.h:137
exprt
Base class for all expressions.
Definition: expr.h:53
conflict_providert
Definition: conflict_provider.h:20
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv_solver.cpp:199
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1196
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv_solver.cpp:467
expr.h
prop_conv_solvert::handle
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...
Definition: prop_conv_solver.cpp:37
prop_conv_solvert::cache
cachet cache
Definition: prop_conv_solver.h:123
prop_conv_solvert::literal
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv_solver.cpp:59
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:27
prop_conv_solvert::post_processing_done
bool post_processing_done
Definition: prop_conv_solver.h:105
prop_conv.h
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv_solver.h:78
prop_conv_solvert::context_prefix
static const char * context_prefix
Definition: prop_conv_solver.h:131
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv_solver.cpp:474
prop_conv_solvert::get_cache
const cachet & get_cache() const
Definition: prop_conv_solver.h:86
prop.h
prop_conv_solvert::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: prop_conv_solver.cpp:503
prop_conv_solvert::set_all_frozen
void set_all_frozen()
Definition: prop_conv_solver.cpp:32
message_handlert
Definition: message.h:27
prop_conv_solvert::cachet
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv_solver.h:84
prop_conv_solvert::get_literal
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv_solver.cpp:74
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
tvt
Definition: threeval.h:20
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
solver_resource_limits.h
literal.h
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:349
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv_solver.h:74
prop_conv_solvert::add_constraints_to_prop
void add_constraints_to_prop(const exprt &expr, bool value)
Helper method used by set_to for adding the constraints to prop.
Definition: prop_conv_solver.cpp:382
prop_conv_solvert::is_in_conflict
bool is_in_conflict(const exprt &expr) const override
Returns true if an expression is in the final conflict leading to UNSAT.
Definition: prop_conv_solver.cpp:15
prop_conv_solvert::symbolst
std::map< irep_idt, literalt > symbolst
Definition: prop_conv_solver.h:83
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
prop_conv_solvert::~prop_conv_solvert
virtual ~prop_conv_solvert()=default
propt::l_get
virtual tvt l_get(literalt a) const =0
prop_conv_solvert::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: prop_conv_solver.cpp:592
solver_resource_limitst
Definition: solver_resource_limits.h:16
prop_conv_solvert::dec_solve
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: prop_conv_solver.cpp:478
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition: prop_conv_solver.h:90
literalt
Definition: literal.h:26
conflict_provider.h
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: prop_conv_solver.cpp:527
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:129
prop_conv_solvert::set_time_limit_seconds
void set_time_limit_seconds(uint32_t lim) override
Set the limit for the solver to time out in seconds.
Definition: prop_conv_solver.h:95
message.h
prop_conv_solvert::push
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
Definition: prop_conv_solver.cpp:566
prop_conv_solvert
Definition: prop_conv_solver.h:30
prop_conv_solvert::pop
void pop() override
Pop whatever is on top of the stack.
Definition: prop_conv_solver.cpp:578
std_expr.h
prop_conv_solvert::get_bool
virtual optionalt< bool > get_bool(const exprt &expr) const
Get a boolean value from the model if the formula is satisfiable.
Definition: prop_conv_solver.cpp:91
literal_expr.h
prop_conv_solvert::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
Definition: prop_conv_solver.cpp:540
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:127
prop_conv_solvert::set_equality_to_true
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv_solver.cpp:356
prop_conv_solvert::get_number_of_solver_calls
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: prop_conv_solver.cpp:533