cprover
decision_procedure.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Decision Procedure Interface
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_DECISION_PROCEDURE_H
13 #define CPROVER_UTIL_DECISION_PROCEDURE_H
14 
15 #include "message.h"
16 
17 class exprt;
18 class namespacet;
19 
21 {
22 public:
23  explicit decision_proceduret(const namespacet &_ns):ns(_ns)
24  {
25  }
26 
27  // get a value from satisfying instance if satisfiable
28  // returns nil if not available
29  virtual exprt get(const exprt &expr) const=0;
30 
31  // print satisfying assignment
32  virtual void print_assignment(std::ostream &out) const=0;
33 
34  // add constraints
35  // the expression must be of Boolean type
36  virtual void set_to(const exprt &expr, bool value)=0;
37 
38  void set_to_true(const exprt &expr)
39  { set_to(expr, true); }
40 
41  void set_to_false(const exprt &expr)
42  { set_to(expr, false); }
43 
44  // solve the problem
46 
47  // will eventually be protected, use below call operator
48  virtual resultt dec_solve()=0;
49 
51  {
52  return dec_solve();
53  }
54 
55  // old-style, will go away
56  virtual bool in_core(const exprt &expr);
57 
58  // return a textual description of the decision procedure
59  virtual std::string decision_procedure_text() const=0;
60 
61 protected:
62  const namespacet &ns;
63 };
64 
66  decision_proceduret &dest,
67  const exprt &src)
68 {
69  dest.set_to_true(src);
70  return dest;
71 }
72 
73 #endif // CPROVER_UTIL_DECISION_PROCEDURE_H
virtual void print_assignment(std::ostream &out) const =0
virtual bool in_core(const exprt &expr)
virtual resultt dec_solve()=0
decision_proceduret & operator<<(decision_proceduret &dest, const exprt &src)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const namespacet & ns
virtual void set_to(const exprt &expr, bool value)=0
void set_to_false(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
void set_to_true(const exprt &expr)
decision_proceduret(const namespacet &_ns)
virtual std::string decision_procedure_text() const =0