 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
0.0% |
0 / 0 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
0.0% |
0 / 0 |
| |
|
Line Coverage: |
100.0% |
1 / 1 |
| |
 |
|
 |
1 : //===- SolverImpl.h - Constraint solver implementation ---------*- C++ -*-===//
2 :
3 : #ifndef KLEE_SOLVERIMPL_H
4 : #define KLEE_SOLVERIMPL_H
5 :
6 : #include <vector>
7 :
8 : namespace klee {
9 : class ExecutionState;
10 : class Expr;
11 : class MemoryObject;
12 : struct Query;
13 :
14 : /// SolverImpl - Abstract base clase for solver implementations.
15 : class SolverImpl {
16 : // DO NOT IMPLEMENT.
17 : SolverImpl(const SolverImpl&);
18 : void operator=(const SolverImpl&);
19 :
20 : public:
21 317: SolverImpl() {}
22 : virtual ~SolverImpl();
23 :
24 : /// computeValidity - Compute a full validity result for the
25 : /// query.
26 : ///
27 : /// The query expression is guaranteed to be non-constant and have
28 : /// bool type.
29 : ///
30 : /// SolverImpl provides a default implementation which uses
31 : /// computeTruth. Clients should override this if a more efficient
32 : /// implementation is available.
33 : virtual bool computeValidity(const Query& query, Solver::Validity &result);
34 :
35 : /// computeTruth - Determine whether the given query is provable.
36 : ///
37 : /// The query expression is guaranteed to be non-constant and have
38 : /// bool type.
39 : virtual bool computeTruth(const Query& query, bool &isValid) = 0;
40 :
41 : /// computeValue - Compute a feasible value for the expression.
42 : ///
43 : /// The query expression is guaranteed to be non-constant.
44 : virtual bool computeValue(const Query& query, ref<Expr> &result) = 0;
45 :
46 : virtual bool computeInitialValues(const Query& query,
47 : const std::vector<const MemoryObject*>
48 : &objects,
49 : std::vector< std::vector<unsigned char> >
50 : &values,
51 : bool &hasSolution) = 0;
52 : };
53 :
54 : }
55 :
56 : #endif
Generated: 2009-05-17 22:47 by zcov