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  // return a textual description of the decision procedure
56  virtual std::string decision_procedure_text() const=0;
57 
58 protected:
59  const namespacet &ns;
60 };
61 
63  decision_proceduret &dest,
64  const exprt &src)
65 {
66  dest.set_to_true(src);
67  return dest;
68 }
69 
70 #endif // CPROVER_UTIL_DECISION_PROCEDURE_H
virtual void print_assignment(std::ostream &out) const =0
virtual resultt dec_solve()=0
decision_proceduret & operator<<(decision_proceduret &dest, const exprt &src)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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:42
void set_to_true(const exprt &expr)
decision_proceduret(const namespacet &_ns)
virtual std::string decision_procedure_text() const =0