From 9b4cf1559dd431a716b351b4d14105ea27efb263 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Nov 2018 15:33:46 -0800
Subject: [PATCH] recover error stream from dimacs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp        |  6 ++++-
 src/sat/dimacs.cpp            | 47 ++++++++++++++++++++---------------
 src/sat/dimacs.h              |  2 +-
 src/shell/dimacs_frontend.cpp |  6 ++---
 4 files changed, 36 insertions(+), 25 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index cb4ae19db..a5ad7b525 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -183,8 +183,12 @@ extern "C" {
         }
         else if (ext && std::string("dimacs") == ext) {
             ast_manager& m = to_solver_ref(s)->get_manager();
+            std::stringstream err;
             sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
-            parse_dimacs(is, solver);
+            if (!parse_dimacs(is, err, solver)) {
+                SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());
+                return;
+            }
             sat2goal s2g;
             ref<sat2goal::mc> mc;
             atom2bool_var a2b(m);
diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp
index 463418b23..970e682b3 100644
--- a/src/sat/dimacs.cpp
+++ b/src/sat/dimacs.cpp
@@ -21,6 +21,8 @@ Revision History:
 #undef min
 #include "sat/sat_solver.h"
 
+struct lex_error {};
+
 class stream_buffer {
     std::istream & m_stream;
     int            m_val;
@@ -67,7 +69,7 @@ void skip_line(Buffer & in) {
 }
 
 template<typename Buffer>
-int parse_int(Buffer & in) {
+int parse_int(Buffer & in, std::ostream& err) {
     int     val = 0;
     bool    neg = false;
     skip_whitespace(in);
@@ -81,9 +83,8 @@ int parse_int(Buffer & in) {
     }
 
     if (*in < '0' || *in > '9') {
-        std::cerr << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
-        exit(3);
-        exit(ERR_PARSER);
+        err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
+        throw lex_error();
     }
 
     while (*in >= '0' && *in <= '9') {
@@ -95,14 +96,14 @@ int parse_int(Buffer & in) {
 }
 
 template<typename Buffer>
-void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) {
+void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) {
     int     parsed_lit;
     int     var;
     
     lits.reset();
 
     while (true) { 
-        parsed_lit = parse_int(in);
+        parsed_lit = parse_int(in, err);
         if (parsed_lit == 0)
             break;
         var = abs(parsed_lit);
@@ -114,24 +115,30 @@ void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits)
 }
 
 template<typename Buffer>
-void parse_dimacs_core(Buffer & in, sat::solver & solver) {
+bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) {
     sat::literal_vector lits;
-    while (true) {
-        skip_whitespace(in);
-        if (*in == EOF) {
-            break;
-        }
-        else if (*in == 'c' || *in == 'p') {
-            skip_line(in);
-        }
-        else {
-            read_clause(in, solver, lits);
-            solver.mk_clause(lits.size(), lits.c_ptr());
+    try {
+        while (true) {
+            skip_whitespace(in);
+            if (*in == EOF) {
+                break;
+            }
+            else if (*in == 'c' || *in == 'p') {
+                skip_line(in);
+            }
+            else {
+                read_clause(in, err, solver, lits);
+                solver.mk_clause(lits.size(), lits.c_ptr());
+            }
         }
     }
+    catch (lex_error) {
+        return false;
+    }
+    return true;
 }
 
-void parse_dimacs(std::istream & in, sat::solver & solver) {
+bool parse_dimacs(std::istream & in, std::ostream& err, sat::solver & solver) {
     stream_buffer _in(in);
-    parse_dimacs_core(_in, solver);
+    return parse_dimacs_core(_in, err, solver);
 }
diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h
index 50ebec0c8..4c5d51502 100644
--- a/src/sat/dimacs.h
+++ b/src/sat/dimacs.h
@@ -21,7 +21,7 @@ Revision History:
 
 #include "sat/sat_types.h"
 
-void parse_dimacs(std::istream & s, sat::solver & solver);
+bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver);
 
 #endif /* DIMACS_PARSER_H_ */
 
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index 3a2af72cf..738566ce2 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -136,7 +136,7 @@ void verify_solution(char const * file_name) {
         std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
         exit(ERR_OPEN_FILE);
     }
-    parse_dimacs(in, solver);
+    parse_dimacs(in, std::cerr, solver);
     
     sat::model const & m = g_solver->get_model();
     for (unsigned i = 1; i < m.size(); i++) {
@@ -178,10 +178,10 @@ unsigned read_dimacs(char const * file_name) {
             std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
             exit(ERR_OPEN_FILE);
         }
-        parse_dimacs(in, solver);
+        parse_dimacs(in, std::cerr, solver);
     }
     else {
-        parse_dimacs(std::cin, solver);
+        parse_dimacs(std::cin, std::cerr, solver);
     }
     IF_VERBOSE(20, solver.display_status(verbose_stream()););