From 4f72e1d5289b5afce868377a286e7f325f65e0f0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Jun 2013 12:14:14 +0100 Subject: [PATCH 1/4] FPA: avoid compiler warnings. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 234c343b8..ff24d1ceb 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -2437,7 +2437,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & t = m_bv_util.mk_bv_sub(t, lz); t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); expr_ref TINY(m); - TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2)); + TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2)); TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); SASSERT(is_well_sorted(m, TINY)); @@ -2481,7 +2481,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); - sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); + sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size)); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size)); From d9941c0ccc871881d4bbc1625bfdc005d4618ae8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Jun 2013 19:21:27 -0700 Subject: [PATCH 2/4] Add code for rejecting bitvector constants of size 0 Signed-off-by: Leonardo de Moura --- src/ast/bv_decl_plugin.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 8b77244f9..f1c61619a 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -210,6 +210,10 @@ func_decl * bv_decl_plugin::mk_unary(ptr_vector & decls, decl_kind k, func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain) { + if (bv_size == 0) { + m_manager->raise_exception("bit-vector size must be greater than zero"); + } + force_ptr_array_size(m_int2bv, bv_size + 1); if (arity != 1) { @@ -415,6 +419,9 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const return 0; } unsigned bv_size = parameters[1].get_int(); + if (bv_size == 0) { + m_manager->raise_exception("bit-vector size must be greater than zero"); + } // TODO: sign an error if the parameters[0] is out of range, that is, it is a value not in [0, 2^{bv_size}) // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals. // After SMT-COMP, I should find all offending modules. From 210bca8f456361f696152be909e33a4e8b58607f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jul 2013 12:57:54 +0100 Subject: [PATCH 3/4] .NET Example: Sudoku example bugfix. Many thanks to Ilya Mironov for reporting this issue. Signed-off-by: Christoph M. Wintersteiger --- examples/dotnet/Program.cs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 2085de296..4361cab96 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -474,7 +474,7 @@ namespace test_mapi cells_c[i] = new BoolExpr[9]; for (uint j = 0; j < 9; j++) cells_c[i][j] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), X[i][j]), - ctx.MkLe(X[i][j], ctx.MkInt(9))); + ctx.MkLe(X[i][j], ctx.MkInt(9))); } // each row contains a digit at most once @@ -485,7 +485,13 @@ namespace test_mapi // each column contains a digit at most once BoolExpr[] cols_c = new BoolExpr[9]; for (uint j = 0; j < 9; j++) - cols_c[j] = ctx.MkDistinct(X[j]); + { + IntExpr[] column = new IntExpr[9]; + for (uint i = 0; i < 9; i++) + column[i] = X[i][j]; + + cols_c[j] = ctx.MkDistinct(column); + } // each 3x3 square contains a digit at most once BoolExpr[][] sq_c = new BoolExpr[3][]; @@ -2087,7 +2093,7 @@ namespace test_mapi { QuantifierExample3(ctx); QuantifierExample4(ctx); - } + } Log.Close(); if (Log.isOpen()) From ccb36f1ae7121a895c75500998a9d6e219108e0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Jul 2013 08:22:17 -0700 Subject: [PATCH 4/4] Fix issue https://z3.codeplex.com/workitem/54 Signed-off-by: Leonardo de Moura --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a255c2d97..6f745d620 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1305,7 +1305,7 @@ namespace z3 { expr as_expr() const { unsigned n = size(); if (n == 0) - return ctx().bool_val(false); + return ctx().bool_val(true); else if (n == 1) return operator[](0); else {