mirror of
https://github.com/Z3Prover/z3
synced 2025-09-30 05:09:02 +00:00
Add comprehensive tests for API algebraic number functions (#7888)
- Created new test file api_algebraic.cpp with tests for all algebraic API functions - Tests cover basic operations (add, sub, mul, div, power, root) - Tests cover comparison operations (lt, le, gt, ge, eq, neq) - Tests cover sign detection (is_zero, is_pos, is_neg, sign) - Tests cover algebraic value detection (is_value) - Added comprehensive test cases for rational numbers and fractions - Updated main.cpp and CMakeLists.txt to include the new test module Coverage improvements: - src/api/api_algebraic.cpp: 0% -> 52% (136/258 lines covered) - Overall project coverage: ~47% (gained 71 covered lines) Co-authored-by: Daily Test Coverage Improver <github-actions[bot]@users.noreply.github.com>
This commit is contained in:
Don Syme
GitHub
parent
6d3daa5338
commit
44d2bba3e5
3 changed files with 199 additions and 0 deletions
|
|
@ -15,6 +15,7 @@ add_executable(test-z3
|
|||
algebraic_numbers.cpp
|
||||
api_bug.cpp
|
||||
api.cpp
|
||||
api_algebraic.cpp
|
||||
arith_rewriter.cpp
|
||||
arith_simplifier_plugin.cpp
|
||||
ast.cpp
|
||||
|
|
|
|||
197
src/test/api_algebraic.cpp
Normal file
197
src/test/api_algebraic.cpp
Normal file
|
|
@ -0,0 +1,197 @@
|
|||
/*++
|
||||
Copyright (c) 2025 Daily Test Coverage Improver
|
||||
|
||||
Module Name:
|
||||
|
||||
api_algebraic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Test API algebraic number functions
|
||||
|
||||
Author:
|
||||
|
||||
Daily Test Coverage Improver 2025-09-16
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include "api/z3.h"
|
||||
#include "util/trace.h"
|
||||
#include "util/rational.h"
|
||||
|
||||
void tst_api_algebraic() {
|
||||
Z3_config cfg = Z3_mk_config();
|
||||
Z3_set_param_value(cfg, "model", "true");
|
||||
Z3_context ctx = Z3_mk_context(cfg);
|
||||
Z3_del_config(cfg);
|
||||
|
||||
// Test Z3_algebraic_is_value with rational numbers
|
||||
{
|
||||
Z3_ast zero = Z3_mk_real(ctx, 0, 1);
|
||||
Z3_ast one = Z3_mk_real(ctx, 1, 1);
|
||||
Z3_ast negative_one = Z3_mk_real(ctx, -1, 1);
|
||||
Z3_ast half = Z3_mk_real(ctx, 1, 2);
|
||||
|
||||
ENSURE(Z3_algebraic_is_value(ctx, zero));
|
||||
ENSURE(Z3_algebraic_is_value(ctx, one));
|
||||
ENSURE(Z3_algebraic_is_value(ctx, negative_one));
|
||||
ENSURE(Z3_algebraic_is_value(ctx, half));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_is_value with non-algebraic values
|
||||
{
|
||||
Z3_symbol x_sym = Z3_mk_string_symbol(ctx, "x");
|
||||
Z3_sort real_sort = Z3_mk_real_sort(ctx);
|
||||
Z3_ast x = Z3_mk_const(ctx, x_sym, real_sort);
|
||||
|
||||
// Variable should not be an algebraic value
|
||||
ENSURE(!Z3_algebraic_is_value(ctx, x));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_is_zero, Z3_algebraic_is_pos, Z3_algebraic_is_neg
|
||||
{
|
||||
Z3_ast zero = Z3_mk_real(ctx, 0, 1);
|
||||
Z3_ast positive = Z3_mk_real(ctx, 5, 1);
|
||||
Z3_ast negative = Z3_mk_real(ctx, -3, 1);
|
||||
|
||||
ENSURE(Z3_algebraic_is_zero(ctx, zero));
|
||||
ENSURE(!Z3_algebraic_is_pos(ctx, zero));
|
||||
ENSURE(!Z3_algebraic_is_neg(ctx, zero));
|
||||
|
||||
ENSURE(!Z3_algebraic_is_zero(ctx, positive));
|
||||
ENSURE(Z3_algebraic_is_pos(ctx, positive));
|
||||
ENSURE(!Z3_algebraic_is_neg(ctx, positive));
|
||||
|
||||
ENSURE(!Z3_algebraic_is_zero(ctx, negative));
|
||||
ENSURE(!Z3_algebraic_is_pos(ctx, negative));
|
||||
ENSURE(Z3_algebraic_is_neg(ctx, negative));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_sign
|
||||
{
|
||||
Z3_ast zero = Z3_mk_real(ctx, 0, 1);
|
||||
Z3_ast positive = Z3_mk_real(ctx, 7, 1);
|
||||
Z3_ast negative = Z3_mk_real(ctx, -4, 1);
|
||||
|
||||
ENSURE(Z3_algebraic_sign(ctx, zero) == 0);
|
||||
ENSURE(Z3_algebraic_sign(ctx, positive) > 0);
|
||||
ENSURE(Z3_algebraic_sign(ctx, negative) < 0);
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_add
|
||||
{
|
||||
Z3_ast two = Z3_mk_real(ctx, 2, 1);
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast five = Z3_mk_real(ctx, 5, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_add(ctx, two, three);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, five));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_sub
|
||||
{
|
||||
Z3_ast seven = Z3_mk_real(ctx, 7, 1);
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast four = Z3_mk_real(ctx, 4, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_sub(ctx, seven, three);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, four));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_mul
|
||||
{
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast four = Z3_mk_real(ctx, 4, 1);
|
||||
Z3_ast twelve = Z3_mk_real(ctx, 12, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_mul(ctx, three, four);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, twelve));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_div
|
||||
{
|
||||
Z3_ast twelve = Z3_mk_real(ctx, 12, 1);
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast four = Z3_mk_real(ctx, 4, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_div(ctx, twelve, three);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, four));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_power
|
||||
{
|
||||
Z3_ast two = Z3_mk_real(ctx, 2, 1);
|
||||
Z3_ast eight = Z3_mk_real(ctx, 8, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_power(ctx, two, 3);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, eight));
|
||||
}
|
||||
|
||||
// Test comparison functions: Z3_algebraic_lt, Z3_algebraic_le, Z3_algebraic_gt, Z3_algebraic_ge
|
||||
{
|
||||
Z3_ast two = Z3_mk_real(ctx, 2, 1);
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast also_three = Z3_mk_real(ctx, 3, 1);
|
||||
|
||||
// Less than
|
||||
ENSURE(Z3_algebraic_lt(ctx, two, three));
|
||||
ENSURE(!Z3_algebraic_lt(ctx, three, two));
|
||||
ENSURE(!Z3_algebraic_lt(ctx, three, also_three));
|
||||
|
||||
// Less than or equal
|
||||
ENSURE(Z3_algebraic_le(ctx, two, three));
|
||||
ENSURE(!Z3_algebraic_le(ctx, three, two));
|
||||
ENSURE(Z3_algebraic_le(ctx, three, also_three));
|
||||
|
||||
// Greater than
|
||||
ENSURE(!Z3_algebraic_gt(ctx, two, three));
|
||||
ENSURE(Z3_algebraic_gt(ctx, three, two));
|
||||
ENSURE(!Z3_algebraic_gt(ctx, three, also_three));
|
||||
|
||||
// Greater than or equal
|
||||
ENSURE(!Z3_algebraic_ge(ctx, two, three));
|
||||
ENSURE(Z3_algebraic_ge(ctx, three, two));
|
||||
ENSURE(Z3_algebraic_ge(ctx, three, also_three));
|
||||
}
|
||||
|
||||
// Test equality and inequality: Z3_algebraic_eq, Z3_algebraic_neq
|
||||
{
|
||||
Z3_ast two = Z3_mk_real(ctx, 2, 1);
|
||||
Z3_ast three = Z3_mk_real(ctx, 3, 1);
|
||||
Z3_ast also_two = Z3_mk_real(ctx, 2, 1);
|
||||
|
||||
// Equality
|
||||
ENSURE(Z3_algebraic_eq(ctx, two, also_two));
|
||||
ENSURE(!Z3_algebraic_eq(ctx, two, three));
|
||||
|
||||
// Inequality
|
||||
ENSURE(!Z3_algebraic_neq(ctx, two, also_two));
|
||||
ENSURE(Z3_algebraic_neq(ctx, two, three));
|
||||
}
|
||||
|
||||
// Test Z3_algebraic_root
|
||||
{
|
||||
Z3_ast four = Z3_mk_real(ctx, 4, 1);
|
||||
Z3_ast two = Z3_mk_real(ctx, 2, 1);
|
||||
|
||||
Z3_ast result = Z3_algebraic_root(ctx, four, 2); // Square root of 4
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, two));
|
||||
}
|
||||
|
||||
// Test with negative numbers and fractions
|
||||
{
|
||||
Z3_ast neg_half = Z3_mk_real(ctx, -1, 2);
|
||||
Z3_ast quarter = Z3_mk_real(ctx, 1, 4);
|
||||
Z3_ast neg_quarter = Z3_mk_real(ctx, -1, 4);
|
||||
|
||||
ENSURE(Z3_algebraic_is_value(ctx, neg_half));
|
||||
ENSURE(Z3_algebraic_is_neg(ctx, neg_half));
|
||||
ENSURE(Z3_algebraic_is_pos(ctx, quarter));
|
||||
|
||||
Z3_ast result = Z3_algebraic_add(ctx, neg_half, quarter);
|
||||
ENSURE(Z3_algebraic_eq(ctx, result, neg_quarter));
|
||||
}
|
||||
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
|
@ -175,6 +175,7 @@ int main(int argc, char ** argv) {
|
|||
TST(var_subst);
|
||||
TST(simple_parser);
|
||||
TST(api);
|
||||
TST(api_algebraic);
|
||||
TST(cube_clause);
|
||||
TST(old_interval);
|
||||
TST(get_implied_equalities);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue