From cb75a55095bc33cce8da48d9f80910e36f90c3d8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Jan 2017 13:41:08 +0000 Subject: [PATCH 1/2] Fixed initialization order warning. --- src/sat/sat_config.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 58505f8ac..7e0a7c50c 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -23,10 +23,10 @@ Revision History: namespace sat { config::config(params_ref const & p): + m_restart_max(0), m_always_true("always_true"), m_always_false("always_false"), m_caching("caching"), - m_restart_max(0), m_random("random"), m_geometric("geometric"), m_luby("luby"), From ae9a3bfc241ce9490d74aa8af4916195deadfe81 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Jan 2017 09:14:09 -0800 Subject: [PATCH 2/2] add operator for issue #860 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 3 ++- src/api/dotnet/Solver.cs | 9 +++++++++ src/api/z3_api.h | 1 + 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index efa3ec098..08a931fdc 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1063,9 +1063,10 @@ extern "C" { case OP_BV2INT: return Z3_OP_BV2INT; case OP_CARRY: return Z3_OP_CARRY; case OP_XOR3: return Z3_OP_XOR3; + case OP_BIT2BOOL: return Z3_OP_BIT2BOOL; case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; - case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; + case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; case OP_BSDIV_I: return Z3_OP_BSDIV_I; case OP_BUDIV_I: return Z3_OP_BUDIV_I; case OP_BSREM_I: return Z3_OP_BSREM_I; diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 8cb7670d7..dff2677df 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -18,6 +18,7 @@ Notes: --*/ using System; +using System.Linq; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -126,6 +127,14 @@ namespace Microsoft.Z3 Assert(constraints); } + /// + /// Alias for Assert. + /// + public void Add(IEnumerable constraints) + { + Assert(constraints.ToArray()); + } + /// /// Assert multiple constraints into the solver, and track them (in the unsat) core /// using the Boolean constants in ps. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 356f933d4..b80ce3177 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1060,6 +1060,7 @@ typedef enum { Z3_OP_EXT_ROTATE_LEFT, Z3_OP_EXT_ROTATE_RIGHT, + Z3_OP_BIT2BOOL, Z3_OP_INT2BV, Z3_OP_BV2INT, Z3_OP_CARRY,