Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 70 insertions, 0 deletions

diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
new file mode 100644
index 00000000..875216d9
--- /dev/null
+++ b/lib/Core/TimingSolver.h
@@ -0,0 +1,70 @@
+//===-- TimingSolver.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_TIMINGSOLVER_H
+#define KLEE_TIMINGSOLVER_H
+
+#include "klee/Expr.h"
+#include "klee/Solver.h"
+
+#include <vector>
+
+namespace klee {
+  class ExecutionState;
+  class Solver;
+  class STPSolver;
+
+  /// TimingSolver - A simple class which wraps a solver and handles
+  /// tracking the statistics that we care about.
+  class TimingSolver {
+  public:
+    Solver *solver;
+    STPSolver *stpSolver;
+    bool simplifyExprs;
+
+  public:
+    /// TimingSolver - Construct a new timing solver.
+    ///
+    /// \param _simplifyExprs - Whether expressions should be
+    /// simplified (via the constraint manager interface) prior to
+    /// querying.
+    TimingSolver(Solver *_solver, STPSolver *_stpSolver, 
+                 bool _simplifyExprs = true) 
+      : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {}
+    ~TimingSolver() {
+      delete solver;
+    }
+
+    void setTimeout(double t) {
+      stpSolver->setTimeout(t);
+    }
+
+    bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
+
+    bool mustBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+
+    bool mustBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+
+    bool mayBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+
+    bool mayBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+
+    bool getValue(const ExecutionState &, ref<Expr> expr, ref<Expr> &result);
+
+    bool getInitialValues(const ExecutionState&, 
+                          const std::vector<const Array*> &objects,
+                          std::vector< std::vector<unsigned char> > &result);
+
+    virtual std::pair< ref<Expr>, ref<Expr> >
+    getRange(const ExecutionState&, ref<Expr> query);
+  };
+
+}
+
+#endif