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  bool use_cache = true;
73  bool equality_propagation = true;
74  bool freeze_all = false; // freezing variables (for incremental solving)
75 
76  virtual void clear_cache()
77  {
78  cache.clear();
79  }
80 
81  typedef std::map<irep_idt, literalt> symbolst;
82  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;
83 
84  const cachet &get_cache() const
85  {
86  return cache;
87  }
88  const symbolst &get_symbols() const
89  {
90  return symbols;
91  }
92 
93  void set_time_limit_seconds(uint32_t lim) override
94  {
96  }
97 
98  std::size_t get_number_of_solver_calls() const override;
99 
100  void with_solver_hardness(handlert handler) override;
101  void enable_hardness_collection() override;
102 
103 protected:
104  virtual void post_process();
105 
106  bool post_processing_done = false;
107 
111  virtual optionalt<bool> get_bool(const exprt &expr) const;
112 
113  virtual literalt convert_rest(const exprt &expr);
114  virtual literalt convert_bool(const exprt &expr);
115 
116  virtual bool set_equality_to_true(const equal_exprt &expr);
117 
118  // symbols
120 
121  virtual literalt get_literal(const irep_idt &symbol);
122 
123  // cache
125 
126  virtual void ignoring(const exprt &expr);
127 
129 
131 
132  static const char *context_prefix;
133 
136 
138  std::size_t context_literal_counter = 0;
139 
142  std::vector<size_t> context_size_stack;
143 
144 private:
147  void add_constraints_to_prop(const exprt &expr, bool value);
148 };
149 
150 #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:73
prop_conv_solvert::assumption_stack
bvt assumption_stack
Assumptions on the stack.
Definition: prop_conv_solver.h:135
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:142
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:119
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:74
prop_conv_solvert::context_literal_counter
std::size_t context_literal_counter
To generate unique literal names for contexts.
Definition: prop_conv_solver.h:138
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:591
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv_solver.cpp:185
equal_exprt
Equality.
Definition: std_expr.h:1139
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv_solver.cpp:453
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:38
prop_conv_solvert::cache
cachet cache
Definition: prop_conv_solver.h:124
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:28
prop_conv_solvert::post_processing_done
bool post_processing_done
Definition: prop_conv_solver.h:106
prop_conv.h
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv_solver.h:76
prop_conv_solvert::context_prefix
static const char * context_prefix
Definition: prop_conv_solver.h:132
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv_solver.cpp:460
prop_conv_solvert::get_cache
const cachet & get_cache() const
Definition: prop_conv_solver.h:84
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:497
prop_conv_solvert::set_all_frozen
void set_all_frozen()
Definition: prop_conv_solver.cpp:33
message_handlert
Definition: message.h:28
prop_conv_solvert::cachet
std::unordered_map< exprt, literalt, irep_hash > cachet
Definition: prop_conv_solver.h:82
prop_conv_solvert::get_literal
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv_solver.cpp:60
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:154
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:335
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv_solver.h:72
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:368
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:16
prop_conv_solvert::symbolst
std::map< irep_idt, literalt > symbolst
Definition: prop_conv_solver.h:81
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:586
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:464
prop_conv_solvert::get_symbols
const symbolst & get_symbols() const
Definition: prop_conv_solver.h:88
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:521
hardness_collectort
Definition: hardness_collector.h:23
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:130
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:93
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:560
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:572
std_expr.h
API to expression classes.
prop_conv_solvert::enable_hardness_collection
void enable_hardness_collection() override
Definition: prop_conv_solver.cpp:596
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:77
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:534
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
prop_conv_solvert::set_equality_to_true
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv_solver.cpp:342
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:527