From e13bf2424e9641fb9e0c38ed626ebad8239a1723 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 08:29:24 -0700 Subject: [PATCH 1/6] fix type checking for non-associative basic operations, fixes issue #160 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 59efb2a89..2881f1b62 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2 } app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { - if (decl->get_arity() != num_args && !decl->is_right_associative() && - !decl->is_left_associative() && !decl->is_chainable()) { + bool type_error = + decl->get_arity() != num_args && !decl->is_right_associative() && + !decl->is_left_associative() && !decl->is_chainable(); + + type_error |= (decl->get_arity() != num_args && num_args < 2 && + decl->get_family_id() == m_basic_family_id && !decl->is_associative()); + + if (type_error) { std::ostringstream buffer; buffer << "Wrong number of arguments (" << num_args << ") passed to function " << mk_pp(decl, *this); From 96c8b1e7ffc4b9d55f6ac20fa0e117c2d636366d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 12:44:07 -0700 Subject: [PATCH 2/6] fixup model construction on undef results for arithmetic. Fixes issue #161 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 1 + src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 +- src/smt/theory_arith_aux.h | 6 +++--- src/smt/theory_arith_core.h | 4 ++++ 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 9d1f4343f..5245b9685 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -417,6 +417,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) { app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { if (is_int && !val.is_int()) { + SASSERT(false); m_manager->raise_exception("invalid rational value passed as an integer"); } if (val.is_unsigned()) { diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 98b7592c8..622d67a34 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -125,7 +125,7 @@ protected: m_solver.assert_expr(fml1); lbool is_sat = m_solver.check(); TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";); - if (is_sat != l_false) { + if (is_sat == l_true) { TRACE("ctx_solver_simplify_tactic", tout << "result is not equivalent to input\n"; tout << mk_pp(fml1, m) << "\n";); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 397f6683b..ebdd1386c 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1479,9 +1479,9 @@ namespace smt { SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(min_gain.is_minus_one() || !min_gain.is_neg()); - SASSERT(!is_int(x_i) || min_gain.is_pos()); - SASSERT(!is_int(x_i) || min_gain.is_int()); - SASSERT(!is_int(x_i) || max_gain.is_int()); + //SASSERT(!is_int(x_i) || min_gain.is_pos()); + //SASSERT(!is_int(x_i) || min_gain.is_int()); + //SASSERT(!is_int(x_i) || max_gain.is_int()); return is_tighter; } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 2b91452a9..c47585606 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3065,6 +3065,10 @@ namespace smt { SASSERT(v != null_theory_var); inf_numeral const & val = get_value(v); rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); + if (is_int(v) && !num.is_int()) { + TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";); + num = floor(num); + } return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); } From 6e22250d1a3486d760bb539b4b77710d8901a9f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Jul 2015 12:44:55 -0700 Subject: [PATCH 3/6] fixup model construction on undef results for arithmetic. Fixes issue #161 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 5245b9685..9d1f4343f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -417,7 +417,6 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) { app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { if (is_int && !val.is_int()) { - SASSERT(false); m_manager->raise_exception("invalid rational value passed as an integer"); } if (val.is_unsigned()) { From f9e2ad76fa9622305b3579c84210d6ee4273ee46 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Jul 2015 12:05:45 -0700 Subject: [PATCH 4/6] Bugfix for fp.to_sbv Fixes #114. --- src/ast/fpa/fpa2bv_converter.cpp | 8 ++++---- src/ast/fpa_decl_plugin.cpp | 1 - 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index baba7b701..389f785ab 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2975,7 +2975,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_zero_extend(2, lz)); shift = m_bv_util.mk_bv_sub(exp_m_lz, - m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); + m_bv_util.mk_numeral(bv_sz, ebits + 2)); shift_neg = m_bv_util.mk_bv_neg(shift); bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift); @@ -2987,8 +2987,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // [1][ ... sig ... ][r][g][ ... s ...] // [ ... ubv ... ][r][g][ ... s ... ] - expr_ref max_shift(m); - max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); + // expr_ref max_shift(m); + // max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); @@ -3440,7 +3440,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result) void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { #ifdef Z3DEBUG - return; + // return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); new_e = m.mk_fresh_const(prefix, m.get_sort(e)); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 0b28c4277..c59480ee2 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -629,7 +629,6 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par symbol name("fp.to_sbv"); sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters); return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters)); - } func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, From 5f755a5bd8c2e88f4635b77cec352c1dcd114662 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Jul 2015 13:07:16 -0700 Subject: [PATCH 5/6] Adjusted return types of set functions to ArrayExprs in Java and .NET Fixes #137 --- src/api/dotnet/Context.cs | 36 +++++++++++++++--------------- src/api/java/Context.java | 47 +++++++++++++++++---------------------- 2 files changed, 38 insertions(+), 45 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index eaf4e4777..0aee3f7d8 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2134,31 +2134,31 @@ namespace Microsoft.Z3 /// /// Create an empty set. /// - public Expr MkEmptySet(Sort domain) + public ArrayExpr MkEmptySet(Sort domain) { Contract.Requires(domain != null); Contract.Ensures(Contract.Result() != null); CheckContextMatch(domain); - return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject)); } /// /// Create the full set. /// - public Expr MkFullSet(Sort domain) + public ArrayExpr MkFullSet(Sort domain) { Contract.Requires(domain != null); Contract.Ensures(Contract.Result() != null); CheckContextMatch(domain); - return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject)); } /// /// Add an element to the set. /// - public Expr MkSetAdd(Expr set, Expr element) + public ArrayExpr MkSetAdd(ArrayExpr set, Expr element) { Contract.Requires(set != null); Contract.Requires(element != null); @@ -2166,14 +2166,14 @@ namespace Microsoft.Z3 CheckContextMatch(set); CheckContextMatch(element); - return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject)); } /// /// Remove an element from a set. /// - public Expr MkSetDel(Expr set, Expr element) + public ArrayExpr MkSetDel(ArrayExpr set, Expr element) { Contract.Requires(set != null); Contract.Requires(element != null); @@ -2181,38 +2181,38 @@ namespace Microsoft.Z3 CheckContextMatch(set); CheckContextMatch(element); - return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject)); } /// /// Take the union of a list of sets. /// - public Expr MkSetUnion(params Expr[] args) + public ArrayExpr MkSetUnion(params ArrayExpr[] args) { Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); CheckContextMatch(args); - return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } /// /// Take the intersection of a list of sets. /// - public Expr MkSetIntersection(params Expr[] args) + public ArrayExpr MkSetIntersection(params ArrayExpr[] args) { Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); Contract.Ensures(Contract.Result() != null); CheckContextMatch(args); - return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); } /// /// Take the difference between two sets. /// - public Expr MkSetDifference(Expr arg1, Expr arg2) + public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2) { Contract.Requires(arg1 != null); Contract.Requires(arg2 != null); @@ -2220,25 +2220,25 @@ namespace Microsoft.Z3 CheckContextMatch(arg1); CheckContextMatch(arg2); - return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject)); } /// /// Take the complement of a set. /// - public Expr MkSetComplement(Expr arg) + public ArrayExpr MkSetComplement(ArrayExpr arg) { Contract.Requires(arg != null); Contract.Ensures(Contract.Result() != null); CheckContextMatch(arg); - return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject)); + return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject)); } /// /// Check for set membership. /// - public BoolExpr MkSetMembership(Expr elem, Expr set) + public BoolExpr MkSetMembership(Expr elem, ArrayExpr set) { Contract.Requires(elem != null); Contract.Requires(set != null); @@ -2252,7 +2252,7 @@ namespace Microsoft.Z3 /// /// Check for subsetness of sets. /// - public BoolExpr MkSetSubset(Expr arg1, Expr arg2) + public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2) { Contract.Requires(arg1 != null); Contract.Requires(arg2 != null); diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b2d77e792..bec5da024 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1725,32 +1725,31 @@ public class Context extends IDisposable /** * Create an empty set. **/ - public Expr mkEmptySet(Sort domain) + public ArrayExpr mkEmptySet(Sort domain) { checkContextMatch(domain); - return Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkEmptySet(nCtx(), domain.getNativeObject())); } /** * Create the full set. **/ - public Expr mkFullSet(Sort domain) + public ArrayExpr mkFullSet(Sort domain) { checkContextMatch(domain); - return Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkFullSet(nCtx(), domain.getNativeObject())); } /** * Add an element to the set. **/ - public Expr mkSetAdd(Expr set, Expr element) + public ArrayExpr mkSetAdd(ArrayExpr set, Expr element) { checkContextMatch(set); checkContextMatch(element); - return Expr.create( - this, + return (ArrayExpr)Expr.create(this, Native.mkSetAdd(nCtx(), set.getNativeObject(), element.getNativeObject())); } @@ -1758,12 +1757,11 @@ public class Context extends IDisposable /** * Remove an element from a set. **/ - public Expr mkSetDel(Expr set, Expr element) + public ArrayExpr mkSetDel(ArrayExpr set, Expr element) { checkContextMatch(set); checkContextMatch(element); - return Expr.create( - this, + return (ArrayExpr)Expr.create(this, Native.mkSetDel(nCtx(), set.getNativeObject(), element.getNativeObject())); } @@ -1771,11 +1769,10 @@ public class Context extends IDisposable /** * Take the union of a list of sets. **/ - public Expr mkSetUnion(Expr... args) + public ArrayExpr mkSetUnion(ArrayExpr... args) { checkContextMatch(args); - return Expr.create( - this, + return (ArrayExpr)Expr.create(this, Native.mkSetUnion(nCtx(), (int) args.length, AST.arrayToNative(args))); } @@ -1783,11 +1780,10 @@ public class Context extends IDisposable /** * Take the intersection of a list of sets. **/ - public Expr mkSetIntersection(Expr... args) + public ArrayExpr mkSetIntersection(ArrayExpr... args) { checkContextMatch(args); - return Expr.create( - this, + return (ArrayExpr)Expr.create(this, Native.mkSetIntersect(nCtx(), (int) args.length, AST.arrayToNative(args))); } @@ -1795,12 +1791,11 @@ public class Context extends IDisposable /** * Take the difference between two sets. **/ - public Expr mkSetDifference(Expr arg1, Expr arg2) + public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2) { checkContextMatch(arg1); checkContextMatch(arg2); - return Expr.create( - this, + return (ArrayExpr)Expr.create(this, Native.mkSetDifference(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } @@ -1808,22 +1803,21 @@ public class Context extends IDisposable /** * Take the complement of a set. **/ - public Expr mkSetComplement(Expr arg) + public ArrayExpr mkSetComplement(ArrayExpr arg) { checkContextMatch(arg); - return Expr.create(this, + return (ArrayExpr)Expr.create(this, Native.mkSetComplement(nCtx(), arg.getNativeObject())); } /** * Check for set membership. **/ - public BoolExpr mkSetMembership(Expr elem, Expr set) + public BoolExpr mkSetMembership(Expr elem, ArrayExpr set) { checkContextMatch(elem); checkContextMatch(set); - return (BoolExpr) Expr.create( - this, + return (BoolExpr) Expr.create(this, Native.mkSetMember(nCtx(), elem.getNativeObject(), set.getNativeObject())); } @@ -1831,12 +1825,11 @@ public class Context extends IDisposable /** * Check for subsetness of sets. **/ - public BoolExpr mkSetSubset(Expr arg1, Expr arg2) + public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2) { checkContextMatch(arg1); checkContextMatch(arg2); - return (BoolExpr) Expr.create( - this, + return (BoolExpr) Expr.create(this, Native.mkSetSubset(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); } From 1bad61464650e681727d7225e0914ddb845a08ef Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Jul 2015 13:09:00 -0700 Subject: [PATCH 6/6] Fixed .equals for AST, FuncDecl, and Sort, and AST.compareTo in Java Fixes #143 --- src/api/java/AST.java | 15 +++++++++------ src/api/java/FuncDecl.java | 23 ++++++----------------- src/api/java/Sort.java | 9 ++++++--- 3 files changed, 21 insertions(+), 26 deletions(-) diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 436a9fdcb..6b5493bf9 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -22,10 +22,8 @@ import com.microsoft.z3.enumerations.Z3_ast_kind; /** * The abstract syntax tree (AST) class. **/ -public class AST extends Z3Object +public class AST extends Z3Object implements Comparable { - /* Overloaded operators are not translated. */ - /** * Object comparison. * @@ -35,7 +33,7 @@ public class AST extends Z3Object { AST casted = null; - try + try { casted = AST.class.cast(o); } catch (ClassCastException e) @@ -43,8 +41,13 @@ public class AST extends Z3Object return false; } - return this.getNativeObject() == casted.getNativeObject(); - } + return + (this == casted) || + (this != null) && + (casted != null) && + (getContext().nCtx() == casted.getContext().nCtx()) && + (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject())); +} /** * Object Comparison. diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 28cdf2a2d..bc2baab91 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind; **/ public class FuncDecl extends AST { - /** - * Comparison operator. - * - * @return True if {@code a"/> and and