6 files changed, 37 insertions, 55 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index cc186db7..6a72692d 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -29,6 +29,8 @@ extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
 extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
+extern llvm::cl::opt<bool> UseAssignmentValidatingSolver;
+
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
 {
diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h
index 62f514ff..1cad98fd 100644
--- a/include/klee/Internal/Module/KInstruction.h
+++ b/include/klee/Internal/Module/KInstruction.h
@@ -11,7 +11,11 @@
 #define KLEE_KINSTRUCTION_H
 
 #include "klee/Config/Version.h"
+#include "klee/Internal/Module/InstructionInfoTable.h"
+
 #include "llvm/Support/DataTypes.h"
+#include "llvm/Support/raw_ostream.h"
+
 #include <vector>
 
 namespace llvm {
@@ -39,7 +43,9 @@ namespace klee {
     unsigned dest;
 
   public:
-    virtual ~KInstruction(); 
+    virtual ~KInstruction();
+    void printFileLine(llvm::raw_ostream &);
+
   };
 
   struct KGEPInstruction : KInstruction {
diff --git a/include/klee/Internal/Support/FileHandling.h b/include/klee/Internal/Support/FileHandling.h
new file mode 100644
index 00000000..bee06b9b
--- /dev/null
+++ b/include/klee/Internal/Support/FileHandling.h
@@ -0,0 +1,19 @@
+//===-- FileHandling.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_FILE_HANDLING_H__
+#define __KLEE_FILE_HANDLING_H__
+#include "llvm/Support/raw_ostream.h"
+#include <string>
+
+namespace klee {
+llvm::raw_fd_ostream *klee_open_output_file(std::string &path,
+                                            std::string &error);
+}
+
+#endif
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 4c428994..40f59ff1 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -138,6 +138,8 @@ public:
 
   virtual void setInhibitForking(bool value) = 0;
 
+  virtual void prepareForEarlyExit() = 0;
+
   /*** State accessor methods ***/
 
   virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 2f613992..e669c6f4 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -203,60 +203,6 @@ namespace klee {
     virtual void setCoreSolverTimeout(double timeout);
   };
 
-#ifdef ENABLE_STP
-  /// STPSolver - A complete solver based on STP.
-  class STPSolver : public Solver {
-  public:
-    /// STPSolver - Construct a new STPSolver.
-    ///
-    /// \param useForkedSTP - Whether STP should be run in a separate process
-    /// (required for using timeouts).
-    /// \param optimizeDivides - Whether constant division operations should
-    /// be optimized into add/shift/multiply operations.
-    STPSolver(bool useForkedSTP, bool optimizeDivides = true);
-
-    /// getConstraintLog - Return the constraint log for the given state in CVC
-    /// format.
-    virtual char *getConstraintLog(const Query&);
-
-    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0
-    /// is off.
-    virtual void setCoreSolverTimeout(double timeout);
-  };
-#endif // ENABLE_STP
-
-#ifdef ENABLE_Z3
-  /// Z3Solver - A solver complete solver based on Z3
-  class Z3Solver : public Solver {
-  public:
-    /// Z3Solver - Construct a new Z3Solver.
-    Z3Solver();
-
-    /// Get the query in SMT-LIBv2 format.
-    /// \return A C-style string. The caller is responsible for freeing this.
-    virtual char *getConstraintLog(const Query &);
-
-    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given
-    /// value; 0
-    /// is off.
-    virtual void setCoreSolverTimeout(double timeout);
-  };
-#endif // ENABLE_Z3
-
-#ifdef ENABLE_METASMT
-  
-  template<typename SolverContext>
-  class MetaSMTSolver : public Solver {
-  public:
-    MetaSMTSolver(bool useForked, bool optimizeDivides);
-    virtual ~MetaSMTSolver();
-  
-    virtual char *getConstraintLog(const Query&);
-    virtual void setCoreSolverTimeout(double timeout);
-};
-
-#endif /* ENABLE_METASMT */
-
   /* *** */
 
   /// createValidatingSolver - Create a solver which will validate all query
@@ -268,6 +214,12 @@ namespace klee {
   /// \param oracle - The solver to check query results against.
   Solver *createValidatingSolver(Solver *s, Solver *oracle);
 
+  /// createAssignmentValidatingSolver - Create a solver that when requested
+  /// for an assignment will check that the computed assignment satisfies
+  /// the Query.
+  /// \param s - The underlying solver to use.
+  Solver *createAssignmentValidatingSolver(Solver *s);
+
   /// createCachingSolver - Create a solver which will cache the queries in
   /// memory (without eviction).
   ///
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 5d8aa1ab..55e681de 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -46,6 +46,7 @@ namespace klee {
     
     ref<Expr> evaluate(const Array *mo, unsigned index) const;
     ref<Expr> evaluate(ref<Expr> e);
+    void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const;
 
     template<typename InputIterator>
     bool satisfies(InputIterator begin, InputIterator end);