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<symbol> 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<expr*> 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<div> 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<app_ref_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<true>(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<Ext>::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<typename Ext>
+ theory_var theory_arith<Ext>::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);