mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

merge

Browse source
This commit is contained in:
Ken McMillan 2015-04-03 11:25:43 -07:00
commit d797b0c285
11 changed files with 127 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/dotnet/ASTVector.cs
View file

@ -25,7 +25,7 @@ namespace Microsoft.Z3
/// <summary>
/// Vectors of ASTs.
/// </summary>
internal class ASTVector : Z3Object
public class ASTVector : Z3Object
{
/// <summary>
/// The size of the vector

6
src/api/dotnet/InterpolationContext.cs
View file

@ -13,7 +13,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the C/C++ API, which is well documented.</remarks>
[ContractVerification(true)]
class InterpolationContext : Context
public class InterpolationContext : Context
{
/// <summary>
@ -47,7 +47,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_get_interpolant in the C/C++ API, which is
/// well documented.</remarks>
Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
{
Contract.Requires(pf != null);
Contract.Requires(pat != null);
@ -72,7 +72,7 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_compute_interpolant in the C/C++ API, which is
/// well documented.</remarks>
Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
{
Contract.Requires(pat != null);
Contract.Requires(p != null);

2
src/api/java/ASTVector.java
View file

@ -20,7 +20,7 @@ package com.microsoft.z3;
/**
* Vectors of ASTs.
**/
class ASTVector extends Z3Object
public class ASTVector extends Z3Object
{
/**
* The size of the vector

4
src/api/java/InterpolationContext.java
View file

@ -73,7 +73,7 @@ public class InterpolationContext extends Context
* well documented.
* @throws Z3Exception
**/
Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
public Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
{
checkContextMatch(pf);
checkContextMatch(pat);
@ -94,7 +94,7 @@ public class InterpolationContext extends Context
* well documented.
* @throws Z3Exception
**/
Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
public Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
{
checkContextMatch(pat);
checkContextMatch(p);

72
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1837,7 +1837,10 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_neg(args[0], result);
expr_ref t1(m), t2(m);
mk_is_nan(args[0], t1);
mk_is_neg(args[0], t2);
result = m.mk_and(m.mk_not(t1), t2);
TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
}
@ -2104,6 +2107,64 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_fp(sgn, e, s, result);
}
else if (m_util.au().is_numeral(x)) {
rational q;
bool is_int;
m_util.au().is_numeral(x, q, is_int);
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn);
mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz);
scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager);
scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager);
m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq());
m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq());
m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq());
m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq());
m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq());
expr_ref v1(m), v2(m), v3(m), v4(m);
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v1);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v2);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v3);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v4);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, result);
mk_ite(rm_tn, v4, result, result);
mk_ite(rm_tp, v3, result, result);
mk_ite(rm_nte, v2, result, result);
mk_ite(rm_nta, v1, result, result);
}
else {
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2952,11 +3013,16 @@ void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
}
void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp;
expr * sgn, *sig, *exp;
split_fp(e, sgn, exp, sig);
expr_ref zero(m);
expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
m_simp.mk_eq(exp, zero, result);
m_simp.mk_eq(exp, zero, zexp);
mk_is_zero(e, is_zero);
m_simp.mk_not(is_zero, n_is_zero);
m_simp.mk_and(n_is_zero, zexp, result);
}
void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {

20
src/smt/asserted_formulas.cpp
View file

@ -603,11 +603,11 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager);
unsigned i = 0;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
for (unsigned i = 0; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
if (m_manager.is_eq(n)) {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
@ -615,9 +615,11 @@ void asserted_formulas::propagate_values() {
if (m_manager.is_value(lhs))
std::swap(lhs, rhs);
if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
new_exprs1.push_back(n);
if (m_manager.proofs_enabled())
new_prs1.push_back(pr);
if (i >= m_asserted_qhead) {
new_exprs1.push_back(n);
if (m_manager.proofs_enabled())
new_prs1.push_back(pr);
}
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";);
m_simplifier.cache_result(lhs, rhs, pr);
found = true;
@ -625,9 +627,11 @@ void asserted_formulas::propagate_values() {
}
}
}
new_exprs2.push_back(n);
if (m_manager.proofs_enabled())
new_prs2.push_back(pr);
if (i >= m_asserted_qhead) {
new_exprs2.push_back(n);
if (m_manager.proofs_enabled())
new_prs2.push_back(pr);
}
}
TRACE("propagate_values", tout << "found: " << found << "\n";);
// If C is not empty, then reduce R using the updated simplifier cache with entries

4
src/util/mpf.cpp
View file

@ -1350,11 +1350,11 @@ bool mpf_manager::is_ninf(mpf const & x) {
}
bool mpf_manager::is_normal(mpf const & x) {
return !has_bot_exp(x) && !has_top_exp(x);
return !(has_top_exp(x) || is_denormal(x));
}
bool mpf_manager::is_denormal(mpf const & x) {
return has_bot_exp(x);
return !is_zero(x) && has_bot_exp(x);
}
bool mpf_manager::is_int(mpf const & x) {