diff --git a/README.md b/README.md index 8ebf6a078..447034a84 100644 --- a/README.md +++ b/README.md @@ -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. diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7e143e1a3..12ca136c5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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) { diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index d688c840c..c441fb4ce 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -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)); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 186abda48..e5cac969f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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: diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index aabe43110..11f800b25 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -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); - } } diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index e8a1c5139..88b4c398d 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -31,6 +31,7 @@ Revision History: #include "muz/base/dl_rule.h" #include "muz/base/dl_util.h" #include "util/stopwatch.h" +#include 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; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1950a199d..69177e290 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -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; } diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index 0d076aadd..df1f6cd00 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -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; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 9ff81fa08..049555297 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -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()) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 94841603d..db8dbd340 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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]); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 21aedd7e3..a17b29eba 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -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 m_deps; - svector m_updates; - unsigned_vector m_limit; + svector 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);