fixed-size min-heap for tracking top-k literals (#7752)

* very basic setup

* ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743

Signed-off-by: Nikolaj Bjorner <[email protected]>

* respect smt configuration parameter in elim_unconstrained simplifier

Signed-off-by: Nikolaj Bjorner <[email protected]>

* indentation

* add bash files for test runs

* add option to selectively disable variable solving for only ground expressions

Signed-off-by: Nikolaj Bjorner <[email protected]>

* remove verbose output

Signed-off-by: Nikolaj Bjorner <[email protected]>

* fix #7745

axioms for len(substr(...)) escaped due to nested rewriting

* ensure atomic constraints are processed by arithmetic solver

* #7739 optimization

add simplification rule for at(x, offset) = ""

Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions.
The example highlights some opportunities for simplification, noteworthy at(..) = "".
The example is solved in both versions after adding this simplification.

* fix unsound len(substr) axiom

Signed-off-by: Nikolaj Bjorner <[email protected]>

* FreshConst is_sort (#7748)

* #7750

add pre-processing simplification

* Add parameter validation for selected API functions

* updates to ac-plugin

fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop.

* enable passive, add check for bloom up-to-date

* add top-k fixed-sized min-heap priority queue for top scoring literals

---------

Signed-off-by: Nikolaj Bjorner <[email protected]>
Co-authored-by: Nikolaj Bjorner <[email protected]>
Co-authored-by: humnrdble <[email protected]>

Author: 3 people

run_local_tests.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+# run from inside ./z3/build
+
+Z3=./z3
+OPTIONS="-v:0 -st smt.threads=4"
+OUT_FILE="../z3_results.txt"
+BASE_PATH="../../z3-poly-testing/inputs/"
+
+# List of relative test files (relative to BASE_PATH)
+REL_TEST_FILES=(
+    "QF_NIA_small/Ton_Chanh_15__Singapore_v1_false-termination.c__p27381_terminationG_0.smt2"
+    "QF_UFDTLIA_SAT/52759_bec3a2272267494faeecb6bfaf253e3b_10_QF_UFDTLIA.smt2"
+)
+
+# Clear output file
+> "$OUT_FILE"
+
+# Loop through and run Z3 on each file
+for rel_path in "${REL_TEST_FILES[@]}"; do
+    full_path="$BASE_PATH$rel_path"
+    test_name="$rel_path"
+
+    echo "Running: $test_name"
+    echo "===== $test_name =====" | tee -a "$OUT_FILE"
+
+    # Run Z3 and pipe output to both screen and file
+    $Z3 "$full_path" $OPTIONS 2>&1 | tee -a "$OUT_FILE"
+
+    echo "" | tee -a "$OUT_FILE"
+done
+
+echo "Results written to $OUT_FILE"

src/api/api_ast.cpp

@@ -225,13 +225,15 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(range, nullptr);
+        CHECK_SORTS(domain_size, domain, nullptr);
         if (prefix == nullptr) {
             prefix = "";
         }
 
         func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
                                                        domain_size,
-                                                       reinterpret_cast<sort*const*>(domain),
+                                                       to_sorts(domain),
                                                        to_sort(range), false);
 
         mk_c(c)->save_ast_trail(d);
@@ -243,9 +245,11 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_fresh_const(c, prefix, ty);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(ty, nullptr);
         if (prefix == nullptr) {
             prefix = "";
         }
+
         app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false);
         mk_c(c)->save_ast_trail(a);
         RETURN_Z3(of_ast(a));
@@ -654,6 +658,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_get_sort_name(c, t);
         RESET_ERROR_CODE();
+        CHECK_IS_SORT(t, of_symbol(symbol::null));
         CHECK_VALID_AST(t, of_symbol(symbol::null));
         return of_symbol(to_sort(t)->get_name());
         Z3_CATCH_RETURN(of_symbol(symbol::null));

src/api/api_context.h

@@ -286,10 +286,13 @@ namespace api {
 inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
 #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }
 #define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
-#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
-#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
+#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
+#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
 inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
-#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
+#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == nullptr || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
+#define CHECK_IS_SORT(_p_, _ret_) { if (_p_ == nullptr || !is_sort(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
+#define CHECK_SORTS(_n_, _ps_, _ret_) { for (unsigned i = 0; i < _n_; ++i) if (!is_sort(_ps_[i])) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
+
 inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
-#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
+#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
 inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

src/api/api_util.h

@@ -67,6 +67,7 @@ inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* con
 
 inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
 inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
+inline bool is_sort(Z3_sort a) { return is_sort(to_sort(a)); }
 
 inline sort * const *  to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
 inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }

src/api/python/z3/z3.py

@@ -1506,6 +1506,8 @@ def Consts(names, sort):
 
 def FreshConst(sort, prefix="c"):
     """Create a fresh constant of a specified sort"""
+    if z3_debug():
+        _z3_assert(is_sort(sort), f"Z3 sort expected, got {type(sort)}")
     ctx = _get_ctx(sort.ctx)
     return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)