mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-24 12:43:14 +01:00
parent a1d870f19f e3a40459bf
commit 2e3c335e14
11 changed files with 64 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
README.md
View file

@ -189,3 +189,6 @@ python -c 'import z3; print(z3.get_version_string())'
See [``examples/python``](examples/python) for examples.
### ``Web Assembly``
[WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel.

7
src/ast/ast.cpp
View file

@ -2254,7 +2254,12 @@ var * ast_manager::mk_var(unsigned idx, sort * s) {
unsigned sz = var::get_obj_size();
void * mem = allocate_node(sz);
var * new_node = new (mem) var(idx, s);
return register_node(new_node);
var * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-var] #" << r->get_id() << "\n";
}
return r;
}
app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, expr * n) {

2
src/ast/pattern/expr_pattern_match.cpp
View file

@ -387,7 +387,7 @@ expr_pattern_match::initialize(char const * spec_string) {
m_instrs.push_back(instr(BACKTRACK));
std::istringstream is(spec_string);
cmd_context ctx(true, &m_manager);
cmd_context ctx(true, &m_manager);
bool ps = ctx.print_success_enabled();
ctx.set_print_success(false);
VERIFY(parse_smt2_commands(ctx, is));

3
src/ast/rewriter/seq_rewriter.cpp
View file

@ -367,6 +367,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2);
return mk_re_concat(args[0], args[1], result);
case OP_RE_UNION:
if (num_args == 1) {
result = args[0]; return BR_DONE;
}
SASSERT(num_args == 2);
return mk_re_union(args[0], args[1], result);
case OP_RE_RANGE:

14
src/cmd_context/cmd_context.cpp
View file

@ -718,8 +718,8 @@ void cmd_context::init_manager_core(bool new_manager) {
}
m_dt_eh = alloc(dt_eh, *this);
m_pmanager->set_new_datatype_eh(m_dt_eh.get());
if (!has_logic()) {
TRACE("cmd_context", tout << "init manager\n";);
if (!has_logic() && new_manager) {
TRACE("cmd_context", tout << "init manager " << m_logic << "\n";);
// add list type only if the logic is not specified.
// it prevents clashes with builtin types.
insert(pm().mk_plist_decl());
@ -757,6 +757,7 @@ void cmd_context::init_external_manager() {
}
bool cmd_context::set_logic(symbol const & s) {
TRACE("cmd_context", tout << s << "\n";);
if (has_logic())
throw cmd_exception("the logic has already been set");
if (has_manager() && m_main_ctx)
@ -1240,7 +1241,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
m_aux_pdecls.push_back(p);
}
void cmd_context::reset(bool finalize) {
void cmd_context::reset(bool finalize) {
m_processing_pareto = false;
m_logic = symbol::null;
m_check_sat_result = nullptr;
@ -1350,9 +1351,10 @@ void cmd_context::restore_func_decls(unsigned old_sz) {
}
void cmd_context::restore_psort_inst(unsigned old_sz) {
for (unsigned i = old_sz; i < m_psort_inst_stack.size(); ++i) {
for (unsigned i = m_psort_inst_stack.size(); i-- > old_sz; ) {
pdecl * s = m_psort_inst_stack[i];
s->reset_cache(*m_pmanager);
s->reset_cache(pm());
pm().dec_ref(s);
}
m_psort_inst_stack.resize(old_sz);
}
@ -2024,8 +2026,8 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
}
}
if (m_owner.m_scopes.size() > 0) {
m_owner.pm().inc_ref(pd);
m_owner.m_psort_inst_stack.push_back(pd);
}
}

5
src/muz/base/dl_util.cpp
View file

@ -31,6 +31,7 @@ Revision History:
#include "muz/base/dl_rule.h"
#include "muz/base/dl_util.h"
#include "util/stopwatch.h"
#include <inttypes.h>
namespace datalog {
@ -623,9 +624,9 @@ namespace datalog {
bool string_to_uint64(const char * s, uint64_t & res) {
#if _WINDOWS
int converted = sscanf_s(s, "%I64u", &res);
int converted = sscanf_s(s, "%" SCNu64, &res);
#else
int converted = sscanf(s, "%I64u", &res);
int converted = sscanf(s, "%" SCNu64, &res);
#endif
if(converted==0) {
return false;

4
src/opt/opt_context.cpp
View file

@ -265,6 +265,9 @@ namespace opt {
normalize();
internalize();
update_solver();
if (contains_quantifiers()) {
warning_msg("optimization with quantified constraints is not supported");
}
#if 0
if (is_qsat_opt()) {
return run_qsat_opt();
@ -368,7 +371,6 @@ namespace opt {
if (result == l_true && committed) m_optsmt.commit_assignment(index);
if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
throw default_exception("unbounded objectives on quantified constraints is not supported");
result = l_undef;
}
return result;
}

2
src/parsers/util/pattern_validation.cpp
View file

@ -48,7 +48,7 @@ struct pattern_validation_functor {
bool is_forbidden(func_decl const * decl) {
family_id fid = decl->get_family_id();
if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
if (fid == m_bfid && decl->get_decl_kind() != OP_EQ && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
return true;
if (fid == m_lfid)
return true;

2
src/smt/theory_datatype.cpp
View file

@ -461,7 +461,7 @@ namespace smt {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
// first: explain that root=v, given that app=cstor(…,v,…)
// first: explain that root=v, given that app=cstor(...,v,...)
for (enode * arg : enode::args(oc_get_cstor(app))) {
// found an argument which is equal to root
if (arg->get_root() == root->get_root()) {

36
src/smt/theory_seq.cpp
View file

@ -1473,7 +1473,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps) {
if (l == r) {
return false;
}
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";);
TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n"; display_deps(tout, deps););
m_new_solution = true;
m_rep.update(l, r, deps);
enode* n1 = ensure_enode(l);
@ -1513,7 +1513,9 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
change = canonize(r, rs, dep2) || change;
deps = m_dm.mk_join(dep2, deps);
TRACE("seq", tout << l << " = " << r << " ==> ";
tout << ls << " = " << rs << "\n";);
tout << ls << " = " << rs << "\n";
display_deps(tout, deps);
);
if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
return true;
}
@ -2358,9 +2360,21 @@ bool theory_seq::check_int_string() {
void theory_seq::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
SASSERT(m_util.str.is_stoi(e));
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
expr* s = nullptr;
VERIFY (m_util.str.is_stoi(e, s));
// stoi(s) >= -1
literal l = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(-1)));
add_axiom(l);
// stoi(s) >= 0 <=> s in (0-9)+
expr_ref num_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
app_ref in_re(m_util.re.mk_in_re(s, num_re), m);
literal ge0 = mk_simplified_literal(m_autil.mk_ge(e, m_autil.mk_int(0)));
add_axiom(~ge0, mk_literal(in_re));
add_axiom(ge0, ~mk_literal(in_re));
}
bool theory_seq::add_stoi_val_axiom(expr* e) {
@ -2404,8 +2418,9 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char));
}
for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
coeff = m_autil.mk_int(c);
rational c(1);
for (unsigned i = sz; i-- > 0; c *= rational(10)) {
coeff = m_autil.mk_numeral(c, true);
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
num = m_autil.mk_add(nums.size(), nums.c_ptr());
@ -2674,7 +2689,12 @@ void theory_seq::init_model(expr_ref_vector const& es) {
}
}
void theory_seq::finalize_model(model_generator& mg) {
m_rep.pop_scope(1);
}
void theory_seq::init_model(model_generator & mg) {
m_rep.push_scope();
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (ne const& n : m_nqs) {
@ -3475,8 +3495,8 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
literal_vector lits;
lits.push_back(~lit);
for (unsigned i = 0; i < states.size(); ++i) {
lits.push_back(mk_accept(e1, zero, e3, states[i]));
for (unsigned s : states) {
lits.push_back(mk_accept(e1, zero, e3, s));
}
if (lits.size() == 2) {
propagate_lit(nullptr, 1, &lit, lits[1]);

13
src/smt/theory_seq.h
View file

@ -64,14 +64,14 @@ namespace smt {
// + a cache for normalization.
class solution_map {
enum map_update { INS, DEL };
ast_manager& m;
ast_manager& m;
dependency_manager& m_dm;
eqdep_map_t m_map;
eval_cache m_cache;
expr_ref_vector m_lhs, m_rhs;
eqdep_map_t m_map;
eval_cache m_cache;
expr_ref_vector m_lhs, m_rhs;
ptr_vector<dependency> m_deps;
svector<map_update> m_updates;
unsigned_vector m_limit;
svector<map_update> m_updates;
unsigned_vector m_limit;
void add_trail(map_update op, expr* l, expr* r, dependency* d);
public:
@ -362,6 +362,7 @@ namespace smt {
void collect_statistics(::statistics & st) const override;
model_value_proc * mk_value(enode * n, model_generator & mg) override;
void init_model(model_generator & mg) override;
void finalize_model(model_generator & mg) override;
void init_search_eh() override;
void init_model(expr_ref_vector const& es);