 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
20.0% |
1 / 5 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
40.0% |
2 / 5 |
| |
|
Line Coverage: |
100.0% |
2 / 2 |
| |
 |
|
 |
1 : //===- IncompleteSolver.h - Adapter for incomplete solvers ------*- C++ -*-===//
2 :
3 : #ifndef KLEE_INCOMPLETESOLVER_H
4 : #define KLEE_INCOMPLETESOLVER_H
5 :
6 : #include "klee/Solver.h"
7 : #include "klee/SolverImpl.h"
8 :
9 : namespace klee {
10 :
11 : /// IncompleteSolver - Base class for incomplete solver
12 : /// implementations.
13 : ///
14 : /// Incomplete solvers are useful for implementing optimizations which
15 : /// may quickly compute an answer, but cannot always compute the
16 : /// correct answer. They can be used with the StagedSolver to provide
17 : /// a complete Solver implementation.
18 : class IncompleteSolver {
19 : public:
20 : /// PartialValidity - Represent a possibility incomplete query
21 : /// validity.
22 : enum PartialValidity {
23 : /// The query is provably true.
24 : MustBeTrue = 1,
25 :
26 : /// The query is provably false.
27 : MustBeFalse = -1,
28 :
29 : /// The query is not provably false (a true assignment is known to
30 : /// exist).
31 : MayBeTrue = 2,
32 :
33 : /// The query is not provably true (a false assignment is known to
34 : /// exist).
35 : MayBeFalse = -2,
36 :
37 : /// The query is known to have both true and false assignments.
38 : TrueOrFalse = 0,
39 :
40 : /// The validity of the query is unknown.
41 : None = 3
42 : };
43 :
44 : static PartialValidity negatePartialValidity(PartialValidity pv);
45 :
46 : public:
47 1: IncompleteSolver() {};
0: branch 0 not taken
1: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 7 not taken
48 1: virtual ~IncompleteSolver() {};
49 :
50 : /// computeValidity - Compute a partial validity for the given query.
51 : ///
52 : /// The passed expression is non-constant with bool type.
53 : ///
54 : /// The IncompleteSolver class provides an implementation of
55 : /// computeValidity using computeTruth. Sub-classes may override
56 : /// this if a more efficient implementation is available.
57 : virtual IncompleteSolver::PartialValidity computeValidity(const Query&);
58 :
59 : /// computeValidity - Compute a partial validity for the given query.
60 : ///
61 : /// The passed expression is non-constant with bool type.
62 : virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0;
63 :
64 : /// computeValue - Attempt to compute a value for the given expression.
65 : virtual bool computeValue(const Query&, ref<Expr> &result) = 0;
66 :
67 : /// computeInitialValues - Attempt to compute the constant values
68 : /// for the initial state of each given object. If a correct result
69 : /// is not found, then the values array must be unmodified.
70 : virtual bool computeInitialValues(const Query&,
71 : const std::vector<const MemoryObject*>
72 : &objects,
73 : std::vector< std::vector<unsigned char> >
74 : &values,
75 : bool &hasSolution) = 0;
76 : };
77 :
78 : /// StagedSolver - Adapter class for staging an incomplete solver with
79 : /// a complete secondary solver, to form an (optimized) complete
80 : /// solver.
81 : class StagedSolverImpl : public SolverImpl {
82 : private:
83 : IncompleteSolver *primary;
84 : Solver *secondary;
85 :
86 : public:
87 : StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
88 : ~StagedSolverImpl();
89 :
90 : bool computeTruth(const Query&, bool &isValid);
91 : bool computeValidity(const Query&, Solver::Validity &result);
92 : bool computeValue(const Query&, ref<Expr> &result);
93 : bool computeInitialValues(const Query&,
94 : const std::vector<const MemoryObject*> &objects,
95 : std::vector< std::vector<unsigned char> > &values,
96 : bool &hasSolution);
97 : };
98 :
99 : }
100 :
101 : #endif
Generated: 2009-05-17 22:47 by zcov