mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
recover error stream from dimacs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ef9b46b2e5
commit
9b4cf1559d
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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_ */
|
||||
|
||||
|
|
|
@ -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()););
|
||||
|
||||
|
|
Loading…
Reference in a new issue