Add SimpleModel which simply starts as an empty model and use that

in place of `FileSerializableModel` where appropriate.

include/jfs/Core/SimpleModel.h

@@ -0,0 +1,27 @@
+//===----------------------------------------------------------------------===//
+//
+//                        JFS - The JIT Fuzzing Solver
+//
+// Copyright 2017-2018 Alastair Donaldson
+//
+// This file is distributed under the MIT license.
+// See LICENSE.txt for details.
+//
+//===----------------------------------------------------------------------===//
+#ifndef JFS_CORE_SIMPLE_MODEL_H
+#define JFS_CORE_SIMPLE_MODEL_H
+#include "jfs/Core/Model.h"
+
+namespace jfs {
+namespace core {
+
+// A model that on creation is empty
+class SimpleModel : public Model {
+public:
+  SimpleModel(JFSContext& ctx);
+};
+
+} // namespace core
+} // namespace jfs
+
+#endif

lib/Core/CMakeLists.txt

@@ -13,6 +13,7 @@ jfs_add_component(JFSCore
   Model.cpp
   ModelValidator.cpp
   Query.cpp
+  SimpleModel.cpp
   SMTLIB2Parser.cpp
   Solver.cpp
   ToolErrorHandler.cpp

lib/Core/SimpleModel.cpp

@@ -0,0 +1,20 @@
+//===----------------------------------------------------------------------===//
+//
+//                        JFS - The JIT Fuzzing Solver
+//
+// Copyright 2017-2018 Alastair Donaldson
+//
+// This file is distributed under the MIT license.
+// See LICENSE.txt for details.
+//
+//===----------------------------------------------------------------------===//
+#include "jfs/Core/SimpleModel.h"
+
+namespace jfs {
+namespace core {
+
+SimpleModel::SimpleModel(JFSContext& ctx) : Model(ctx) {
+  z3Model = Z3ModelHandle(::Z3_mk_model(ctx.getZ3Ctx()), ctx.getZ3Ctx());
+}
+} // namespace core
+} // namespace jfs

lib/FuzzingCommon/FuzzingSolver.cpp

@@ -10,7 +10,7 @@
 //===----------------------------------------------------------------------===//
 #include "jfs/FuzzingCommon/FuzzingSolver.h"
 #include "jfs/Core/IfVerbose.h"
-#include "jfs/FuzzingCommon/FileSerializableModel.h"
+#include "jfs/Core/SimpleModel.h"
 #include "jfs/FuzzingCommon/FuzzingAnalysisInfo.h"
 #include "jfs/FuzzingCommon/FuzzingSolverOptions.h"
 #include "jfs/Transform/QueryPassManager.h"
@@ -83,8 +83,8 @@ class FuzzingSolverImpl {
           new TrivialFuzzingSolverResponse(SolverResponse::SAT));
       if (produceModel) {
         // Make empty model
-        auto model = std::unique_ptr<FileSerializableModel>(
-            new FileSerializableModel(q.getContext()));
+        auto model =
+            std::unique_ptr<SimpleModel>(new SimpleModel(q.getContext()));
         resp->setModel(std::move(model));
       }
       return resp;
@@ -149,8 +149,7 @@ class FuzzingSolverImpl {
           new TrivialFuzzingSolverResponse(SolverResponse::SAT));
       if (produceModel) {
         // Make empty model
-        auto model = std::unique_ptr<FileSerializableModel>(
-            new FileSerializableModel(q.getContext()));
+        auto model = std::unique_ptr<Model>(new SimpleModel(q.getContext()));
         // Now convert model so that it satisfies the query given to the
         // preprocessing passes.
         bool convertModelSuccess =