mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-04 14:49:41 +00:00
commit bfd836e911
2 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/python/z3.py
View file

@ -8524,11 +8524,11 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(-2.25, FPSort(8, 24)) >>> v = FPVal(-2.25, FPSort(8, 24))
>>> v >>> v
-1.125*(2**1) -1.125*(2**1)
>>> v = FPVal(-0.0, FPSort(8, 24)) >>> FPVal(-0.0, FPSort(8, 24))
-0.0 -0.0
>>> v = FPVal(0.0, FPSort(8, 24)) >>> FPVal(0.0, FPSort(8, 24))
+0.0 +0.0
>>> v = FPVal(+0.0, FPSort(8, 24)) >>> FPVal(+0.0, FPSort(8, 24))
+0.0 +0.0
""" """
ctx = _get_ctx(ctx) ctx = _get_ctx(ctx)
@ -8911,7 +8911,7 @@ def fpNEQ(a, b, ctx=None):
>>> fpNEQ(x, y) >>> fpNEQ(x, y)
Not(fpEQ(x, y)) Not(fpEQ(x, y))
>>> (x != y).sexpr() >>> (x != y).sexpr()
'(not (fp.eq x y))' '(distinct x y)'
""" """
return Not(fpEQ(a, b, ctx)) return Not(fpEQ(a, b, ctx))

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -151,6 +151,7 @@ public:
lbool r = internalize_formulas(); lbool r = internalize_formulas();
if (r != l_true) return r; if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm); r = internalize_assumptions(sz, assumptions, dep2asm);
SASSERT(sz == m_asms.size());
if (r != l_true) return r; if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@ -300,6 +301,7 @@ private:
lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
if (sz == 0) { if (sz == 0) {
m_asms.shrink(0);
return l_true; return l_true;
} }
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
@ -331,6 +333,7 @@ private:
sat::literal lit; sat::literal lit;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
if (dep2asm.find(asms[i], lit)) { if (dep2asm.find(asms[i], lit)) {
SASSERT(lit.var() <= m_solver.num_vars());
m_asms.push_back(lit); m_asms.push_back(lit);
if (i != j && !m_weights.empty()) { if (i != j && !m_weights.empty()) {
m_weights[j] = m_weights[i]; m_weights[j] = m_weights[i];