From 1f2346073a79eb144199fe4c4c389dac16f5cba0 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Mon, 11 Jul 2022 18:24:03 +0200 Subject: [PATCH 1/3] Fixed missing assignment for binary clauses (#6148) * Added function to select the next variable to split on * Fixed typo * Small fixes * uint -> int * Fixed missing assignment for binary clauses --- src/smt/smt_internalizer.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 451136351..092bc0127 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1429,7 +1429,10 @@ namespace smt { inc_ref(l2); m_watches[(~l1).index()].insert_literal(l2); m_watches[(~l2).index()].insert_literal(l1); - if (get_assignment(l2) == l_false) { + if (get_assignment(l1) == l_false) { + assign(l2, b_justification(~l1)); + } + else if (get_assignment(l2) == l_false) { assign(l1, b_justification(~l2)); } m_clause_proof.add(l1, l2, k, j); From 99212a2726d2d1de8ba5d404d89bd9643983fc0c Mon Sep 17 00:00:00 2001 From: Stefan Muenzel Date: Mon, 11 Jul 2022 23:25:05 +0700 Subject: [PATCH 2/3] Use int64 for ocaml api functions that require it (#6150) * Use int64 for ocaml api functions that require it Signed-off-by: Stefan Muenzel * Use elif Signed-off-by: Stefan Muenzel --- scripts/update_api.py | 12 +++++++----- src/api/ml/z3.mli | 12 ++++++------ 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 43903e92c..8c6275c56 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -91,7 +91,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', # Mapping to ML types -Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', +Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int64', UINT64 : 'int64', DOUBLE : 'float', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' } @@ -254,8 +254,10 @@ def param2pystr(p): def param2ml(p): k = param_kind(p) if k == OUT: - if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64: + if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL: return "int" + elif param_type(p) == INT64 or param_type(p) == UINT64: + return "int64" elif param_type(p) == STRING: return "string" else: @@ -1252,9 +1254,9 @@ def ml_unwrap(t, ts, s): elif t == UINT: return '(' + ts + ') Unsigned_int_val(' + s + ')' elif t == INT64: - return '(' + ts + ') Long_val(' + s + ')' + return '(' + ts + ') Int64_val(' + s + ')' elif t == UINT64: - return '(' + ts + ') Unsigned_long_val(' + s + ')' + return '(' + ts + ') Int64_val(' + s + ')' elif t == DOUBLE: return '(' + ts + ') Double_val(' + s + ')' elif ml_has_plus_type(ts): @@ -1271,7 +1273,7 @@ def ml_set_wrap(t, d, n): elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL: return d + ' = Val_int(' + n + ');' elif t == INT64 or t == UINT64: - return d + ' = Val_long(' + n + ');' + return d + ' = caml_copy_int64(' + n + ');' elif t == DOUBLE: return d + '= caml_copy_double(' + n + ');' elif t == STRING: diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 74320dd72..a7c629018 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -927,10 +927,10 @@ end module FiniteDomain : sig (** Create a new finite domain sort. *) - val mk_sort : context -> Symbol.symbol -> int -> Sort.sort + val mk_sort : context -> Symbol.symbol -> int64 -> Sort.sort (** Create a new finite domain sort. *) - val mk_sort_s : context -> string -> int -> Sort.sort + val mk_sort_s : context -> string -> int64 -> Sort.sort (** Indicates whether the term is of an array sort. *) val is_finite_domain : Expr.expr -> bool @@ -939,7 +939,7 @@ sig val is_lt : Expr.expr -> bool (** The size of the finite domain sort. *) - val get_size : Sort.sort -> int + val get_size : Sort.sort -> int64 end @@ -2078,7 +2078,7 @@ sig val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) - val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr + val mk_numeral_i_u : context -> bool -> int64 -> int64 -> Sort.sort -> Expr.expr (** Create a numeral of FloatingPoint sort from a string *) val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr @@ -2303,7 +2303,7 @@ sig val get_numeral_exponent_string : context -> Expr.expr -> bool -> string (** Return the exponent value of a floating-point numeral as a signed integer *) - val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int + val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int64 (** Return the exponent of a floating-point numeral as a bit-vector expression. Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *) @@ -2320,7 +2320,7 @@ sig Remark: This function extracts the significand bits, without the hidden bit or normalization. Throws an exception if the significand does not fit into an int. *) - val get_numeral_significand_uint : context -> Expr.expr -> bool * int + val get_numeral_significand_uint : context -> Expr.expr -> bool * int64 (** Indicates whether a floating-point numeral is a NaN. *) val is_numeral_nan : context -> Expr.expr -> bool From 7ae1a338a7917c3dd944aa09e222b818c895c281 Mon Sep 17 00:00:00 2001 From: Anthony Romano Date: Mon, 11 Jul 2022 09:26:11 -0700 Subject: [PATCH 3/3] parallel-tactic: fix deadlocking race between shutdown and get_task (#6152) Deadlock/Race is as follows: 1. get_task() reads m_shutdown == false and enters loop body 2. shutdown() is called; sets m_shutdown = true 3. shutdown() calls m_cond.notify_all() 4. get_task() finds no task in try_get_task() 5. get_task() calls m_cond.wait(), missing the notification 6. solve() waits forever on join() Provided patch wraps (2) and (3) with the condition variable lock so that step (5) cannot miss the notification. Co-authored-by: Anthony Romano --- src/solver/parallel_tactic.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index c79f52084..1d24ed1e6 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -113,9 +113,9 @@ class parallel_tactic : public tactic { void shutdown() { if (!m_shutdown) { + std::lock_guard lock(m_mutex); m_shutdown = true; m_cond.notify_all(); - std::lock_guard lock(m_mutex); for (solver_state* st : m_active) { st->m().limit().cancel(); } @@ -147,7 +147,9 @@ class parallel_tactic : public tactic { } { std::unique_lock lock(m_mutex); - m_cond.wait(lock); + if (!m_shutdown) { + m_cond.wait(lock); + } } dec_wait(); }