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
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
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:44
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv_solver.h:71
prop_conv_solvert::assumption_stack
bvt assumption_stack
Assumptions on the stack.
Definition: prop_conv_solver.h:133
hardness_collector.h
Capability to collect the statistics of the complexity of individual solver queries.
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:140
prop_conv_solvert::prop_conv_solvert
prop_conv_solvert(propt &_prop, message_handlert &message_handler)
Definition: prop_conv_solver.h:31
prop_convt
Definition: prop_conv.h:22
bvt
std::vector< literalt > bvt
Definition: literal.h:201
hardness_collectort::handlert
std::function< void(solver_hardnesst &)> handlert
Definition: hardness_collector.h:25
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv_solver.h:117
propt::set_time_limit_seconds
virtual void set_time_limit_seconds(uint32_t)
Definition: prop.h:115
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv_solver.h:72
prop_conv_solvert::context_literal_counter
std::size_t context_literal_counter
To generate unique literal names for contexts.
Definition: prop_conv_solver.h:136
exprt
Base class for all expressions.
Definition: expr.h:54
conflict_providert
Definition: conflict_provider.h:20
prop_conv_solvert::with_solver_hardness
void with_solver_hardness(handlert handler) override
Definition: prop_conv_solver.cpp:563
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv_solver.cpp:192
equal_exprt
Equality.
Definition: std_expr.h:1225
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv_solver.cpp:425
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:40
prop_conv_solvert::cache
cachet cache
Definition: prop_conv_solver.h:122
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:30
prop_conv_solvert::post_processing_done
bool post_processing_done
Definition: prop_conv_solver.h:104
prop_conv.h
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv_solver.h:74
prop_conv_solvert::context_prefix
static const char * context_prefix
Definition: prop_conv_solver.h:130
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv_solver.cpp:432
prop_conv_solvert::get_cache
const cachet & get_cache() const
Definition: prop_conv_solver.h:82
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:469
prop_conv_solvert::set_all_frozen
void set_all_frozen()
Definition: prop_conv_solver.cpp:35
message_handlert
Definition: message.h:28
prop_conv_solvert::cachet
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv_solver.h:80
prop_conv_solvert::get_literal
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv_solver.cpp:62
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:156
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
solver_resource_limits.h
Solver capability to set resource limits.
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:307
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv_solver.h:70
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:340
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:18
prop_conv_solvert::symbolst
std::map< irep_idt, literalt > symbolst
Definition: prop_conv_solver.h:79
propt
TO_BE_DOCUMENTED.
Definition: prop.h:23
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:558
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:436
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition: prop_conv_solver.h:86
literalt
Definition: literal.h:26
conflict_provider.h
Capability to check whether an expression is a reason for the solver returning UNSAT.
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: prop_conv_solver.cpp:493
hardness_collectort
Definition: hardness_collector.h:23
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:128
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:91
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:532
prop_conv_solvert
Definition: prop_conv_solver.h:29
prop_conv_solvert::pop
void pop() override
Pop whatever is on top of the stack.
Definition: prop_conv_solver.cpp:544
prop_conv_solvert::enable_hardness_collection
void enable_hardness_collection() override
Definition: prop_conv_solver.cpp:568
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:79
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:506
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:126
prop_conv_solvert::set_equality_to_true
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv_solver.cpp:314
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:499