From 441dbbb94bc7bd71f56d440b0029b473a3918e21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Nov 2016 13:08:50 -0800 Subject: [PATCH 01/42] streamline logging in arithmetic Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 ++-- src/smt/theory_arith_core.h | 8 +++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 50bfee20e..de357c8d3 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -417,8 +417,8 @@ namespace smt { template void theory_arith::atom::display(theory_arith const& th, std::ostream& out) const { literal l(get_bool_var(), !m_is_true); - out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " "; - out << l << ":"; + // out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " "; + // out << l << ":"; th.get_context().display_detailed_literal(out, l); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 07d30222b..a08ee50ab 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1069,7 +1069,7 @@ namespace smt { template void theory_arith::flush_bound_axioms() { - CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";); + CTRACE("arith_verbose", !m_new_atoms.empty(), tout << "flush bound axioms\n";); while (!m_new_atoms.empty()) { ptr_vector atoms; @@ -1084,7 +1084,7 @@ namespace smt { --i; } } - CTRACE("arith", !atoms.empty(), + CTRACE("arith", atoms.size() > 1, for (unsigned i = 0; i < atoms.size(); ++i) { atoms[i]->display(*this, tout); tout << "\n"; }); @@ -1292,7 +1292,7 @@ namespace smt { template void theory_arith::assign_eh(bool_var v, bool is_true) { - TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";); + TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";); atom * a = get_bv2a(v); if (!a) return; SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef); @@ -3043,12 +3043,14 @@ namespace smt { m_stats.m_conflicts++; m_num_conflicts++; TRACE("arith_conflict", + tout << "scope: " << ctx.get_scope_level() << "\n"; for (unsigned i = 0; i < num_literals; i++) { ctx.display_detailed_literal(tout, lits[i]); tout << " "; if (coeffs_enabled()) { tout << "bound: " << bounds.lit_coeffs()[i] << "\n"; } + tout << "\n"; } for (unsigned i = 0; i < num_eqs; i++) { tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " "; From 024082a45f11505b5d6992472f8a50a409920606 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Nov 2016 09:52:05 -0800 Subject: [PATCH 02/42] adding preferred sat, currently disabled, to wmax. Fixing issue #815 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 4 + src/opt/opt_solver.h | 1 + src/opt/wmax.cpp | 256 ++++++++++++++-- src/smt/smt_consequences.cpp | 200 ++++++++++-- src/smt/smt_context.cpp | 162 +++++----- src/smt/smt_context.h | 27 +- src/smt/smt_context_inv.cpp | 3 + src/smt/smt_kernel.cpp | 9 + src/smt/smt_kernel.h | 7 +- src/smt/theory_wmaxsat.cpp | 577 +++++++++++++++++++---------------- src/smt/theory_wmaxsat.h | 30 +- src/solver/solver.cpp | 4 + src/solver/solver.h | 12 +- 13 files changed, 887 insertions(+), 405 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 0d0283232..868303660 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -198,6 +198,10 @@ namespace opt { return m_context.find_mutexes(vars, mutexes); } + lbool opt_solver::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_context.preferred_sat(asms, cores); + } + /** diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 16c2061c7..094023ba2 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -107,6 +107,7 @@ namespace opt { virtual std::ostream& display(std::ostream & out) const; virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index d8ffe9f66..228e14cd6 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -32,64 +32,286 @@ namespace opt { class wmax : public maxsmt_solver_base { + obj_map m_weights; + obj_map m_keys; + expr_ref_vector m_trail, m_defs; + + void reset() { + m_weights.reset(); + m_keys.reset(); + m_trail.reset(); + m_defs.reset(); + } + public: wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft) {} + maxsmt_solver_base(c, ws, soft), + m_trail(m), + m_defs(m) {} + virtual ~wmax() {} lbool operator()() { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); obj_map soft; + reset(); lbool is_sat = find_mutexes(soft); if (is_sat != l_true) { return is_sat; } - rational offset = m_lower; - m_upper = offset; + m_upper = m_lower; bool was_sat = false; - expr_ref_vector disj(m); + expr_ref_vector disj(m), asms(m); + vector cores; obj_map::iterator it = soft.begin(), end = soft.end(); for (; it != end; ++it) { - expr_ref tmp(m); - bool is_true = m_model->eval(it->m_key, tmp) && m.is_true(tmp); - expr* c = wth().assert_weighted(it->m_key, it->m_value, is_true); - if (!is_true) { + expr* c = assert_weighted(wth(), it->m_key, it->m_value); + if (!is_true(it->m_key)) { + disj.push_back(m.mk_not(c)); m_upper += it->m_value; - disj.push_back(c); } } + wth().init_min_cost(m_upper - m_lower); s().assert_expr(mk_or(disj)); trace_bounds("wmax"); - while (l_true == is_sat && m_lower < m_upper) { + + while (!m.canceled() && m_lower < m_upper) { + //mk_assumptions(asms); + //is_sat = s().preferred_sat(asms, cores); is_sat = s().check_sat(0, 0); if (m.canceled()) { is_sat = l_undef; } + if (is_sat == l_false) { + break; + } if (is_sat == l_true) { if (wth().is_optimal()) { - m_upper = offset + wth().get_min_cost(); + m_upper = m_lower + wth().get_cost(); s().get_model(m_model); } expr_ref fml = wth().mk_block(); + //DEBUG_CODE(verify_cores(cores);); s().assert_expr(fml); was_sat = true; } + else { + //DEBUG_CODE(verify_cores(cores);); + } + update_cores(wth(), cores); + wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); + SASSERT(m_lower <= m_upper); } - if (was_sat) { - wth().get_assignment(m_assignment); - m_upper = offset + wth().get_min_cost(); - } - if (is_sat == l_false && was_sat) { + + update_assignment(); + + if (!m.canceled() && is_sat == l_undef && m_lower == m_upper) { is_sat = l_true; } - if (is_sat == l_true) { + if (is_sat == l_false) { + is_sat = l_true; m_lower = m_upper; } TRACE("opt", tout << "min cost: " << m_upper << "\n";); return is_sat; } + + bool is_true(expr* e) { + expr_ref tmp(m); + return m_model->eval(e, tmp) && m.is_true(tmp); + } + + void update_assignment() { + m_assignment.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment.push_back(is_true(m_soft[i])); + } + } + + struct compare_asm { + wmax& max; + compare_asm(wmax& max):max(max) {} + bool operator()(expr* a, expr* b) const { + return max.m_weights[a] > max.m_weights[b]; + } + }; + + void mk_assumptions(expr_ref_vector& asms) { + ptr_vector _asms; + obj_map::iterator it = m_weights.begin(), end = m_weights.end(); + for (; it != end; ++it) { + _asms.push_back(it->m_key); + } + compare_asm comp(*this); + std::sort(_asms.begin(),_asms.end(), comp); + asms.reset(); + for (unsigned i = 0; i < _asms.size(); ++i) { + asms.push_back(m.mk_not(_asms[i])); + } + } + + void verify_cores(vector const& cores) { + for (unsigned i = 0; i < cores.size(); ++i) { + verify_core(cores[i]); + } + } + + void verify_core(expr_ref_vector const& core) { + s().push(); + s().assert_expr(core); + VERIFY(l_false == s().check_sat(0, 0)); + s().pop(1); + } + + void update_cores(smt::theory_wmaxsat& th, vector const& cores) { + obj_hashtable seen; + bool updated = false; + unsigned min_core_size = UINT_MAX; + for (unsigned i = 0; i < cores.size(); ++i) { + expr_ref_vector const& core = cores[i]; + if (core.size() <= 20) { + s().assert_expr(m.mk_not(mk_and(core))); + } + min_core_size = std::min(core.size(), min_core_size); + if (core.size() >= 11) { + continue; + } + bool found = false; + for (unsigned j = 0; !found && j < core.size(); ++j) { + found = seen.contains(core[j]); + } + if (found) { + continue; + } + for (unsigned j = 0; j < core.size(); ++j) { + seen.insert(core[j]); + } + update_core(th, core); + updated = true; + } + // if no core was selected, then take the smallest cores. + for (unsigned i = 0; !updated && i < cores.size(); ++i) { + expr_ref_vector const& core = cores[i]; + if (core.size() > min_core_size + 2) { + continue; + } + bool found = false; + for (unsigned j = 0; !found && j < core.size(); ++j) { + found = seen.contains(core[j]); + } + if (found) { + continue; + } + for (unsigned j = 0; j < core.size(); ++j) { + seen.insert(core[j]); + } + update_core(th, core); + } + } + + + rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector& keys, vector& weights) { + rational min_weight(-1); + for (unsigned i = 0; i < core.size(); ++i) { + expr* e; + VERIFY(m.is_not(core[i], e)); + keys.push_back(m_keys[e]); + rational weight = m_weights[e]; + if (i == 0 || weight < min_weight) { + min_weight = weight; + } + weights.push_back(weight); + m_weights.erase(e); + m_keys.erase(e); + th.disable_var(e); + } + for (unsigned i = 0; i < core.size(); ++i) { + rational weight = weights[i]; + if (weight > min_weight) { + weight -= min_weight; + assert_weighted(th, keys[i], weight); + } + } + return min_weight; + } + + // assert maxres clauses + // assert new core members with value of current model. + // update lower bound + // bounds get re-normalized when solver is invoked. + // each element of core is negated literal from theory_wmaxsat + // disable those literals from th + + void update_core(smt::theory_wmaxsat& th, expr_ref_vector const& core) { + ptr_vector keys; + vector weights; + rational min_weight = remove_negations(th, core, keys, weights); + max_resolve(th, keys, min_weight); + m_lower += min_weight; + // std::cout << core << " " << min_weight << "\n"; + } + + void max_resolve(smt::theory_wmaxsat& th, ptr_vector const& core, rational const& w) { + SASSERT(!core.empty()); + expr_ref fml(m), asum(m); + app_ref cls(m), d(m), dd(m); + // + // d_0 := true + // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 + // soft (b_i or !d_i) + // == (b_i or !(!b_{i-1} or d_{i-1})) + // == (b_i or b_0 & b_1 & ... & b_{i-1}) + // + // Soft constraint is satisfied if previous soft constraint + // holds or if it is the first soft constraint to fail. + // + // Soundness of this rule can be established using MaxRes + // + for (unsigned i = 1; i < core.size(); ++i) { + expr* b_i = core[i-1]; + expr* b_i1 = core[i]; + if (i == 1) { + d = to_app(b_i); + } + else if (i == 2) { + d = m.mk_and(b_i, d); + m_trail.push_back(d); + } + else { + dd = mk_fresh_bool("d"); + fml = m.mk_implies(dd, d); + s().assert_expr(fml); + m_defs.push_back(fml); + fml = m.mk_implies(dd, b_i); + s().assert_expr(fml); + m_defs.push_back(fml); + fml = m.mk_and(d, b_i); + update_model(dd, fml); + d = dd; + } + cls = m.mk_or(b_i1, d); + m_trail.push_back(cls); + assert_weighted(th, cls, w); + } + } + + expr* assert_weighted(smt::theory_wmaxsat& th, expr* key, rational const& w) { + expr* c = th.assert_weighted(key, w); + m_weights.insert(c, w); + m_keys.insert(c, key); + m_trail.push_back(c); + return c; + } + + void update_model(expr* def, expr* value) { + expr_ref val(m); + if (m_model && m_model->eval(value, val, true)) { + m_model->register_decl(to_app(def)->get_decl(), val); + } + } + }; maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index e6edbf87e..ab1971a3e 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -56,36 +56,7 @@ namespace smt { s.insert(lit.var()); } else { - b_justification js = get_justification(lit.var()); - switch (js.get_kind()) { - case b_justification::CLAUSE: { - clause * cls = js.get_clause(); - if (!cls) break; - unsigned num_lits = cls->get_num_literals(); - for (unsigned j = 0; j < num_lits; ++j) { - literal lit2 = cls->get_literal(j); - if (lit2.var() != lit.var()) { - s |= m_antecedents.find(lit2.var()); - } - } - break; - } - case b_justification::BIN_CLAUSE: { - s |= m_antecedents.find(js.get_literal().var()); - break; - } - case b_justification::AXIOM: { - break; - } - case b_justification::JUSTIFICATION: { - literal_vector literals; - m_conflict_resolution->justification2literals(js.get_justification(), literals); - for (unsigned j = 0; j < literals.size(); ++j) { - s |= m_antecedents.find(literals[j].var()); - } - break; - } - } + justify(lit, s); } m_antecedents.insert(lit.var(), s); TRACE("context", display_literal_verbose(tout, lit); @@ -122,6 +93,39 @@ namespace smt { } } + void context::justify(literal lit, index_set& s) { + b_justification js = get_justification(lit.var()); + switch (js.get_kind()) { + case b_justification::CLAUSE: { + clause * cls = js.get_clause(); + if (!cls) break; + unsigned num_lits = cls->get_num_literals(); + for (unsigned j = 0; j < num_lits; ++j) { + literal lit2 = cls->get_literal(j); + if (lit2.var() != lit.var()) { + s |= m_antecedents.find(lit2.var()); + } + } + break; + } + case b_justification::BIN_CLAUSE: { + s |= m_antecedents.find(js.get_literal().var()); + break; + } + case b_justification::AXIOM: { + break; + } + case b_justification::JUSTIFICATION: { + literal_vector literals; + m_conflict_resolution->justification2literals(js.get_justification(), literals); + for (unsigned j = 0; j < literals.size(); ++j) { + s |= m_antecedents.find(literals[j].var()); + } + break; + } + } + } + void context::extract_fixed_consequences(unsigned& start, obj_map& vars, index_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); SASSERT(!inconsistent()); @@ -369,6 +373,142 @@ namespace smt { << ")\n"; } + void context::extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size) { + index_set _asms, _nasms; + u_map var2expr; + for (unsigned i = 0; i < asms.size(); ++i) { + literal lit = get_literal(asms[i]); + _asms.insert(lit.index()); + _nasms.insert((~lit).index()); + var2expr.insert(lit.var(), asms[i]); + } + + m_antecedents.reset(); + literal_vector const& lits = assigned_literals(); + for (unsigned i = 0; i < lits.size(); ++i) { + literal lit = lits[i]; + index_set s; + if (_asms.contains(lit.index())) { + s.insert(lit.var()); + } + else { + justify(lit, s); + } + m_antecedents.insert(lit.var(), s); + if (_nasms.contains(lit.index())) { + expr_ref_vector core(m_manager); + index_set::iterator it = s.begin(), end = s.end(); + for (; it != end; ++it) { + core.push_back(var2expr[*it]); + } + core.push_back(var2expr[lit.var()]); + cores.push_back(core); + min_core_size = std::min(min_core_size, core.size()); + } + } + } + + void context::preferred_sat(literal_vector& lits) { + bool retry = true; + while (retry) { + retry = false; + for (unsigned i = 0; i < lits.size(); ++i) { + literal lit = lits[i]; + if (lit == null_literal || get_assignment(lit) != l_undef) { + continue; + } + push_scope(); + assign(lit, b_justification::mk_axiom(), true); + while (!propagate()) { + lits[i] = null_literal; + retry = true; + if (!resolve_conflict() || inconsistent()) { + SASSERT(inconsistent()); + return; + } + } + } + } + } + + void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) { + unsigned num_true = 0, num_false = 0, num_undef = 0; + for (unsigned i = 0; i < asms.size(); ++i) { + literal lit = get_literal(asms[i]); + if (get_assignment(lit) == l_false) { + ++num_false; + } + if (get_assignment(lit) == l_true) { + ++num_true; + } + if (get_assignment(lit) == l_undef) { + ++num_undef; + } + } + out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n"; + } + + lbool context::preferred_sat(expr_ref_vector const& asms, vector& cores) { + pop_to_base_lvl(); + cores.reset(); + setup_context(false); + internalize_assertions(); + if (m_asserted_formulas.inconsistent() || inconsistent()) { + return l_false; + } + scoped_mk_model smk(*this); + init_search(); + flet l(m_searching, true); + unsigned level = m_scope_lvl; + unsigned min_core_size = UINT_MAX; + lbool is_sat = l_true; + unsigned num_restarts = 0; + + while (true) { + if (m_manager.canceled()) { + is_sat = l_undef; + break; + } + literal_vector lits; + for (unsigned i = 0; i < asms.size(); ++i) { + lits.push_back(get_literal(asms[i])); + } + preferred_sat(lits); + if (inconsistent()) { + SASSERT(m_scope_lvl == level); + is_sat = l_false; + break; + } + extract_cores(asms, cores, min_core_size); + IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size);); + + if (min_core_size <= 10) { + is_sat = l_undef; + break; + } + + is_sat = bounded_search(); + if (!restart(is_sat, level)) { + break; + } + ++num_restarts; + if (num_restarts >= min_core_size) { + is_sat = l_undef; + while (num_restarts <= 10*min_core_size) { + is_sat = bounded_search(); + if (!restart(is_sat, level)) { + break; + } + ++num_restarts; + } + break; + } + } + end_search(); + + return check_finalize(is_sat); + } + struct neg_literal { unsigned negate(unsigned i) { return (~to_literal(i)).index(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6b3d92602..e6d4d0c07 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1111,6 +1111,8 @@ namespace smt { if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); + //return false; + theory_id t1 = r1->m_th_var_list.get_th_id(); if (t1 == null_theory_id) return false; return get_theory(t1)->use_diseqs(); @@ -3293,19 +3295,6 @@ namespace smt { m_num_conflicts_since_restart = 0; } - struct context::scoped_mk_model { - context & m_ctx; - scoped_mk_model(context & ctx):m_ctx(ctx) { - m_ctx.m_proto_model = 0; - m_ctx.m_model = 0; - } - ~scoped_mk_model() { - if (m_ctx.m_proto_model.get() != 0) { - m_ctx.m_model = m_ctx.m_proto_model->mk_model(); - m_ctx.m_proto_model = 0; // proto_model is not needed anymore. - } - } - }; lbool context::search() { #ifndef _EXTERNAL_RELEASE @@ -3333,79 +3322,10 @@ namespace smt { TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";); TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << ", num_assigned: " << m_assigned_literals.size() << "\n";); - - if (m_last_search_failure != OK) { - if (status != l_false) { - // build candidate model before returning - mk_proto_model(status); - // status = l_undef; - } + + if (!restart(status, curr_lvl)) { break; } - - bool force_restart = false; - - if (status == l_false) { - break; - } - else if (status == l_true) { - SASSERT(!inconsistent()); - mk_proto_model(l_true); - // possible outcomes DONE l_true, DONE l_undef, CONTINUE - quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); - if (cmr == quantifier_manager::SAT) { - // done - break; - } - if (cmr == quantifier_manager::UNKNOWN) { - IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";); - // giving up - m_last_search_failure = QUANTIFIERS; - status = l_undef; - break; - } - status = l_undef; - force_restart = true; - } - - SASSERT(status == l_undef); - inc_limits(); - if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { - SASSERT(!inconsistent()); - IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations - << " :decisions " << m_stats.m_num_decisions - << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; - if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { - verbose_stream() << " :restart-outer " << m_restart_outer_threshold; - } - if (m_fparams.m_restart_adaptive) { - verbose_stream() << " :agility " << m_agility; - } - verbose_stream() << ")" << std::endl; verbose_stream().flush();); - // execute the restart - m_stats.m_num_restarts++; - if (m_scope_lvl > curr_lvl) { - pop_scope(m_scope_lvl - curr_lvl); - SASSERT(at_search_level()); - } - ptr_vector::iterator it = m_theory_set.begin(); - ptr_vector::iterator end = m_theory_set.end(); - for (; it != end && !inconsistent(); ++it) - (*it)->restart_eh(); - TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); - if (!inconsistent()) { - m_qmanager->restart_eh(); - } - if (inconsistent()) { - VERIFY(!resolve_conflict()); - status = l_false; - break; - } - } - if (m_fparams.m_simplify_clauses) - simplify_clauses(); - if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART) - del_inactive_lemmas(); } TRACE("search_lite", tout << "status: " << status << "\n";); @@ -3419,6 +3339,80 @@ namespace smt { end_search(); return status; } + + bool context::restart(lbool& status, unsigned curr_lvl) { + + if (m_last_search_failure != OK) { + if (status != l_false) { + // build candidate model before returning + mk_proto_model(status); + // status = l_undef; + } + return false; + } + + if (status == l_false) { + return false; + } + if (status == l_true) { + SASSERT(!inconsistent()); + mk_proto_model(l_true); + // possible outcomes DONE l_true, DONE l_undef, CONTINUE + quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); + if (cmr == quantifier_manager::SAT) { + // done + status = l_true; + return false; + } + if (cmr == quantifier_manager::UNKNOWN) { + IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";); + // giving up + m_last_search_failure = QUANTIFIERS; + status = l_undef; + return false; + } + } + inc_limits(); + if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { + SASSERT(!inconsistent()); + IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations + << " :decisions " << m_stats.m_num_decisions + << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; + if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { + verbose_stream() << " :restart-outer " << m_restart_outer_threshold; + } + if (m_fparams.m_restart_adaptive) { + verbose_stream() << " :agility " << m_agility; + } + verbose_stream() << ")" << std::endl; verbose_stream().flush();); + // execute the restart + m_stats.m_num_restarts++; + if (m_scope_lvl > curr_lvl) { + pop_scope(m_scope_lvl - curr_lvl); + SASSERT(at_search_level()); + } + ptr_vector::iterator it = m_theory_set.begin(); + ptr_vector::iterator end = m_theory_set.end(); + for (; it != end && !inconsistent(); ++it) + (*it)->restart_eh(); + TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); + if (!inconsistent()) { + m_qmanager->restart_eh(); + } + if (inconsistent()) { + VERIFY(!resolve_conflict()); + status = l_false; + return false; + } + } + if (m_fparams.m_simplify_clauses) + simplify_clauses(); + if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART) + del_inactive_lemmas(); + + status = l_undef; + return true; + } void context::tick(unsigned & counter) const { counter++; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 21d628e1a..c63d0614d 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -200,7 +200,20 @@ namespace smt { model_ref m_model; std::string m_unknown; void mk_proto_model(lbool r); - struct scoped_mk_model; + struct scoped_mk_model { + context & m_ctx; + scoped_mk_model(context & ctx):m_ctx(ctx) { + m_ctx.m_proto_model = 0; + m_ctx.m_model = 0; + } + ~scoped_mk_model() { + if (m_ctx.m_proto_model.get() != 0) { + m_ctx.m_model = m_ctx.m_proto_model->mk_model(); + m_ctx.m_proto_model = 0; // proto_model is not needed anymore. + } + } + }; + // ----------------------------------- // @@ -234,7 +247,6 @@ namespace smt { return m_params; } - bool get_cancel_flag() { return !m_manager.limit().inc(); } region & get_region() { @@ -1056,6 +1068,8 @@ namespace smt { void inc_limits(); + bool restart(lbool& status, unsigned curr_lvl); + void tick(unsigned & counter) const; lbool bounded_search(); @@ -1367,6 +1381,13 @@ namespace smt { void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector const& conseq, expr_ref_vector const& unfixed); + void justify(literal lit, index_set& s); + + void extract_cores(expr_ref_vector const& asms, vector& cores, unsigned& min_core_size); + + void preferred_sat(literal_vector& literals); + + void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size); public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); @@ -1410,6 +1431,8 @@ namespace smt { lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + + lbool preferred_sat(expr_ref_vector const& asms, vector& cores); lbool setup_and_check(bool reset_cancel = true); diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 6b626c2de..5e3b091bc 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -322,6 +322,9 @@ namespace smt { bool context::check_th_diseq_propagation() const { TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";); int num = get_num_bool_vars(); + if (inconsistent()) { + return true; + } for (bool_var v = 0; v < num; v++) { if (has_enode(v)) { enode * n = bool_var2enode(v); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index df39b4186..9bdf962ec 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -115,6 +115,11 @@ namespace smt { return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } + lbool preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_kernel.preferred_sat(asms, cores); + } + + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_kernel.find_mutexes(vars, mutexes); } @@ -282,6 +287,10 @@ namespace smt { return m_imp->get_consequences(assumptions, vars, conseq, unfixed); } + lbool kernel::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return m_imp->preferred_sat(asms, cores); + } + lbool kernel::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_imp->find_mutexes(vars, mutexes); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index ea09081ec..264fae011 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -133,11 +133,16 @@ namespace smt { lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed); - /* + /** \brief find mutually exclusive variables. */ lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + /** + \brief Preferential SAT. + */ + lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + /** \brief Return the model associated with the last check command. */ diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index fd07188e5..b665c2a94 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -21,294 +21,351 @@ Notes: #include "smt_context.h" #include "ast_pp.h" #include "theory_wmaxsat.h" +#include "smt_justification.h" namespace smt { -theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc): - theory(m.mk_family_id("weighted_maxsat")), - m_mc(mc), - m_vars(m), - m_fmls(m), - m_zweights(m_mpz), - m_old_values(m_mpz), - m_zcost(m_mpz), - m_zmin_cost(m_mpz), - m_found_optimal(false), - m_propagate(false), - m_normalize(false), - m_den(1) -{} - -theory_wmaxsat::~theory_wmaxsat() { - m_old_values.reset(); -} - -/** - \brief return the complement of variables that are currently assigned. -*/ -void theory_wmaxsat::get_assignment(svector& result) { - result.reset(); + theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc): + theory(m.mk_family_id("weighted_maxsat")), + m_mc(mc), + m_vars(m), + m_fmls(m), + m_zweights(m_mpz), + m_old_values(m_mpz), + m_zcost(m_mpz), + m_zmin_cost(m_mpz), + m_found_optimal(false), + m_propagate(false), + m_normalize(false), + m_den(1) + {} - if (!m_found_optimal) { - for (unsigned i = 0; i < m_vars.size(); ++i) { - result.push_back(false); - } + theory_wmaxsat::~theory_wmaxsat() { + m_old_values.reset(); } - else { - std::sort(m_cost_save.begin(), m_cost_save.end()); - for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) { - if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) { + + /** + \brief return the complement of variables that are currently assigned. + */ + void theory_wmaxsat::get_assignment(svector& result) { + result.reset(); + + if (!m_found_optimal) { + for (unsigned i = 0; i < m_vars.size(); ++i) { result.push_back(false); - ++j; - } - else { - result.push_back(true); } } + else { + std::sort(m_cost_save.begin(), m_cost_save.end()); + for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) { + if (j < m_cost_save.size() && m_cost_save[j] == static_cast(i)) { + result.push_back(false); + ++j; + } + else { + result.push_back(true); + } + } + } + TRACE("opt", + tout << "cost save: "; + for (unsigned i = 0; i < m_cost_save.size(); ++i) { + tout << m_cost_save[i] << " "; + } + tout << "\nvars: "; + for (unsigned i = 0; i < m_vars.size(); ++i) { + tout << mk_pp(m_vars[i].get(), get_manager()) << " "; + } + tout << "\nassignment: "; + for (unsigned i = 0; i < result.size(); ++i) { + tout << result[i] << " "; + } + tout << "\n";); } - TRACE("opt", - tout << "cost save: "; - for (unsigned i = 0; i < m_cost_save.size(); ++i) { - tout << m_cost_save[i] << " "; - } - tout << "\nvars: "; - for (unsigned i = 0; i < m_vars.size(); ++i) { - tout << mk_pp(m_vars[i].get(), get_manager()) << " "; - } - tout << "\nassignment: "; - for (unsigned i = 0; i < result.size(); ++i) { - tout << result[i] << " "; - } - tout << "\n";); -} - -void theory_wmaxsat::init_search_eh() { - m_propagate = true; -} - -expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true) { - context & ctx = get_context(); - ast_manager& m = get_manager(); - app_ref var(m), wfml(m); - var = m.mk_fresh_const("w", m.mk_bool_sort()); - m_mc.insert(var->get_decl()); - wfml = m.mk_or(var, fml); - ctx.assert_expr(wfml); - m_rweights.push_back(w); - m_vars.push_back(var); - m_fmls.push_back(fml); - m_assigned.push_back(false); - if (!is_true) { - m_rmin_cost += w; + void theory_wmaxsat::init_search_eh() { + m_propagate = true; } - m_normalize = true; - return ctx.bool_var2expr(register_var(var, true)); -} - -bool_var theory_wmaxsat::register_var(app* var, bool attach) { - context & ctx = get_context(); - bool_var bv; - SASSERT(!ctx.e_internalized(var)); - enode* x = ctx.mk_enode(var, false, true, true); - if (ctx.b_internalized(var)) { - bv = ctx.get_bool_var(var); + + expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w) { + context & ctx = get_context(); + ast_manager& m = get_manager(); + app_ref var(m), wfml(m); + var = m.mk_fresh_const("w", m.mk_bool_sort()); + m_mc.insert(var->get_decl()); + wfml = m.mk_or(var, fml); + ctx.assert_expr(wfml); + m_rweights.push_back(w); + m_vars.push_back(var); + m_fmls.push_back(fml); + m_assigned.push_back(false); + m_enabled.push_back(true); + m_normalize = true; + bool_var bv = register_var(var, true); + TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n"; + tout << wfml << "\n";); + return var; } - else { - bv = ctx.mk_bool_var(var); - } - ctx.set_enode_flag(bv, true); - if (attach) { - ctx.set_var_theory(bv, get_id()); - theory_var v = mk_var(x); - ctx.attach_th_var(x, this, v); - m_bool2var.insert(bv, v); - SASSERT(v == static_cast(m_var2bool.size())); - m_var2bool.push_back(bv); - SASSERT(ctx.bool_var2enode(bv)); - } - return bv; -} -rational const& theory_wmaxsat::get_min_cost() { - unsynch_mpq_manager mgr; - scoped_mpq q(mgr); - mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); - m_rmin_cost = rational(q); - return m_rmin_cost; -} - -void theory_wmaxsat::assign_eh(bool_var v, bool is_true) { - TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";); - if (is_true) { - if (m_normalize) normalize(); + void theory_wmaxsat::disable_var(expr* var) { context& ctx = get_context(); - theory_var tv = m_bool2var[v]; - if (m_assigned[tv]) return; - scoped_mpz w(m_mpz); - w = m_zweights[tv]; - ctx.push_trail(numeral_trail(m_zcost, m_old_values)); - ctx.push_trail(push_back_vector >(m_costs)); - ctx.push_trail(value_trail(m_assigned[tv])); - m_zcost += w; - m_costs.push_back(tv); - m_assigned[tv] = true; - if (m_zcost > m_zmin_cost) { - block(); + SASSERT(ctx.b_internalized(var)); + bool_var bv = ctx.get_bool_var(var); + theory_var tv = m_bool2var[bv]; + m_enabled[tv] = false; + TRACE("opt", tout << "disable: v" << tv << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";); + } + + bool_var theory_wmaxsat::register_var(app* var, bool attach) { + context & ctx = get_context(); + bool_var bv; + SASSERT(!ctx.e_internalized(var)); + enode* x = ctx.mk_enode(var, false, true, true); + if (ctx.b_internalized(var)) { + bv = ctx.get_bool_var(var); } - } -} - -final_check_status theory_wmaxsat::final_check_eh() { - if (m_normalize) normalize(); - return FC_DONE; -} - - -void theory_wmaxsat::reset_eh() { - theory::reset_eh(); - reset_local(); -} - -void theory_wmaxsat::reset_local() { - m_vars.reset(); - m_fmls.reset(); - m_rweights.reset(); - m_rmin_cost.reset(); - m_rcost.reset(); - m_zweights.reset(); - m_zcost.reset(); - m_zmin_cost.reset(); - m_cost_save.reset(); - m_bool2var.reset(); - m_var2bool.reset(); - m_propagate = false; - m_found_optimal = false; - m_assigned.reset(); -} - - -void theory_wmaxsat::propagate() { - context& ctx = get_context(); - for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { - bool_var bv = m_var2bool[i]; - lbool asgn = ctx.get_assignment(bv); - if (asgn == l_true) { - assign_eh(bv, true); + else { + bv = ctx.mk_bool_var(var); } + ctx.set_enode_flag(bv, true); + if (attach) { + ctx.set_var_theory(bv, get_id()); + theory_var v = mk_var(x); + ctx.attach_th_var(x, this, v); + m_bool2var.insert(bv, v); + SASSERT(v == static_cast(m_var2bool.size())); + m_var2bool.push_back(bv); + SASSERT(ctx.bool_var2enode(bv)); + } + return bv; } - m_propagate = false; -} - -bool theory_wmaxsat::is_optimal() const { - return !m_found_optimal || m_zcost < m_zmin_cost; -} - -expr_ref theory_wmaxsat::mk_block() { - ++m_stats.m_num_blocks; - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { - weight += m_zweights[costs[i]]; - disj.push_back(m.mk_not(m_vars[costs[i]].get())); - } - if (is_optimal()) { + + rational theory_wmaxsat::get_cost() { unsynch_mpq_manager mgr; scoped_mpq q(mgr); - mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); - rational rw = rational(q); - m_zmin_cost = weight; - m_found_optimal = true; + mgr.set(q, m_zcost, m_den.to_mpq().numerator()); + return rational(q); + } + + void theory_wmaxsat::init_min_cost(rational const& r) { + m_rmin_cost = r; + m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator(); + } + + + void theory_wmaxsat::assign_eh(bool_var v, bool is_true) { + if (is_true) { + if (m_normalize) normalize(); + context& ctx = get_context(); + theory_var tv = m_bool2var[v]; + if (m_assigned[tv] || !m_enabled[tv]) return; + scoped_mpz w(m_mpz); + w = m_zweights[tv]; + ctx.push_trail(numeral_trail(m_zcost, m_old_values)); + ctx.push_trail(push_back_vector >(m_costs)); + ctx.push_trail(value_trail(m_assigned[tv])); + m_zcost += w; + TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";); + m_costs.push_back(tv); + m_assigned[tv] = true; + if (m_zcost >= m_zmin_cost) { + block(); + } + else { + m_can_propagate = true; + } + } + } + + final_check_status theory_wmaxsat::final_check_eh() { + if (m_normalize) normalize(); + // std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n"; + return FC_DONE; + } + + + void theory_wmaxsat::reset_eh() { + theory::reset_eh(); + reset_local(); + } + + void theory_wmaxsat::reset_local() { + m_vars.reset(); + m_fmls.reset(); + m_rweights.reset(); + m_rmin_cost.reset(); + m_zweights.reset(); + m_zcost.reset(); + m_zmin_cost.reset(); m_cost_save.reset(); - m_cost_save.append(m_costs); + m_bool2var.reset(); + m_var2bool.reset(); + m_propagate = false; + m_can_propagate = false; + m_found_optimal = false; + m_assigned.reset(); + m_enabled.reset(); + } + + + void theory_wmaxsat::propagate() { + context& ctx = get_context(); + for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { + bool_var bv = m_var2bool[i]; + lbool asgn = ctx.get_assignment(bv); + if (asgn == l_true) { + assign_eh(bv, true); + } + } + m_propagate = false; + //while (m_found_optimal && max_unassigned_is_blocked() && !ctx.inconsistent()) { } + + m_can_propagate = false; + } + + bool theory_wmaxsat::is_optimal() const { + return !m_found_optimal || m_zcost < m_zmin_cost; + } + + expr_ref theory_wmaxsat::mk_block() { + ++m_stats.m_num_blocks; + ast_manager& m = get_manager(); + expr_ref_vector disj(m); + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { + theory_var tv = costs[i]; + if (m_enabled[tv]) { + weight += m_zweights[tv]; + disj.push_back(m.mk_not(m_vars[tv].get())); + } + } + if (is_optimal()) { + m_found_optimal = true; + m_cost_save.reset(); + m_cost_save.append(m_costs); + TRACE("opt", + tout << "costs: "; + for (unsigned i = 0; i < m_costs.size(); ++i) { + tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; + } + tout << "\n"; + //get_context().display(tout); + ); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); TRACE("opt", - tout << "costs: "; - for (unsigned i = 0; i < m_costs.size(); ++i) { - tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; - } - tout << "\n"; - get_context().display(tout); - ); + tout << result << " weight: " << weight << "\n"; + tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); + return result; } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - TRACE("opt", - tout << result << " weight: " << weight << "\n"; - tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); - return result; -} -expr_ref theory_wmaxsat::mk_optimal_block(svector const& ws, rational const& weight) { - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - rational new_w = weight*m_den; - m_zmin_cost = new_w.to_mpq().numerator(); - m_cost_save.reset(); - for (unsigned i = 0; i < ws.size(); ++i) { - bool_var bv = ws[i]; - theory_var v = m_bool2var[bv]; - m_cost_save.push_back(v); - disj.push_back(m.mk_not(m_vars[v].get())); - } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - return result; -} + void theory_wmaxsat::restart_eh() {} -void theory_wmaxsat::block() { - if (m_vars.empty()) { - return; + void theory_wmaxsat::block() { + if (m_vars.empty()) { + return; + } + ++m_stats.m_num_blocks; + context& ctx = get_context(); + literal_vector lits; + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { + weight += m_zweights[costs[i]]; + lits.push_back(literal(m_var2bool[costs[i]])); + } + TRACE("opt", ctx.display_literals_verbose(tout, lits); tout << "\n";); + + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, 0, 0))); + } + + bool theory_wmaxsat::max_unassigned_is_blocked() { + context& ctx = get_context(); + unsigned max_unassigned = m_max_unassigned_index; + if (max_unassigned < m_sorted_vars.size() && + m_zcost + m_zweights[m_sorted_vars[max_unassigned]] < m_zmin_cost) { + return false; + } + // update value of max-unassigned + while (max_unassigned < m_sorted_vars.size() && + ctx.get_assignment(m_var2bool[m_sorted_vars[max_unassigned]]) != l_undef) { + ++max_unassigned; + } + // + if (max_unassigned > m_max_unassigned_index) { + ctx.push_trail(value_trail(m_max_unassigned_index)); + m_max_unassigned_index = max_unassigned; + } + if (max_unassigned < m_sorted_vars.size() && + m_zcost + m_zweights[m_sorted_vars[max_unassigned]] >= m_zmin_cost) { + theory_var tv = m_sorted_vars[max_unassigned]; + propagate(m_var2bool[tv]); + m_max_unassigned_index++; + return true; + } + + return false; } - ++m_stats.m_num_blocks; - context& ctx = get_context(); - literal_vector lits; - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { - weight += m_zweights[costs[i]]; - lits.push_back(~literal(m_var2bool[costs[i]])); - } - TRACE("opt", - ast_manager& m = get_manager(); - tout << "block: "; - for (unsigned i = 0; i < lits.size(); ++i) { - expr_ref tmp(m); - ctx.literal2expr(lits[i], tmp); - tout << tmp << " "; - } - tout << "\n"; - ); - - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); -} + void theory_wmaxsat::propagate(bool_var v) { + ++m_stats.m_num_propagations; + context& ctx = get_context(); + literal_vector lits; + literal lit(v, true); + + SASSERT(ctx.get_assignment(lit) == l_undef); + + for (unsigned i = 0; i < m_costs.size(); ++i) { + bool_var w = m_var2bool[m_costs[i]]; + lits.push_back(literal(w)); + } + TRACE("opt", + ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); + ctx.display_literal_verbose(tout << " --> ", lit);); + + region& r = ctx.get_region(); + ctx.assign(lit, ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), r, lits.size(), lits.c_ptr(), 0, 0, lit, 0, 0))); + } -void theory_wmaxsat::normalize() { - m_den = rational::one(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - m_den = lcm(m_den, denominator(m_rweights[i])); + void theory_wmaxsat::normalize() { + m_den = rational::one(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + if (m_enabled[i]) { + m_den = lcm(m_den, denominator(m_rweights[i])); + } + } + m_den = lcm(m_den, denominator(m_rmin_cost)); + SASSERT(!m_den.is_zero()); + m_zweights.reset(); + m_sorted_vars.reset(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + rational r = m_rweights[i]*m_den; + SASSERT(r.is_int()); + mpq const& q = r.to_mpq(); + m_zweights.push_back(q.numerator()); + m_sorted_vars.push_back(i); + } + compare_cost compare_cost(*this); + std::sort(m_sorted_vars.begin(), m_sorted_vars.end(), compare_cost); + m_max_unassigned_index = 0; + + m_zcost.reset(); + rational r = m_rmin_cost * m_den; + m_zmin_cost = r.to_mpq().numerator(); + m_normalize = false; } - m_den = lcm(m_den, denominator(m_rmin_cost)); - SASSERT(!m_den.is_zero()); - m_zweights.reset(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - rational r = m_rweights[i]*m_den; - SASSERT(r.is_int()); - mpq const& q = r.to_mpq(); - m_zweights.push_back(q.numerator()); - } - rational r = m_rcost* m_den; - m_zcost = r.to_mpq().numerator(); - r = m_rmin_cost * m_den; - m_zmin_cost = r.to_mpq().numerator(); - m_normalize = false; -} }; diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index 0804c4b68..0f711b9f8 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -28,6 +28,7 @@ namespace smt { class theory_wmaxsat : public theory { struct stats { unsigned m_num_blocks; + unsigned m_num_propagations; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; @@ -39,27 +40,31 @@ namespace smt { scoped_mpz_vector m_zweights; scoped_mpz_vector m_old_values; svector m_costs; // set of asserted theory variables + unsigned m_max_unassigned_index; // index of literal that is not yet assigned and has maximal weight. + svector m_sorted_vars; // set of all theory variables, sorted by cost svector m_cost_save; // set of asserted theory variables - rational m_rcost; // current sum of asserted costs rational m_rmin_cost; // current maximal cost assignment. scoped_mpz m_zcost; // current sum of asserted costs scoped_mpz m_zmin_cost; // current maximal cost assignment. bool m_found_optimal; u_map m_bool2var; // bool_var -> theory_var svector m_var2bool; // theory_var -> bool_var - bool m_propagate; + bool m_propagate; + bool m_can_propagate; bool m_normalize; rational m_den; // lcm of denominators for rational weights. - svector m_assigned; + svector m_assigned, m_enabled; stats m_stats; public: theory_wmaxsat(ast_manager& m, filter_model_converter& mc); virtual ~theory_wmaxsat(); void get_assignment(svector& result); - virtual void init_search_eh(); - expr* assert_weighted(expr* fml, rational const& w, bool is_true); + expr* assert_weighted(expr* fml, rational const& w); + void disable_var(expr* var); bool_var register_var(app* var, bool attach); - rational const& get_min_cost(); + rational get_cost(); + void init_min_cost(rational const& r); + class numeral_trail : public trail { typedef scoped_mpz T; T & m_value; @@ -79,6 +84,8 @@ namespace smt { m_old_values.shrink(m_old_values.size() - 1); } }; + + virtual void init_search_eh(); virtual void assign_eh(bool_var v, bool is_true); virtual final_check_status final_check_eh(); virtual bool use_diseqs() const { @@ -95,23 +102,30 @@ namespace smt { virtual void new_eq_eh(theory_var v1, theory_var v2) { } virtual void new_diseq_eh(theory_var v1, theory_var v2) { } virtual void display(std::ostream& out) const {} + virtual void restart_eh(); virtual void collect_statistics(::statistics & st) const { st.update("wmaxsat num blocks", m_stats.m_num_blocks); + st.update("wmaxsat num props", m_stats.m_num_propagations); } virtual bool can_propagate() { - return m_propagate; + return m_propagate || m_can_propagate; } virtual void propagate(); + bool is_optimal() const; expr_ref mk_block(); - expr_ref mk_optimal_block(svector const& ws, rational const& weight); + + private: void block(); + void propagate(bool_var v); void normalize(); + + bool max_unassigned_is_blocked(); class compare_cost { theory_wmaxsat& m_th; diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 441ece429..9163cfeda 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -154,6 +154,10 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector& return l_true; } +lbool solver::preferred_sat(expr_ref_vector const& asms, vector& cores) { + return check_sat(0, 0); +} + bool solver::is_literal(ast_manager& m, expr* e) { return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 15932fd5d..d5d9ccfd5 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -151,9 +151,9 @@ public: /** \brief under assumptions, asms, retrieve set of consequences that - fix values for expressions that can be built from vars. - The consequences are clauses whose first literal constrain one of the - functions from vars and the other literals are negations of literals from asms. + fix values for expressions that can be built from vars. + The consequences are clauses whose first literal constrain one of the + functions from vars and the other literals are negations of literals from asms. */ virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); @@ -166,6 +166,12 @@ public: virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes); + /** + \brief Preferential SAT. Prefer assumptions to be true, produce cores that witness cases when not all assumptions can be met. + by default, preferred sat ignores the assumptions. + */ + virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + /** \brief Display the content of this solver. */ From 42b26c63e52ae05338e2638d525f62c4badf826d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 1 Dec 2016 14:01:20 +0000 Subject: [PATCH 03/42] make a few functions static --- src/smt/smt_context_stat.cpp | 12 ++++++------ src/smt/smt_internalizer.cpp | 4 ++-- src/smt/smt_model_checker.cpp | 3 --- src/smt/smt_setup.cpp | 8 ++++---- src/tactic/aig/aig.cpp | 24 ++++++++++++------------ 5 files changed, 24 insertions(+), 27 deletions(-) diff --git a/src/smt/smt_context_stat.cpp b/src/smt/smt_context_stat.cpp index 5e82923f0..3838a88b5 100644 --- a/src/smt/smt_context_stat.cpp +++ b/src/smt/smt_context_stat.cpp @@ -32,7 +32,7 @@ namespace smt { return static_cast(acc / m_lemmas.size()); } - void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) { + static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) { unsigned num_lits = cls->get_num_literals(); for (unsigned i = 0; i < num_lits; i++) { literal l = cls->get_literal(i); @@ -40,7 +40,7 @@ namespace smt { } } - void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) { + static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) { clause_vector::const_iterator it = v.begin(); clause_vector::const_iterator end = v.end(); for (; it != end; ++it) @@ -79,7 +79,7 @@ namespace smt { out << (m_assigned_literals.size() - n) << "]"; } - void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) { + static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) { unsigned num_lits = cls->get_num_literals(); for (unsigned i = 0; i < num_lits; i++) { literal l = cls->get_literal(i); @@ -87,7 +87,7 @@ namespace smt { } } - void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) { + static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) { clause_vector::const_iterator it = v.begin(); clause_vector::const_iterator end = v.end(); for (; it != end; ++it) @@ -114,7 +114,7 @@ namespace smt { out << "\n"; } - void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) { + static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) { unsigned num_lits = cls->get_num_literals(); bool_var min_var = cls->get_literal(0).var(); for (unsigned i = 1; i < num_lits; i++) { @@ -125,7 +125,7 @@ namespace smt { var2num_min_occs[min_var]++; } - void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) { + static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) { clause_vector::const_iterator it = v.begin(); clause_vector::const_iterator end = v.end(); for (; it != end; ++it) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 8028feae6..ad1e55ba6 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -335,7 +335,7 @@ namespace smt { } } - bool find_arg(app * n, expr * t, expr * & other) { + static bool find_arg(app * n, expr * t, expr * & other) { SASSERT(n->get_num_args() == 2); if (n->get_arg(0) == t) { other = n->get_arg(1); @@ -348,7 +348,7 @@ namespace smt { return false; } - bool check_args(app * n, expr * t1, expr * t2) { + static bool check_args(app * n, expr * t1, expr * t2) { SASSERT(n->get_num_args() == 2); return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index a7f415aad..5329cd80f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -363,9 +363,6 @@ namespace smt { } } - struct scoped_set_relevancy { - }; - bool model_checker::check(proto_model * md, obj_map const & root2value) { SASSERT(md != 0); m_root2value = &root2value; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 9f7656471..ee92c4f61 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -188,7 +188,7 @@ namespace smt { } } - void check_no_arithmetic(static_features const & st, char const * logic) { + static void check_no_arithmetic(static_features const & st, char const * logic) { if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) throw default_exception("Benchmark constains arithmetic, but specified loging does not support it."); } @@ -231,21 +231,21 @@ namespace smt { (st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9; } - bool is_in_diff_logic(static_features const & st) { + static bool is_in_diff_logic(static_features const & st) { return st.m_num_arith_eqs == st.m_num_diff_eqs && st.m_num_arith_terms == st.m_num_diff_terms && st.m_num_arith_ineqs == st.m_num_diff_ineqs; } - bool is_diff_logic(static_features const & st) { + static bool is_diff_logic(static_features const & st) { return is_in_diff_logic(st) && (st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0) ; } - void check_no_uninterpreted_functions(static_features const & st, char const * logic) { + static void check_no_uninterpreted_functions(static_features const & st, char const * logic) { if (st.m_num_uninterpreted_functions != 0) throw default_exception("Benchmark contains uninterpreted function symbols, but specified logic does not support them."); } diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index b84ae68f0..1312b0dea 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -53,26 +53,26 @@ struct aig { aig() {} }; -inline bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; } -inline bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; } -inline bool is_var(aig * n) { return n->m_children[0].is_null(); } -inline bool is_var(aig_lit const & n) { return is_var(n.ptr()); } -inline unsigned id(aig_lit const & n) { return n.ptr()->m_id; } -inline unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; } -inline aig_lit left(aig * n) { return n->m_children[0]; } -inline aig_lit right(aig * n) { return n->m_children[1]; } -inline aig_lit left(aig_lit const & n) { return left(n.ptr()); } -inline aig_lit right(aig_lit const & n) { return right(n.ptr()); } +static bool is_true(aig_lit const & r) { return !r.is_inverted() && r.ptr_non_inverted()->m_id == 0; } +static bool is_false(aig_lit const & r) { return r.is_inverted() && r.ptr()->m_id == 0; } +static bool is_var(aig * n) { return n->m_children[0].is_null(); } +static bool is_var(aig_lit const & n) { return is_var(n.ptr()); } +static unsigned id(aig_lit const & n) { return n.ptr()->m_id; } +static unsigned ref_count(aig_lit const & n) { return n.ptr()->m_ref_count; } +static aig_lit left(aig * n) { return n->m_children[0]; } +static aig_lit right(aig * n) { return n->m_children[1]; } +static aig_lit left(aig_lit const & n) { return left(n.ptr()); } +static aig_lit right(aig_lit const & n) { return right(n.ptr()); } inline unsigned to_idx(aig * p) { SASSERT(!is_var(p)); return p->m_id - FIRST_NODE_ID; } -void unmark(unsigned sz, aig_lit const * ns) { +static void unmark(unsigned sz, aig_lit const * ns) { for (unsigned i = 0; i < sz; i++) { ns[i].ptr()->m_mark = false; } } -void unmark(unsigned sz, aig * const * ns) { +static void unmark(unsigned sz, aig * const * ns) { for (unsigned i = 0; i < sz; i++) { ns[i]->m_mark = false; } From e697d3e8109e8c614412d137d9e1da83374beed7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 1 Dec 2016 14:10:31 +0000 Subject: [PATCH 04/42] remove 2 outdated comments --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index e8d8c4e4b..68f2a2b8e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -66,9 +66,6 @@ struct blaster_cfg { void mk_nor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_nor(a, b, r); } }; -// CMW: GCC/LLVM do not like this definition because a symbol of the same name exists in assert_set_bit_blaster.o -// template class bit_blaster_tpl; - class blaster : public bit_blaster_tpl { bool_rewriter m_rewriter; bv_util m_util; @@ -625,9 +622,6 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } }; -// CMW: GCC/LLVM do not like this definition because a symbol of the same name exists in assert_set_bit_blaster.o -// template class rewriter_tpl; - struct bit_blaster_rewriter::imp : public rewriter_tpl { blaster m_blaster; blaster_rewriter_cfg m_cfg; From dedae29300ccd8a33f7c1c7d7dd6a17ca2569d09 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 1 Dec 2016 17:37:07 +0000 Subject: [PATCH 05/42] add a few more statics to avoid symbol clashes --- src/tactic/sls/sls_tactic.cpp | 4 ++-- src/tactic/smtlogics/qfbv_tactic.cpp | 4 ++-- src/tactic/smtlogics/qfnia_tactic.cpp | 6 +++--- src/tactic/ufbv/ufbv_tactic.cpp | 4 ++-- src/tactic/ufbv/ufbv_tactic.h | 2 -- 5 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 4e49e0d76..f4ef300e4 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -94,13 +94,13 @@ public: }; -tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) { +static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) { return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported. clean(alloc(sls_tactic, m, p))); } -tactic * mk_preamble(ast_manager & m, params_ref const & p) { +static tactic * mk_preamble(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); // main_p.set_bool("pull_cheap_ite", true); diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 7cc875fba..918e0fc6d 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -32,7 +32,7 @@ Notes: #define MEMLIMIT 300 -tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { +static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { params_ref solve_eq_p; // conservative guassian elimination. @@ -80,7 +80,7 @@ static tactic * main_p(tactic* t) { } -tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { +static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 950291221..5a71281fb 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -29,7 +29,7 @@ Notes: #include"ctx_simplify_tactic.h" #include"cofactor_term_ite_tactic.h" -tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { +static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { params_ref p = p_ref; p.set_bool("flat", false); p.set_bool("hi_div0", true); @@ -51,7 +51,7 @@ tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { return r; } -tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { +static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { params_ref pull_ite_p = p_ref; pull_ite_p.set_bool("pull_cheap_ite", true); pull_ite_p.set_bool("local_ctx", true); @@ -77,7 +77,7 @@ tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) { using_params(mk_simplify_tactic(m), simp_p)); } -tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { +static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { params_ref nia2sat_p = p; nia2sat_p.set_uint("nla2bv_max_bv_size", 64); diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 7a185c854..19d41be68 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -31,11 +31,11 @@ Notes: #include"ufbv_tactic.h" -tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { +static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p))); } -tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { +static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { params_ref no_elim_and(p); no_elim_and.set_bool("elim_and", false); diff --git a/src/tactic/ufbv/ufbv_tactic.h b/src/tactic/ufbv/ufbv_tactic.h index 2d5454de5..300fdd84a 100644 --- a/src/tactic/ufbv/ufbv_tactic.h +++ b/src/tactic/ufbv/ufbv_tactic.h @@ -23,8 +23,6 @@ Notes: class ast_manager; class tactic; -tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref()); - tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); /* From f1a704484b56555311b52dad2ab4146a5577f257 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 1 Dec 2016 23:16:15 +0000 Subject: [PATCH 06/42] Re-added context creation locks in the Java API. Relates to #819. --- src/api/java/Context.java | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b7656c5da..d50968a32 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -31,13 +31,17 @@ public class Context implements AutoCloseable { static final Object creation_lock = new Object(); public Context () { - m_ctx = Native.mkContextRc(0); - init(); + synchronized (creation_lock) { + m_ctx = Native.mkContextRc(0); + init(); + } } protected Context (long m_ctx) { - this.m_ctx = m_ctx; - init(); + synchronized (creation_lock) { + this.m_ctx = m_ctx; + init(); + } } @@ -59,13 +63,15 @@ public class Context implements AutoCloseable { * module parameters. For this purpose we should now use {@code Global.setParameter} **/ public Context(Map settings) { - long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) { - Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + synchronized (creation_lock) { + long cfg = Native.mkConfig(); + for (Map.Entry kv : settings.entrySet()) { + Native.setParamValue(cfg, kv.getKey(), kv.getValue()); + } + m_ctx = Native.mkContextRc(cfg); + Native.delConfig(cfg); + init(); } - m_ctx = Native.mkContextRc(cfg); - Native.delConfig(cfg); - init(); } private void init() { @@ -4037,7 +4043,9 @@ public class Context implements AutoCloseable { m_intSort = null; m_realSort = null; m_stringSort = null; - - Native.delContext(m_ctx); + + synchronized (creation_lock) { + Native.delContext(m_ctx); + } } } From dc0d29a00c51bcdd4f1d6158863f67a208a37011 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 8 Dec 2016 16:14:54 +0000 Subject: [PATCH 07/42] Bugfix for model construction. Fixes #828. --- src/model/model_core.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index bef2e6494..6b8ff8d63 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -93,6 +93,7 @@ void model_core::unregister_decl(func_decl * d) { m_manager.dec_ref(ec->get_data().m_key); m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); + m_const_decls.erase(d); return; } @@ -101,5 +102,6 @@ void model_core::unregister_decl(func_decl * d) { m_manager.dec_ref(ef->get_data().m_key); dealloc(ef->get_data().m_value); m_finterp.remove(d); + m_func_decls.erase(d); } } \ No newline at end of file From feb801564ba6a9a72259f60f854081333e3eda44 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2016 18:28:27 +0100 Subject: [PATCH 08/42] adding range to C API. Issue #831 Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 2 +- src/api/c++/z3++.h | 4 ++++ src/api/z3_api.h | 8 ++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 5704ffdb0..0fde6303a 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -145,7 +145,7 @@ extern "C" { MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP); - + MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP); }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 2a9c771a1..14702a4ea 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -934,6 +934,8 @@ namespace z3 { check_error(); return expr(ctx(), r); } + friend expr range(expr const& lo, expr const& hi); + @@ -1225,6 +1227,8 @@ namespace z3 { inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); } + inline expr range(expr const& lo, expr const& hi) { check_context(lo, hi); Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); lo.check_error(); return expr(lo.ctx(), r); } + diff --git a/src/api/z3_api.h b/src/api/z3_api.h index c7749ebef..d8570b852 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3367,6 +3367,14 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Create the range regular expression over two sequences of length 1. + + def_API('Z3_mk_re_range' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); + /*@}*/ From 4e25bffab6318b3f5aa0643e9551bc8b740e8bbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Dec 2016 18:33:02 +0100 Subject: [PATCH 09/42] add range constructor to .NET API Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index c3c33a41e..421c81fae 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2609,6 +2609,19 @@ namespace Microsoft.Z3 CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + + + /// + /// Create a range expression. + /// + public ReExpr MkRange(SeqExpr lo, SeqExpr hi) + { + Contract.Requires(lo != null); + Contract.Requires(hi != null); + Contract.Ensures(Contract.Result() != null); + CheckContextMatch(lo, hi); + return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); + } #endregion From a82b5e21fe98817604f6bda5dfd016fde972c05a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 06:11:36 +0100 Subject: [PATCH 10/42] add regular expression operations to C and C++ API Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 36 +++++++++++++++++++++++-------- src/api/c++/z3++.h | 48 +++++++++++++++++++++++++++++++++++------ src/api/z3_api.h | 52 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 121 insertions(+), 15 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 0fde6303a..e80d98553 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -116,15 +116,18 @@ extern "C" { Z3_CATCH_RETURN(""); } - Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq) { - Z3_TRY; - LOG_Z3_mk_seq_empty(c, seq); - RESET_ERROR_CODE(); - app* a = mk_c(c)->sutil().str.mk_empty(to_sort(seq)); - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - Z3_CATCH_RETURN(0); - } +#define MK_SORTED(NAME, FN ) \ + Z3_ast Z3_API NAME(Z3_context c, Z3_sort s) { \ + Z3_TRY; \ + LOG_ ## NAME(c, s); \ + RESET_ERROR_CODE(); \ + app* a = FN(to_sort(s)); \ + mk_c(c)->save_ast_trail(a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(0); \ + } + + MK_SORTED(Z3_mk_seq_empty, mk_c(c)->sutil().str.mk_empty); MK_UNARY(Z3_mk_seq_unit, mk_c(c)->get_seq_fid(), OP_SEQ_UNIT, SKIP); MK_NARY(Z3_mk_seq_concat, mk_c(c)->get_seq_fid(), OP_SEQ_CONCAT, SKIP); @@ -139,13 +142,28 @@ extern "C" { MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP); MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP); + Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { + Z3_TRY; + LOG_Z3_mk_re_loop(c, r, lo, hi); + RESET_ERROR_CODE(); + app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP); MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); + MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); + MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP); MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP); + MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty); + MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full); + + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 14702a4ea..f8c1c57dc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -934,9 +934,20 @@ namespace z3 { check_error(); return expr(ctx(), r); } - friend expr range(expr const& lo, expr const& hi); - - + friend expr range(expr const& lo, expr const& hi); + /** + \brief create a looping regular expression. + */ + expr loop(unsigned lo) { + Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0); + check_error(); + return expr(ctx(), r); + } + expr loop(unsigned lo, unsigned hi) { + Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi); + check_error(); + return expr(ctx(), r); + } /** @@ -1227,9 +1238,6 @@ namespace z3 { inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); } - inline expr range(expr const& lo, expr const& hi) { check_context(lo, hi); Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); lo.check_error(); return expr(lo.ctx(), r); } - - /** @@ -2465,6 +2473,34 @@ namespace z3 { re.check_error(); return expr(re.ctx(), r); } + inline expr re_empty(sort const& s) { + Z3_ast r = Z3_mk_re_empty(s.ctx(), s); + s.check_error(); + return expr(s.ctx(), r); + } + inline expr re_full(sort const& s) { + Z3_ast r = Z3_mk_re_full(s.ctx(), s); + s.check_error(); + return expr(s.ctx(), r); + } + inline expr re_intersect(expr_vector const& args) { + assert(args.size() > 0); + context& ctx = args[0].ctx(); + array _args(args); + Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr()); + ctx.check_error(); + return expr(ctx, r); + } + inline expr range(expr const& lo, expr const& hi) { + check_context(lo, hi); + Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); + lo.check_error(); + return expr(lo.ctx(), r); + } + + + + inline expr interpolant(expr const& a) { return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a)); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d8570b852..356f933d4 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1154,6 +1154,12 @@ typedef enum { Z3_OP_RE_OPTION, Z3_OP_RE_CONCAT, Z3_OP_RE_UNION, + Z3_OP_RE_RANGE, + Z3_OP_RE_LOOP, + Z3_OP_RE_INTERSECT, + Z3_OP_RE_EMPTY_SET, + Z3_OP_RE_FULL_SET, + Z3_OP_RE_COMPLEMENT, // Auxiliary Z3_OP_LABEL = 0x700, @@ -3375,6 +3381,52 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); + /** + \brief Create a regular expression loop. The supplied regular expression \c r is repated + between \c lo and \c hi times. The \c lo should be below \c hi with one exection: when + supplying the value \c hi as 0, the meaning is to repeat the argument \c r at least + \c lo number of times, and with an unbounded upper bound. + + def_API('Z3_mk_re_loop', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in(UINT))) + */ + Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi); + + /** + \brief Create the intersection of the regular languages. + + \pre n > 0 + + def_API('Z3_mk_re_intersect' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + */ + Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]); + + /** + \brief Create the complement of the regular language \c re. + + def_API('Z3_mk_re_complement' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re); + + /** + \brief Create an empty regular expression of sort \c re. + + \pre re is a regular expression sort. + + def_API('Z3_mk_re_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re); + + + /** + \brief Create an universal regular expression of sort \c re. + + \pre re is a regular expression sort. + + def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); + + /*@}*/ From 0473d2ef56c230f52d573df67027dcd7cf654c9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 06:17:13 +0100 Subject: [PATCH 11/42] add regular expression features to C# API Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 43 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 421c81fae..494b29a00 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2564,6 +2564,16 @@ namespace Microsoft.Z3 return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject)); } + /// + /// Take the bounded Kleene star of a regular expression. + /// + public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0) + { + Contract.Requires(re != null); + Contract.Ensures(Contract.Result() != null); + return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi)); + } + /// /// Take the Kleene plus of a regular expression. /// @@ -2610,6 +2620,39 @@ namespace Microsoft.Z3 return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + /// + /// Create the intersection of regular languages. + /// + public ReExpr MkIntersect(params ReExpr[] t) + { + Contract.Requires(t != null); + Contract.Requires(Contract.ForAll(t, a => a != null)); + Contract.Ensures(Contract.Result() != null); + + CheckContextMatch(t); + return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + } + + /// + /// Create the empty regular expression. + /// + public ReExpr MkEmptyRe(Sort s) + { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result() != null); + return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject)); + } + + /// + /// Create the full regular expression. + /// + public ReExpr MkFullRe(Sort s) + { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result() != null); + return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject)); + } + /// /// Create a range expression. From 976fadf7714f6a35528e8b0fbd0d4910e22324b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 06:21:57 +0100 Subject: [PATCH 12/42] add missing complement Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 24 ++++++++---------------- src/api/dotnet/Context.cs | 14 ++++++++++++-- 2 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f8c1c57dc..86dc77ad5 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2448,30 +2448,19 @@ namespace z3 { return expr(s.ctx(), r); } inline expr to_re(expr const& s) { - Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s); - s.check_error(); - return expr(s.ctx(), r); + MK_EXPR1(Z3_mk_seq_to_re, s); } inline expr in_re(expr const& s, expr const& re) { - check_context(s, re); - Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re); - s.check_error(); - return expr(s.ctx(), r); + MK_EXPR2(Z3_mk_seq_in_re, s, re); } inline expr plus(expr const& re) { - Z3_ast r = Z3_mk_re_plus(re.ctx(), re); - re.check_error(); - return expr(re.ctx(), r); + MK_EXPR1(Z3_mk_re_plus, re); } inline expr option(expr const& re) { - Z3_ast r = Z3_mk_re_option(re.ctx(), re); - re.check_error(); - return expr(re.ctx(), r); + MK_EXPR1(Z3_mk_re_option, re); } inline expr star(expr const& re) { - Z3_ast r = Z3_mk_re_star(re.ctx(), re); - re.check_error(); - return expr(re.ctx(), r); + MK_EXPR1(Z3_mk_re_star, re); } inline expr re_empty(sort const& s) { Z3_ast r = Z3_mk_re_empty(s.ctx(), s); @@ -2491,6 +2480,9 @@ namespace z3 { ctx.check_error(); return expr(ctx, r); } + inline expr re_complement(expr const& a) { + MK_EXPR1(Z3_mk_re_complement, a); + } inline expr range(expr const& lo, expr const& hi) { check_context(lo, hi); Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 494b29a00..f12ad58ea 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2577,7 +2577,7 @@ namespace Microsoft.Z3 /// /// Take the Kleene plus of a regular expression. /// - public ReExpr MPlus(ReExpr re) + public ReExpr MkPlus(ReExpr re) { Contract.Requires(re != null); Contract.Ensures(Contract.Result() != null); @@ -2587,13 +2587,23 @@ namespace Microsoft.Z3 /// /// Create the optional regular expression. /// - public ReExpr MOption(ReExpr re) + public ReExpr MkOption(ReExpr re) { Contract.Requires(re != null); Contract.Ensures(Contract.Result() != null); return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); } + /// + /// Create the complement regular expression. + /// + public ReExpr MkComplement(ReExpr re) + { + Contract.Requires(re != null); + Contract.Ensures(Contract.Result() != null); + return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject)); + } + /// /// Create the concatenation of regular languages. /// From 8e6600c6bedaffc6fd866dd6a473665c4bf6cc90 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 09:09:03 +0100 Subject: [PATCH 13/42] add python API for newly exposed regex constructors Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 44 ++++++++++++++++++++++++++++--- src/ast/rewriter/seq_rewriter.cpp | 6 ++--- src/ast/seq_decl_plugin.cpp | 6 ++--- 3 files changed, 47 insertions(+), 9 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 478ee0ce3..22b2f60e6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -9384,6 +9384,7 @@ class SeqSortRef(SortRef): False """ return Z3_is_string_sort(self.ctx_ref(), self.ast) + def StringSort(ctx=None): """Create a string sort @@ -9507,8 +9508,29 @@ def Empty(s): >>> e3 = Empty(SeqSort(IntSort())) >>> print(e3) seq.empty + >>> e4 = Empty(ReSort(SeqSort(IntSort()))) + >>> print(e4) + re.empty """ - return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) + if isinstance(s, SeqSortRef): + return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) + if isinstance(s, ReSortRef): + return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx) + raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") + +def Full(s): + """Create the regular expression that accepts the universal langauge + >>> e = Full(ReSort(SeqSort(IntSort()))) + >>> print(e) + re.all + >>> e1 = Full(ReSort(StringSort())) + >>> print(e1) + re.allchar + """ + if isinstance(s, ReSortRef): + return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) + raise Z3Exception("Non-sequence, non-regular expression sort passed to Full") + def Unit(a): """Create a singleton sequence""" @@ -9624,10 +9646,10 @@ class ReSortRef(SortRef): def ReSort(s): if is_ast(s): - return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.as_ast()), ctx) + return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx) if s is None or isinstance(s, Context): ctx = _get_ctx(s) - return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), ctx) + return ReSortRef(Z3_mk_re_sort(ctx.ref(), Z3_mk_string_sort(ctx.ref())), s.ctx) raise Z3Exception("Regular expression sort constructor expects either a string or a context or no argument") @@ -9698,6 +9720,10 @@ def Option(re): """ return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) +def Complement(re): + """Create the complement regular expression.""" + return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx) + def Star(re): """Create the regular expression accepting zero or more repetitions of argument. >>> re = Star(Re("a")) @@ -9709,3 +9735,15 @@ def Star(re): True """ return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) + +def Loop(re, lo, hi=0): + """Create the regular expression accepting between a lower and upper bound repetitions + >>> re = Loop(Re("a"), 1, 3) + >>> print(simplify(InRe("aa", re))) + True + >>> print(simplify(InRe("aaaa", re))) + False + >>> print(simplify(InRe("", re))) + False + """ + return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 80fee36d4..cc948de9a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -243,9 +243,9 @@ eautomaton* re2automaton::re2aut(expr* e) { TRACE("seq", tout << "Range expression is not handled: " << mk_pp(e, m) << "\n";); } } - else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) { - return m_sa->mk_complement(*a); - } + else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) { + return m_sa->mk_complement(*a); + } else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) { scoped_ptr eps = eautomaton::mk_epsilon(sm); b = eautomaton::mk_epsilon(sm); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index e9d87b90b..c645aa1a7 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -601,7 +601,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k)); } - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k)); case _OP_REGEXP_EMPTY: @@ -617,7 +617,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k)); } - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k)); case OP_RE_LOOP: switch (arity) { @@ -861,7 +861,7 @@ app* seq_util::re::mk_full(sort* s) { return m.mk_app(m_fid, OP_RE_FULL_SET, 0, 0, 0, 0, s); } -app* seq_util::re::mk_empty(sort* s) { +app* seq_util::re::mk_empty(sort* s) { return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, 0, 0, 0, s); } From 99b7c26e9f4b3e9dd6d9ccbb5cde385dce594c26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 13:05:02 +0100 Subject: [PATCH 14/42] exposing regular expression features to address issue #831 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index eda6831b5..efa3ec098 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1128,6 +1128,10 @@ extern "C" { case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION; case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT; case Z3_OP_RE_UNION: return Z3_OP_RE_UNION; + case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT; + case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP; + case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET; + case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET; default: return Z3_OP_INTERNAL; } From 0ab2067b69d876914a79ae7467db41a698f9a3ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 13:15:40 +0100 Subject: [PATCH 15/42] produce error message for cores with optimization. Issue #825 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 5 +++++ src/opt/opt_context.h | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 624671e2b..b95bb62e8 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -169,6 +169,11 @@ namespace opt { r.append(m_labels); } + void context::get_unsat_core(ptr_vector & r) { + throw default_exception("Unsat cores are not supported with optimization"); + } + + void context::set_hard_constraints(ptr_vector& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 18af756bf..ef02a4cbe 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -190,7 +190,7 @@ namespace opt { virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } virtual void get_labels(svector & r); - virtual void get_unsat_core(ptr_vector & r) {} + virtual void get_unsat_core(ptr_vector & r); virtual std::string reason_unknown() const; virtual void set_reason_unknown(char const* msg) { m_unknown = msg; } From 9df5c314852a69ed237553d00ecf317524daea29 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 9 Dec 2016 13:40:46 +0000 Subject: [PATCH 16/42] Whitespace --- src/util/mpf.cpp | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 03b720ae1..3199b13ef 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1224,7 +1224,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m m_mpz_manager.machine_div2k(sig, 1); exp++; } - + const mpz & pl = m_powers2(sbits-1); while (m_mpz_manager.lt(sig, pl)) { m_mpz_manager.mul2k(sig, 1); @@ -1235,7 +1235,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) { unsigned ebits = x.ebits; unsigned sbits = x.sbits; - + SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX); SASSERT(exp_diff < ebits+sbits || partial); @@ -1252,7 +1252,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits))); SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1))); - // 1. Compute a/b + // 1. Compute a/b bool x_div_y_sgn = x.sign != y.sign; mpf_exp_t x_div_y_exp = D; scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager); @@ -1271,7 +1271,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex mpf_exp_t Q_exp = x_div_y_exp; scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager); unsigned Q_shft = (sbits-1) + (sbits+3) - (unsigned) (partial ? N :Q_exp); - if (partial) { + if (partial) { // Round according to MPF_ROUND_TOWARD_ZERO SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX); m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig); @@ -1294,7 +1294,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl; tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl; tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;); - + if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig)) return; // This means x % y = x. @@ -1308,7 +1308,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex bool YQ_sgn = x.sign; scoped_mpz YQ_sig(m_mpz_manager); mpf_exp_t YQ_exp = Q_exp + y.exponent; - m_mpz_manager.mul(y.significand, Q_sig, YQ_sig); + m_mpz_manager.mul(y.significand, Q_sig, YQ_sig); renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits. (void)YQ_sgn; @@ -1317,11 +1317,11 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl; tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;); - // `sbits-1' extra bits in YQ_sig. + // `sbits-1' extra bits in YQ_sig. SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1))); SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits)); - // 4. Compute X-Y*Q + // 4. Compute X-Y*Q mpf_exp_t X_YQ_exp = x.exponent; scoped_mpz X_YQ_sig(m_mpz_manager); mpf_exp_t exp_delta = exp(x) - YQ_exp; @@ -1339,14 +1339,14 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2))); SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1))); SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2))); - + if (exp_delta != 0) { scoped_mpz sticky_rem(m_mpz_manager); m_mpz_manager.set(sticky_rem, 0); if (exp_delta > sbits+5) - sticky_rem.swap(subtrahend); + sticky_rem.swap(subtrahend); else if (exp_delta > 0) - m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem); + m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem); else { SASSERT(exp_delta < 0); exp_delta = -exp_delta; @@ -1356,7 +1356,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex m_mpz_manager.inc(subtrahend); TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;); } - + m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig); TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;); @@ -1374,7 +1374,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl; tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl; tout << "X_YQ_exp=" << X_YQ_exp << std::endl; - tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl; + tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl; tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;); // `sbits-1' extra bits in X_YQ_sig @@ -1384,7 +1384,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; ); // Round to nearest, ties to even. - if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie. + if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie. if (m_mpz_manager.is_odd(X_YQ_sig)) { m_mpz_manager.inc(X_YQ_sig); } @@ -1430,7 +1430,7 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { mpf_exp_t D; do { if (ST0.exponent() < ST1.exponent() - 1) { - D = 0; + D = 0; } else { D = ST0.exponent() - ST1.exponent(); @@ -1889,7 +1889,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) { const mpz & p_m1 = m_powers2(o.sbits+2); const mpz & p_m2 = m_powers2(o.sbits+3); - (void)p_m1; + (void)p_m1; TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl << "p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;); From 56b1a8b086de13dd065bded9b134c63012f72456 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 9 Dec 2016 13:43:05 +0000 Subject: [PATCH 17/42] Bugfix for special-case handling in fp.fma. Thanks to Florian Schanda for reporting this bug. --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++--- src/smt/smt_model_checker.cpp | 43 ++++++++++++++++---------------- 2 files changed, 31 insertions(+), 24 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index ba6d436cc..2c0ba1ce1 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1463,11 +1463,17 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, v6 = z; // (x is 0) || (y is 0) -> z + expr_ref c71(m), xy_sgn(m), xyz_sgn(m); m_simp.mk_or(x_is_zero, y_is_zero, c7); - expr_ref ite_c(m), rm_is_not_to_neg(m); + m_simp.mk_xor(x_is_neg, y_is_neg, xy_sgn); + + m_simp.mk_xor(xy_sgn, z_is_neg, xyz_sgn); + m_simp.mk_and(z_is_zero, xyz_sgn, c71); + + expr_ref zero_cond(m), rm_is_not_to_neg(m); rm_is_not_to_neg = m.mk_not(rm_is_to_neg); - m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c); - mk_ite(ite_c, pzero, z, v7); + m_simp.mk_ite(rm_is_to_neg, nzero, pzero, zero_cond); + mk_ite(c71, zero_cond, z, v7); // else comes the fused multiplication. unsigned ebits = m_util.get_ebits(f->get_range()); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 5329cd80f..9ebdc5640 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -53,8 +53,8 @@ namespace smt { } void model_checker::set_qm(quantifier_manager & qm) { - SASSERT(m_qm == 0); - SASSERT(m_context == 0); + SASSERT(m_qm == 0); + SASSERT(m_context == 0); m_qm = &qm; m_context = &(m_qm->get_context()); } @@ -112,7 +112,7 @@ namespace smt { if (!m_curr_model->eval(q->get_expr(), tmp, true)) { return; } - TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); + TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); ptr_buffer subst_args; unsigned num_decls = q->get_num_decls(); subst_args.resize(num_decls, 0); @@ -139,7 +139,7 @@ namespace smt { bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) { if (cex == 0) { TRACE("model_checker", tout << "no model is available\n";); - return false; + return false; } unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. @@ -187,20 +187,20 @@ namespace smt { } bindings.set(num_decls - i - 1, sk_value); } - + TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: "; for (unsigned i = 0; i < num_decls; i++) { tout << mk_ismt2_pp(bindings[i].get(), m) << " "; } tout << "\n";); - + max_generation = std::max(m_qm->get_generation(q), max_generation); add_instance(q, bindings, max_generation); return true; } void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { - for (unsigned i = 0; i < bindings.size(); i++) + for (unsigned i = 0; i < bindings.size(); i++) m_new_instances_bindings.push_back(bindings[i]); void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation); @@ -260,41 +260,42 @@ namespace smt { bool model_checker::check(quantifier * q) { SASSERT(!m_aux_context->relevancy()); m_aux_context->push(); - + quantifier * flat_q = get_flat_quantifier(q); - TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << + TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(flat_q->get_expr(), m) << "\n";); expr_ref_vector sks(m); assert_neg_q_m(flat_q, sks); - TRACE("model_checker", tout << "skolems:\n"; + TRACE("model_checker", tout << "skolems:\n"; for (unsigned i = 0; i < sks.size(); i++) { expr * sk = sks.get(i); tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n"; }); - + lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); if (r != l_true) { m_aux_context->pop(1); return r == l_false; // quantifier is satisfied by m_curr_model } - + model_ref complete_cex; - m_aux_context->get_model(complete_cex); - + m_aux_context->get_model(complete_cex); + // try to find new instances using instantiation sets. m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks); - + unsigned num_new_instances = 0; while (true) { lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) - break; + break; model_ref cex; m_aux_context->get_model(cex); + TRACE("model_checker", tout << "[restricted] model-checker model cex:\n"; model_pp(tout, *cex);); if (!add_instance(q, cex.get(), sks, true)) { break; } @@ -302,7 +303,7 @@ namespace smt { if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { TRACE("model_checker", tout << "Add blocking clause failed\n";); // add_blocking_clause failed... stop the search for new counter-examples... - break; + break; } } @@ -396,7 +397,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; if(!m_qm->mbqi_enabled(q)) continue; - TRACE("model_checker", + TRACE("model_checker", tout << "Check: " << mk_pp(q, m) << "\n"; tout << m_context->get_assignment(q) << "\n";); @@ -418,12 +419,12 @@ namespace smt { } } } - + if (found_relevant) m_iteration_idx++; TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); - TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); + TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; if (num_failures == 0 && !m_context->validate_model()) { @@ -492,7 +493,7 @@ namespace smt { expr * b = inst->m_bindings[i]; tout << mk_pp(b, m) << "\n"; }); - TRACE("model_checker_instance", + TRACE("model_checker_instance", expr_ref inst_expr(m); instantiate(m, q, inst->m_bindings, inst_expr); tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";); From acba529bce28d98204c95bb6493a9de45478ff12 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 15:32:15 +0100 Subject: [PATCH 18/42] fix bug in encoding of axioms for indexof. Issue #806 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 245ffe438..3be3fd5f8 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2916,7 +2916,7 @@ void theory_seq::add_indexof_axiom(expr* i) { expr_ref len_t(m_util.str.mk_length(t), m); literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero)); - add_axiom(offset_ge_len, mk_eq(i, minus_one, false)); + add_axiom(~offset_ge_len, mk_eq(i, minus_one, false)); expr_ref x = mk_skolem(m_indexof_left, t, s, offset); expr_ref y = mk_skolem(m_indexof_right, t, s, offset); From 16b32ecf124880d2896b1a1c2012f4706d09af76 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 9 Dec 2016 15:03:31 +0000 Subject: [PATCH 19/42] Bugfix for special-case handling in fp.fma. Thanks to Florian Schanda for reporting this bug. (+reversed accidental debug code commit). --- src/smt/smt_model_checker.cpp | 43 +++++++++++++++++------------------ src/util/mpf.cpp | 5 ++-- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 9ebdc5640..5329cd80f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -53,8 +53,8 @@ namespace smt { } void model_checker::set_qm(quantifier_manager & qm) { - SASSERT(m_qm == 0); - SASSERT(m_context == 0); + SASSERT(m_qm == 0); + SASSERT(m_context == 0); m_qm = &qm; m_context = &(m_qm->get_context()); } @@ -112,7 +112,7 @@ namespace smt { if (!m_curr_model->eval(q->get_expr(), tmp, true)) { return; } - TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); + TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); ptr_buffer subst_args; unsigned num_decls = q->get_num_decls(); subst_args.resize(num_decls, 0); @@ -139,7 +139,7 @@ namespace smt { bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) { if (cex == 0) { TRACE("model_checker", tout << "no model is available\n";); - return false; + return false; } unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. @@ -187,20 +187,20 @@ namespace smt { } bindings.set(num_decls - i - 1, sk_value); } - + TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: "; for (unsigned i = 0; i < num_decls; i++) { tout << mk_ismt2_pp(bindings[i].get(), m) << " "; } tout << "\n";); - + max_generation = std::max(m_qm->get_generation(q), max_generation); add_instance(q, bindings, max_generation); return true; } void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { - for (unsigned i = 0; i < bindings.size(); i++) + for (unsigned i = 0; i < bindings.size(); i++) m_new_instances_bindings.push_back(bindings[i]); void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation); @@ -260,42 +260,41 @@ namespace smt { bool model_checker::check(quantifier * q) { SASSERT(!m_aux_context->relevancy()); m_aux_context->push(); - + quantifier * flat_q = get_flat_quantifier(q); - TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << + TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(flat_q->get_expr(), m) << "\n";); expr_ref_vector sks(m); assert_neg_q_m(flat_q, sks); - TRACE("model_checker", tout << "skolems:\n"; + TRACE("model_checker", tout << "skolems:\n"; for (unsigned i = 0; i < sks.size(); i++) { expr * sk = sks.get(i); tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n"; }); - + lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); if (r != l_true) { m_aux_context->pop(1); return r == l_false; // quantifier is satisfied by m_curr_model } - + model_ref complete_cex; - m_aux_context->get_model(complete_cex); - + m_aux_context->get_model(complete_cex); + // try to find new instances using instantiation sets. m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks); - + unsigned num_new_instances = 0; while (true) { lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) - break; + break; model_ref cex; m_aux_context->get_model(cex); - TRACE("model_checker", tout << "[restricted] model-checker model cex:\n"; model_pp(tout, *cex);); if (!add_instance(q, cex.get(), sks, true)) { break; } @@ -303,7 +302,7 @@ namespace smt { if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { TRACE("model_checker", tout << "Add blocking clause failed\n";); // add_blocking_clause failed... stop the search for new counter-examples... - break; + break; } } @@ -397,7 +396,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; if(!m_qm->mbqi_enabled(q)) continue; - TRACE("model_checker", + TRACE("model_checker", tout << "Check: " << mk_pp(q, m) << "\n"; tout << m_context->get_assignment(q) << "\n";); @@ -419,12 +418,12 @@ namespace smt { } } } - + if (found_relevant) m_iteration_idx++; TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); - TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); + TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; if (num_failures == 0 && !m_context->validate_model()) { @@ -493,7 +492,7 @@ namespace smt { expr * b = inst->m_bindings[i]; tout << mk_pp(b, m) << "\n"; }); - TRACE("model_checker_instance", + TRACE("model_checker_instance", expr_ref inst_expr(m); instantiate(m, q, inst->m_bindings, inst_expr); tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 3199b13ef..e9d108cec 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -795,8 +795,9 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co set(o, z); } else if (is_zero(x) || is_zero(y)) { - if (is_zero(z) && rm != MPF_ROUND_TOWARD_NEGATIVE) - mk_pzero(x.ebits, x.sbits, o); + bool xy_sgn = is_neg(x) ^ is_neg(y); + if (is_zero(z) && xy_sgn ^ is_neg(z)) + mk_zero(x.ebits, x.sbits, rm != MPF_ROUND_TOWARD_NEGATIVE, o); else set(o, z); } From 649d47468652160b21a0a103b0ae9b49685c261c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 9 Dec 2016 19:09:47 +0000 Subject: [PATCH 20/42] Build fix for C++ example --- scripts/mk_util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index cdd7bdeec..890c60501 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2086,12 +2086,12 @@ class CppExampleComponent(ExampleComponent): exefile = '%s$(EXE_EXT)' % self.name out.write('%s: %s %s\n' % (exefile, dll, objfiles)) - out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles)) + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s ' % (exefile, objfiles)) if IS_WINDOWS: out.write('%s.lib' % dll_name) else: out.write(dll) - out.write(' $(LINK_EXTRA_FLAGS)\n') + out.write(' $(SLINK_EXTRA_FLAGS)\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) class CExampleComponent(CppExampleComponent): From e092232f6765c9c9b7b699d77ccf4c372c071764 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2016 23:17:52 +0100 Subject: [PATCH 21/42] add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 4 ++-- src/math/automata/boolean_algebra.h | 2 ++ src/math/subpaving/tactic/subpaving_tactic.cpp | 2 ++ src/tactic/arith/add_bounds_tactic.cpp | 11 ++++++----- src/tactic/arith/diff_neq_tactic.cpp | 10 +++++----- src/tactic/arith/fm_tactic.cpp | 10 +++++----- src/tactic/arith/lia2pb_tactic.cpp | 10 +++++----- src/tactic/arith/normalize_bounds_tactic.cpp | 10 +++++----- src/tactic/arith/pb2bv_tactic.cpp | 10 +++++----- src/tactic/core/elim_uncnstr_tactic.cpp | 2 +- 10 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index e80d98553..138ea6fb0 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -155,9 +155,9 @@ extern "C" { MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP); MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP); MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); - MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP); + MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_COMPLEMENT, SKIP); MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); - MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP); + MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP); MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP); MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP); diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h index e3977b4cd..4f5527f5e 100644 --- a/src/math/automata/boolean_algebra.h +++ b/src/math/automata/boolean_algebra.h @@ -26,6 +26,7 @@ Revision History: template class positive_boolean_algebra { public: + virtual ~positive_boolean_algebra() {} virtual T mk_false() = 0; virtual T mk_true() = 0; virtual T mk_and(T x, T y) = 0; @@ -38,6 +39,7 @@ public: template class boolean_algebra : public positive_boolean_algebra { public: + virtual ~boolean_algebra() {} virtual T mk_not(T x) = 0; //virtual lbool are_equivalent(T x, T y) = 0; //virtual T simplify(T x) = 0; diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index 27e096777..2d0199223 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -35,6 +35,8 @@ class subpaving_tactic : public tactic { display_var_proc(expr2var & e2v):m_inv(e2v.m()) { e2v.mk_inv(m_inv); } + + virtual ~display_var_proc() {} ast_manager & m() const { return m_inv.get_manager(); } diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 950248698..8ff82af17 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -51,6 +51,7 @@ public: virtual result operator()(goal const & g) { return is_unbounded(g); } + virtual ~is_unbounded_probe() {} }; probe * mk_is_unbounded_probe() { @@ -109,11 +110,11 @@ class add_bounds_tactic : public tactic { void operator()(quantifier*) {} }; - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; tactic_report report("add-bounds", *g); bound_manager bm(m); diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 410185cf8..d63c2fcf4 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -312,11 +312,11 @@ class diff_neq_tactic : public tactic { return md; } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); m_produce_models = g->models_enabled(); mc = 0; pc = 0; core = 0; result.reset(); diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 5c82bbbc3..6db0f5ad3 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1549,11 +1549,11 @@ class fm_tactic : public tactic { throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; tactic_report report("fm", *g); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 8d637bada..2b54dd463 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -188,11 +188,11 @@ class lia2pb_tactic : public tactic { return true; } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); fail_if_proof_generation("lia2pb", g); m_produce_models = g->models_enabled(); diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index b3ec505ea..06f1368a2 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -80,11 +80,11 @@ class normalize_bounds_tactic : public tactic { return false; } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; bool produce_models = in->models_enabled(); bool produce_proofs = in->proofs_enabled(); diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 6348ddd74..3931a1ea4 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -885,11 +885,11 @@ private: r.erase("elim_and"); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { TRACE("pb2bv", g->display(tout);); SASSERT(g->is_well_sorted()); fail_if_proof_generation("pb2bv", g); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 156f69388..df3b9f0f5 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -819,7 +819,7 @@ class elim_uncnstr_tactic : public tactic { m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps); } - virtual void operator()(goal_ref const & g, + void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, From fe10f2d244989b549b0e8e4c8f5291a4e82173e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2016 07:51:16 +0100 Subject: [PATCH 22/42] address #835 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_relation_manager.cpp | 4 ++++ src/qe/qe_arrays.cpp | 2 +- src/qe/qe_datatypes.cpp | 2 +- src/smt/smt_model_finder.cpp | 2 +- src/tactic/fpa/fpa2bv_tactic.cpp | 10 +++++----- 5 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 7a73afd03..f8125f7a6 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1622,6 +1622,8 @@ namespace datalog { m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast(0)); } + virtual ~default_table_map() {} + virtual void operator()(table_base & t) { SASSERT(t.get_signature()==m_aux_table->get_signature()); if(!m_aux_table->empty()) { @@ -1678,6 +1680,8 @@ namespace datalog { m_former_row.resize(get_result_signature().size()); } + virtual ~default_table_project_with_reduce_fn() {} + virtual void modify_fact(table_fact & f) const { unsigned ofs=1; unsigned r_i=1; diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index f8f44b6d9..a010c4ae4 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -110,7 +110,7 @@ namespace qe { imp(ast_manager& m): m(m), a(m) {} ~imp() {} - virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index aa67d28a3..8536e337f 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -37,7 +37,7 @@ namespace qe { imp(ast_manager& m): m(m), dt(m), m_val(m) {} - virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return lift_foreign(vars, lits); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index b8320f329..ff84992e1 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -498,7 +498,7 @@ namespace smt { m_bvsimp = static_cast(s.get_plugin(m.mk_family_id("bv"))); } - ~auf_solver() { + virtual ~auf_solver() { flush_nodes(); reset_eval_cache(); } diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 28597c6ec..d55a2e25c 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -46,11 +46,11 @@ class fpa2bv_tactic : public tactic { m_rw.cfg().updt_params(p); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); m_proofs_enabled = g->proofs_enabled(); m_produce_models = g->models_enabled(); From 8e078cf9e20990de2168922dd6172014afa7423b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2016 07:52:00 +0100 Subject: [PATCH 23/42] address #835 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_relation_manager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index f8125f7a6..74206a1f6 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1622,7 +1622,7 @@ namespace datalog { m_union_fn = plugin.mk_union_fn(t, *m_aux_table, static_cast(0)); } - virtual ~default_table_map() {} + virtual ~default_table_map_fn() {} virtual void operator()(table_base & t) { SASSERT(t.get_signature()==m_aux_table->get_signature()); From dea3b8ddf7b64150d8cfa0dd41118419e3580c11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2016 13:14:36 +0100 Subject: [PATCH 24/42] address warnings from #836 Signed-off-by: Nikolaj Bjorner --- src/duality/duality_solver.cpp | 2 +- src/muz/base/dl_context.h | 1 - src/muz/base/dl_engine_base.h | 2 +- src/muz/rel/dl_table_relation.cpp | 2 +- src/muz/rel/dl_table_relation.h | 2 +- src/opt/opt_solver.cpp | 6 +++--- src/opt/opt_solver.h | 2 +- src/smt/proto_model/numeral_factory.cpp | 2 +- src/smt/proto_model/numeral_factory.h | 2 +- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_core.h | 2 +- src/smt/theory_dense_diff_logic.h | 6 +++--- src/smt/theory_dense_diff_logic_def.h | 13 +++++++------ src/smt/theory_diff_logic.h | 7 ++++--- src/smt/theory_diff_logic_def.h | 13 +++++++------ src/smt/theory_opt.h | 1 - src/smt/theory_seq.cpp | 12 ++++++------ src/smt/theory_seq.h | 2 +- src/smt/theory_utvpi_def.h | 2 +- 19 files changed, 41 insertions(+), 40 deletions(-) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index b3a96aea4..1869b74ce 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -3099,7 +3099,7 @@ namespace Duality { // Maps nodes of derivation tree into old subtree hash_map cex_map; - virtual void ChooseExpand(const std::set &choices, std::set &best){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool, bool){ if(old_node == 0){ Heuristic::ChooseExpand(choices,best); return; diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 3c1a7bfaa..ba841c84f 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -119,7 +119,6 @@ namespace datalog { virtual expr_ref try_get_formula(func_decl * pred) const = 0; virtual void display_output_facts(rule_set const& rules, std::ostream & out) const = 0; virtual void display_facts(std::ostream & out) const = 0; - virtual void display_profile(std::ostream& out) = 0; virtual void restrict_predicates(func_decl_set const& predicates) = 0; virtual bool result_contains_fact(relation_fact const& f) = 0; virtual void add_fact(func_decl* pred, relation_fact const& fact) = 0; diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index f353fbf2e..9878f3a9e 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -66,7 +66,7 @@ namespace datalog { } virtual void reset_statistics() {} - virtual void display_profile(std::ostream& out) const {} + virtual void display_profile(std::ostream& out) {} virtual void collect_statistics(statistics& st) const {} virtual unsigned get_num_levels(func_decl* pred) { throw default_exception(std::string("get_num_levels is not supported for ") + m_name); diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index d42d071aa..00a25d169 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -54,7 +54,7 @@ namespace datalog { return alloc(table_relation, *this, s, t); } - relation_base * table_relation_plugin::mk_full(const relation_signature & s, func_decl* p, family_id kind) { + relation_base * table_relation_plugin::mk_full_relation(const relation_signature & s, func_decl* p, family_id kind) { table_signature tsig; if(!get_manager().relation_signature_to_table(s, tsig)) { return 0; diff --git a/src/muz/rel/dl_table_relation.h b/src/muz/rel/dl_table_relation.h index 8266995da..56ca509fa 100644 --- a/src/muz/rel/dl_table_relation.h +++ b/src/muz/rel/dl_table_relation.h @@ -49,7 +49,7 @@ namespace datalog { virtual bool can_handle_signature(const relation_signature & s); virtual relation_base * mk_empty(const relation_signature & s); - virtual relation_base * mk_full(const relation_signature & s, func_decl* p, family_id kind); + virtual relation_base * mk_full_relation(const relation_signature & s, func_decl* p, family_id kind); relation_base * mk_from_table(const relation_signature & s, table_base * t); protected: diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 868303660..42129be70 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -57,7 +57,7 @@ namespace opt { opt_solver::~opt_solver() { } - void opt_solver::updt_params(params_ref & _p) { + void opt_solver::updt_params(params_ref const & _p) { opt_params p(_p); m_dump_benchmarks = p.dump_benchmarks(); m_params.updt_params(_p); @@ -383,13 +383,13 @@ namespace opt { if (typeid(smt::theory_idl) == typeid(opt)) { smt::theory_idl& th = dynamic_cast(opt); - return th.mk_ge(m_fm, v, val.get_rational()); + return th.mk_ge(m_fm, v, val); } if (typeid(smt::theory_rdl) == typeid(opt) && val.get_infinitesimal().is_zero()) { smt::theory_rdl& th = dynamic_cast(opt); - return th.mk_ge(m_fm, v, val.get_rational()); + return th.mk_ge(m_fm, v, val); } // difference logic? diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 094023ba2..cdaad3cf2 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -88,7 +88,7 @@ namespace opt { virtual ~opt_solver(); virtual solver* translate(ast_manager& m, params_ref const& p); - virtual void updt_params(params_ref & p); + virtual void updt_params(params_ref const& p); virtual void collect_param_descrs(param_descrs & r); virtual void collect_statistics(statistics & st) const; virtual void assert_expr(expr * t); diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp index a67b6c075..413cc1b9e 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/src/smt/proto_model/numeral_factory.cpp @@ -31,7 +31,7 @@ arith_factory::arith_factory(ast_manager & m): arith_factory::~arith_factory() { } -app * arith_factory::mk_value(rational const & val, bool is_int) { +app * arith_factory::mk_num_value(rational const & val, bool is_int) { return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real()); } diff --git a/src/smt/proto_model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h index 3c5d41040..e0d3cf6b5 100644 --- a/src/smt/proto_model/numeral_factory.h +++ b/src/smt/proto_model/numeral_factory.h @@ -38,7 +38,7 @@ public: arith_factory(ast_manager & m); virtual ~arith_factory(); - app * mk_value(rational const & val, bool is_int); + app * mk_num_value(rational const & val, bool is_int); }; class bv_factory : public numeral_factory { diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 39f991c72..5a0f8db95 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1080,7 +1080,7 @@ namespace smt { virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps_rational value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); void enable_record_conflict(expr* bound); void record_conflict(unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs, diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a08ee50ab..a8d771d1a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3231,7 +3231,7 @@ namespace smt { TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";); num = floor(num); } - return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v)))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(var2expr(v)))); } // ----------------------------------- diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index 1b1653eb7..c2be89bc3 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -198,7 +198,7 @@ namespace smt { void del_vars(unsigned old_num_vars); void init_model(); bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); - expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict); + expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict); #ifdef Z3DEBUG bool check_vector_sizes() const; bool check_matrix() const; @@ -270,8 +270,8 @@ namespace smt { virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps_rational value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_gt(theory_var v, inf_rational const& val); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val); + virtual expr_ref mk_gt(theory_var v, inf_eps const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val); // ----------------------------------- // diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index fd388b5bd..877d4f659 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -828,7 +828,7 @@ namespace smt { SASSERT(v != null_theory_var); numeral const & val = m_assignment[v]; rational num = val.get_rational().to_rational() + m_epsilon * val.get_infinitesimal().to_rational(); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int(v))); } // TBD: code is common to both sparse and dense difference logic solvers. @@ -1002,9 +1002,10 @@ namespace smt { m_assignment[i] = a; // TBD: if epsilon is != 0, then adjust a by some small fraction. } - blocker = mk_gt(v, r); + inf_eps result(rational(0), r); + blocker = mk_gt(v, result); IF_VERBOSE(10, verbose_stream() << blocker << "\n";); - return inf_eps(rational(0), r); + return result; } default: TRACE("opt", tout << "unbounded\n"; ); @@ -1034,18 +1035,18 @@ namespace smt { } template - expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_rational const& val) { + expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_eps const& val) { return mk_ineq(v, val, true); } template expr_ref theory_dense_diff_logic::mk_ge( - filter_model_converter& fm, theory_var v, inf_rational const& val) { + filter_model_converter& fm, theory_var v, inf_eps const& val) { return mk_ineq(v, val, false); } template - expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) { + expr_ref theory_dense_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h index 6fb9e6454..f47e61548 100644 --- a/src/smt/theory_diff_logic.h +++ b/src/smt/theory_diff_logic.h @@ -324,14 +324,15 @@ namespace smt { virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared); virtual inf_eps value(theory_var v); virtual theory_var add_objective(app* term); - virtual expr_ref mk_gt(theory_var v, inf_rational const& val); - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val); + expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val); bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); private: - expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict); + expr_ref mk_gt(theory_var v, inf_eps const& val); + + expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict); virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j); diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 98f94c6d2..372786c01 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -905,7 +905,7 @@ model_value_proc * theory_diff_logic::mk_value(enode * n, model_generator & numeral val = m_graph.get_assignment(v); rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational(); TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner()))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner()))); } template @@ -1242,7 +1242,8 @@ theory_diff_logic::maximize(theory_var v, expr_ref& blocker, bool& has_shar rational r = rational(val.first) + m_delta*rational(val.second); m_graph.set_assignment(i, numeral(r)); } - blocker = mk_gt(v, r); + inf_eps r1(rational(0), r); + blocker = mk_gt(v, r1); return inf_eps(rational(0), r + m_objective_consts[v]); } default: @@ -1273,7 +1274,7 @@ theory_var theory_diff_logic::add_objective(app* term) { } template -expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) { +expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); @@ -1304,7 +1305,7 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, return f; } - inf_rational new_val = val; // - inf_rational(m_objective_consts[v]); + inf_eps new_val = val; // - inf_rational(m_objective_consts[v]); e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f)); if (new_val.get_infinitesimal().is_neg()) { @@ -1328,12 +1329,12 @@ expr_ref theory_diff_logic::mk_ineq(theory_var v, inf_rational const& val, } template -expr_ref theory_diff_logic::mk_gt(theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::mk_gt(theory_var v, inf_eps const& val) { return mk_ineq(v, val, true); } template -expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) { +expr_ref theory_diff_logic::mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { return mk_ineq(v, val, false); } diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index 58e039140..421e6feca 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -33,7 +33,6 @@ namespace smt { virtual inf_eps value(theory_var) = 0; virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0; virtual theory_var add_objective(app* term) = 0; - virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return expr_ref(*((ast_manager*)0)); } bool is_linear(ast_manager& m, expr* term); bool is_numeral(arith_util& a, expr* term); }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3be3fd5f8..4f2683ca9 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2236,7 +2236,7 @@ bool theory_seq::add_stoi_axiom(expr* e) { expr* n; rational val; VERIFY(m_util.str.is_stoi(e, n)); - if (get_value(e, val) && !m_stoi_axioms.contains(val)) { + if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) { m_stoi_axioms.insert(val); if (!val.is_minus_one()) { app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); @@ -2260,7 +2260,7 @@ bool theory_seq::add_itos_axiom(expr* e) { rational val; expr* n; VERIFY(m_util.str.is_itos(e, n)); - if (get_value(n, val)) { + if (get_num_value(n, val)) { if (!m_itos_axioms.contains(val)) { m_itos_axioms.insert(val); app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); @@ -2741,7 +2741,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { } else if (m_util.str.is_itos(e, e1)) { rational val; - if (get_value(e1, val)) { + if (get_num_value(e1, val)) { TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";); expr_ref num(m), res(m); num = m_autil.mk_numeral(val, true); @@ -3024,7 +3024,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { unsigned num_char1 = 1, num_char2 = 1; rational len1, len2; rational ten(10); - if (get_value(n, len1)) { + if (get_num_value(n, len1)) { bool neg = len1.is_neg(); if (neg) len1.neg(); num_char1 = neg?2:1; @@ -3038,7 +3038,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { } SASSERT(len1 <= upper); } - if (get_value(len, len2) && len2.is_unsigned()) { + if (get_num_value(len, len2) && len2.is_unsigned()) { num_char2 = len2.get_unsigned(); } unsigned num_char = std::max(num_char1, num_char2); @@ -3172,7 +3172,7 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { } } -bool theory_seq::get_value(expr* e, rational& val) const { +bool theory_seq::get_num_value(expr* e, rational& val) const { context& ctx = get_context(); theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _val(m); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 21955bf30..0e06997ad 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -512,7 +512,7 @@ namespace smt { // arithmetic integration - bool get_value(expr* s, rational& val) const; + bool get_num_value(expr* s, rational& val) const; bool lower_bound(expr* s, rational& lo) const; bool upper_bound(expr* s, rational& hi) const; bool get_length(expr* s, rational& val) const; diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index ff295d5a3..5f370c29c 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -901,7 +901,7 @@ namespace smt { bool is_int = a.is_int(n->get_owner()); rational num = mk_value(v, is_int); TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int)); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int)); } /** From 6594c3a0461a106a528e330b1d5427bbc8e4bebd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2016 13:58:39 +0100 Subject: [PATCH 25/42] add virtual destructor to intermediary class in case this helps for #835 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_base.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 1c7a81444..9b573f71f 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -220,6 +220,8 @@ namespace datalog { */ class mutator_fn : public base_fn { public: + virtual ~mutator_fn() {} + virtual void operator()(base_object & t) = 0; virtual bool supports_attachment(base_object& other) { return false; } From 32c63ce4cdae0e244c2b01ac0f0e0637035ec6d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Dec 2016 17:23:59 +0100 Subject: [PATCH 26/42] address other warnings per input from delcypher Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter.h | 2 +- src/cmd_context/parametric_cmd.h | 1 + src/muz/rel/dl_base.h | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 401d00d89..fc596cabd 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -111,7 +111,7 @@ protected: void elim_reflex_prs(unsigned spos); public: rewriter_core(ast_manager & m, bool proof_gen); - ~rewriter_core(); + virtual ~rewriter_core(); ast_manager & m() const { return m_manager; } void reset(); void cleanup(); diff --git a/src/cmd_context/parametric_cmd.h b/src/cmd_context/parametric_cmd.h index 3e95832c4..cac5fe38e 100644 --- a/src/cmd_context/parametric_cmd.h +++ b/src/cmd_context/parametric_cmd.h @@ -72,6 +72,7 @@ public: // m_params.set_func_decl(m_last, f); // m_last = symbol::null; } + virtual void set_next_arg(cmd_context & ctx, sexpr * n) { UNREACHABLE(); } }; #endif diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 9b573f71f..9a2db4dbb 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -871,6 +871,7 @@ namespace datalog { class table_row_mutator_fn { public: + virtual ~table_row_mutator_fn() {} /** \brief The function is called for a particular table row. The \c func_columns contains a pointer to an array of functional column values that can be modified. If the function From 20790c46ee1b461749657b59f71508eded6e2363 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 04:23:07 +0100 Subject: [PATCH 27/42] bail out on failure to properly project Signed-off-by: Nikolaj Bjorner --- src/model/model_core.cpp | 30 +++++++++++++------------- src/model/model_core.h | 2 +- src/qe/qe_mbp.cpp | 2 ++ src/qe/qsat.cpp | 1 + src/tactic/smtlogics/quant_tactics.cpp | 9 -------- 5 files changed, 19 insertions(+), 25 deletions(-) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 6b8ff8d63..503abac2f 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -88,20 +88,20 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { } void model_core::unregister_decl(func_decl * d) { - decl2expr::obj_map_entry * ec = m_interp.find_core(d); - if (ec && ec->get_data().m_value != 0) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); - m_interp.remove(d); + decl2expr::obj_map_entry * ec = m_interp.find_core(d); + if (ec && ec->get_data().m_value != 0) { + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); + m_interp.remove(d); m_const_decls.erase(d); - return; - } - - decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); - if (ef && ef->get_data().m_value != 0) { - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); - m_finterp.remove(d); + return; + } + + decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); + if (ef && ef->get_data().m_value != 0) { + m_manager.dec_ref(ef->get_data().m_key); + dealloc(ef->get_data().m_value); + m_finterp.remove(d); m_func_decls.erase(d); - } -} \ No newline at end of file + } +} diff --git a/src/model/model_core.h b/src/model/model_core.h index 371106b05..c42451c5a 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -60,7 +60,7 @@ public: void register_decl(func_decl * d, expr * v); void register_decl(func_decl * f, func_interp * fi); - void unregister_decl(func_decl * d); + void unregister_decl(func_decl * d); virtual expr * get_some_value(sort * s) = 0; diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index eaedc470b..8aa6f509e 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -294,6 +294,7 @@ public: void extract_literals(model& model, expr_ref_vector& fmls) { expr_ref val(m); + TRACE("qe", tout << fmls << "\n";); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3; SASSERT(m.is_bool(fml)); @@ -404,6 +405,7 @@ public: // TBD other Boolean operations. } } + TRACE("qe", tout << fmls << "\n";); m_visited.reset(); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 1bfd53597..e378c7fdf 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -909,6 +909,7 @@ namespace qe { num_scopes = 2; } else { + if (level.max() + 2 > m_level) return false; SASSERT(level.max() + 2 <= m_level); num_scopes = m_level - level.max(); SASSERT(num_scopes >= 2); diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index bc3585d09..044511c33 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -104,21 +104,12 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) { } tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { -#if 0 - tactic * st = and_then(mk_quant_preprocessor(m), - or_else(try_for(mk_smt_tactic(), 100), - try_for(qe::mk_sat_tactic(m), 1000), - try_for(mk_smt_tactic(), 1000), - and_then(mk_qe_tactic(m), mk_smt_tactic()) - )); -#else tactic * st = and_then(mk_quant_preprocessor(m), mk_qe_lite_tactic(m, p), cond(mk_has_quantifier_probe(), or_else(mk_qsat_tactic(m, p), and_then(mk_qe_tactic(m), mk_smt_tactic())), mk_smt_tactic())); -#endif st->updt_params(p); return st; } From ff46a925a2f31cab964e5ee696a03bbbb99a9207 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 04:25:05 +0100 Subject: [PATCH 28/42] bail out on failure to properly project. issue #837 Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index e378c7fdf..841bdde9b 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -909,7 +909,7 @@ namespace qe { num_scopes = 2; } else { - if (level.max() + 2 > m_level) return false; + if (level.max() + 2 > m_level) return false; SASSERT(level.max() + 2 <= m_level); num_scopes = m_level - level.max(); SASSERT(num_scopes >= 2); From 70bb92d0163d4a9b1a033ab6c819207e231fdea4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 05:16:31 +0100 Subject: [PATCH 29/42] remove nested booleans during pre-processing. issue #837 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbp.cpp | 57 ++++++++++++++++++++++++++++++----------------- 1 file changed, 37 insertions(+), 20 deletions(-) diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 8aa6f509e..f4c0c9339 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -29,6 +29,7 @@ Revision History: #include "model_v2_pp.h" #include "expr_functors.h" #include "for_each_expr.h" +#include "model_evaluator.h" using namespace qe; @@ -125,6 +126,7 @@ class mbp::impl { th_rewriter m_rw; ptr_vector m_plugins; expr_mark m_visited; + expr_mark m_bool_visited; void add_plugin(project_plugin* p) { family_id fid = p->get_family_id(); @@ -212,10 +214,12 @@ class mbp::impl { } } - - void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) { + bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) { TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";); ptr_vector todo; + expr_safe_replace sub(m); + m_visited.reset(); + bool found_bool = false; if (is_app(fml)) { todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); } @@ -226,16 +230,16 @@ class mbp::impl { continue; } m_visited.mark(e); - if (m.is_bool(e)) { - expr_ref val(m); - VERIFY(model.eval(e, val)); + if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e)) { + expr_ref val = eval(e); TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";); - if (m.is_true(val)) { - fmls.push_back(e); - } - else { - fmls.push_back(mk_not(m, e)); + SASSERT(m.is_true(val) || m.is_false(val)); + if (!m_bool_visited.is_marked(e)) { + fmls.push_back(m.is_true(val) ? e : mk_not(m, e)); } + sub.insert(e, val); + m_bool_visited.mark(e); + found_bool = true; } else if (is_app(e)) { todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); @@ -244,6 +248,14 @@ class mbp::impl { TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";); } } + if (found_bool) { + expr_ref tmp(m); + sub(fml, tmp); + expr_ref val = eval(tmp); + SASSERT(m.is_true(val) || m.is_false(val)); + fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp)); + } + return found_bool; } void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { @@ -294,6 +306,7 @@ public: void extract_literals(model& model, expr_ref_vector& fmls) { expr_ref val(m); + model_evaluator eval(model); TRACE("qe", tout << fmls << "\n";); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3; @@ -304,7 +317,7 @@ public: } else if (m.is_or(fml)) { for (unsigned j = 0; j < to_app(fml)->get_num_args(); ++j) { - VERIFY (model.eval(to_app(fml)->get_arg(j), val)); + val = eval(to_app(fml)->get_arg(j)); if (m.is_true(val)) { fmls[i] = to_app(fml)->get_arg(j); --i; @@ -317,7 +330,7 @@ public: project_plugin::erase(fmls, i); } else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { - VERIFY (model.eval(f1, val)); + val = eval(f1); if (m.is_false(val)) { f1 = mk_not(m, f1); f2 = mk_not(m, f2); @@ -327,7 +340,7 @@ public: --i; } else if (m.is_implies(fml, f1, f2)) { - VERIFY (model.eval(f2, val)); + val = eval(f2); if (m.is_true(val)) { fmls[i] = f2; } @@ -337,7 +350,7 @@ public: --i; } else if (m.is_ite(fml, f1, f2, f3)) { - VERIFY (model.eval(f1, val)); + val = eval(f1); if (m.is_true(val)) { project_plugin::push_back(fmls, f1); project_plugin::push_back(fmls, f2); @@ -354,7 +367,7 @@ public: } else if (m.is_not(fml, nfml) && m.is_and(nfml)) { for (unsigned j = 0; j < to_app(nfml)->get_num_args(); ++j) { - VERIFY (model.eval(to_app(nfml)->get_arg(j), val)); + val = eval(to_app(nfml)->get_arg(j)); if (m.is_false(val)) { fmls[i] = mk_not(m, to_app(nfml)->get_arg(j)); --i; @@ -369,7 +382,7 @@ public: project_plugin::erase(fmls, i); } else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { - VERIFY (model.eval(f1, val)); + val = eval(f1); if (m.is_true(val)) { f2 = mk_not(m, f2); } @@ -386,7 +399,7 @@ public: project_plugin::erase(fmls, i); } else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { - VERIFY (model.eval(f1, val)); + val = eval(f1); if (m.is_true(val)) { project_plugin::push_back(fmls, f1); project_plugin::push_back(fmls, mk_not(m, f2)); @@ -398,15 +411,19 @@ public: project_plugin::erase(fmls, i); } else if (m.is_not(fml, nfml)) { - extract_bools(model, fmls, nfml); + if (extract_bools(eval, fmls, nfml)) { + project_plugin::erase(fmls, i); + } } else { - extract_bools(model, fmls, fml); + if (extract_bools(eval, fmls, fml)) { + project_plugin::erase(fmls, i); + } // TBD other Boolean operations. } } TRACE("qe", tout << fmls << "\n";); - m_visited.reset(); + m_bool_visited.reset(); } impl(ast_manager& m):m(m), m_rw(m) { From 0765eea486f1bd55aba5ac30a6ce45f08f9ef67a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 05:45:40 +0100 Subject: [PATCH 30/42] add suggestions from #835 Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 2 +- src/muz/rel/dl_base.h | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 91bff5ab5..027cce09d 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -494,7 +494,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; for (unsigned i = 0; i < var_mapping.size(); i++) { if (var_mapping[i] != 0) - tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); + tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); }); subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t); } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 9a2db4dbb..d3422f882 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -885,6 +885,7 @@ namespace datalog { class table_row_pair_reduce_fn { public: + virtual ~table_row_pair_reduce_fn() {} /** \brief The function is called for pair of table rows that became duplicit due to projection. The values that are in the first array after return from the function will be used for the From 2307a7ffa73fb06c80b206503b03d0c4af4fb12b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 10:19:57 +0100 Subject: [PATCH 31/42] fix bug in handling of repeated soft constraints. #815 Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 3 ++- src/opt/maxsmt.cpp | 11 +++++++++-- src/opt/maxsmt.h | 2 +- src/opt/opt_context.cpp | 27 +++++++++++++++++++++++++++ src/opt/opt_context.h | 1 + 5 files changed, 40 insertions(+), 4 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 7f9183d9a..54e7f351c 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -805,8 +805,9 @@ public: lbool init_local() { m_lower.reset(); m_trail.reset(); + lbool is_sat = l_true; obj_map new_soft; - lbool is_sat = find_mutexes(new_soft); + is_sat = find_mutexes(new_soft); if (is_sat != l_true) { return is_sat; } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 85b19e427..21537a570 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -333,8 +333,15 @@ namespace opt { TRACE("opt", tout << mk_pp(f, m) << " weight: " << w << "\n";); SASSERT(m.is_bool(f)); SASSERT(w.is_pos()); - m_soft_constraints.push_back(f); - m_weights.push_back(w); + unsigned index = 0; + if (m_soft_constraint_index.find(f, index)) { + m_weights[index] += w; + } + else { + m_soft_constraint_index.insert(f, m_weights.size()); + m_soft_constraints.push_back(f); + m_weights.push_back(w); + } m_upper += w; } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 5ecb023f6..358ff4995 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -120,6 +120,7 @@ namespace opt { unsigned m_index; scoped_ptr m_msolver; expr_ref_vector m_soft_constraints; + obj_map m_soft_constraint_index; expr_ref_vector m_answer; vector m_weights; rational m_lower; @@ -138,7 +139,6 @@ namespace opt { expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; } rational weight(unsigned idx) const { return m_weights[idx]; } void commit_assignment(); - rational get_value() const; rational get_lower() const; rational get_upper() const; void update_lower(rational const& r); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b95bb62e8..e63e29dc5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -360,6 +360,7 @@ namespace opt { } if (scoped) get_solver().pop(1); if (result == l_true && committed) ms.commit_assignment(); + DEBUG_CODE(if (result == l_true) validate_maxsat(id);); return result; } @@ -1448,6 +1449,32 @@ namespace opt { return out.str(); } + void context::validate_maxsat(symbol const& id) { + maxsmt& ms = *m_maxsmts.find(id); + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + if (obj.m_id == id) { + SASSERT(obj.m_type == O_MAXSMT); + rational value(0); + expr_ref val(m); + for (unsigned i = 0; i < obj.m_terms.size(); ++i) { + bool evaluated = m_model->eval(obj.m_terms[i], val); + SASSERT(evaluated); + CTRACE("opt", evaluated && !m.is_true(val) && !m.is_false(val), tout << mk_pp(obj.m_terms[i], m) << " " << val << "\n";); + CTRACE("opt", !evaluated, tout << mk_pp(obj.m_terms[i], m) << "\n";); + if (evaluated && !m.is_true(val)) { + value += obj.m_weights[i]; + } + // TBD: check that optimal was not changed. + } + value = obj.m_adjust_value(value); + rational value0 = ms.get_lower(); + TRACE("opt", tout << "value " << value << " " << value0 << "\n";); + SASSERT(value == value0); + } + } + } + void context::validate_lex() { rational r1; expr_ref val(m); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index ef02a4cbe..461506258 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -291,6 +291,7 @@ namespace opt { void validate_lex(); + void validate_maxsat(symbol const& id); void display_benchmark(); From 7cc093eee0adeeb7682bb8dcd529f13e2491449d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 11:05:12 +0100 Subject: [PATCH 32/42] Add rewrite rule for property encoded in #812 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index cc948de9a..b97d832b1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -524,7 +524,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { result = m().mk_bool_val(c.contains(d)); return BR_DONE; } - // check if subsequence of b is in a. + // check if subsequence of a is in b. expr_ref_vector as(m()), bs(m()); m_util.str.get_concat(a, as); m_util.str.get_concat(b, bs); @@ -587,6 +587,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { SASSERT(sz > offs); result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b); return BR_REWRITE2; + } + + expr* x, *y, *z; + if (m_util.str.is_extract(b, x, y, z) && x == a) { + result = m().mk_true(); + return BR_DONE; } return BR_FAILED; From bd1f07f864a7f1790cec08a306ccc17507f7e5a8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 11 Dec 2016 23:07:48 +0000 Subject: [PATCH 33/42] Fix implementation of `scoped_timer` under Linux where it was incorrectly assumed that `pthread_cond_timedwait()` would exit due to a condition variable being signaled or a timeout occuring. According to the documentation `pthread_cond_timedwait()` might spuriously wake so we introduce a new variable `m_signal_sent` (that is guarded by an existing mutex) that is used as the variable to check that the thread wake was not spurious. This is intended to partially fix #839 . --- src/util/scoped_timer.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 335b2c3bb..3b87f880f 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -73,6 +73,7 @@ struct scoped_timer::imp { pthread_cond_t m_cond; unsigned m_ms; bool m_initialized; + bool m_signal_sent; #else // Other #endif @@ -119,10 +120,18 @@ struct scoped_timer::imp { pthread_mutex_lock(&st->m_mutex); st->m_initialized = true; - int e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time); - ENSURE(e == 0 || e == ETIMEDOUT); - + int e = 0; + // `pthread_cond_timedwait()` may spuriously wake even if the signal + // was not sent so we loop until a timeout occurs or the signal was + // **really** sent. + while (!(e == 0 && st->m_signal_sent)) { + e = pthread_cond_timedwait(&st->m_cond, &st->m_mutex, &end_time); + ENSURE(e == 0 || e == ETIMEDOUT); + if (e == ETIMEDOUT) + break; + } pthread_mutex_unlock(&st->m_mutex); + if (e == ETIMEDOUT) st->m_eh->operator()(); return 0; @@ -170,6 +179,7 @@ struct scoped_timer::imp { // Linux & FreeBSD m_ms = ms; m_initialized = false; + m_signal_sent = false; ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0); ENSURE(pthread_cond_init(&m_cond, NULL) == 0); ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0); @@ -218,7 +228,10 @@ struct scoped_timer::imp { if (!init) sched_yield(); } + pthread_mutex_lock(&m_mutex); + m_signal_sent = true; pthread_cond_signal(&m_cond); + pthread_mutex_unlock(&m_mutex); pthread_join(m_thread_id, NULL); pthread_cond_destroy(&m_cond); From c1480b43894cf191cb67dfcf4283a64e855f7508 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Dec 2016 00:33:10 +0100 Subject: [PATCH 34/42] handle model generation from issue #748. Deal with warnings from #836 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/muz/rel/dl_product_relation.cpp | 6 +- src/muz/rel/dl_sieve_relation.cpp | 2 +- src/muz/rel/dl_sieve_relation.h | 3 +- src/smt/proto_model/numeral_factory.cpp | 2 +- src/smt/proto_model/numeral_factory.h | 2 +- src/smt/theory_bv.cpp | 2 +- src/smt/theory_seq.cpp | 121 +++++++++++++++++++++--- src/smt/theory_seq.h | 2 + 9 files changed, 118 insertions(+), 24 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b97d832b1..26c3e23e4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1721,7 +1721,7 @@ bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr* } } - if (szr == 1 && m_util.str.is_itos(rs[0], r)) { + if (szr == 1 && m_util.str.is_itos(rs[0], r) && !m_util.str.is_itos(ls[0])) { return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat); } diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp index 1bc5e3545..817ff194c 100644 --- a/src/muz/rel/dl_product_relation.cpp +++ b/src/muz/rel/dl_product_relation.cpp @@ -255,7 +255,7 @@ namespace datalog { table_plugin & tplugin = rmgr.get_appropriate_plugin(tsig); relation_plugin & inner_plugin = rmgr.get_table_relation_plugin(tplugin); - return sieve_relation_plugin::get_plugin(rmgr).mk_full(p, sig, inner_plugin); + return sieve_relation_plugin::get_plugin(rmgr).full(p, sig, inner_plugin); } void init(relation_signature const& r1_sig, unsigned num_rels1, relation_base const* const* r1, @@ -294,7 +294,7 @@ namespace datalog { rel2 = r1_plugin.mk_full(p, r2_sig, r1_kind); } else { - rel2 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r2_sig, r1_plugin); + rel2 = sieve_relation_plugin::get_plugin(rmgr).full(p, r2_sig, r1_plugin); } m_offset1.push_back(i); m_kind1.push_back(T_INPUT); @@ -318,7 +318,7 @@ namespace datalog { rel1 = r2_plugin.mk_full(p, r1_sig, r2_kind); } else { - rel1 = sieve_relation_plugin::get_plugin(rmgr).mk_full(p, r1_sig, r2_plugin); + rel1 = sieve_relation_plugin::get_plugin(rmgr).full(p, r1_sig, r2_plugin); } m_offset1.push_back(m_full.size()); m_kind1.push_back(T_FULL); diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index 9f9419089..7729ec2eb 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/src/muz/rel/dl_sieve_relation.cpp @@ -253,7 +253,7 @@ namespace datalog { return mk_from_inner(s, inner_cols, inner); } - sieve_relation * sieve_relation_plugin::mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) { + sieve_relation * sieve_relation_plugin::full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin) { SASSERT(!inner_plugin.is_sieve_relation()); //it does not make sense to make a sieve of a sieve svector inner_cols(s.size()); extract_inner_columns(s, inner_plugin, inner_cols); diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h index da6c9bbff..4d89a66ae 100644 --- a/src/muz/rel/dl_sieve_relation.h +++ b/src/muz/rel/dl_sieve_relation.h @@ -104,8 +104,7 @@ namespace datalog { sieve_relation * mk_empty(const relation_signature & s, relation_plugin & inner_plugin); virtual relation_base * mk_full(func_decl* p, const relation_signature & s); - sieve_relation * mk_full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin); - + sieve_relation * full(func_decl* p, const relation_signature & s, relation_plugin & inner_plugin); sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, relation_base * inner_rel); diff --git a/src/smt/proto_model/numeral_factory.cpp b/src/smt/proto_model/numeral_factory.cpp index 413cc1b9e..49ff15167 100644 --- a/src/smt/proto_model/numeral_factory.cpp +++ b/src/smt/proto_model/numeral_factory.cpp @@ -47,6 +47,6 @@ app * bv_factory::mk_value_core(rational const & val, sort * s) { return m_util.mk_numeral(val, s); } -app * bv_factory::mk_value(rational const & val, unsigned bv_size) { +app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) { return numeral_factory::mk_value(val, m_util.mk_sort(bv_size)); } diff --git a/src/smt/proto_model/numeral_factory.h b/src/smt/proto_model/numeral_factory.h index e0d3cf6b5..9b1ff6a81 100644 --- a/src/smt/proto_model/numeral_factory.h +++ b/src/smt/proto_model/numeral_factory.h @@ -50,7 +50,7 @@ public: bv_factory(ast_manager & m); virtual ~bv_factory(); - app * mk_value(rational const & val, unsigned bv_size); + app * mk_num_value(rational const & val, unsigned bv_size); }; #endif /* NUMERAL_FACTORY_H_ */ diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a53580b73..a886c8a1e 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1583,7 +1583,7 @@ namespace smt { #endif get_fixed_value(v, val); SASSERT(r); - return alloc(expr_wrapper_proc, m_factory->mk_value(val, get_bv_size(v))); + return alloc(expr_wrapper_proc, m_factory->mk_num_value(val, get_bv_size(v))); } void theory_bv::display_var(std::ostream & out, theory_var v) const { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4f2683ca9..ed95ef8d7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2235,6 +2235,7 @@ bool theory_seq::add_stoi_axiom(expr* e) { context& ctx = get_context(); expr* n; rational val; + TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_stoi(e, n)); if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) { m_stoi_axioms.insert(val); @@ -2252,13 +2253,70 @@ bool theory_seq::add_stoi_axiom(expr* e) { return true; } } + if (upper_bound(n, val) && get_length(n, val) && val.is_pos() && !m_stoi_axioms.contains(val)) { + zstring s; + SASSERT(val.is_unsigned()); + unsigned sz = val.get_unsigned(); + expr_ref len1(m), len2(m), ith_char(m), num(m), coeff(m); + expr_ref_vector nums(m); + len1 = m_util.str.mk_length(n); + len2 = m_autil.mk_int(sz); + literal lit = mk_eq(len1, len2, false); + literal_vector lits; + lits.push_back(~lit); + for (unsigned i = 0; i < sz; ++i) { + ith_char = mk_nth(n, m_autil.mk_int(i)); + lits.push_back(~is_digit(ith_char)); + nums.push_back(digit2int(ith_char)); + } + for (unsigned i = sz-1, c = 1; i > 0; c *= 10) { + --i; + coeff = m_autil.mk_int(c); + nums[i] = m_autil.mk_mul(coeff, nums[i].get()); + } + num = m_autil.mk_add(nums.size(), nums.c_ptr()); + lits.push_back(mk_eq(e, num, false)); + ++m_stats.m_add_axiom; + m_new_propagation = true; + for (unsigned i = 0; i < lits.size(); ++i) { + ctx.mark_as_relevant(lits[i]); + } + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + m_stoi_axioms.insert(val); + m_trail_stack.push(insert_map(m_stoi_axioms, val)); + m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); + return true; + } + return false; } +literal theory_seq::is_digit(expr* ch) { + bv_util bv(m); + literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, 0, 0, m.mk_bool_sort())); + expr_ref d2i = digit2int(ch); + expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m); + expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m); + literal lo = mk_literal(_lo); + literal hi = mk_literal(_hi); + add_axiom(~lo, ~hi, isd); + add_axiom(~isd, lo); + add_axiom(~isd, hi); + for (unsigned i = 0; i < 10; ++i) { + add_axiom(~mk_eq(ch, bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), false), mk_eq(d2i, m_autil.mk_int(i), false)); + } + return isd; +} + +expr_ref theory_seq::digit2int(expr* ch) { + return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, 0, 0, m_autil.mk_int()), m); +} + bool theory_seq::add_itos_axiom(expr* e) { context& ctx = get_context(); rational val; expr* n; + TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_itos(e, n)); if (get_num_value(n, val)) { if (!m_itos_axioms.contains(val)) { @@ -2282,6 +2340,9 @@ bool theory_seq::add_itos_axiom(expr* e) { else { // stoi(itos(n)) = n app_ref e2(m_util.str.mk_stoi(e), m); + if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) { + return false; + } add_axiom(mk_eq(e2, n, false)); m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); return true; @@ -2464,22 +2525,27 @@ void theory_seq::init_model(model_generator & mg) { class theory_seq::seq_value_proc : public model_value_proc { + enum source_t { unit_source, int_source, string_source }; theory_seq& th; sort* m_sort; svector m_dependencies; ptr_vector m_strings; - svector m_source; + svector m_source; public: seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) { } virtual ~seq_value_proc() {} - void add_dependency(enode* n) { + void add_unit(enode* n) { m_dependencies.push_back(model_value_dependency(n)); - m_source.push_back(true); + m_source.push_back(unit_source); + } + void add_int(enode* n) { + m_dependencies.push_back(model_value_dependency(n)); + m_source.push_back(int_source); } void add_string(expr* n) { m_strings.push_back(n); - m_source.push_back(false); + m_source.push_back(string_source); } virtual void get_dependencies(buffer & result) { result.append(m_dependencies.size(), m_dependencies.c_ptr()); @@ -2504,11 +2570,13 @@ public: unsigned sz; for (unsigned i = 0; i < m_source.size(); ++i) { - if (m_source[i]) { + switch (m_source[i]) { + case unit_source: { VERIFY(bv.is_numeral(values[j++], val, sz)); sbuffer.push_back(val.get_unsigned()); + break; } - else { + case string_source: { dependency* deps = 0; expr_ref tmp = th.canonize(m_strings[k], deps); zstring zs; @@ -2519,17 +2587,34 @@ public: TRACE("seq", tout << "Not a string: " << tmp << "\n";); } ++k; + break; + } + case int_source: { + std::ostringstream strm; + arith_util arith(th.m); + VERIFY(arith.is_numeral(values[j++], val)); + if (val.is_neg()) strm << "-"; + strm << abs(val); + zstring zs(strm.str().c_str()); + add_buffer(sbuffer, zs); + break; + } } } result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr())); } else { for (unsigned i = 0; i < m_source.size(); ++i) { - if (m_source[i]) { + switch (m_source[i]) { + case unit_source: args.push_back(th.m_util.str.mk_unit(values[j++])); - } - else { + break; + case string_source: args.push_back(m_strings[k++]); + break; + case int_source: + UNREACHABLE(); + break; } } result = th.mk_concat(args, m_sort); @@ -2567,7 +2652,12 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { TRACE("seq", tout << mk_pp(c, m) << "\n";); if (m_util.str.is_unit(c, c1)) { if (ctx.e_internalized(c1)) { - sv->add_dependency(ctx.get_enode(c1)); + sv->add_unit(ctx.get_enode(c1)); + } + } + else if (m_util.str.is_itos(c, c1)) { + if (ctx.e_internalized(c1)) { + sv->add_int(ctx.get_enode(c1)); } } else if (m_util.str.is_string(c)) { @@ -2741,6 +2831,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { } else if (m_util.str.is_itos(e, e1)) { rational val; + TRACE("seq", tout << mk_pp(e, m) << "\n";); if (get_num_value(e1, val)) { TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";); expr_ref num(m), res(m); @@ -3177,13 +3268,12 @@ bool theory_seq::get_num_value(expr* e, rational& val) const { theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); expr_ref _val(m); if (!tha) return false; - enode* next = ctx.get_enode(e), *n; + enode* next = ctx.get_enode(e), *n = next; do { - n = next; - if (tha->get_value(n, _val) && m_autil.is_numeral(_val, val) && val.is_int()) { + if (tha->get_value(next, _val) && m_autil.is_numeral(_val, val) && val.is_int()) { return true; } - next = n->get_next(); + next = next->get_next(); } while (next != n); return false; @@ -3692,7 +3782,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { else if (is_skolem(symbol("seq.split"), e)) { // propagate equalities } + else if (is_skolem(symbol("seq.is_digit"), e)) { + } else { + TRACE("seq", tout << mk_pp(e, m) << "\n";); UNREACHABLE(); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 0e06997ad..aa7ddec1b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -499,6 +499,8 @@ namespace smt { void add_in_re_axiom(expr* n); bool add_stoi_axiom(expr* n); bool add_itos_axiom(expr* n); + literal is_digit(expr* ch); + expr_ref digit2int(expr* ch); void add_itos_length_axiom(expr* n); literal mk_literal(expr* n); literal mk_eq_empty(expr* n, bool phase = true); From a1a662b23f4c9e2d072dc3a813d276537c488fb7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 16 Dec 2016 04:51:07 -0800 Subject: [PATCH 35/42] Build fix for C/C++ example programs. --- scripts/mk_util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 890c60501..cdd7bdeec 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2086,12 +2086,12 @@ class CppExampleComponent(ExampleComponent): exefile = '%s$(EXE_EXT)' % self.name out.write('%s: %s %s\n' % (exefile, dll, objfiles)) - out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s ' % (exefile, objfiles)) + out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles)) if IS_WINDOWS: out.write('%s.lib' % dll_name) else: out.write(dll) - out.write(' $(SLINK_EXTRA_FLAGS)\n') + out.write(' $(LINK_EXTRA_FLAGS)\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) class CExampleComponent(CppExampleComponent): From 6ce903b1d698c9aa7976a1356b4bc62635a30582 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 16 Dec 2016 20:04:29 +0000 Subject: [PATCH 36/42] Style, whitespace. --- src/util/rlimit.cpp | 15 +++++++-------- src/util/rlimit.h | 6 +++--- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 9f6c692cc..bda06157d 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -20,7 +20,7 @@ Revision History: #include "common_msgs.h" reslimit::reslimit(): - m_cancel(false), + m_cancel(0), m_count(0), m_limit(0) { } @@ -29,7 +29,6 @@ uint64 reslimit::count() const { return m_count; } - bool reslimit::inc() { ++m_count; return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); @@ -46,7 +45,7 @@ void reslimit::push(unsigned delta_limit) { new_limit = 0; } m_limits.push_back(m_limit); - m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit); + m_limit = m_limit==0 ? new_limit : std::min(new_limit, m_limit); m_cancel = 0; } @@ -71,14 +70,14 @@ char const* reslimit::get_cancel_msg() const { void reslimit::push_child(reslimit* r) { #pragma omp critical (reslimit_cancel) { - m_children.push_back(r); + m_children.push_back(r); } } void reslimit::pop_child() { #pragma omp critical (reslimit_cancel) { - m_children.pop_back(); + m_children.pop_back(); } } @@ -99,7 +98,7 @@ void reslimit::reset_cancel() { void reslimit::inc_cancel() { #pragma omp critical (reslimit_cancel) - { + { set_cancel(m_cancel+1); } } @@ -114,8 +113,8 @@ void reslimit::dec_cancel() { } } -void reslimit::set_cancel(unsigned f) { - m_cancel = f; +void reslimit::set_cancel(unsigned f) { + m_cancel = f; for (unsigned i = 0; i < m_children.size(); ++i) { m_children[i]->set_cancel(f); } diff --git a/src/util/rlimit.h b/src/util/rlimit.h index ac5db6136..913984768 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -29,8 +29,8 @@ class reslimit { ptr_vector m_children; void set_cancel(unsigned f); - -public: + +public: reslimit(); void push(unsigned delta_limit); void pop(); @@ -39,7 +39,7 @@ public: bool inc(); bool inc(unsigned offset); - uint64 count() const; + uint64 count() const; bool get_cancel_flag() const { return m_cancel > 0; } From 5cb21924ad844bda646a3f2c7b293d5790439e70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Dec 2016 16:02:54 -0800 Subject: [PATCH 37/42] ensure that FD logic understands pb from command context Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 2 +- src/cmd_context/check_logic.cpp | 7 ++++++- src/cmd_context/cmd_context.cpp | 7 ++++++- src/cmd_context/cmd_context.h | 1 + src/solver/smt_logics.cpp | 4 ++++ src/solver/smt_logics.h | 1 + 6 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index 18a652859..09f020ca6 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -91,7 +91,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null) { + if (logic == symbol::null || logic == "QF_FD") { op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K)); op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index d598dfa39..c75c12689 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -21,6 +21,7 @@ Revision History: #include"array_decl_plugin.h" #include"bv_decl_plugin.h" #include"seq_decl_plugin.h" +#include"pb_decl_plugin.h" #include"datatype_decl_plugin.h" #include"ast_pp.h" #include"for_each_expr.h" @@ -34,6 +35,7 @@ struct check_logic::imp { array_util m_ar_util; seq_util m_seq_util; datatype_util m_dt_util; + pb_util m_pb_util; bool m_uf; // true if the logic supports uninterpreted functions bool m_arrays; // true if the logic supports arbitrary arrays bool m_bv_arrays; // true if the logic supports only bv arrays @@ -45,7 +47,7 @@ struct check_logic::imp { bool m_quantifiers; // true if the logic supports quantifiers bool m_unknown_logic; - imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m) { + imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m), m_pb_util(m) { reset(); } @@ -443,6 +445,9 @@ struct check_logic::imp { else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") { // nothing to check } + else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") { + // nothing to check + } else { std::stringstream strm; strm << "logic does not support theory " << m.get_family_name(fid); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index eb7b3ff44..67b1df50c 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -519,6 +519,10 @@ bool cmd_context::logic_has_seq() const { return !has_logic() || smt_logics::logic_has_seq(m_logic); } +bool cmd_context::logic_has_pb() const { + return !has_logic() || smt_logics::logic_has_pb(m_logic); +} + bool cmd_context::logic_has_fpa() const { return !has_logic() || smt_logics::logic_has_fpa(m_logic); } @@ -547,7 +551,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); - register_plugin(symbol("pb"), alloc(pb_decl_plugin), !has_logic()); + register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb()); register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); } @@ -563,6 +567,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("datatype"), logic_has_datatype(), fids); load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); + load_plugin(symbol("pb"), logic_has_pb(), fids); svector::iterator it = fids.begin(); svector::iterator end = fids.end(); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 34d93c97b..8eee632dc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -251,6 +251,7 @@ protected: bool logic_has_arith() const; bool logic_has_bv() const; + bool logic_has_pb() const; bool logic_has_seq() const; bool logic_has_array() const; bool logic_has_datatype() const; diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 9ee047839..210a09f96 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -144,6 +144,10 @@ bool smt_logics::logic_has_horn(symbol const& s) { return s == "HORN"; } +bool smt_logics::logic_has_pb(symbol const& s) { + return s == "QF_FD" || s == "ALL"; +} + bool smt_logics::logic_has_datatype(symbol const& s) { return s == "QF_FD"; } diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h index f283040d9..72c3b8764 100644 --- a/src/solver/smt_logics.h +++ b/src/solver/smt_logics.h @@ -32,6 +32,7 @@ public: static bool logic_has_seq(symbol const & s); static bool logic_has_fpa(symbol const & s); static bool logic_has_horn(symbol const& s); + static bool logic_has_pb(symbol const& s); static bool logic_has_fd(symbol const& s) { return s == "QF_FD"; } static bool logic_has_datatype(symbol const& s); }; From e16577ff61a09123dd2609c3fdb17f6671995cf2 Mon Sep 17 00:00:00 2001 From: Kevin Chung Date: Sun, 18 Dec 2016 17:27:55 -0500 Subject: [PATCH 38/42] Making z3 python look in its installation directory for the z3 lib --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 04378b371..3a3b2c40a 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1611,7 +1611,7 @@ _lib = None def lib(): global _lib if _lib is None: - _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None] + _dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None] for _dir in _dirs: try: init(_dir) From 189d449cff42d5612e99386038e375e1dd534eb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Dec 2016 14:49:45 -0800 Subject: [PATCH 39/42] fix generation of wcnf Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 6 ++-- src/sat/sat_solver/inc_sat_solver.cpp | 10 +++++- src/sat/tactic/goal2sat.cpp | 50 +++++++++++++++++++++++++-- 3 files changed, 60 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 9cf13afe4..e6fa15a4c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2917,6 +2917,7 @@ namespace sat { ++max_weight; out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n"; + out << "c soft " << sz << "\n"; for (unsigned i = 0; i < m_trail.size(); i++) { out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n"; @@ -2940,9 +2941,9 @@ namespace sat { clause_vector::const_iterator end = cs.end(); for (; it != end; ++it) { clause const & c = *(*it); - unsigned sz = c.size(); + unsigned clsz = c.size(); out << max_weight << " "; - for (unsigned j = 0; j < sz; j++) + for (unsigned j = 0; j < clsz; j++) out << dimacs_lit(c[j]) << " "; out << "0\n"; } @@ -2950,6 +2951,7 @@ namespace sat { for (unsigned i = 0; i < sz; ++i) { out << weights[i] << " " << lits[i] << " 0\n"; } + out.flush(); } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e56abc50c..e3a220cd2 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -115,10 +115,18 @@ public: if (weights != 0) { for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]); } + init_preprocess(); m_solver.pop_to_base_level(); dep2asm_t dep2asm; + expr_ref_vector asms(m); + for (unsigned i = 0; i < sz; ++i) { + expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m); + expr_ref fml(m.mk_implies(a, assumptions[i]), m); + assert_expr(fml); + asms.push_back(a); + } VERIFY(l_true == internalize_formulas()); - VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm)); + VERIFY(l_true == internalize_assumptions(sz, asms.c_ptr(), dep2asm)); svector nweights; for (unsigned i = 0; i < m_asms.size(); ++i) { nweights.push_back((unsigned) m_weights[i]); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 136921914..742a4fb1d 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -174,6 +174,7 @@ struct goal2sat::imp { switch (to_app(t)->get_decl_kind()) { case OP_NOT: case OP_OR: + case OP_AND: case OP_IFF: m_frame_stack.push_back(frame(to_app(t), root, sign, 0)); return false; @@ -185,7 +186,6 @@ struct goal2sat::imp { } convert_atom(t, root, sign); return true; - case OP_AND: case OP_XOR: case OP_IMPLIES: case OP_DISTINCT: { @@ -215,8 +215,8 @@ struct goal2sat::imp { } else { mk_clause(m_result_stack.size(), m_result_stack.c_ptr()); - m_result_stack.reset(); } + m_result_stack.reset(); } else { SASSERT(num <= m_result_stack.size()); @@ -240,6 +240,48 @@ struct goal2sat::imp { } } + void convert_and(app * t, bool root, bool sign) { + TRACE("goal2sat", tout << "convert_and:\n" << mk_ismt2_pp(t, m) << "\n";); + unsigned num = t->get_num_args(); + if (root) { + if (sign) { + for (unsigned i = 0; i < num; ++i) { + m_result_stack[i].neg(); + } + } + else { + for (unsigned i = 0; i < num; ++i) { + mk_clause(m_result_stack[i]); + } + } + m_result_stack.reset(); + } + else { + SASSERT(num <= m_result_stack.size()); + sat::bool_var k = m_solver.mk_var(); + sat::literal l(k, false); + m_cache.insert(t, l); + // l => /\ lits + sat::literal * lits = m_result_stack.end() - num; + for (unsigned i = 0; i < num; i++) { + mk_clause(~l, lits[i]); + } + // /\ lits => l + for (unsigned i = 0; i < num; ++i) { + m_result_stack[m_result_stack.size() - num + i].neg(); + } + m_result_stack.push_back(l); + lits = m_result_stack.end() - num - 1; + mk_clause(num+1, lits); + unsigned old_sz = m_result_stack.size() - num - 1; + m_result_stack.shrink(old_sz); + if (sign) + l.neg(); + m_result_stack.push_back(l); + } + } + + void convert_ite(app * n, bool root, bool sign) { unsigned sz = m_result_stack.size(); SASSERT(sz >= 3); @@ -316,6 +358,9 @@ struct goal2sat::imp { case OP_OR: convert_or(t, root, sign); break; + case OP_AND: + convert_and(t, root, sign); + break; case OP_ITE: convert_ite(t, root, sign); break; @@ -456,7 +501,6 @@ struct unsupported_bool_proc { void operator()(app * n) { if (n->get_family_id() == m.get_basic_family_id()) { switch (n->get_decl_kind()) { - case OP_AND: case OP_XOR: case OP_IMPLIES: case OP_DISTINCT: From 2c32e30fed1d6fe10bfa99fe8bc55d1882b67121 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 19 Dec 2016 16:47:28 +0000 Subject: [PATCH 40/42] Build fix for static binaries + shared examples --- scripts/mk_util.py | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index cdd7bdeec..8973da65f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1168,7 +1168,8 @@ class ExeComponent(Component): c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) out.write('\n') - out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile) + extra_opt = '-static' if not IS_WINDOWS and STATIC_BIN else '' + out.write('\t$(LINK) %s $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (extra_opt, exefile)) for obj in objs: out.write(' ') out.write(obj) @@ -2506,10 +2507,7 @@ def mk_config(): config.write('AR_OUTFLAG=\n') config.write('EXE_EXT=\n') config.write('LINK=%s\n' % CXX) - if STATIC_BIN: - config.write('LINK_FLAGS=-static\n') - else: - config.write('LINK_FLAGS=\n') + config.write('LINK_FLAGS=\n') config.write('LINK_OUT_FLAG=-o \n') config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) config.write('SO_EXT=%s\n' % SO_EXT) From 251d1ec031d02d4a56f6253a83e65746f4f3ea03 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 19 Dec 2016 16:58:25 +0000 Subject: [PATCH 41/42] Fix for parallel builds of the OCaml API. Relates to #797. --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8973da65f..235453845 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1973,7 +1973,7 @@ class MLComponent(Component): z3mls = os.path.join(self.sub_dir, 'z3ml') out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso)) out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3)) - out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso)) + out.write('%s.cmxa: %s %s %s %s.cma\n' % (z3mls, cmxs, stubso, z3dllso, z3mls)) out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3)) out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls)) out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls)) From b5aa6d5eb5d9d71a55d51ee2eef5cde952cf3a51 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 19 Dec 2016 22:36:42 +0000 Subject: [PATCH 42/42] Fix issue with bd1f07f864a7f1790cec08a306ccc17507f7e5a8 pointed out by @nunolopes . If `pthread_cond_signal()` is called while `m_mutex` is held then the timing thread might be woken up twice due to waking up from `pthread_cond_timeout()` (due to being signaled) but then being forced to sleep again because the thread calling `~imp()` is still holding `m_mutex` (which the timing thread needs to acquire). --- src/util/scoped_timer.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 3b87f880f..f6b0429d9 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -230,8 +230,9 @@ struct scoped_timer::imp { } pthread_mutex_lock(&m_mutex); m_signal_sent = true; - pthread_cond_signal(&m_cond); pthread_mutex_unlock(&m_mutex); + // Perform signal outside of lock to avoid waking timing thread twice. + pthread_cond_signal(&m_cond); pthread_join(m_thread_id, NULL); pthread_cond_destroy(&m_cond);