From fad1e611aa53d4134139b656a123f823906e290c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Jul 2018 12:34:55 -0700 Subject: [PATCH] build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type Signed-off-by: Nikolaj Bjorner --- src/api/api_arith.cpp | 6 ++-- src/api/dotnet/Expr.cs | 4 +-- src/api/java/Expr.java | 4 +-- src/api/z3_api.h | 4 +-- src/smt/theory_seq.cpp | 6 ++-- src/smt/theory_seq.h | 2 +- src/tactic/core/reduce_invertible_tactic.cpp | 29 ++++++++++++++++++-- src/test/bdd.cpp | 4 +-- 8 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index cc1ccf59e..524d9393d 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -119,10 +119,10 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { + int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { LOG_Z3_is_algebraic_number(c, a); - Z3_bool r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? Z3_TRUE : Z3_FALSE; - IF_VERBOSE(10, verbose_stream() << r << "\n"); + int r = mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)) ? 1 : 0; + //IF_VERBOSE(10, verbose_stream() << r << "\n"); return r; } diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 1e0f495f5..942baffab 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -239,7 +239,7 @@ namespace Microsoft.Z3 /// public bool IsAlgebraicNumber { - get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } + get { return 0 != Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } } #endregion @@ -1823,7 +1823,7 @@ namespace Microsoft.Z3 Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); if ( // Z3_sort_kind.Z3_REAL_SORT == sk && - Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? + 0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index db5c33e79..75ec9aa75 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -275,7 +275,7 @@ public class Expr extends AST **/ public boolean isAlgebraicNumber() { - return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); + return 0 != Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject()); } /** @@ -2108,7 +2108,7 @@ public class Expr extends AST Z3_sort_kind sk = Z3_sort_kind .fromInt(Native.getSortKind(ctx.nCtx(), s)); - if (Native.isAlgebraicNumber(ctx.nCtx(), obj)) // is this a numeral ast? + if (Native.isAlgebraicNumber(ctx.nCtx(), obj) != 0) // is this a numeral ast? return new AlgebraicNum(ctx, obj); if (Native.isNumeralAst(ctx.nCtx(), obj)) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7e12f2fa7..74f0fd254 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4397,9 +4397,9 @@ extern "C" { /** \brief Return true if the given AST is a real algebraic number. - def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST))) + def_API('Z3_is_algebraic_number', INT, (_in(CONTEXT), _in(AST))) */ - Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); + int Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a); /** \brief Convert an \c ast into an \c APP_AST. This is just type casting. diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 40aae8043..c2c3b1cfb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -199,6 +199,9 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_reset_cache(false), m_eq_id(0), m_find(*this), + m_overlap(m), + m_overlap2(m), + m_len_prop_lvl(-1), m_factory(nullptr), m_exclude(m), m_axioms(m), @@ -216,9 +219,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_atoms_qhead(0), m_new_solution(false), m_new_propagation(false), - m_len_prop_lvl(-1), - m_overlap(m), - m_overlap2(m), m_mk_aut(m) { m_prefix = "seq.p.suffix"; m_suffix = "seq.s.prefix"; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f32b6254b..f03bdeb60 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -50,7 +50,6 @@ namespace smt { class seq_value_proc; - theory_seq_params const & m_params; // cache to track evaluations under equalities class eval_cache { @@ -295,6 +294,7 @@ namespace smt { typedef hashtable rational_set; ast_manager& m; + theory_seq_params const& m_params; dependency_manager m_dm; solution_map m_rep; // unification representative. bool m_reset_cache; // invalidate cache. diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 13af1f376..75b8cae0c 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -258,17 +258,37 @@ private: rest = arg; } if (!rest) return false; - expr_ref zero(m_arith.mk_numeral(rational::zero(), false), m); + expr_ref zero(m_arith.mk_real(0), m); new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v); if (mc) { ensure_mc(mc); expr_ref def(m_arith.mk_div(v, rest), m); (*mc)->add(v, def); } - return true; + return true; } + expr* e1 = nullptr, *e2 = nullptr; + + // t / v -> if t = 0 then 0 else v + // inverse: t = 0 then 1 else v / t + if (m_arith.is_div(p, e1, e2) && e2 == v) { + expr_ref zero(m_arith.mk_real(0), m); + new_v = m.mk_ite(m.mk_eq(zero, e1), zero, v); + if (mc) { + ensure_mc(mc); + expr_ref def(m.mk_ite(m.mk_eq(zero, e1), m_arith.mk_real(1), m_arith.mk_div(e1, v)), m); + (*mc)->add(v, def); + } + return true; + } + + // v / t unless t != 0 + if (m_arith.is_div(p, e1, e2) && e1 == v) { + return false; + } + if (m.is_eq(p, e1, e2)) { if (mc && has_diagonal(e1)) { ensure_mc(mc); @@ -294,12 +314,15 @@ private: bool has_diagonal(expr* e) { return m_bv.is_bv(e) || - m.is_bool(e); + m.is_bool(e) || + m_arith.is_int_real(e); } expr * mk_diagonal(expr* e) { if (m_bv.is_bv(e)) return m_bv.mk_bv_neg(e); if (m.is_bool(e)) return m.mk_not(e); + if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e); + if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e); UNREACHABLE(); return e; } diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index ea5a0bc34..423142557 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -30,8 +30,8 @@ namespace sat { SASSERT(m.mk_ite(v1,v0,v0) == v0); SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); - SASSERT(!(v0 && v1) == (!v0 || !v1)); - SASSERT(!(v0 || v1) == (!v0 && !v1)); + SASSERT((!(v0 && v1)) == (!v0 || !v1)); + SASSERT((!(v0 || v1)) == (!v0 && !v1)); } static void test3() {