Merge pull request #13 from martinjonas/dev

Merge Q3B 1.0
martinjonas · Feb 7, 2019 · 10b19ad · 10b19ad
2 parents dc77ac2 + ef38338
commit 10b19ad
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 4 deletions.
diff --git a/app/main.cpp b/app/main.cpp
@@ -17,7 +17,7 @@ using namespace std;
 using namespace z3;
 using namespace antlr4;
 
-const std::string version = "0.9 dev";
+const std::string version = "1.0";
 
 void print_usage()
 {
@@ -180,6 +180,11 @@ int main(int argc, char* argv[])
 
     std::ifstream stream;
     stream.open(filename);
+    if (!stream.good())
+    {
+        std::cout << "(error \"failed to open file '" << filename << "'\")" << std::endl;
+        return 1;
+    }
 
     ANTLRInputStream input(stream);
     SMTLIBv2Lexer lexer(&input);

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