From 8e2ad4e461a4469d345a7b93b17f6acb23e64d38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Jul 2019 06:20:24 +0700 Subject: [PATCH] #2379 and #2380 Signed-off-by: Nikolaj Bjorner --- cmake/msvc_legacy_quirks.cmake | 3 +++ scripts/mk_util.py | 3 +++ src/muz/fp/dl_cmds.cpp | 3 --- src/qe/nlqsat.cpp | 42 ++++++++++++++++++++++++++-------- src/smt/theory_arith.h | 1 + src/smt/theory_arith_core.h | 25 ++++++++++++++++---- src/smt/theory_seq.cpp | 16 ++++++------- 7 files changed, 68 insertions(+), 25 deletions(-) diff --git a/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake index d34351c1d..09ee90d2a 100644 --- a/cmake/msvc_legacy_quirks.cmake +++ b/cmake/msvc_legacy_quirks.cmake @@ -182,5 +182,8 @@ foreach (_build_type ${_build_types_as_upper}) # Indicate that the executable is compatible with DEP # See https://msdn.microsoft.com/en-us/library/ms235442.aspx string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT") + + # per GitHub issue #2380, enable checksum + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /RELEASE") endif() endforeach() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 54ad7f6d8..398aafca0 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -98,6 +98,7 @@ JS_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False STATIC_BIN=False +ADD_CHECKSUM=True VER_MAJOR=None VER_MINOR=None VER_BUILD=None @@ -2441,6 +2442,8 @@ def mk_config(): static_opt = '/MT' else: static_opt = '/MD' + if ADD_CHECKSUM: + extra_opt = ' %s /RELEASE' % extra_opt maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO' if DEBUG_MODE: static_opt = static_opt + 'd' diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 811511050..651509bd8 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -344,9 +344,6 @@ private: expr_ref query_result(dlctx.get_answer_as_formula(), m); sbuffer var_names; unsigned num_decls = 0; - if (is_quantifier(m_target)) { - num_decls = to_quantifier(m_target)->get_num_decls(); - } ctx.display(ctx.regular_stream(), query_result, 0, num_decls, "X", var_names); ctx.regular_stream() << std::endl; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index a37aef052..87dd69f9d 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -86,6 +86,7 @@ namespace qe { nlsat::literal_vector m_assumptions; u_map m_asm2fml; expr_ref_vector m_trail; + app_ref m_delta0, m_delta1; lbool check_sat() { while (true) { @@ -511,6 +512,20 @@ namespace qe { bool has_divs() const { return m_has_divs; } }; + /* + Ackermanize division + + For each p/q: + p = 0 & q = 0 => div = delta0 + p != 0 & q = 0 => div = p*delta1 + q != 0 => div*q = p + + delta0 stands for 0/0 + delta1 stands for 1/0 + assumption: p * 1/0 = p/0 for p != 0, + so 2/0 != a * 1/0 & a = 2 is unsat by fiat. + */ + void purify(expr_ref& fml, div_rewriter_star& rw, expr_ref_vector& paxioms) { is_pure_proc is_pure(*this); { @@ -520,14 +535,16 @@ namespace qe { if (is_pure.has_divs()) { arith_util arith(m); proof_ref pr(m); - TRACE("qe", tout << fml << "\n";); rw(fml, fml, pr); - TRACE("qe", tout << fml << "\n";); + m_delta0 = m.mk_fresh_const("delta0", arith.mk_real()); + m_delta1 = m.mk_fresh_const("delta1", arith.mk_real()); vector
const& divs = rw.divs(); for (unsigned i = 0; i < divs.size(); ++i) { - paxioms.push_back( - m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)), - m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); + expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m); + expr_ref num_is0(m.mk_eq(divs[i].num, arith.mk_real(0)), m); + paxioms.push_back(m.mk_or(den_is0, m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); + paxioms.push_back(m.mk_or(m.mk_not(den_is0), m.mk_not(num_is0), m.mk_eq(divs[i].name, m_delta0))); + paxioms.push_back(m.mk_or(m.mk_not(den_is0), num_is0, m.mk_eq(divs[i].name, arith.mk_mul(divs[i].num, m_delta1)))); for (unsigned j = i + 1; j < divs.size(); ++j) { paxioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)), m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), @@ -546,6 +563,8 @@ namespace qe { return; } expr_ref ante = mk_and(paxioms); + qvars[0].push_back(m_delta0); + qvars[0].push_back(m_delta1); for (div const& d : rw.divs()) { qvars[qvars.size()-2].push_back(d.name); } @@ -555,6 +574,7 @@ namespace qe { else { fml = m.mk_and(fml, ante); } + TRACE("qe", tout << fml << "\n";); } @@ -675,6 +695,7 @@ namespace qe { if (m_a2b.is_var(v)) { SASSERT(m.is_bool(v)); nlsat::bool_var b = m_a2b.to_var(v); + TRACE("qe", tout << mk_pp(v, m) << " |-> b" << b << "\n";); m_bound_bvars.back().push_back(b); set_level(b, lvl); } @@ -703,14 +724,13 @@ namespace qe { } void init_expr2var(vector const& qvars) { - for (unsigned i = 0; i < qvars.size(); ++i) { - init_expr2var(qvars[i]); + for (app_ref_vector const& qvs : qvars) { + init_expr2var(qvs); } } void init_expr2var(app_ref_vector const& qvars) { - for (unsigned i = 0; i < qvars.size(); ++i) { - app* v = qvars[i]; + for (app* v : qvars) { if (m.is_bool(v)) { m_a2b.insert(v, m_solver.mk_bool_var()); } @@ -784,7 +804,9 @@ namespace qe { m_cancel(false), m_answer(m), m_answer_simplify(m), - m_trail(m) + m_trail(m), + m_delta0(m), + m_delta1(m) { m_solver.get_explain().set_signed_project(true); m_nftactic = mk_tseitin_cnf_tactic(m); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 384b44de7..4d66c8387 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -603,6 +603,7 @@ namespace smt { theory_var internalize_to_int(app * n); void internalize_is_int(app * n); theory_var internalize_numeral(app * n); + theory_var internalize_numeral(app * n, numeral const& val); theory_var internalize_term_core(app * n); void mk_axiom(expr * n1, expr * n2, bool simplify_conseq = true); void mk_idiv_mod_axioms(expr * dividend, expr * divisor); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 398bc3b3d..c1c1dbeab 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -240,12 +240,23 @@ namespace smt { return; } } - rational _val; + rational _val1, _val2; expr* arg1, *arg2; - if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val) && is_app(arg1) && is_app(arg2)) { + if (m_util.is_mul(m, arg1, arg2) && m_util.is_numeral(arg1, _val1) && is_app(arg1) && is_app(arg2)) { SASSERT(m->get_num_args() == 2); - numeral val(_val); - theory_var v = internalize_term_core(to_app(arg2)); + if (m_util.is_numeral(arg2, _val2)) { + numeral val(_val1 + _val2); + theory_var v = internalize_numeral(m, val); + if (reflection_enabled()) { + internalize_term_core(to_app(arg1)); + internalize_term_core(to_app(arg2)); + mk_enode(m); + } + add_row_entry(r_id, numeral::one(), v); + return; + } + numeral val(_val1); + theory_var v = internalize_term_core(to_app(arg2)); if (reflection_enabled()) { internalize_term_core(to_app(arg1)); mk_enode(m); @@ -329,6 +340,7 @@ namespace smt { theory_var theory_arith::internalize_mul(app * m) { rational _val; SASSERT(m_util.is_mul(m)); + SASSERT(!m_util.is_numeral(m->get_arg(1))); if (m_util.is_numeral(m->get_arg(0), _val)) { SASSERT(m->get_num_args() == 2); numeral val(_val); @@ -713,6 +725,11 @@ namespace smt { rational _val; VERIFY(m_util.is_numeral(n, _val)); numeral val(_val); + return internalize_numeral(n, val); + } + + template + theory_var theory_arith::internalize_numeral(app * n, numeral const& val) { SASSERT(!get_context().e_internalized(n)); enode * e = mk_enode(n); // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5852992da..e51082ab7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5923,10 +5923,11 @@ void theory_seq::propagate_not_suffix(expr* e) { e1 < e2 => e1 = empty or e1 = xcy e1 < e2 => e1 = empty or c < d e1 < e2 => e2 = xdz - !(e1 < e2) => e1 = e2 or e2 = empty or e2 = xcy - !(e1 < e2) => e1 = e2 or e2 = empty or c < d - !(e1 < e2) => e1 = e2 or e1 = xdz + !(e1 < e2) => e1 = e2 or e2 = empty or e2 = xdz + !(e1 < e2) => e1 = e2 or e2 = empty or d < c + !(e1 < e2) => e1 = e2 or e1 = xcy +optional: e1 < e2 or e1 = e2 or e2 < e1 !(e1 = e2) or !(e1 < e2) !(e1 = e2) or !(e2 < e1) @@ -5952,15 +5953,14 @@ void theory_seq::add_lt_axiom(expr* n) { literal eq = mk_eq(e1, e2, false); literal e1xcy = mk_eq(e1, xcy, false); literal e2xdz = mk_eq(e2, xdz, false); - literal e2xcy = mk_eq(e2, xcy, false); - literal e1xdz = mk_eq(e1, xdz, false); literal ltcd = mk_literal(m_util.mk_lt(c, d)); + literal ltdc = mk_literal(m_util.mk_lt(d, c)); add_axiom(~lt, e2xdz); add_axiom(~lt, emp1, e1xcy); add_axiom(~lt, emp1, ltcd); - add_axiom(lt, eq, e1xdz); - add_axiom(lt, eq, emp2, ltcd); - add_axiom(lt, eq, emp2, e2xcy); + add_axiom(lt, eq, e1xcy); + add_axiom(lt, eq, emp2, ltdc); + add_axiom(lt, eq, emp2, e2xdz); if (e1->get_id() <= e2->get_id()) { literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1)); add_axiom(lt, eq, gt);