mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

add debugging facilities for github issues #384 #367

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-22 10:43:18 -08:00
parent 65da0f9f3a
commit 9c6271dded
14 changed files with 529 additions and 479 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -1079,7 +1079,7 @@ def def_API(name, result, params):
def mk_bindings():
exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n")
for key, val in API2Id.items():
exe_c.write(" in.register_cmd(%s, exec_%s);\n" % (key, val))
exe_c.write(" in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val))
exe_c.write("}\n")
def ml_method_name(name):

2
src/api/api_ast.cpp
View file

@ -776,6 +776,8 @@ extern "C" {
SET_ERROR_CODE(Z3_SORT_ERROR);
RETURN_Z3(of_expr(0));
}
SASSERT(from[i]->get_ref_count() > 0);
SASSERT(to[i]->get_ref_count() > 0);
}
expr_safe_replace subst(m);
for (unsigned i = 0; i < num_exprs; i++) {

1
src/api/api_ast_vector.cpp
View file

@ -26,6 +26,7 @@ Revision History:
extern "C" {
Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c) {
std::cout << "ast-vector\n";
Z3_TRY;
LOG_Z3_mk_ast_vector(c);
RESET_ERROR_CODE();

1
src/api/java/Context.java
View file

@ -3822,6 +3822,7 @@ public class Context extends IDisposable
m_Params_DRQ.clear(this);
m_Probe_DRQ.clear(this);
m_Solver_DRQ.clear(this);
m_Optimize_DRQ.clear(this);
m_Statistics_DRQ.clear(this);
m_Tactic_DRQ.clear(this);
m_Fixedpoint_DRQ.clear(this);

912
src/api/ml/z3.ml
View file

File diff suppressed because it is too large Load diff

10
src/api/z3_replayer.cpp
View file

@ -46,6 +46,7 @@ struct z3_replayer::imp {
size_t m_ptr;
size_t_map<void *> m_heap;
svector<z3_replayer_cmd> m_cmds;
vector<std::string> m_cmds_names;
enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
@ -509,6 +510,7 @@ struct z3_replayer::imp {
if (idx >= m_cmds.size())
throw z3_replayer_exception("invalid command");
try {
TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";);
m_cmds[idx](m_owner);
}
catch (z3_error & ex) {
@ -672,9 +674,11 @@ struct z3_replayer::imp {
m_result = obj;
}
void register_cmd(unsigned id, z3_replayer_cmd cmd) {
void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
m_cmds.reserve(id+1, 0);
m_cmds_names.reserve(id+1, "");
m_cmds[id] = cmd;
m_cmds_names[id] = name;
}
void reset() {
@ -786,8 +790,8 @@ void z3_replayer::store_result(void * obj) {
return m_imp->store_result(obj);
}
void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd) {
return m_imp->register_cmd(id, cmd);
void z3_replayer::register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
return m_imp->register_cmd(id, cmd, name);
}
void z3_replayer::parse() {

2
src/api/z3_replayer.h
View file

@ -62,7 +62,7 @@ public:
void ** get_obj_addr(unsigned pos);
void store_result(void * obj);
void register_cmd(unsigned id, z3_replayer_cmd cmd);
void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name);
};
#endif

1
src/ast/ast.cpp
View file

@ -1656,6 +1656,7 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
// increment reference counters

16
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -20,9 +20,11 @@ Revision History:
#include "expr_safe_replace.h"
#include "rewriter.h"
#include "ast_pp.h"
void expr_safe_replace::insert(expr* src, expr* dst) {
SASSERT(m.get_sort(src) == m.get_sort(dst));
m_src.push_back(src);
m_dst.push_back(dst);
m_subst.insert(src, dst);
@ -30,7 +32,7 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_todo.push_back(e);
expr* a, *b, *d;
expr* a, *b;
while (!m_todo.empty()) {
a = m_todo.back();
@ -39,7 +41,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
}
else if (m_subst.find(a, b)) {
m_cache.insert(a, b);
m_todo.pop_back();
m_todo.pop_back();
}
else if (is_var(a)) {
m_cache.insert(a, a);
@ -51,18 +53,21 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) {
if (m_cache.find(c->get_arg(i), d)) {
expr* d = 0, *arg = c->get_arg(i);
if (m_cache.find(arg, d)) {
m_args.push_back(d);
arg_differs |= c->get_arg(i) != d;
arg_differs |= arg != d;
SASSERT(m.get_sort(arg) == m.get_sort(d));
}
else {
m_todo.push_back(c->get_arg(i));
m_todo.push_back(arg);
}
}
if (m_args.size() == n) {
if (arg_differs) {
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
m_refs.push_back(b);
SASSERT(m.get_sort(a) == m.get_sort(b));
} else {
b = a;
}
@ -71,6 +76,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
}
}
else {
(std::cout << "q\n").flush();
SASSERT(is_quantifier(a));
quantifier* q = to_quantifier(a);
expr_safe_replace replace(m);

23
src/ast/seq_decl_plugin.cpp
View file

@ -163,6 +163,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const {
seq_decl_plugin::seq_decl_plugin(): m_init(false),
m_stringc_sym("String"),
m_charc_sym("Char"),
m_string(0),
m_char(0) {}
@ -369,7 +370,8 @@ void seq_decl_plugin::init() {
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
decl_plugin::set_manager(m, id);
m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0));
bv_util bv(*m);
m_char = bv.mk_sort(8);
m->inc_ref(m_char);
parameter param(m_char);
m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
@ -401,8 +403,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
case _STRING_SORT:
return m_string;
case _CHAR_SORT:
return m_char;
default:
UNREACHABLE();
return 0;
@ -470,6 +470,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_STRING_CONST:
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
m.raise_exception("invalid string declaration");
@ -583,7 +585,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
app* seq_decl_plugin::mk_string(symbol const& s) {
parameter param(s);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}
@ -591,10 +593,11 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
symbol sym(s.encode().c_str());
parameter param(sym);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}
bool seq_decl_plugin::is_value(app* e) const {
return is_app_of(e, m_family_id, OP_STRING_CONST);
}
@ -609,11 +612,21 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); }
app* seq_util::str::mk_char(zstring const& s, unsigned idx) {
bv_util bvu(m);
return bvu.mk_numeral(s[idx], s.num_bits());
}
bool seq_util::str::is_char(expr* n, zstring& c) const {
if (u.is_char(n)) {
c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
return true;
}
else {
return false;
}
}
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {

9
src/ast/seq_decl_plugin.h
View file

@ -22,13 +22,13 @@ Revision History:
#define SEQ_DECL_PLUGIN_H_
#include "ast.h"
#include "bv_decl_plugin.h"
enum seq_sort_kind {
SEQ_SORT,
RE_SORT,
_STRING_SORT, // internal only
_CHAR_SORT // internal only
_STRING_SORT // internal only
};
enum seq_op_kind {
@ -131,6 +131,7 @@ class seq_decl_plugin : public decl_plugin {
ptr_vector<psig> m_sigs;
bool m_init;
symbol m_stringc_sym;
symbol m_charc_sym;
sort* m_string;
sort* m_char;
@ -187,6 +188,7 @@ public:
ast_manager& get_manager() const { return m; }
bool is_char(sort* s) const { return seq.is_char(s); }
bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
@ -195,6 +197,7 @@ public:
bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@ -215,6 +218,7 @@ public:
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
app* mk_string(zstring const& s);
app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
app* mk_char(char ch);
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
app* mk_concat(expr* a, expr* b, expr* c) {
return mk_concat(mk_concat(a, b), c);
@ -238,6 +242,7 @@ public:
}
bool is_string(expr const* n, zstring& s) const;
bool is_char(expr* n, zstring& s) const;
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);

6
src/smt/theory_seq.cpp
View file

@ -331,7 +331,7 @@ bool theory_seq::check_length_coherence_tbd() {
if (is_var(f) && f == e) {
expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m);
TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";);
#if 0
#if 1
if (!assume_equality(e, emp)) {
// e = emp \/ e = unit(head.elem(e))*tail(e)
sort* char_sort = 0;
@ -341,9 +341,11 @@ bool theory_seq::check_length_coherence_tbd() {
expr_ref head(m_util.str.mk_unit(v), m);
expr_ref conc(m_util.str.mk_concat(head, tail), m);
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
assume_equality(tail, emp);
}
#endif
coherent = false;
m_branch_variable_head = j + 1;
return false;
}
}
return coherent;

7
src/smt/theory_seq_empty.h
View file

@ -30,6 +30,7 @@ namespace smt {
seq_util u;
symbol_set m_strings;
unsigned m_next;
char m_char;
std::string m_unique_prefix;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
@ -41,6 +42,7 @@ namespace smt {
m_model(md),
u(m),
m_next(0),
m_char(0),
m_unique_prefix("#B"),
m_trail(m)
{
@ -99,6 +101,11 @@ namespace smt {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
if (u.is_char(s)) {
//char s[2] = { ++m_char, 0 };
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
NOT_IMPLEMENTED_YET();
return 0;
}

16
src/util/mpf.cpp
View file

@ -239,16 +239,26 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
else {
scoped_mpq sig(m_mpq_manager);
scoped_mpz exp(m_mpq_manager);
scoped_mpq pow(m_mpq_manager);
m_mpq_manager.set(sig, significand);
m_mpq_manager.abs(sig);
m_mpz_manager.set(exp, exponent);
m_mpq_manager.set(pow, mpq(2));
// Normalize
while (m_mpq_manager.ge(sig, 2)) {
m_mpq_manager.div(sig, mpq(2), sig);
unsigned loop = 0;
while (m_mpq_manager.ge(sig, pow)) {
m_mpq_manager.mul(pow, 2, pow);
m_mpz_manager.inc(exp);
++loop;
if (loop % 1000 == 0) std::cout << loop << "\n";
}
std::cout << loop << "\n";
if (loop > 0) {
m_mpq_manager.div(sig, pow, sig);
}
std::cout << loop << "\n";
while (m_mpq_manager.lt(sig, 1)) {
m_mpq_manager.mul(sig, 2, sig);