IncompleteSolver.h

Go to the documentation of this file.
00001 //===-- IncompleteSolver.h --------------------------------------*- C++ -*-===//
00002 //
00003 //                     The KLEE Symbolic Virtual Machine
00004 //
00005 // This file is distributed under the University of Illinois Open Source
00006 // License. See LICENSE.TXT for details.
00007 //
00008 //===----------------------------------------------------------------------===//
00009 
00010 #ifndef KLEE_INCOMPLETESOLVER_H
00011 #define KLEE_INCOMPLETESOLVER_H
00012 
00013 #include "klee/Solver.h"
00014 #include "klee/SolverImpl.h"
00015 
00016 namespace klee {
00017 
00025 class IncompleteSolver {
00026 public:
00029   enum PartialValidity {
00031     MustBeTrue = 1,
00032 
00034     MustBeFalse = -1,
00035 
00038     MayBeTrue = 2,
00039 
00042     MayBeFalse = -2,
00043 
00045     TrueOrFalse = 0,
00046 
00048     None = 3
00049   };
00050 
00051   static PartialValidity negatePartialValidity(PartialValidity pv);
00052 
00053 public:
00054   IncompleteSolver() {};
00055   virtual ~IncompleteSolver() {};
00056 
00064   virtual IncompleteSolver::PartialValidity computeValidity(const Query&);
00065 
00069   virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0;
00070   
00072   virtual bool computeValue(const Query&, ref<Expr> &result) = 0;
00073 
00077   virtual bool computeInitialValues(const Query&,
00078                                     const std::vector<const Array*> 
00079                                       &objects,
00080                                     std::vector< std::vector<unsigned char> > 
00081                                       &values,
00082                                     bool &hasSolution) = 0;
00083 };
00084 
00088 class StagedSolverImpl : public SolverImpl {
00089 private:
00090   IncompleteSolver *primary;
00091   Solver *secondary;
00092   
00093 public:
00094   StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
00095   ~StagedSolverImpl();
00096     
00097   bool computeTruth(const Query&, bool &isValid);
00098   bool computeValidity(const Query&, Solver::Validity &result);
00099   bool computeValue(const Query&, ref<Expr> &result);
00100   bool computeInitialValues(const Query&,
00101                             const std::vector<const Array*> &objects,
00102                             std::vector< std::vector<unsigned char> > &values,
00103                             bool &hasSolution);
00104 };
00105 
00106 }
00107 
00108 #endif