CBMC
solver.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Solver
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPROVER_SOLVER_H
13 #define CPROVER_CPROVER_SOLVER_H
14 
15 #include <vector>
16 
17 class exprt;
18 class namespacet;
19 
20 enum class solver_resultt
21 {
22  ALL_PASS,
23  SOME_FAIL,
24  ERROR
25 };
26 
27 class solver_optionst
28 {
29 public:
30  bool trace;
31  bool verbose;
32  std::size_t loop_limit;
33 };
34 
35 solver_resultt
36 solver(const std::vector<exprt> &, const solver_optionst &, const namespacet &);
37 
38 #endif // CPROVER_CPROVER_SOLVER_H
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
solver_optionst
Definition: solver.h:28
solver_optionst::verbose
bool verbose
Definition: solver.h:31
solver_optionst::loop_limit
std::size_t loop_limit
Definition: solver.h:32
solver_optionst::trace
bool trace
Definition: solver.h:30
solver
solver_resultt solver(const std::vector< exprt > &, const solver_optionst &, const namespacet &)
Definition: solver.cpp:107
solver_resultt
solver_resultt
Definition: solver.h:21