mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

add specbot tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-02 00:44:47 -07:00
parent 2245451e96
commit 251127e45f
2 changed files with 1432 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

960
specbot/test_deeptest_seq.c Normal file
View file

@ -0,0 +1,960 @@
/*
* DeepTest: High-coverage tests for Z3-c3 seq solver (Nielsen graph)
* Targets under-exercised SPECBOT invariants/pre/postconditions in seq_nielsen.cpp
*
* Groups:
* A: Prefix/suffix cancellation (simplify pass 2)
* B: Symbol clash / conflict paths
* C: Deep variable chains (clone_from + apply_subst depth)
* D: Quadratic / VarNielsen modifier tests
* E: Regex derivatives + membership
* F: Power/repeat tests (simplify passes 3a-3e)
* G: Incremental solving stress (push/pop cycles)
* H: UNSAT / conflict collection
* I: Contains/replace/substr operation expansion
* J: Mixed theory (string + integer + boolean)
*/
#include "z3.h"
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <setjmp.h>
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
#include <signal.h>
static jmp_buf jmp_env;
static volatile int in_test = 0;
void abort_handler(int sig) {
(void)sig;
if (in_test) {
in_test = 0;
signal(SIGABRT, abort_handler);
longjmp(jmp_env, 1);
}
}
void suppress_dialogs() {
SetErrorMode(SEM_FAILCRITICALERRORS | SEM_NOGPFAULTERRORBOX);
_CrtSetReportMode(_CRT_ASSERT, _CRTDBG_MODE_FILE);
_CrtSetReportFile(_CRT_ASSERT, _CRTDBG_FILE_STDERR);
_CrtSetReportMode(_CRT_ERROR, _CRTDBG_MODE_FILE);
_CrtSetReportFile(_CRT_ERROR, _CRTDBG_FILE_STDERR);
_set_invalid_parameter_handler(
(void (*)(const wchar_t*,const wchar_t*,const wchar_t*,unsigned int,uintptr_t))0
);
_set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT);
signal(SIGABRT, abort_handler);
}
#else
void suppress_dialogs() {}
#endif
static int tests_run = 0;
static int tests_passed = 0;
static int tests_crashed = 0;
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
tests_run++; \
in_test = 1; \
if (setjmp(jmp_env) == 0) { \
__try { \
name(); \
in_test = 0; \
tests_passed++; \
fprintf(stderr, "[TEST] PASS %s\n", #name); \
} __except(EXCEPTION_EXECUTE_HANDLER) { \
in_test = 0; \
tests_crashed++; \
fprintf(stderr, "[TEST] CRASH %s (exception 0x%08lx)\n", #name, GetExceptionCode()); \
} \
} else { \
tests_crashed++; \
fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \
} \
} while(0)
/* ===== Helpers ===== */
static Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); }
static Z3_ast mk_str(Z3_context ctx, const char* s) { return Z3_mk_string(ctx, s); }
static Z3_ast mk_svar(Z3_context ctx, const char* name) {
return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), Z3_mk_string_sort(ctx));
}
static Z3_ast mk_cat(Z3_context ctx, Z3_ast a, Z3_ast b) {
Z3_ast args[2] = {a, b};
return Z3_mk_seq_concat(ctx, 2, args);
}
static Z3_ast mk_cat3(Z3_context ctx, Z3_ast a, Z3_ast b, Z3_ast c) {
Z3_ast args[3] = {a, b, c};
return Z3_mk_seq_concat(ctx, 3, args);
}
static Z3_ast mk_len(Z3_context ctx, Z3_ast s) { return Z3_mk_seq_length(ctx, s); }
static Z3_ast mk_int(Z3_context ctx, int v) { return Z3_mk_int(ctx, v, Z3_mk_int_sort(ctx)); }
/* Create nseq solver with timeout */
static Z3_solver mk_nseq(Z3_context ctx, unsigned timeout_ms) {
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_symbol(ctx, p,
Z3_mk_string_symbol(ctx, "smt.string_solver"),
Z3_mk_string_symbol(ctx, "nseq"));
Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), timeout_ms);
Z3_solver_set_params(ctx, s, p);
Z3_params_dec_ref(ctx, p);
return s;
}
/* Create context + solver, return both */
typedef struct { Z3_config cfg; Z3_context ctx; Z3_solver sol; } TestEnv;
static TestEnv mk_env(unsigned timeout_ms) {
TestEnv e;
e.cfg = Z3_mk_config();
e.ctx = Z3_mk_context(e.cfg);
e.sol = mk_nseq(e.ctx, timeout_ms);
return e;
}
static void free_env(TestEnv* e) {
Z3_solver_dec_ref(e->ctx, e->sol);
Z3_del_config(e->cfg);
Z3_del_context(e->ctx);
}
/* Helper: char range regex [lo-hi] */
static Z3_ast mk_range(Z3_context ctx, const char* lo, const char* hi) {
return Z3_mk_re_range(ctx, mk_str(ctx, lo), mk_str(ctx, hi));
}
/* Helper: regex from literal string */
static Z3_ast mk_re_lit(Z3_context ctx, const char* s) {
return Z3_mk_seq_to_re(ctx, mk_str(ctx, s));
}
/* =====================================================================
* GROUP A: Prefix/suffix cancellation (simplify_and_init pass 2)
* ===================================================================== */
/* "abc" ++ x = "abc" ++ y => prefix cancellation */
void test_prefix_cancel() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), x);
Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), y);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ "xyz" = y ++ "xyz" => suffix cancellation */
void test_suffix_cancel() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat(e.ctx, x, mk_str(e.ctx, "xyz"));
Z3_ast rhs = mk_cat(e.ctx, y, mk_str(e.ctx, "xyz"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* "ab" ++ x ++ "cd" = "ab" ++ y ++ "cd" => both prefix and suffix cancelled */
void test_prefix_suffix_cancel() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat3(e.ctx, mk_str(e.ctx, "ab"), x, mk_str(e.ctx, "cd"));
Z3_ast rhs = mk_cat3(e.ctx, mk_str(e.ctx, "ab"), y, mk_str(e.ctx, "cd"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Long shared prefix: "hello_world_" ++ x = "hello_world_" ++ y with length constraints */
void test_long_prefix_cancel() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "hello_world_"), x);
Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "hello_world_"), y);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Partial prefix overlap: "abc" ++ x = "abd" ++ y => 'ab' cancels, then 'c' vs 'd' clash */
void test_partial_prefix_clash() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat(e.ctx, mk_str(e.ctx, "abc"), x);
Z3_ast rhs = mk_cat(e.ctx, mk_str(e.ctx, "abd"), y);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP B: Symbol clash / conflict detection
* ===================================================================== */
/* "a" ++ x = "b" ++ y => first char clash */
void test_symbol_clash_ab() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, mk_str(e.ctx, "a"), x),
mk_cat(e.ctx, mk_str(e.ctx, "b"), y)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* "x" ++ a = "y" ++ a => prefix clash, same suffix */
void test_symbol_clash_same_suffix() {
TestEnv e = mk_env(10000);
Z3_ast a = mk_svar(e.ctx, "a");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, mk_str(e.ctx, "x"), a),
mk_cat(e.ctx, mk_str(e.ctx, "y"), a)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* "abc" = "abd" => direct constant clash (UNSAT) */
void test_const_clash() {
TestEnv e = mk_env(10000);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_str(e.ctx, "abc"), mk_str(e.ctx, "abd")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Multiple clash patterns in conjunction */
void test_multi_clash() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast z = mk_svar(e.ctx, "z");
/* "a"++x = "b"++y AND "c"++y = "d"++z */
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, mk_str(e.ctx, "a"), x),
mk_cat(e.ctx, mk_str(e.ctx, "b"), y)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, mk_str(e.ctx, "c"), y),
mk_cat(e.ctx, mk_str(e.ctx, "d"), z)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Clash with length constraint making it clearly UNSAT */
void test_clash_with_length() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, mk_str(e.ctx, "aa"), x),
mk_cat(e.ctx, mk_str(e.ctx, "bb"), x)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP C: Deep variable chains (many clone_from + apply_subst)
* ===================================================================== */
/* Chain of 10 equations: x1++x2=x3, x3++x4=x5, ..., x9++x10=result="abcdefghij" */
void test_deep_chain_10() {
TestEnv e = mk_env(15000);
char name[16];
Z3_ast vars[11];
for (int i = 0; i < 11; i++) {
sprintf(name, "v%d", i);
vars[i] = mk_svar(e.ctx, name);
}
/* v0++v1=v2, v2++v3=v4, v4++v5=v6, v6++v7=v8, v8++v9=v10 */
for (int i = 0; i < 10; i += 2) {
Z3_ast cat = mk_cat(e.ctx, vars[i], vars[i+1]);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, cat, vars[i+2 < 11 ? i+2 : 10]));
}
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, vars[10], mk_str(e.ctx, "abcdefghij")));
/* Constrain first var to single char to force cascading resolution */
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, vars[0]), mk_int(e.ctx, 1)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Linear chain: x1=a++x2, x2=b++x3, ..., x7=h++x8, x8="" => forces all substitutions */
void test_linear_subst_chain() {
TestEnv e = mk_env(15000);
char name[16];
Z3_ast vars[9];
const char* letters[] = {"a","b","c","d","e","f","g","h"};
for (int i = 0; i < 9; i++) {
sprintf(name, "w%d", i);
vars[i] = mk_svar(e.ctx, name);
}
for (int i = 0; i < 8; i++) {
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
vars[i], mk_cat(e.ctx, mk_str(e.ctx, letters[i]), vars[i+1])));
}
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, vars[8], mk_str(e.ctx, "")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Diamond pattern: x++y=z, x++w=z, y=w => forces clone + merge */
void test_diamond_subst() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast z = mk_svar(e.ctx, "z");
Z3_ast w = mk_svar(e.ctx, "w");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), z));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, w), z));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, z, mk_str(e.ctx, "abcdef")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Wide fan: x=a1++a2++a3++a4++a5 with all ai having length constraints */
void test_wide_fan() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
char nm[8];
Z3_ast parts[5];
for (int i = 0; i < 5; i++) {
sprintf(nm, "a%d", i);
parts[i] = mk_svar(e.ctx, nm);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, parts[i]), mk_int(e.ctx, 2)));
}
/* x = a0 ++ a1 ++ a2 ++ a3 ++ a4 */
Z3_ast cat01 = mk_cat(e.ctx, parts[0], parts[1]);
Z3_ast cat012 = mk_cat(e.ctx, cat01, parts[2]);
Z3_ast cat0123 = mk_cat(e.ctx, cat012, parts[3]);
Z3_ast cat01234 = mk_cat(e.ctx, cat0123, parts[4]);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, cat01234));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "aabbccddee")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP D: Quadratic / VarNielsen modifier
* ===================================================================== */
/* x ++ y = y ++ x (commutativity — classic quadratic) */
void test_commutative_eq() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_cat(e.ctx, y, x)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 3)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ x ++ x = y ++ y (repeated variable, power reasoning) */
void test_triple_double() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast xxx = mk_cat3(e.ctx, x, x, x);
Z3_ast yy = mk_cat(e.ctx, y, y);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, xxx, yy));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 2)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ "a" ++ y = y ++ "a" ++ x (interleaved constant in quadratic) */
void test_quadratic_interleaved() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast a = mk_str(e.ctx, "a");
Z3_ast lhs = mk_cat3(e.ctx, x, a, y);
Z3_ast rhs = mk_cat3(e.ctx, y, a, x);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, rhs));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 1)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 1)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ y ++ x = "abcab" (variable appears on both sides) */
void test_var_both_sides() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lhs = mk_cat3(e.ctx, x, y, x);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, lhs, mk_str(e.ctx, "abcab")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ x = "abab" (power / repeat equation) */
void test_power_eq() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast xx = mk_cat(e.ctx, x, x);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, xx, mk_str(e.ctx, "abab")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP E: Regex derivatives + membership
* ===================================================================== */
/* x in (a|b)* with |x| = 5 */
void test_regex_star_len() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast re_a = mk_re_lit(e.ctx, "a");
Z3_ast re_b = mk_re_lit(e.ctx, "b");
Z3_ast re_ab[2] = {re_a, re_b};
Z3_ast re_union = Z3_mk_re_union(e.ctx, 2, re_ab);
Z3_ast re_star = Z3_mk_re_star(e.ctx, re_union);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_star));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x in [0-9]{3}-[0-9]{4} (phone pattern) */
void test_regex_phone() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast digit = mk_range(e.ctx, "0", "9");
Z3_ast d3 = Z3_mk_re_loop(e.ctx, digit, 3, 3);
Z3_ast dash = mk_re_lit(e.ctx, "-");
Z3_ast d4 = Z3_mk_re_loop(e.ctx, digit, 4, 4);
Z3_ast parts[3] = {d3, dash, d4};
Z3_ast phone_re = Z3_mk_re_concat(e.ctx, 3, parts);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, phone_re));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x in (ab)* intersect (a|b){6} (intersection + bounded loop) */
void test_regex_intersect() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast re_ab_star = Z3_mk_re_star(e.ctx, mk_re_lit(e.ctx, "ab"));
Z3_ast re_a = mk_re_lit(e.ctx, "a");
Z3_ast re_b = mk_re_lit(e.ctx, "b");
Z3_ast ab_union[2] = {re_a, re_b};
Z3_ast re_ab_single = Z3_mk_re_union(e.ctx, 2, ab_union);
Z3_ast re_6 = Z3_mk_re_loop(e.ctx, re_ab_single, 6, 6);
Z3_ast inter[2] = {re_ab_star, re_6};
Z3_ast re_isect = Z3_mk_re_intersect(e.ctx, 2, inter);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_isect));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Multiple regex memberships: x in [a-z]+ AND x in .*"abc".* */
void test_regex_multi_member() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
/* x in [a-z]+ */
Z3_ast lower = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower));
/* x in .*abc.* (contains "abc" via regex) */
Z3_ast any = Z3_mk_re_star(e.ctx, Z3_mk_re_full(e.ctx,
Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx))));
Z3_ast abc_lit = mk_re_lit(e.ctx, "abc");
Z3_ast contain_parts[3] = {any, abc_lit, any};
Z3_ast contain_re = Z3_mk_re_concat(e.ctx, 3, contain_parts);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, contain_re));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Regex with complement: x in [a-z]+ AND x NOT in .*"bad".* */
void test_regex_complement() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast lower_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower_plus));
/* NOT contain "bad" */
Z3_ast any = Z3_mk_re_star(e.ctx, Z3_mk_re_full(e.ctx,
Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx))));
Z3_ast bad_re_parts[3] = {any, mk_re_lit(e.ctx, "bad"), any};
Z3_ast bad_re = Z3_mk_re_concat(e.ctx, 3, bad_re_parts);
Z3_ast no_bad = Z3_mk_re_complement(e.ctx, bad_re);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, no_bad));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Regex + equation: x in [a-z]{3} AND x ++ y = "abcdef" */
void test_regex_plus_eq() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast lower3 = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 3, 3);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower3));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "abcdef")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP F: Power/repeat (simplify passes 3a-3e)
* ===================================================================== */
/* x in a{3,5} with |x| = 4 */
void test_power_bounded_loop() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast re_a = mk_re_lit(e.ctx, "a");
Z3_ast re_loop = Z3_mk_re_loop(e.ctx, re_a, 3, 5);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_loop));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ x = y with |y| = 10 => forces power reasoning */
void test_power_double_eq() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, x), y));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, y), mk_int(e.ctx, 10)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x in (ab){2,4} (multi-char repeat) */
void test_power_multichar_loop() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast re_ab = mk_re_lit(e.ctx, "ab");
Z3_ast re_loop = Z3_mk_re_loop(e.ctx, re_ab, 2, 4);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re_loop));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x ++ x ++ x ++ x = "abcdabcdabcdabcd" (x repeated 4 times) */
void test_power_four_repeat() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast x4_inner = mk_cat(e.ctx, x, x);
Z3_ast x4 = mk_cat(e.ctx, x4_inner, x4_inner);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x4, mk_str(e.ctx, "abcdabcdabcdabcd")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* x in [a-z]{1,3} AND y in [0-9]{2,4} AND x++y has fixed length 5 */
void test_power_mixed_ranges() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast alpha_re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 1, 3);
Z3_ast digit_re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "0", "9"), 2, 4);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, alpha_re));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, y, digit_re));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_len(e.ctx, mk_cat(e.ctx, x, y)), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP G: Incremental solving stress (push/pop cycles)
* ===================================================================== */
/* 50 rounds of push/assert/check/pop with simple equations */
void test_incremental_simple_50() {
TestEnv e = mk_env(30000);
Z3_ast x = mk_svar(e.ctx, "x");
for (int i = 0; i < 50; i++) {
char val[32];
sprintf(val, "round_%d", i);
Z3_solver_push(e.ctx, e.sol);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, val)));
Z3_solver_check(e.ctx, e.sol);
Z3_solver_pop(e.ctx, e.sol, 1);
}
free_env(&e);
}
/* Incremental with concat equations of increasing complexity */
void test_incremental_concat_varying() {
TestEnv e = mk_env(30000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
for (int i = 0; i < 30; i++) {
Z3_solver_push(e.ctx, e.sol);
char s1[16], s2[16];
sprintf(s1, "a%d", i);
sprintf(s2, "b%d", i);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, x, y), mk_str(e.ctx, s1)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_len(e.ctx, x), mk_int(e.ctx, 1)));
Z3_solver_check(e.ctx, e.sol);
Z3_solver_pop(e.ctx, e.sol, 1);
}
free_env(&e);
}
/* Incremental with regex memberships */
void test_incremental_regex() {
TestEnv e = mk_env(30000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast lower_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "a", "z"));
/* Keep regex membership across all pushes */
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, lower_plus));
for (int i = 1; i <= 20; i++) {
Z3_solver_push(e.ctx, e.sol);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, i)));
Z3_solver_check(e.ctx, e.sol);
Z3_solver_pop(e.ctx, e.sol, 1);
}
free_env(&e);
}
/* Nested push/pop: 2 levels deep with string constraints */
void test_incremental_nested() {
TestEnv e = mk_env(15000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
for (int i = 0; i < 10; i++) {
Z3_solver_push(e.ctx, e.sol);
char v1[16];
sprintf(v1, "outer_%d", i);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_cat(e.ctx, x, y), mk_str(e.ctx, v1)));
Z3_solver_check(e.ctx, e.sol);
for (int j = 0; j < 5; j++) {
Z3_solver_push(e.ctx, e.sol);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx,
mk_len(e.ctx, x), mk_int(e.ctx, j)));
Z3_solver_check(e.ctx, e.sol);
Z3_solver_pop(e.ctx, e.sol, 1);
}
Z3_solver_pop(e.ctx, e.sol, 1);
}
free_env(&e);
}
/* =====================================================================
* GROUP H: UNSAT / conflict collection paths
* ===================================================================== */
/* x = "abc" AND x = "def" (direct contradiction) */
void test_unsat_direct() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "abc")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "def")));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_direct] result=%d\n", r);
free_env(&e);
}
/* |x| = 3 AND x in [a-z]{5} (length conflict) */
void test_unsat_length_regex() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3)));
Z3_ast re = Z3_mk_re_loop(e.ctx, mk_range(e.ctx, "a", "z"), 5, 5);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, re));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_length_regex] result=%d\n", r);
free_env(&e);
}
/* x ++ y = "ab" AND |x| = 3 (length impossible: |x|+|y|=2, |x|=3) */
void test_unsat_length_impossible() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "ab")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3)));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_length_impossible] result=%d\n", r);
free_env(&e);
}
/* x in empty regex */
void test_unsat_empty_regex() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_sort re_sort = Z3_mk_re_sort(e.ctx, Z3_mk_string_sort(e.ctx));
Z3_ast empty_re = Z3_mk_re_empty(e.ctx, re_sort);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, empty_re));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_empty_regex] result=%d\n", r);
free_env(&e);
}
/* x = "abc" AND NOT(x = "abc") (tautological unsat) */
void test_unsat_negation() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast abc = mk_str(e.ctx, "abc");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, abc));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_not(e.ctx, Z3_mk_eq(e.ctx, x, abc)));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_negation] result=%d\n", r);
free_env(&e);
}
/* x ++ y = "abc" AND x = "ab" AND y = "cd" (suffix mismatch) */
void test_unsat_concat_mismatch() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), mk_str(e.ctx, "abc")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "ab")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, y, mk_str(e.ctx, "cd")));
Z3_lbool r = Z3_solver_check(e.ctx, e.sol);
fprintf(stderr, " [unsat_concat_mismatch] result=%d\n", r);
free_env(&e);
}
/* =====================================================================
* GROUP I: Contains/replace/substr operation expansion
* ===================================================================== */
/* contains(x, "needle") AND |x| = 6 (exact fit) */
void test_contains_exact() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "needle")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 6)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* replace(x, "old", "new") = y AND x = "hold" */
void test_replace_known() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast replaced = Z3_mk_seq_replace(e.ctx, x, mk_str(e.ctx, "old"), mk_str(e.ctx, "new"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, replaced, y));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "hold")));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* substr(x, 1, 3) = "ell" AND prefix(x, "h") => x starts with "hell" */
void test_substr_extract() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast sub = Z3_mk_seq_extract(e.ctx, x, mk_int(e.ctx, 1), mk_int(e.ctx, 3));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, sub, mk_str(e.ctx, "ell")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_prefix(e.ctx, mk_str(e.ctx, "h"), x));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* indexof(x, "bc", 0) = 1 AND |x| = 5 */
void test_indexof_constraint() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast idx = Z3_mk_seq_index(e.ctx, x, mk_str(e.ctx, "bc"), mk_int(e.ctx, 0));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, idx, mk_int(e.ctx, 1)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* contains(x, "ab") AND contains(x, "cd") AND |x| = 4 => x must be "abcd" or similar */
void test_multi_contains() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "ab")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "cd")));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 4)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* prefix and suffix constraints together */
void test_prefix_suffix_ops() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_prefix(e.ctx, mk_str(e.ctx, "hel"), x));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_suffix(e.ctx, mk_str(e.ctx, "llo"), x));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 5)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* GROUP J: Mixed theory (string + integer + boolean)
* ===================================================================== */
/* |x| + |y| = 10 AND x ++ y = z AND |x| > |y| */
void test_mixed_len_arith() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_ast z = mk_svar(e.ctx, "z");
Z3_ast int_sort_args[2] = {mk_len(e.ctx, x), mk_len(e.ctx, y)};
Z3_ast len_sum = Z3_mk_add(e.ctx, 2, int_sort_args);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, len_sum, mk_int(e.ctx, 10)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_cat(e.ctx, x, y), z));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_gt(e.ctx, mk_len(e.ctx, x), mk_len(e.ctx, y)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* ite(contains(x, "a"), x = "abc", x = "def") */
void test_mixed_ite_contains() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast cond = Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "a"));
Z3_ast then_eq = Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "abc"));
Z3_ast else_eq = Z3_mk_eq(e.ctx, x, mk_str(e.ctx, "def"));
Z3_ast ite = Z3_mk_ite(e.ctx, cond, then_eq, else_eq);
Z3_solver_assert(e.ctx, e.sol, ite);
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* str.to_int(x) = 42 AND x in [0-9]+ */
void test_mixed_str_to_int() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast to_int = Z3_mk_str_to_int(e.ctx, x);
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, to_int, mk_int(e.ctx, 42)));
Z3_ast digit_plus = Z3_mk_re_plus(e.ctx, mk_range(e.ctx, "0", "9"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_in_re(e.ctx, x, digit_plus));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* int.to_str(n) = x AND n >= 100 AND n <= 999 */
void test_mixed_int_to_str() {
TestEnv e = mk_env(10000);
Z3_ast n = Z3_mk_const(e.ctx, Z3_mk_string_symbol(e.ctx, "n"), Z3_mk_int_sort(e.ctx));
Z3_ast x = mk_svar(e.ctx, "x");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, Z3_mk_int_to_str(e.ctx, n), x));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_ge(e.ctx, n, mk_int(e.ctx, 100)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_le(e.ctx, n, mk_int(e.ctx, 999)));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 3)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* Multiple string ops combined: contains + replace + length */
void test_mixed_ops_combined() {
TestEnv e = mk_env(10000);
Z3_ast x = mk_svar(e.ctx, "x");
Z3_ast y = mk_svar(e.ctx, "y");
Z3_solver_assert(e.ctx, e.sol, Z3_mk_seq_contains(e.ctx, x, mk_str(e.ctx, "hello")));
Z3_ast replaced = Z3_mk_seq_replace(e.ctx, x, mk_str(e.ctx, "hello"), mk_str(e.ctx, "world"));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, replaced, y));
Z3_solver_assert(e.ctx, e.sol, Z3_mk_eq(e.ctx, mk_len(e.ctx, x), mk_int(e.ctx, 8)));
Z3_solver_check(e.ctx, e.sol);
free_env(&e);
}
/* =====================================================================
* MAIN
* ===================================================================== */
int main() {
suppress_dialogs();
fprintf(stderr, "[SPECBOT] Starting DeepTest Z3-c3 seq solver tests\n");
Z3_global_param_set("smt.string_solver", "nseq");
/* Group A: Prefix/suffix cancellation */
RUN_TEST(test_prefix_cancel);
RUN_TEST(test_suffix_cancel);
RUN_TEST(test_prefix_suffix_cancel);
RUN_TEST(test_long_prefix_cancel);
RUN_TEST(test_partial_prefix_clash);
/* Group B: Symbol clash */
RUN_TEST(test_symbol_clash_ab);
RUN_TEST(test_symbol_clash_same_suffix);
RUN_TEST(test_const_clash);
RUN_TEST(test_multi_clash);
RUN_TEST(test_clash_with_length);
/* Group C: Deep variable chains */
RUN_TEST(test_deep_chain_10);
RUN_TEST(test_linear_subst_chain);
RUN_TEST(test_diamond_subst);
RUN_TEST(test_wide_fan);
/* Group D: Quadratic / VarNielsen */
RUN_TEST(test_commutative_eq);
RUN_TEST(test_triple_double);
RUN_TEST(test_quadratic_interleaved);
RUN_TEST(test_var_both_sides);
RUN_TEST(test_power_eq);
/* Group E: Regex derivatives */
RUN_TEST(test_regex_star_len);
RUN_TEST(test_regex_phone);
RUN_TEST(test_regex_intersect);
RUN_TEST(test_regex_multi_member);
RUN_TEST(test_regex_complement);
RUN_TEST(test_regex_plus_eq);
/* Group F: Power/repeat */
RUN_TEST(test_power_bounded_loop);
RUN_TEST(test_power_double_eq);
RUN_TEST(test_power_multichar_loop);
RUN_TEST(test_power_four_repeat);
RUN_TEST(test_power_mixed_ranges);
/* Group G: Incremental stress */
RUN_TEST(test_incremental_simple_50);
RUN_TEST(test_incremental_concat_varying);
RUN_TEST(test_incremental_regex);
RUN_TEST(test_incremental_nested);
/* Group H: UNSAT / conflict */
RUN_TEST(test_unsat_direct);
RUN_TEST(test_unsat_length_regex);
RUN_TEST(test_unsat_length_impossible);
RUN_TEST(test_unsat_empty_regex);
RUN_TEST(test_unsat_negation);
RUN_TEST(test_unsat_concat_mismatch);
/* Group I: Contains/replace/substr */
RUN_TEST(test_contains_exact);
RUN_TEST(test_replace_known);
RUN_TEST(test_substr_extract);
RUN_TEST(test_indexof_constraint);
RUN_TEST(test_multi_contains);
RUN_TEST(test_prefix_suffix_ops);
/* Group J: Mixed theory */
RUN_TEST(test_mixed_len_arith);
RUN_TEST(test_mixed_ite_contains);
RUN_TEST(test_mixed_str_to_int);
RUN_TEST(test_mixed_int_to_str);
RUN_TEST(test_mixed_ops_combined);
printf("=== DeepTest Z3-c3 Seq: %d/%d passed, %d crashed ===\n",
tests_passed, tests_run, tests_crashed);
return tests_run - tests_passed;
}

472
specbot/test_specbot_seq.c Normal file
View file

@ -0,0 +1,472 @@
#include "z3.h"
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <setjmp.h>
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
#include <signal.h>
static jmp_buf jmp_env;
static volatile int in_test = 0;
void abort_handler(int sig) {
(void)sig;
if (in_test) {
in_test = 0;
signal(SIGABRT, abort_handler);
longjmp(jmp_env, 1);
}
}
void suppress_dialogs() {
SetErrorMode(SEM_FAILCRITICALERRORS | SEM_NOGPFAULTERRORBOX);
_CrtSetReportMode(_CRT_ASSERT, _CRTDBG_MODE_FILE);
_CrtSetReportFile(_CRT_ASSERT, _CRTDBG_FILE_STDERR);
_CrtSetReportMode(_CRT_ERROR, _CRTDBG_MODE_FILE);
_CrtSetReportFile(_CRT_ERROR, _CRTDBG_FILE_STDERR);
_set_invalid_parameter_handler(
(void (*)(const wchar_t*,const wchar_t*,const wchar_t*,unsigned int,uintptr_t))0
);
_set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT);
signal(SIGABRT, abort_handler);
}
#else
void suppress_dialogs() {}
#endif
static int tests_run = 0;
static int tests_passed = 0;
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
tests_run++; \
in_test = 1; \
if (setjmp(jmp_env) == 0) { \
__try { \
name(); \
in_test = 0; \
tests_passed++; \
fprintf(stderr, "[TEST] PASS %s\n", #name); \
} __except(EXCEPTION_EXECUTE_HANDLER) { \
in_test = 0; \
fprintf(stderr, "[TEST] CRASH %s (exception 0x%08lx)\n", #name, GetExceptionCode()); \
} \
} else { \
fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \
} \
} while(0)
/* Helper to create string sort, variables, constants */
Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); }
Z3_ast mk_string_var(Z3_context ctx, const char* name) {
return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), Z3_mk_string_sort(ctx));
}
Z3_ast mk_string_val(Z3_context ctx, const char* s) {
return Z3_mk_string(ctx, s);
}
Z3_ast mk_concat(Z3_context ctx, Z3_ast a, Z3_ast b) {
Z3_ast args[2] = {a, b};
return Z3_mk_seq_concat(ctx, 2, args);
}
/* Create a solver configured to use the nseq (Nielsen) string solver */
Z3_solver mk_nseq_solver(Z3_context ctx) {
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_symbol(ctx, p, Z3_mk_string_symbol(ctx, "smt.string_solver"),
Z3_mk_string_symbol(ctx, "nseq"));
Z3_solver_set_params(ctx, s, p);
Z3_params_dec_ref(ctx, p);
return s;
}
/* === TEST GROUPS === */
/* Group A: Basic equations - exercises clone_from, simplify, solve */
void test_simple_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast hello = mk_string_val(ctx, "hello");
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, hello));
Z3_lbool r = Z3_solver_check(ctx, s);
(void)r;
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_concat_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast xy = mk_concat(ctx, x, y);
Z3_ast abc = mk_string_val(ctx, "abc");
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, abc));
Z3_lbool r = Z3_solver_check(ctx, s);
(void)r;
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_unsat_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "a")));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "b")));
Z3_lbool r = Z3_solver_check(ctx, s);
(void)r;
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_multi_var_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast z = mk_string_var(ctx, "z");
Z3_ast xy = mk_concat(ctx, x, y);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, z));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, z, mk_string_val(ctx, "test")));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_empty_string() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast empty = mk_string_val(ctx, "");
Z3_ast xe = mk_concat(ctx, x, empty);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xe, x));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
/* Group B: Regex membership - exercises add_str_mem, regex processing */
void test_regex_basic() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "a"), mk_string_val(ctx, "z")));
Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_regex_combined() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "0"), mk_string_val(ctx, "9")));
Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re));
Z3_ast xy = mk_concat(ctx, x, mk_concat(ctx, mk_string_val(ctx, "-"), y));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, mk_string_val(ctx, "123-abc")));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
/* Group C: Length constraints */
void test_length_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast len_x = Z3_mk_seq_length(ctx, x);
Z3_ast five = Z3_mk_int(ctx, 5, Z3_mk_int_sort(ctx));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, len_x, five));
Z3_ast re = Z3_mk_re_plus(ctx, Z3_mk_re_range(ctx, mk_string_val(ctx, "a"), mk_string_val(ctx, "z")));
Z3_solver_assert(ctx, s, Z3_mk_seq_in_re(ctx, x, re));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_length_sum() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast z = mk_string_var(ctx, "z");
Z3_ast xy = mk_concat(ctx, x, y);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, z));
Z3_ast ten = Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx));
Z3_ast len_z = Z3_mk_seq_length(ctx, z);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, len_z, ten));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
/* Group D: Nielsen-specific stress */
void test_quadratic_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000);
Z3_solver_set_params(ctx, s, p);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast xx = mk_concat(ctx, x, x);
Z3_ast yy = mk_concat(ctx, y, y);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xx, yy));
Z3_solver_check(ctx, s);
Z3_params_dec_ref(ctx, p);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_many_vars() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000);
Z3_solver_set_params(ctx, s, p);
char name[16];
Z3_ast vars[10];
for (int i = 0; i < 10; i++) {
sprintf(name, "x%d", i);
vars[i] = mk_string_var(ctx, name);
}
for (int i = 0; i < 8; i += 2) {
Z3_ast cat = mk_concat(ctx, vars[i], vars[i+1]);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, cat, vars[i+2 < 10 ? i+2 : 0]));
}
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, vars[0], mk_string_val(ctx, "ab")));
Z3_solver_check(ctx, s);
Z3_params_dec_ref(ctx, p);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_push_pop() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "hello")));
Z3_solver_check(ctx, s);
Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, "world")));
Z3_solver_check(ctx, s);
Z3_solver_pop(ctx, s, 1);
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_incremental_many() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 5000);
Z3_solver_set_params(ctx, s, p);
Z3_ast x = mk_string_var(ctx, "x");
for (int i = 0; i < 20; i++) {
Z3_solver_push(ctx, s);
char val[32];
sprintf(val, "test_%d", i);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, x, mk_string_val(ctx, val)));
Z3_solver_check(ctx, s);
Z3_solver_pop(ctx, s, 1);
}
Z3_params_dec_ref(ctx, p);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
/* Group E: Edge cases */
void test_contains() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_solver_assert(ctx, s, Z3_mk_seq_contains(ctx, x, mk_string_val(ctx, "needle")));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_length(ctx, x), Z3_mk_int(ctx, 10, Z3_mk_int_sort(ctx))));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_replace() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast replaced = Z3_mk_seq_replace(ctx, x, mk_string_val(ctx, "old"), mk_string_val(ctx, "new"));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, replaced, y));
Z3_solver_assert(ctx, s, Z3_mk_seq_contains(ctx, x, mk_string_val(ctx, "old")));
Z3_solver_check(ctx, s);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
void test_long_string_eq() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_uint(ctx, p, Z3_mk_string_symbol(ctx, "timeout"), 10000);
Z3_solver_set_params(ctx, s, p);
char long_str[101];
memset(long_str, 'a', 100);
long_str[100] = 0;
Z3_ast x = mk_string_var(ctx, "x");
Z3_ast y = mk_string_var(ctx, "y");
Z3_ast xy = mk_concat(ctx, x, y);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, xy, mk_string_val(ctx, long_str)));
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, Z3_mk_seq_length(ctx, x), Z3_mk_int(ctx, 50, Z3_mk_int_sort(ctx))));
Z3_solver_check(ctx, s);
Z3_params_dec_ref(ctx, p);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
}
int main() {
suppress_dialogs();
fprintf(stderr, "[SPECBOT] Starting Z3 c3 seq solver invariant tests\n");
/* Force the Nielsen seq solver globally */
Z3_global_param_set("smt.string_solver", "nseq");
/* Group A: Basic equations */
RUN_TEST(test_simple_eq);
RUN_TEST(test_concat_eq);
RUN_TEST(test_unsat_eq);
RUN_TEST(test_multi_var_eq);
RUN_TEST(test_empty_string);
/* Group B: Regex */
RUN_TEST(test_regex_basic);
RUN_TEST(test_regex_combined);
/* Group C: Length */
RUN_TEST(test_length_eq);
RUN_TEST(test_length_sum);
/* Group D: Nielsen stress */
RUN_TEST(test_quadratic_eq);
RUN_TEST(test_many_vars);
RUN_TEST(test_push_pop);
RUN_TEST(test_incremental_many);
/* Group E: Edge cases */
RUN_TEST(test_contains);
RUN_TEST(test_replace);
RUN_TEST(test_long_string_eq);
printf("=== SpecBot Z3-c3 Seq Tests: %d/%d passed ===\n", tests_passed, tests_run);
return tests_run - tests_passed;
}