mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix error messaging for parsers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-28 11:14:00 -08:00
parent 89971e2a98
commit 92b4b9e7a7
5 changed files with 67 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_opt.cpp
View file

@ -286,11 +286,23 @@ extern "C" {
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
ctx->set_ignore_check(true);
if (!parse_smt2_commands(*ctx.get(), s)) {
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
try {
if (!parse_smt2_commands(*ctx.get(), s)) {
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
}
catch (z3_exception& e) {
errstrm << e.msg();
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return;
}
}
ptr_vector<expr>::const_iterator it = ctx->begin_assertions();
ptr_vector<expr>::const_iterator end = ctx->end_assertions();
for (; it != end; ++it) {

14
src/api/api_parsers.cpp
View file

@ -55,7 +55,19 @@ extern "C" {
psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i]));
ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps));
}
if (!parse_smt2_commands(*ctx.get(), is)) {
std::stringstream errstrm;
ctx->set_regular_stream(errstrm);
try {
if (!parse_smt2_commands(*ctx.get(), is)) {
ctx = nullptr;
mk_c(c)->m_parser_error_buffer = errstrm.str();
SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast(mk_c(c)->m().mk_true());
}
}
catch (z3_exception& e) {
errstrm << e.msg();
mk_c(c)->m_parser_error_buffer = errstrm.str();
ctx = nullptr;
SET_ERROR_CODE(Z3_PARSER_ERROR);
return of_ast(mk_c(c)->m().mk_true());

38
src/api/python/z3/z3.py
View file

@ -6668,11 +6668,17 @@ class Fixedpoint(Z3PPObject):
def parse_string(self, s):
"""Parse rules and queries from a string"""
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
try:
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def parse_file(self, f):
"""Parse rules and queries from a file"""
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
try:
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
@ -6995,15 +7001,21 @@ class Optimize(Z3PPObject):
def upper_values(self, obj):
if not isinstance(obj, OptimizeObjective):
raise Z3Exception("Expecting objective handle returned by maximize/minimize")
return obj.upper_values()
return obj.upper_values()
def from_file(self, filename):
"""Parse assertions and objectives from a file"""
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
try:
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def from_string(self, s):
"""Parse assertions and objectives from a string"""
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
try:
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
except Z3Exception as e:
_handle_parse_error(e, self.ctx)
def assertions(self):
"""Return an AST vector containing all added constraints."""
@ -8071,6 +8083,12 @@ def _dict2darray(decls, ctx):
i = i + 1
return sz, _names, _decls
def _handle_parse_error(ex, ctx):
msg = Z3_get_parser_error(ctx.ref())
if msg != "":
raise Z3Exception(msg)
raise ex
def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
"""Parse a string in SMT 2.0 format using the given sorts and decls.
@ -8089,7 +8107,10 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
ctx = _get_ctx(ctx)
ssz, snames, ssorts = _dict2sarray(sorts, ctx)
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
try:
return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
except Z3Exception as e:
_handle_parse_error(e, ctx)
def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
"""Parse a file in SMT 2.0 format using the given sorts and decls.
@ -8099,7 +8120,10 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
ctx = _get_ctx(ctx)
ssz, snames, ssorts = _dict2sarray(sorts, ctx)
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
try:
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
except Z3Exception as e:
_handle_parse_error(e, ctx)
def Interpolant(a,ctx=None):
"""Create an interpolation operator.

7
src/cmd_context/cmd_context.cpp
View file

@ -339,6 +339,13 @@ void ast_object_ref::finalize(cmd_context & ctx) {
ctx.m().dec_ref(m_ast);
}
void stream_ref::set(std::ostream& out) {
reset();
m_owner = false;
m_name = "caller-owned";
m_stream = &out;
}
void stream_ref::set(char const * name) {
if (!name) {
throw cmd_exception("invalid stream name");

2
src/cmd_context/cmd_context.h
View file

@ -128,6 +128,7 @@ public:
stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
~stream_ref() { reset(); }
void set(char const * name);
void set(std::ostream& strm);
void reset();
std::ostream & operator*() { return *m_stream; }
char const * name() const { return m_name.c_str(); }
@ -404,6 +405,7 @@ public:
void reset_object_refs();
void reset_user_tactics();
void set_regular_stream(char const * name) { m_regular.set(name); }
void set_regular_stream(std::ostream& out) { m_regular.set(out); }
void set_diagnostic_stream(char const * name);
virtual std::ostream & regular_stream() { return *m_regular; }
virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }