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 
21 
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  public hardness_collectort
31 {
32 public:
33  prop_conv_solvert(propt &_prop, message_handlert &message_handler)
34  : prop(_prop), log(message_handler)
35  {
36  }
37 
38  virtual ~prop_conv_solvert() = default;
39 
40  // overloading from decision_proceduret
42  void print_assignment(std::ostream &out) const override;
43  std::string decision_procedure_text() const override;
44  exprt get(const exprt &expr) const override;
45 
46  tvt l_get(literalt a) const override
47  {
48  return prop.l_get(a);
49  }
50 
51  exprt handle(const exprt &expr) override;
52 
53  void set_frozen(literalt);
54  void set_frozen(const bvt &);
55  void set_all_frozen();
56 
57  literalt convert(const exprt &expr) override;
58  bool is_in_conflict(const exprt &expr) const override;
59 
63  void set_to(const exprt &expr, bool value) override;
64 
65  void push() override;
66 
68  void push(const std::vector<exprt> &assumptions) override;
69 
70  void pop() override;
71 
72  // get literal for expression, if available
73  bool literal(const symbol_exprt &expr, literalt &literal) const;
74 
75  bool use_cache = true;
76  bool equality_propagation = true;
77  bool freeze_all = false; // freezing variables (for incremental solving)
78 
79  virtual void clear_cache()
80  {
81  cache.clear();
82  }
83 
84  typedef std::map<irep_idt, literalt> symbolst;
85  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
86 
87  const cachet &get_cache() const
88  {
89  return cache;
90  }
91  const symbolst &get_symbols() const
92  {
93  return symbols;
94  }
95 
96  void set_time_limit_seconds(uint32_t lim) override
97  {
99  }
100 
101  std::size_t get_number_of_solver_calls() const override;
102 
103  void with_solver_hardness(handlert handler) override;
104  void enable_hardness_collection() override;
105 
106 protected:
107  virtual void post_process();
108 
109  bool post_processing_done = false;
110 
114  virtual optionalt<bool> get_bool(const exprt &expr) const;
115 
116  virtual literalt convert_rest(const exprt &expr);
117  virtual literalt convert_bool(const exprt &expr);
118 
119  virtual bool set_equality_to_true(const equal_exprt &expr);
120 
121  // symbols
123 
124  virtual literalt get_literal(const irep_idt &symbol);
125 
126  // cache
128 
129  virtual void ignoring(const exprt &expr);
130 
132 
134 
135  static const char *context_prefix;
136 
139 
141  std::size_t context_literal_counter = 0;
142 
145  std::vector<size_t> context_size_stack;
146 
147 private:
150  void add_constraints_to_prop(const exprt &expr, bool value);
151 };
152 
153 #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:46
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv_solver.h:76
prop_conv_solvert::assumption_stack
bvt assumption_stack
Assumptions on the stack.
Definition: prop_conv_solver.h:138
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:145
prop_conv_solvert::prop_conv_solvert
prop_conv_solvert(propt &_prop, message_handlert &message_handler)
Definition: prop_conv_solver.h:33
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:122
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:77
prop_conv_solvert::context_literal_counter
std::size_t context_literal_counter
To generate unique literal names for contexts.
Definition: prop_conv_solver.h:141
exprt
Base class for all expressions.
Definition: expr.h:53
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:597
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:1190
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:127
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:109
prop_conv.h
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv_solver.h:79
prop_conv_solvert::context_prefix
static const char * context_prefix
Definition: prop_conv_solver.h:135
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:87
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:28
prop_conv_solvert::cachet
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv_solver.h:85
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
Solver capability to set resource limits.
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:75
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:84
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:91
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:527
hardness_collectort
Definition: hardness_collector.h:23
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:133
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:96
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:31
prop_conv_solvert::pop
void pop() override
Pop whatever is on top of the stack.
Definition: prop_conv_solver.cpp:578
std_expr.h
API to expression classes.
prop_conv_solvert::enable_hardness_collection
void enable_hardness_collection() override
Definition: prop_conv_solver.cpp:602
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:131
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