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  virtual ~decision_proceduret();
28 
29  // get a value from satisfying instance if satisfiable
30  // returns nil if not available
31  virtual exprt get(const exprt &expr) const=0;
32 
33  // print satisfying assignment
34  virtual void print_assignment(std::ostream &out) const=0;
35 
36  // add constraints
37  // the expression must be of Boolean type
38  virtual void set_to(const exprt &expr, bool value)=0;
39 
40  void set_to_true(const exprt &expr)
41  { set_to(expr, true); }
42 
43  void set_to_false(const exprt &expr)
44  { set_to(expr, false); }
45 
46  // solve the problem
48 
49  // will eventually be protected, use below call operator
50  virtual resultt dec_solve()=0;
51 
53  {
54  return dec_solve();
55  }
56 
57  // return a textual description of the decision procedure
58  virtual std::string decision_procedure_text() const=0;
59 
60 protected:
61  const namespacet &ns;
62 };
63 
65  decision_proceduret &dest,
66  const exprt &src)
67 {
68  dest.set_to_true(src);
69  return dest;
70 }
71 
72 #endif // CPROVER_UTIL_DECISION_PROCEDURE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
decision_proceduret::get
virtual exprt get(const exprt &expr) const =0
decision_proceduret
Definition: decision_procedure.h:20
decision_proceduret::resultt::D_UNSATISFIABLE
exprt
Base class for all expressions.
Definition: expr.h:54
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
Definition: decision_procedure.h:40
decision_proceduret::decision_proceduret
decision_proceduret(const namespacet &_ns)
Definition: decision_procedure.h:23
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
Definition: decision_procedure.h:43
decision_proceduret::resultt::D_SATISFIABLE
decision_proceduret::set_to
virtual void set_to(const exprt &expr, bool value)=0
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
operator<<
decision_proceduret & operator<<(decision_proceduret &dest, const exprt &src)
Definition: decision_procedure.h:64
decision_proceduret::dec_solve
virtual resultt dec_solve()=0
decision_proceduret::print_assignment
virtual void print_assignment(std::ostream &out) const =0
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
decision_proceduret::resultt::D_ERROR
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
decision_proceduret::~decision_proceduret
virtual ~decision_proceduret()
Definition: decision_procedure.cpp:14
decision_proceduret::operator()
resultt operator()()
Definition: decision_procedure.h:52
message.h