Merge branch 'dev' of https://github.com/martinjonas/q3b into dev

martinjonas · Feb 7, 2019 · ef38338 · ef38338
2 parents 9630b6c + 56a9566
commit ef38338
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 3 deletions.
diff --git a/lib/SMTLIBInterpreter.cpp b/lib/SMTLIBInterpreter.cpp
@@ -345,6 +345,17 @@ antlrcpp::Any SMTLIBInterpreter::visitCommand(SMTLIBv2Parser::CommandContext* co
         }
         std::cout << ")" << std::endl;
     }
+    else if (command->cmd_getValue())
+    {
+        std::cout << "(" << std::endl;
+        for (const auto& t : command->term())
+        {
+            z3::expr termExpr = visitTerm(t);
+            z3::expr value = Solver::substituteModel(termExpr, model).simplify();
+            std::cout << "  (" <<  termExpr << " " << value << ")" << std::endl;
+        }
+        std::cout << ")" << std::endl;
+    }
     else if (command->cmd_defineFun())
     {
         visitFunction_def(command->function_def());

diff --git a/lib/Solver.cpp b/lib/Solver.cpp
@@ -434,7 +434,7 @@ Result Solver::runWithOverApproximations(ExprToBDDTransformer &transformer)
     return runWithApproximations(transformer, OVERAPPROXIMATION);
 }
 
-z3::expr Solver::substituteModel(z3::expr& e, const std::map<std::string, std::vector<bool>>& model) const
+z3::expr Solver::substituteModel(z3::expr& e, const std::map<std::string, std::vector<bool>>& model)
 {
     auto &context = e.ctx();
     z3::expr_vector consts(context);

diff --git a/lib/Solver.h b/lib/Solver.h
@@ -24,6 +24,8 @@ class Solver
 
     static std::mutex m_z3context;
     static std::atomic<bool> resultComputed;
+
+    static z3::expr substituteModel(z3::expr&, const std::map<std::string, std::vector<bool>>&);
 private:
     Config config;
 
@@ -43,8 +45,6 @@ class Solver
     static std::mutex m;
     static std::mutex m_res;
     static std::condition_variable doneCV;
-
-    z3::expr substituteModel(z3::expr&, const std::map<std::string, std::vector<bool>>&) const;
 };
 
 #endif // BDDSOLVER_H