3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-04 02:39:02 +00:00

Merge remote-tracking branch 'origin/master' into c3

# Conflicts:
#	.github/workflows/qf-s-benchmark.lock.yml
#	.github/workflows/qf-s-benchmark.md
#	.github/workflows/zipt-code-reviewer.lock.yml
#	.github/workflows/zipt-code-reviewer.md
#	.gitignore
#	src/ast/rewriter/seq_rewriter.cpp
#	src/test/main.cpp
This commit is contained in:
Nikolaj Bjorner 2026-03-24 17:44:48 -07:00
commit 6a6f9b1892
185 changed files with 16422 additions and 5692 deletions

View file

@ -38,6 +38,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_array_sort_n(c, n, domain, range);
RESET_ERROR_CODE();
if (n == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG, "array sort requires at least one domain sort");
RETURN_Z3(nullptr);
}
vector<parameter> params;
for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i])));
params.push_back(parameter(to_sort(range)));

View file

@ -898,6 +898,10 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
expr * a = to_expr(_a);
if (num_exprs > 0 && (!_from || !_to)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null from/to arrays with non-zero num_exprs");
RETURN_Z3(of_expr(nullptr));
}
expr * const * from = to_exprs(num_exprs, _from);
expr * const * to = to_exprs(num_exprs, _to);
expr * r = nullptr;
@ -1514,6 +1518,10 @@ extern "C" {
LOG_Z3_translate(c, a, target);
RESET_ERROR_CODE();
CHECK_VALID_AST(a, nullptr);
if (!target) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null target context");
RETURN_Z3(nullptr);
}
if (c == target) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);

View file

@ -167,6 +167,7 @@ extern "C" {
RESET_ERROR_CODE();
if (ebits < 2 || sbits < 3) {
SET_ERROR_CODE(Z3_INVALID_ARG, "ebits should be at least 2, sbits at least 3");
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
sort * s = ctx->fpautil().mk_float_sort(ebits, sbits);

View file

@ -64,6 +64,7 @@ extern "C" {
LOG_Z3_model_get_const_interp(c, m, a);
RESET_ERROR_CODE();
CHECK_NON_NULL(m, nullptr);
CHECK_NON_NULL(a, nullptr);
expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a));
if (!r) {
RETURN_Z3(nullptr);
@ -212,6 +213,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_model_translate(c, m, target);
RESET_ERROR_CODE();
if (!target) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null target context");
RETURN_Z3(nullptr);
}
Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
dst->m_model = to_model_ref(m)->translate(tr);
@ -246,7 +251,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_add_func_interp(c, m, f, else_val);
RESET_ERROR_CODE();
CHECK_NON_NULL(f, nullptr);
CHECK_NON_NULL(m, nullptr);
CHECK_NON_NULL(f, nullptr);
func_decl* d = to_func_decl(f);
model* mdl = to_model_ref(m);
Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl);

View file

@ -94,7 +94,11 @@ extern "C" {
Z3_TRY;
LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
RESET_ERROR_CODE();
CHECK_FORMULA(a,0);
CHECK_FORMULA(a,0);
if (!weight) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null weight string");
return 0;
}
rational w(weight);
return to_optimize_ptr(o)->add_soft_constraint(to_expr(a), w, to_symbol(id));
Z3_CATCH_RETURN(0);

View file

@ -321,6 +321,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_pattern(c, num_patterns, terms);
RESET_ERROR_CODE();
if (num_patterns == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG, "pattern requires at least one term");
RETURN_Z3(nullptr);
}
for (unsigned i = 0; i < num_patterns; ++i) {
if (!is_app(to_expr(terms[i]))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);

View file

@ -48,6 +48,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_string(c, str);
RESET_ERROR_CODE();
if (!str) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null string");
RETURN_Z3(nullptr);
}
zstring s(str);
app* a = mk_c(c)->sutil().str.mk_string(s);
mk_c(c)->save_ast_trail(a);
@ -59,6 +63,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_lstring(c, sz, str);
RESET_ERROR_CODE();
if (sz > 0 && !str) {
SET_ERROR_CODE(Z3_INVALID_ARG, "null string buffer");
RETURN_Z3(nullptr);
}
unsigned_vector chs;
for (unsigned i = 0; i < sz; ++i) chs.push_back((unsigned char)str[i]);
zstring s(sz, chs.data());
@ -314,6 +322,10 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_re_loop(c, r, lo, hi);
RESET_ERROR_CODE();
if (hi != 0 && lo > hi) {
SET_ERROR_CODE(Z3_INVALID_ARG, "loop lower bound must not exceed upper bound");
RETURN_Z3(nullptr);
}
app* a = hi == 0 ? mk_c(c)->sutil().re.mk_loop(to_expr(r), lo) : mk_c(c)->sutil().re.mk_loop(to_expr(r), lo, hi);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));

View file

@ -379,14 +379,15 @@ extern "C" {
LOG_Z3_solver_from_file(c, s, file_name);
char const* ext = get_extension(file_name);
std::ifstream is(file_name);
init_solver(c, s);
if (!is) {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
}
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
init_solver(c, s);
solver_from_dimacs_stream(c, s, is);
}
else {
init_solver(c, s);
solver_from_stream(c, s, is);
}
Z3_CATCH;
@ -1153,24 +1154,24 @@ extern "C" {
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*))created_eh;
to_solver_ref(s)->user_propagate_register_created(c);
user_propagator::created_eh_t created_fn = (void(*)(void*, user_propagator::callback*, expr*))created_eh;
to_solver_ref(s)->user_propagate_register_created(created_fn);
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(c);
user_propagator::decide_eh_t decide_fn = (void(*)(void*, user_propagator::callback*, expr*, unsigned, bool))decide_eh;
to_solver_ref(s)->user_propagate_register_decide(decide_fn);
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh binding_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::binding_eh_t c = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
to_solver_ref(s)->user_propagate_register_on_binding(c);
user_propagator::binding_eh_t binding_fn = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
to_solver_ref(s)->user_propagate_register_on_binding(binding_fn);
Z3_CATCH;
}

View file

@ -1533,6 +1533,8 @@ namespace z3 {
expr rotate_left(unsigned i) const { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr rotate_right(unsigned i) const { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr ext_rotate_left(expr const& n) const { Z3_ast r = Z3_mk_ext_rotate_left(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
expr ext_rotate_right(expr const& n) const { Z3_ast r = Z3_mk_ext_rotate_right(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
expr repeat(unsigned i) const { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
friend expr bvredor(expr const & a);

View file

@ -124,3 +124,33 @@ func (c *Context) MkGt(lhs, rhs *Expr) *Expr {
func (c *Context) MkGe(lhs, rhs *Expr) *Expr {
return newExpr(c, C.Z3_mk_ge(c.ptr, lhs.ptr, rhs.ptr))
}
// MkPower creates an exponentiation expression (base^exp).
func (c *Context) MkPower(base, exp *Expr) *Expr {
return newExpr(c, C.Z3_mk_power(c.ptr, base.ptr, exp.ptr))
}
// MkAbs creates an absolute value expression.
func (c *Context) MkAbs(arg *Expr) *Expr {
return newExpr(c, C.Z3_mk_abs(c.ptr, arg.ptr))
}
// MkInt2Real coerces an integer expression to a real.
func (c *Context) MkInt2Real(arg *Expr) *Expr {
return newExpr(c, C.Z3_mk_int2real(c.ptr, arg.ptr))
}
// MkReal2Int converts a real expression to an integer (floor).
func (c *Context) MkReal2Int(arg *Expr) *Expr {
return newExpr(c, C.Z3_mk_real2int(c.ptr, arg.ptr))
}
// MkIsInt creates a predicate that checks whether a real expression is an integer.
func (c *Context) MkIsInt(arg *Expr) *Expr {
return newExpr(c, C.Z3_mk_is_int(c.ptr, arg.ptr))
}
// MkDivides creates an integer divisibility predicate (t1 divides t2).
func (c *Context) MkDivides(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_divides(c.ptr, t1.ptr, t2.ptr))
}

View file

@ -64,3 +64,23 @@ func (c *Context) MkArrayDefault(array *Expr) *Expr {
func (c *Context) MkArrayExt(a1, a2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_array_ext(c.ptr, a1.ptr, a2.ptr))
}
// MkAsArray creates an array from a function declaration.
// The resulting array maps each input to the output of the function.
func (c *Context) MkAsArray(f *FuncDecl) *Expr {
return newExpr(c, C.Z3_mk_as_array(c.ptr, f.ptr))
}
// MkMap applies a function to the elements of one or more arrays, returning a new array.
// The function f is applied element-wise to the given arrays.
func (c *Context) MkMap(f *FuncDecl, arrays ...*Expr) *Expr {
cArrays := make([]C.Z3_ast, len(arrays))
for i, a := range arrays {
cArrays[i] = a.ptr
}
var cArraysPtr *C.Z3_ast
if len(cArrays) > 0 {
cArraysPtr = &cArrays[0]
}
return newExpr(c, C.Z3_mk_map(c.ptr, f.ptr, C.uint(len(arrays)), cArraysPtr))
}

View file

@ -158,3 +158,88 @@ func (c *Context) MkSignExt(i uint, expr *Expr) *Expr {
func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
}
// MkBVRotateLeft rotates the bits of t to the left by i positions.
func (c *Context) MkBVRotateLeft(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_rotate_left(c.ptr, C.uint(i), t.ptr))
}
// MkBVRotateRight rotates the bits of t to the right by i positions.
func (c *Context) MkBVRotateRight(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_rotate_right(c.ptr, C.uint(i), t.ptr))
}
// MkRepeat repeats the given bit-vector t a total of i times.
func (c *Context) MkRepeat(i uint, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_repeat(c.ptr, C.uint(i), t.ptr))
}
// MkBVAddNoOverflow creates a predicate that checks that the bit-wise addition
// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
func (c *Context) MkBVAddNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvadd_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVAddNoUnderflow creates a predicate that checks that the bit-wise signed addition
// of t1 and t2 does not underflow.
func (c *Context) MkBVAddNoUnderflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvadd_no_underflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVSubNoOverflow creates a predicate that checks that the bit-wise signed subtraction
// of t1 and t2 does not overflow.
func (c *Context) MkBVSubNoOverflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvsub_no_overflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVSubNoUnderflow creates a predicate that checks that the bit-wise subtraction
// of t1 and t2 does not underflow. If isSigned is true, checks for signed underflow.
func (c *Context) MkBVSubNoUnderflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvsub_no_underflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVSdivNoOverflow creates a predicate that checks that the bit-wise signed division
// of t1 and t2 does not overflow.
func (c *Context) MkBVSdivNoOverflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvsdiv_no_overflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVNegNoOverflow creates a predicate that checks that bit-wise negation does not overflow
// when t1 is interpreted as a signed bit-vector.
func (c *Context) MkBVNegNoOverflow(t1 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvneg_no_overflow(c.ptr, t1.ptr))
}
// MkBVMulNoOverflow creates a predicate that checks that the bit-wise multiplication
// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
return newExpr(c, C.Z3_mk_bvmul_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
}
// MkBVMulNoUnderflow creates a predicate that checks that the bit-wise signed multiplication
// of t1 and t2 does not underflow.
func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvmul_no_underflow(c.ptr, t1.ptr, t2.ptr))
}
// MkBVRedAnd computes the bitwise AND reduction of a bit-vector, returning a 1-bit vector.
func (c *Context) MkBVRedAnd(t *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvredand(c.ptr, t.ptr))
}
// MkBVRedOr computes the bitwise OR reduction of a bit-vector, returning a 1-bit vector.
func (c *Context) MkBVRedOr(t *Expr) *Expr {
return newExpr(c, C.Z3_mk_bvredor(c.ptr, t.ptr))
}
// MkBVExtRotateLeft rotates the bits of t1 to the left by the number of bits given by t2.
// Both t1 and t2 must be bit-vectors of the same width.
func (c *Context) MkBVExtRotateLeft(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_ext_rotate_left(c.ptr, t1.ptr, t2.ptr))
}
// MkBVExtRotateRight rotates the bits of t1 to the right by the number of bits given by t2.
// Both t1 and t2 must be bit-vectors of the same width.
func (c *Context) MkBVExtRotateRight(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_ext_rotate_right(c.ptr, t1.ptr, t2.ptr))
}

View file

@ -167,3 +167,118 @@ func (c *Context) MkFPToIEEEBV(expr *Expr) *Expr {
func (c *Context) MkFPToReal(expr *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_real(c.ptr, expr.ptr))
}
// MkFPRNE creates the round-nearest-ties-to-even rounding mode.
func (c *Context) MkFPRNE() *Expr {
return newExpr(c, C.Z3_mk_fpa_rne(c.ptr))
}
// MkFPRNA creates the round-nearest-ties-to-away rounding mode.
func (c *Context) MkFPRNA() *Expr {
return newExpr(c, C.Z3_mk_fpa_rna(c.ptr))
}
// MkFPRTP creates the round-toward-positive rounding mode.
func (c *Context) MkFPRTP() *Expr {
return newExpr(c, C.Z3_mk_fpa_rtp(c.ptr))
}
// MkFPRTN creates the round-toward-negative rounding mode.
func (c *Context) MkFPRTN() *Expr {
return newExpr(c, C.Z3_mk_fpa_rtn(c.ptr))
}
// MkFPRTZ creates the round-toward-zero rounding mode.
func (c *Context) MkFPRTZ() *Expr {
return newExpr(c, C.Z3_mk_fpa_rtz(c.ptr))
}
// MkFPFP creates a floating-point number from a sign bit (1-bit BV), exponent BV, and significand BV.
func (c *Context) MkFPFP(sgn, exp, sig *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_fp(c.ptr, sgn.ptr, exp.ptr, sig.ptr))
}
// MkFPNumeralFloat creates a floating-point numeral from a float32 value.
func (c *Context) MkFPNumeralFloat(v float32, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_numeral_float(c.ptr, C.float(v), sort.ptr))
}
// MkFPNumeralDouble creates a floating-point numeral from a float64 value.
func (c *Context) MkFPNumeralDouble(v float64, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_numeral_double(c.ptr, C.double(v), sort.ptr))
}
// MkFPNumeralInt creates a floating-point numeral from a signed integer.
func (c *Context) MkFPNumeralInt(v int, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_numeral_int(c.ptr, C.int(v), sort.ptr))
}
// MkFPNumeralIntUint creates a floating-point numeral from a sign, signed exponent, and unsigned significand.
func (c *Context) MkFPNumeralIntUint(sgn bool, exp int, sig uint, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_numeral_int_uint(c.ptr, C.bool(sgn), C.int(exp), C.uint(sig), sort.ptr))
}
// MkFPNumeralInt64Uint64 creates a floating-point numeral from a sign, int64 exponent, and uint64 significand.
func (c *Context) MkFPNumeralInt64Uint64(sgn bool, exp int64, sig uint64, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_numeral_int64_uint64(c.ptr, C.bool(sgn), C.int64_t(exp), C.uint64_t(sig), sort.ptr))
}
// MkFPFMA creates a floating-point fused multiply-add: round((t1 * t2) + t3, rm).
func (c *Context) MkFPFMA(rm, t1, t2, t3 *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_fma(c.ptr, rm.ptr, t1.ptr, t2.ptr, t3.ptr))
}
// MkFPRem creates a floating-point remainder.
func (c *Context) MkFPRem(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_rem(c.ptr, t1.ptr, t2.ptr))
}
// MkFPMin creates the minimum of two floating-point values.
func (c *Context) MkFPMin(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_min(c.ptr, t1.ptr, t2.ptr))
}
// MkFPMax creates the maximum of two floating-point values.
func (c *Context) MkFPMax(t1, t2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_max(c.ptr, t1.ptr, t2.ptr))
}
// MkFPRoundToIntegral creates a floating-point round-to-integral operation.
func (c *Context) MkFPRoundToIntegral(rm, t *Expr) *Expr {
return newExpr(c, C.Z3_mk_fpa_round_to_integral(c.ptr, rm.ptr, t.ptr))
}
// MkFPToFPBV converts a bit-vector to a floating-point number (reinterpretation of IEEE 754 bits).
func (c *Context) MkFPToFPBV(bv *Expr, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_fp_bv(c.ptr, bv.ptr, sort.ptr))
}
// MkFPToFPFloat converts a floating-point number to another floating-point sort with rounding.
func (c *Context) MkFPToFPFloat(rm, t *Expr, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_fp_float(c.ptr, rm.ptr, t.ptr, sort.ptr))
}
// MkFPToFPReal converts a real number to a floating-point number with rounding.
func (c *Context) MkFPToFPReal(rm, t *Expr, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_fp_real(c.ptr, rm.ptr, t.ptr, sort.ptr))
}
// MkFPToFPSigned converts a signed bit-vector to a floating-point number with rounding.
func (c *Context) MkFPToFPSigned(rm, t *Expr, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_fp_signed(c.ptr, rm.ptr, t.ptr, sort.ptr))
}
// MkFPToFPUnsigned converts an unsigned bit-vector to a floating-point number with rounding.
func (c *Context) MkFPToFPUnsigned(rm, t *Expr, sort *Sort) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_fp_unsigned(c.ptr, rm.ptr, t.ptr, sort.ptr))
}
// MkFPToSBV converts a floating-point number to a signed bit-vector with rounding.
func (c *Context) MkFPToSBV(rm, t *Expr, sz uint) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_sbv(c.ptr, rm.ptr, t.ptr, C.uint(sz)))
}
// MkFPToUBV converts a floating-point number to an unsigned bit-vector with rounding.
func (c *Context) MkFPToUBV(rm, t *Expr, sz uint) *Expr {
return newExpr(c, C.Z3_mk_fpa_to_ubv(c.ptr, rm.ptr, t.ptr, C.uint(sz)))
}

View file

@ -230,3 +230,58 @@ func (c *Context) MkSeqReplaceRe(seq, re, replacement *Expr) *Expr {
func (c *Context) MkSeqReplaceReAll(seq, re, replacement *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_replace_re_all(c.ptr, seq.ptr, re.ptr, replacement.ptr))
}
// MkSeqReplaceAll replaces all occurrences of src with dst in seq.
func (c *Context) MkSeqReplaceAll(seq, src, dst *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_replace_all(c.ptr, seq.ptr, src.ptr, dst.ptr))
}
// MkSeqNth retrieves the n-th element of a sequence as a single-element expression.
func (c *Context) MkSeqNth(seq, index *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_nth(c.ptr, seq.ptr, index.ptr))
}
// MkSeqLastIndex returns the last index of substr in seq.
func (c *Context) MkSeqLastIndex(seq, substr *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_last_index(c.ptr, seq.ptr, substr.ptr))
}
// MkSeqMap applies a function to each element of a sequence, returning a new sequence.
func (c *Context) MkSeqMap(f, seq *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_map(c.ptr, f.ptr, seq.ptr))
}
// MkSeqMapi applies an indexed function to each element of a sequence, returning a new sequence.
func (c *Context) MkSeqMapi(f, i, seq *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_mapi(c.ptr, f.ptr, i.ptr, seq.ptr))
}
// MkSeqFoldl applies a fold-left operation to a sequence.
func (c *Context) MkSeqFoldl(f, a, seq *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_foldl(c.ptr, f.ptr, a.ptr, seq.ptr))
}
// MkSeqFoldli applies an indexed fold-left operation to a sequence.
func (c *Context) MkSeqFoldli(f, i, a, seq *Expr) *Expr {
return newExpr(c, C.Z3_mk_seq_foldli(c.ptr, f.ptr, i.ptr, a.ptr, seq.ptr))
}
// MkStrLt creates a string less-than comparison.
func (c *Context) MkStrLt(s1, s2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_str_lt(c.ptr, s1.ptr, s2.ptr))
}
// MkStrLe creates a string less-than-or-equal comparison.
func (c *Context) MkStrLe(s1, s2 *Expr) *Expr {
return newExpr(c, C.Z3_mk_str_le(c.ptr, s1.ptr, s2.ptr))
}
// MkStringToCode converts a single-character string to its Unicode code point.
func (c *Context) MkStringToCode(s *Expr) *Expr {
return newExpr(c, C.Z3_mk_string_to_code(c.ptr, s.ptr))
}
// MkStringFromCode converts a Unicode code point to a single-character string.
func (c *Context) MkStringFromCode(code *Expr) *Expr {
return newExpr(c, C.Z3_mk_string_from_code(c.ptr, code.ptr))
}

View file

@ -52,3 +52,10 @@ func (s *Simplifier) GetHelp() string {
func (s *Simplifier) GetParamDescrs() *ParamDescrs {
return newParamDescrs(s.ctx, C.Z3_simplifier_get_param_descrs(s.ctx.ptr, s.ptr))
}
// GetSimplifierDescr returns a description of the simplifier with the given name.
func (c *Context) GetSimplifierDescr(name string) string {
cName := C.CString(name)
defer C.free(unsafe.Pointer(cName))
return C.GoString(C.Z3_simplifier_get_descr(c.ptr, cName))
}

View file

@ -501,6 +501,64 @@ func (fi *FuncInterp) GetArity() uint {
return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr))
}
// FuncEntry represents a single entry in a FuncInterp finite map.
type FuncEntry struct {
ctx *Context
ptr C.Z3_func_entry
}
// newFuncEntry creates a new FuncEntry and manages its reference count.
func newFuncEntry(ctx *Context, ptr C.Z3_func_entry) *FuncEntry {
e := &FuncEntry{ctx: ctx, ptr: ptr}
C.Z3_func_entry_inc_ref(ctx.ptr, ptr)
runtime.SetFinalizer(e, func(entry *FuncEntry) {
C.Z3_func_entry_dec_ref(entry.ctx.ptr, entry.ptr)
})
return e
}
// GetEntry returns the i-th entry in the function interpretation.
func (fi *FuncInterp) GetEntry(i uint) *FuncEntry {
return newFuncEntry(fi.ctx, C.Z3_func_interp_get_entry(fi.ctx.ptr, fi.ptr, C.uint(i)))
}
// SetElse sets the else value of the function interpretation.
func (fi *FuncInterp) SetElse(val *Expr) {
C.Z3_func_interp_set_else(fi.ctx.ptr, fi.ptr, val.ptr)
}
// AddEntry adds a new entry to the function interpretation.
// The args slice provides the argument values and val is the return value.
func (fi *FuncInterp) AddEntry(args []*Expr, val *Expr) {
vec := C.Z3_mk_ast_vector(fi.ctx.ptr)
C.Z3_ast_vector_inc_ref(fi.ctx.ptr, vec)
defer C.Z3_ast_vector_dec_ref(fi.ctx.ptr, vec)
for _, a := range args {
C.Z3_ast_vector_push(fi.ctx.ptr, vec, a.ptr)
}
C.Z3_func_interp_add_entry(fi.ctx.ptr, fi.ptr, vec, val.ptr)
}
// GetValue returns the return value of the function entry.
func (e *FuncEntry) GetValue() *Expr {
return newExpr(e.ctx, C.Z3_func_entry_get_value(e.ctx.ptr, e.ptr))
}
// GetNumArgs returns the number of arguments in the function entry.
func (e *FuncEntry) GetNumArgs() uint {
return uint(C.Z3_func_entry_get_num_args(e.ctx.ptr, e.ptr))
}
// GetArg returns the i-th argument of the function entry.
func (e *FuncEntry) GetArg(i uint) *Expr {
return newExpr(e.ctx, C.Z3_func_entry_get_arg(e.ctx.ptr, e.ptr, C.uint(i)))
}
// HasInterp reports whether the model contains an interpretation for the given declaration.
func (m *Model) HasInterp(decl *FuncDecl) bool {
return bool(C.Z3_model_has_interp(m.ctx.ptr, m.ptr, decl.ptr))
}
// SortUniverse returns the universe of values for an uninterpreted sort in the model.
// The universe is represented as a list of distinct expressions.
// Returns nil if the sort is not an uninterpreted sort in this model.
@ -511,3 +569,9 @@ func (m *Model) SortUniverse(sort *Sort) []*Expr {
}
return astVectorToExprs(m.ctx, vec)
}
// Translate creates a copy of the model in the target context.
func (m *Model) Translate(target *Context) *Model {
ptr := C.Z3_model_translate(m.ctx.ptr, m.ptr, target.ptr)
return newModel(target, ptr)
}

View file

@ -78,6 +78,72 @@ func (c *Context) TacticSkip() *Tactic {
return newTactic(c, C.Z3_tactic_skip(c.ptr))
}
// TryFor returns a tactic that applies t for at most ms milliseconds.
// If t does not terminate in ms milliseconds, then it fails.
func (t *Tactic) TryFor(ms uint) *Tactic {
return newTactic(t.ctx, C.Z3_tactic_try_for(t.ctx.ptr, t.ptr, C.uint(ms)))
}
// UsingParams returns a tactic that applies t using the given parameters.
func (t *Tactic) UsingParams(params *Params) *Tactic {
return newTactic(t.ctx, C.Z3_tactic_using_params(t.ctx.ptr, t.ptr, params.ptr))
}
// GetParamDescrs returns parameter descriptions for the tactic.
func (t *Tactic) GetParamDescrs() *ParamDescrs {
return newParamDescrs(t.ctx, C.Z3_tactic_get_param_descrs(t.ctx.ptr, t.ptr))
}
// ApplyEx applies the tactic to a goal with the given parameters.
func (t *Tactic) ApplyEx(g *Goal, params *Params) *ApplyResult {
return newApplyResult(t.ctx, C.Z3_tactic_apply_ex(t.ctx.ptr, t.ptr, g.ptr, params.ptr))
}
// TacticFailIf creates a tactic that fails if the probe p evaluates to false.
func (c *Context) TacticFailIf(p *Probe) *Tactic {
return newTactic(c, C.Z3_tactic_fail_if(c.ptr, p.ptr))
}
// TacticFailIfNotDecided creates a tactic that fails if the goal is not
// trivially satisfiable (empty) or trivially unsatisfiable (contains false).
func (c *Context) TacticFailIfNotDecided() *Tactic {
return newTactic(c, C.Z3_tactic_fail_if_not_decided(c.ptr))
}
// ParOr creates a tactic that applies the given tactics in parallel.
func (c *Context) ParOr(tactics []*Tactic) *Tactic {
cTactics := make([]C.Z3_tactic, len(tactics))
for i, t := range tactics {
cTactics[i] = t.ptr
}
return newTactic(c, C.Z3_tactic_par_or(c.ptr, C.uint(len(tactics)), &cTactics[0]))
}
// ParAndThen creates a tactic that applies t to a goal and then t2 to every
// subgoal produced by t, processing subgoals in parallel.
func (t *Tactic) ParAndThen(t2 *Tactic) *Tactic {
return newTactic(t.ctx, C.Z3_tactic_par_and_then(t.ctx.ptr, t.ptr, t2.ptr))
}
// GetTacticDescr returns a description of the tactic with the given name.
func (c *Context) GetTacticDescr(name string) string {
cName := C.CString(name)
defer C.free(unsafe.Pointer(cName))
return C.GoString(C.Z3_tactic_get_descr(c.ptr, cName))
}
// NewSolverFromTactic creates a solver from the given tactic.
// The solver uses the tactic to solve goals.
func (c *Context) NewSolverFromTactic(t *Tactic) *Solver {
ptr := C.Z3_mk_solver_from_tactic(c.ptr, t.ptr)
s := &Solver{ctx: c, ptr: ptr}
C.Z3_solver_inc_ref(c.ptr, ptr)
runtime.SetFinalizer(s, func(solver *Solver) {
C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
})
return s
}
// Goal represents a set of formulas that can be solved or transformed.
type Goal struct {
ctx *Context
@ -134,6 +200,29 @@ func (g *Goal) Reset() {
C.Z3_goal_reset(g.ctx.ptr, g.ptr)
}
// Depth returns the depth of the goal.
// It tracks how many times the goal was transformed by a tactic.
func (g *Goal) Depth() uint {
return uint(C.Z3_goal_depth(g.ctx.ptr, g.ptr))
}
// Precision returns the precision of the goal as a uint.
// Possible values: 0 = precise, 1 = under-approximation, 2 = over-approximation, 3 = under+over.
func (g *Goal) Precision() uint {
return uint(C.Z3_goal_precision(g.ctx.ptr, g.ptr))
}
// Translate creates a copy of the goal in the target context.
func (g *Goal) Translate(target *Context) *Goal {
return newGoal(target, C.Z3_goal_translate(g.ctx.ptr, g.ptr, target.ptr))
}
// ConvertModel converts a model from the original goal into a model for this goal.
// Use this when a tactic has transformed the goal and you need a model for the original.
func (g *Goal) ConvertModel(m *Model) *Model {
return newModel(g.ctx, C.Z3_goal_convert_model(g.ctx.ptr, g.ptr, m.ptr))
}
// String returns the string representation of the goal.
func (g *Goal) String() string {
return C.GoString(C.Z3_goal_to_string(g.ctx.ptr, g.ptr))
@ -243,6 +332,13 @@ func (p *Probe) Not() *Probe {
return newProbe(p.ctx, C.Z3_probe_not(p.ctx.ptr, p.ptr))
}
// GetProbeDescr returns a description of the probe with the given name.
func (c *Context) GetProbeDescr(name string) string {
cName := C.CString(name)
defer C.free(unsafe.Pointer(cName))
return C.GoString(C.Z3_probe_get_descr(c.ptr, cName))
}
// Params represents a parameter set.
type Params struct {
ctx *Context

View file

@ -471,6 +471,33 @@ func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDe
return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
}
// MkRecFuncDecl creates a recursive function declaration.
// After creating, use AddRecDef to provide the function body.
func (c *Context) MkRecFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl {
cDomain := make([]C.Z3_sort, len(domain))
for i, s := range domain {
cDomain[i] = s.ptr
}
var domainPtr *C.Z3_sort
if len(domain) > 0 {
domainPtr = &cDomain[0]
}
return newFuncDecl(c, C.Z3_mk_rec_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
}
// AddRecDef adds the definition (body) for a recursive function created with MkRecFuncDecl.
func (c *Context) AddRecDef(f *FuncDecl, args []*Expr, body *Expr) {
cArgs := make([]C.Z3_ast, len(args))
for i, a := range args {
cArgs[i] = a.ptr
}
var argsPtr *C.Z3_ast
if len(args) > 0 {
argsPtr = &cArgs[0]
}
C.Z3_add_rec_def(c.ptr, f.ptr, C.uint(len(args)), argsPtr, body.ptr)
}
// MkApp creates a function application.
func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr {
cArgs := make([]C.Z3_ast, len(args))

View file

@ -80,6 +80,16 @@ public class AST extends Z3Object implements Comparable<AST>
return Native.getAstId(getContext().nCtx(), getNativeObject());
}
/**
* The depth of the AST (max nodes on any root-to-leaf path).
* @throws Z3Exception on error
* @return an int
**/
public int getDepth()
{
return Native.getDepth(getContext().nCtx(), getNativeObject());
}
/**
* Translates (copies) the AST to the Context {@code ctx}.
* @param ctx A context

View file

@ -59,6 +59,16 @@ public class ArraySort<D extends Sort, R extends Sort> extends Sort
Native.getArraySortRange(getContext().nCtx(), getNativeObject()));
}
/**
* The number of dimensions of the array sort.
* @throws Z3Exception on error
* @return an int
**/
public int getArity()
{
return Native.getArrayArity(getContext().nCtx(), getNativeObject());
}
ArraySort(Context ctx, long obj)
{
super(ctx, obj);

View file

@ -1152,6 +1152,27 @@ public class Context implements AutoCloseable {
return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject()));
}
/**
* Creates the absolute value of an arithmetic expression.
* Remarks: The argument must have integer or real sort.
**/
public <R extends ArithSort> ArithExpr<R> mkAbs(Expr<? extends R> arg)
{
checkContextMatch(arg);
return (ArithExpr<R>) Expr.create(this, Native.mkAbs(nCtx(), arg.getNativeObject()));
}
/**
* Creates an integer divisibility predicate (t1 divides t2).
* Remarks: Both arguments must have integer sort.
**/
public BoolExpr mkDivides(Expr<IntSort> t1, Expr<IntSort> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
return new BoolExpr(this, Native.mkDivides(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
}
/**
* Bitwise negation.
* Remarks: The argument must have a bit-vector

View file

@ -33,6 +33,17 @@ public class DatatypeSort<R> extends Sort
getNativeObject());
}
/**
* Indicates whether the datatype sort is recursive.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isRecursive()
{
return Native.isRecursiveDatatypeSort(getContext().nCtx(),
getNativeObject());
}
/**
* The constructors.
*

View file

@ -244,6 +244,15 @@ public class Expr<R extends Sort> extends AST
return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
}
/**
* Return the numeral value as a double.
* The expression must be a numeral or an algebraic number.
**/
public double getNumeralDouble()
{
return Native.getNumeralDouble(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the term is well-sorted.
*
@ -306,6 +315,26 @@ public class Expr<R extends Sort> extends AST
return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the term is ground (contains no free variables).
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isGround()
{
return Native.isGround(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the term is a lambda expression.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isLambda()
{
return Native.isLambda(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the term has Boolean sort.
* @throws Z3Exception on error

View file

@ -32,7 +32,17 @@ public class FPExpr extends Expr<FPSort>
* @throws Z3Exception
*/
public int getSBits() { return ((FPSort)getSort()).getSBits(); }
/**
* Indicates whether the floating-point expression is a numeral.
* @throws Z3Exception on error
* @return a boolean
**/
public boolean isNumeral()
{
return Native.fpaIsNumeral(getContext().nCtx(), getNativeObject());
}
public FPExpr(Context ctx, long obj)
{
super(ctx, obj);

View file

@ -52,6 +52,33 @@ public class IntNum extends IntExpr
return res.value;
}
/**
* Retrieve the unsigned 32-bit value.
* The returned Java {@code int} holds the raw bit pattern;
* use {@code Integer.toUnsignedLong(v)} for unsigned interpretation.
**/
public int getUint()
{
Native.IntPtr res = new Native.IntPtr();
if (!Native.getNumeralUint(getContext().nCtx(), getNativeObject(), res))
throw new Z3Exception("Numeral is not a uint");
return res.value;
}
/**
* Retrieve the unsigned 64-bit value.
* The returned Java {@code long} holds the raw bit pattern;
* use {@code Long.toUnsignedString(v)} or {@link #getBigInteger()}
* for values exceeding {@code Long.MAX_VALUE}.
**/
public long getUint64()
{
Native.LongPtr res = new Native.LongPtr();
if (!Native.getNumeralUint64(getContext().nCtx(), getNativeObject(), res))
throw new Z3Exception("Numeral is not a uint64");
return res.value;
}
/**
* Retrieve the BigInteger value.
**/

View file

@ -60,6 +60,34 @@ public class RatNum extends RealExpr
return new BigInteger(n.toString());
}
/**
* Retrieve the numerator and denominator as 64-bit integers.
* Throws if the value does not fit in 64-bit integers.
* @return a two-element array [numerator, denominator]
**/
public long[] getSmall()
{
Native.LongPtr num = new Native.LongPtr();
Native.LongPtr den = new Native.LongPtr();
if (!Native.getNumeralSmall(getContext().nCtx(), getNativeObject(), num, den))
throw new Z3Exception("Numeral does not fit in int64");
return new long[] { num.value, den.value };
}
/**
* Retrieve the numerator and denominator as 64-bit integers.
* Returns null if the value does not fit in 64-bit integers.
* @return a two-element array [numerator, denominator], or null
**/
public long[] getRationalInt64()
{
Native.LongPtr num = new Native.LongPtr();
Native.LongPtr den = new Native.LongPtr();
if (!Native.getNumeralRationalInt64(getContext().nCtx(), getNativeObject(), num, den))
return null;
return new long[] { num.value, den.value };
}
/**
* Returns a string representation in decimal notation.
* Remarks: The result

View file

@ -1024,6 +1024,16 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
val(value: string): Seq<Name> {
return new SeqImpl(check(Z3.mk_string(contextPtr, value)));
},
fromCode(code: Arith<Name> | number | bigint): Seq<Name> {
const codeExpr = isArith(code) ? code : Int.val(code);
return new SeqImpl(check(Z3.mk_string_from_code(contextPtr, codeExpr.ast)));
},
fromInt(n: Arith<Name> | number | bigint): Seq<Name> {
const nExpr = isArith(n) ? n : Int.val(n);
return new SeqImpl(check(Z3.mk_int_to_str(contextPtr, nExpr.ast)));
},
};
const Seq = {
@ -1093,6 +1103,9 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
): SMTArray<Name, [DomainSort], RangeSort> {
return new ArrayImpl<[DomainSort], RangeSort>(check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr)));
},
fromFunc(f: FuncDecl<Name>): SMTArray<Name> {
return new ArrayImpl(check(Z3.mk_as_array(contextPtr, f.ptr)));
},
};
const Set = {
// reference: https://z3prover.github.io/api/html/namespacez3py.html#a545f894afeb24caa1b88b7f2a324ee7e
@ -2812,6 +2825,11 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
return this.getUniverse(sort) as AstVector<Name, AnyExpr<Name>>;
}
translate(target: Context<Name>): Model<Name> {
const ptr = check(Z3.model_translate(contextPtr, this.ptr, target.ptr));
return new (target.Model as unknown as new (ptr: Z3_model) => Model<Name>)(ptr);
}
release() {
Z3.model_dec_ref(contextPtr, this.ptr);
this._ptr = null;
@ -4376,6 +4394,52 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
const dstSeq = isSeq(dst) ? dst : String.val(dst);
return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_all(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
}
replaceRe(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
const dstSeq = isSeq(dst) ? dst : String.val(dst);
return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_re(contextPtr, this.ast, re.ast, dstSeq.ast)));
}
replaceReAll(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
const dstSeq = isSeq(dst) ? dst : String.val(dst);
return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_re_all(contextPtr, this.ast, re.ast, dstSeq.ast)));
}
toInt(): Arith<Name> {
return new ArithImpl(check(Z3.mk_str_to_int(contextPtr, this.ast)));
}
toCode(): Arith<Name> {
return new ArithImpl(check(Z3.mk_string_to_code(contextPtr, this.ast)));
}
lt(other: Seq<Name, ElemSort> | string): Bool<Name> {
const otherSeq = isSeq(other) ? other : String.val(other);
return new BoolImpl(check(Z3.mk_str_lt(contextPtr, this.ast, otherSeq.ast)));
}
le(other: Seq<Name, ElemSort> | string): Bool<Name> {
const otherSeq = isSeq(other) ? other : String.val(other);
return new BoolImpl(check(Z3.mk_str_le(contextPtr, this.ast, otherSeq.ast)));
}
map(f: Expr<Name>): Seq<Name> {
return new SeqImpl(check(Z3.mk_seq_map(contextPtr, f.ast, this.ast)));
}
mapi(f: Expr<Name>, i: Arith<Name> | number | bigint): Seq<Name> {
const iExpr = isArith(i) ? i : Int.val(i);
return new SeqImpl(check(Z3.mk_seq_mapi(contextPtr, f.ast, iExpr.ast, this.ast)));
}
foldl(f: Expr<Name>, a: Expr<Name>): Expr<Name> {
return _toExpr(check(Z3.mk_seq_foldl(contextPtr, f.ast, a.ast, this.ast)));
}
foldli(f: Expr<Name>, i: Arith<Name> | number | bigint, a: Expr<Name>): Expr<Name> {
const iExpr = isArith(i) ? i : Int.val(i);
return _toExpr(check(Z3.mk_seq_foldli(contextPtr, f.ast, iExpr.ast, a.ast, this.ast)));
}
}
class ReSortImpl<SeqSortRef extends SeqSort<Name> = SeqSort<Name>> extends SortImpl implements ReSort<Name, SeqSortRef> {

View file

@ -1883,6 +1883,14 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
*/
sortUniverse(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
/**
* Translate the model to a different context.
*
* @param target - The target context
* @returns A new model in the target context
*/
translate(target: Context<Name>): Model<Name>;
/**
* Manually decrease the reference count of the model
* This is automatically done when the model is garbage collected,
@ -2915,6 +2923,12 @@ export interface SMTArrayCreation<Name extends string> {
domain: DomainSort,
value: SortToExprMap<RangeSort, Name>,
): SMTArray<Name, [DomainSort], RangeSort>;
/**
* Create an array from a function declaration.
* The resulting array maps each input to the output of the function.
*/
fromFunc(f: FuncDecl<Name>): SMTArray<Name>;
}
export type NonEmptySortArray<Name extends string = 'main'> = [Sort<Name>, ...Array<Sort<Name>>];
@ -3469,6 +3483,16 @@ export interface StringCreation<Name extends string> {
* Create a string value
*/
val(value: string): Seq<Name>;
/**
* Create a single-character string from a Unicode code point (str.from_code).
*/
fromCode(code: Arith<Name> | number | bigint): Seq<Name>;
/**
* Convert an integer expression to its string representation (int.to.str).
*/
fromInt(n: Arith<Name> | number | bigint): Seq<Name>;
}
/** @category String/Sequence */
@ -3543,6 +3567,60 @@ export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> =
/** @category Operations */
replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
/** @category Operations */
replaceRe(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
/** @category Operations */
replaceReAll(re: Re<Name>, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
/**
* Convert a string to its integer value (str.to.int).
* @category Operations
*/
toInt(): Arith<Name>;
/**
* Convert a single-character string to its Unicode code point (str.to_code).
* @category Operations
*/
toCode(): Arith<Name>;
/**
* String less-than comparison (str.lt).
* @category Operations
*/
lt(other: Seq<Name, ElemSort> | string): Bool<Name>;
/**
* String less-than-or-equal comparison (str.le).
* @category Operations
*/
le(other: Seq<Name, ElemSort> | string): Bool<Name>;
/**
* Apply function f to each element of the sequence (seq.map).
* @category Operations
*/
map(f: Expr<Name>): Seq<Name>;
/**
* Apply function f to each element and its index in the sequence (seq.mapi).
* @category Operations
*/
mapi(f: Expr<Name>, i: Arith<Name> | number | bigint): Seq<Name>;
/**
* Left-fold function f over the sequence with initial accumulator a (seq.foldl).
* @category Operations
*/
foldl(f: Expr<Name>, a: Expr<Name>): Expr<Name>;
/**
* Left-fold function f with index over the sequence with initial accumulator a (seq.foldli).
* @category Operations
*/
foldli(f: Expr<Name>, i: Arith<Name> | number | bigint, a: Expr<Name>): Expr<Name>;
}
///////////////////////

View file

@ -1692,6 +1692,8 @@ struct
let av = Z3native.model_get_sort_universe (gc x) x s in
AST.ASTVector.to_expr_list av
let translate (x:model) (to_ctx:context) = Z3native.model_translate (gc x) x to_ctx
let to_string (x:model) = Z3native.model_to_string (gc x) x
end
@ -2223,7 +2225,7 @@ struct
let div (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_div ctx a b
let neg (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
let inv (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
let inv (ctx:context) (a:rcf_num) = Z3native.rcf_inv ctx a
let power (ctx:context) (a:rcf_num) (k:int) = Z3native.rcf_power ctx a k

View file

@ -3057,6 +3057,10 @@ sig
@return A list of expressions, where each is an element of the universe of the sort *)
val sort_universe : model -> Sort.sort -> Expr.expr list
(** Translate the model to a different context.
@return A new model in the target context *)
val translate : model -> context -> model
(** Conversion of models to strings.
@return A string representation of the model. *)
val to_string : model -> string

View file

@ -4652,6 +4652,45 @@ def BVRedOr(a):
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
def BvNand(a, b):
"""Return the bitwise NAND of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvNand(x, y)
bvnand(x, y)
"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvnand(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BvNor(a, b):
"""Return the bitwise NOR of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvNor(x, y)
bvnor(x, y)
"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BvXnor(a, b):
"""Return the bitwise XNOR of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvXnor(x, y)
bvxnor(x, y)
"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvxnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def BVAddNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector addition does not overflow"""
_check_bv_args(a, b)
@ -8463,8 +8502,11 @@ class Optimize(Z3PPObject):
self._on_models_id = None
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self, memo={}):
return Optimize(self.optimize, self.ctx)
return self.translate(self.ctx)
def __del__(self):
if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
@ -8672,6 +8714,19 @@ class Optimize(Z3PPObject):
"""
return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
def translate(self, target):
"""Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
>>> c1 = Context()
>>> c2 = Context()
>>> o1 = Optimize(ctx=c1)
>>> o2 = o1.translate(c2)
"""
if z3_debug():
_z3_assert(isinstance(target, Context), "argument must be a Z3 context")
opt = Z3_optimize_translate(self.ctx.ref(), self.optimize, target.ref())
return Optimize(opt, target)
def set_on_model(self, on_model):
"""Register a callback that is invoked with every incremental improvement to
objective values. The callback takes a model as argument.

View file

@ -7656,7 +7656,7 @@ extern "C" {
/**
\brief Convert a solver into a DIMACS formatted string.
\sa Z3_goal_to_diamcs_string for requirements.
\sa Z3_goal_to_dimacs_string for requirements.
def_API('Z3_solver_to_dimacs_string', STRING, (_in(CONTEXT), _in(SOLVER), _in(BOOL)))
*/

View file

@ -173,7 +173,7 @@ void act_cache::insert(expr * k, unsigned offset, expr * v) {
DEBUG_CODE(expected_tag = 0;);
}
DEBUG_CODE({
expr * v2;
expr * v2 = nullptr;
SASSERT(m_table.find(e, v2));
SASSERT(v == UNTAG(expr*, v2));
SASSERT(expected_tag == GET_TAG(v2));
@ -195,7 +195,7 @@ expr * act_cache::find(expr * k, unsigned offset) {
SASSERT(m_unused > 0);
m_unused--;
DEBUG_CODE({
expr * v;
expr * v = nullptr;
SASSERT(m_table.find(e, v));
SASSERT(GET_TAG(v) == 1);
});

View file

@ -1402,6 +1402,7 @@ namespace euf {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}

View file

@ -354,8 +354,8 @@ void bit2int::visit(app* n) {
//
// (pos1 - neg1) mod e2 = (pos1 + (e2 - (neg1 mod e2))) mod e2
//
unsigned sz_p, sz_n, sz;
bool sign_p, sign_n;
unsigned sz_p = 0, sz_n = 0, sz;
bool sign_p = false, sign_n = false;
expr_ref tmp_p(m), tmp_n(m);
VERIFY(extract_bv(pos1, sz_p, sign_p, tmp_p));
VERIFY(extract_bv(neg1, sz_n, sign_n, tmp_n));

View file

@ -64,7 +64,7 @@ struct enum2bv_rewriter::imp {
unsigned bv_size = get_bv_size(s);
sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
if (is_unate(s))
return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort.get());
return m_bv.mk_numeral(rational((1u << idx) - 1), bv_sort.get());
else
return m_bv.mk_numeral(rational(idx), bv_sort.get());
}

View file

@ -226,7 +226,6 @@ namespace seq {
return
e.ls.size() == 1 && e.rs.size() == 1 &&
seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b);
return false;
}
bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) {

View file

@ -4391,6 +4391,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
// disabled
#if 0
expr_ref hd(m()), tl(m());
if (get_head_tail(a, hd, tl)) {
//result = re().mk_in_re(tl, re().mk_derivative(hd, b));
@ -4430,6 +4432,8 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
return BR_REWRITE_FULL;
}
#endif
#if 0
unsigned len = 0;
if (has_fixed_length_constraint(b, len)) {

View file

@ -0,0 +1,190 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
injectivity_simplifier.h
Abstract:
Dependent expression simplifier for injectivity rewriting.
- Discover axioms of the form `forall x. (= (g (f x)) x)`
Mark `f` as injective
- Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective.
Author:
Nicolas Braud-Santoni (t-nibrau) 2017-08-10
Ported to simplifier by Nikolaj Bjorner (nbjorner) 2023
Notes:
* does not support cores nor proofs
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/rewriter_def.h"
class injectivity_simplifier : public dependent_expr_simplifier {
struct inj_map : public obj_map<func_decl, obj_hashtable<func_decl>*> {
ast_manager& m;
inj_map(ast_manager& m) : m(m) {}
~inj_map() {
for (auto& kv : *this) {
for (func_decl* f : *kv.get_value())
m.dec_ref(f);
m.dec_ref(kv.m_key);
dealloc(kv.m_value);
}
}
void insert(func_decl* f, func_decl* g) {
obj_hashtable<func_decl>* inverses;
if (!obj_map::find(f, inverses)) {
m.inc_ref(f);
inverses = alloc(obj_hashtable<func_decl>);
obj_map::insert(f, inverses);
}
if (!inverses->contains(g)) {
m.inc_ref(g);
inverses->insert(g);
}
}
};
struct rw_cfg : public default_rewriter_cfg {
ast_manager& m;
inj_map& m_map;
rw_cfg(ast_manager& m, inj_map& map) : m(m), m_map(map) {}
br_status reduce_app(func_decl* f, unsigned num, expr* const* args,
expr_ref& result, proof_ref& result_pr) {
if (num != 2 || !m.is_eq(f))
return BR_FAILED;
if (!is_app(args[0]) || !is_app(args[1]))
return BR_FAILED;
app* a = to_app(args[0]);
app* b = to_app(args[1]);
if (a->get_decl() != b->get_decl())
return BR_FAILED;
if (a->get_num_args() != 1 || b->get_num_args() != 1)
return BR_FAILED;
if (!m_map.contains(a->get_decl()))
return BR_FAILED;
SASSERT(a->get_arg(0)->get_sort() == b->get_arg(0)->get_sort());
result = m.mk_eq(a->get_arg(0), b->get_arg(0));
result_pr = nullptr;
return BR_DONE;
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(ast_manager& m, inj_map& map) :
rewriter_tpl<rw_cfg>(m, false, m_cfg),
m_cfg(m, map) {}
};
inj_map m_map;
rw m_rw;
bool is_axiom(expr* n, func_decl*& f, func_decl*& g) {
if (!is_forall(n))
return false;
quantifier* q = to_quantifier(n);
if (q->get_num_decls() != 1)
return false;
expr* body = q->get_expr();
if (!m.is_eq(body))
return false;
app* body_a = to_app(body);
if (body_a->get_num_args() != 2)
return false;
expr* a = body_a->get_arg(0);
expr* b = body_a->get_arg(1);
if (is_app(a) && is_var(b)) {
// keep a, b as-is
}
else if (is_app(b) && is_var(a)) {
std::swap(a, b);
}
else
return false;
app* a_app = to_app(a);
var* b_var = to_var(b);
if (b_var->get_idx() != 0)
return false;
if (a_app->get_num_args() != 1)
return false;
g = a_app->get_decl();
expr* a_body = a_app->get_arg(0);
if (!is_app(a_body))
return false;
app* a_body_app = to_app(a_body);
if (a_body_app->get_num_args() != 1)
return false;
f = a_body_app->get_decl();
expr* a_body_body = a_body_app->get_arg(0);
if (a_body_body != b_var)
return false;
return true;
}
public:
injectivity_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) :
dependent_expr_simplifier(m, s), m_map(m), m_rw(m, m_map) {}
char const* name() const override { return "injectivity"; }
void reduce() override {
// Phase 1: Scan for injectivity axioms
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
func_decl* fn = nullptr;
func_decl* inv = nullptr;
if (is_axiom(d.fml(), fn, inv)) {
TRACE(injectivity, tout << "Marking " << fn->get_name() << " as injective\n";);
m_map.insert(fn, inv);
}
}
// Phase 2: Rewrite using injectivity
expr_ref new_fml(m);
proof_ref new_pr(m);
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
m_rw(d.fml(), new_fml, new_pr);
if (new_fml != d.fml())
m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep()));
}
}
};

View file

@ -287,27 +287,36 @@ namespace sls {
if (m.is_eq(e)) {
a = g.find(to_app(e)->get_arg(0));
b = g.find(to_app(e)->get_arg(1));
}
if (lit.sign() && m.is_eq(e)) {
if (a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
UNREACHABLE();
if (lit.sign()) {
if (a && b && a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
UNREACHABLE();
}
}
else {
if (a && b && a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
}
else if (!lit.sign() && m.is_eq(e)) {
if (a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
else if (to_app(e)->get_family_id() != basic_family_id) {
auto* ne = g.find(e);
if (lit.sign()) {
auto* nf = g.find(m.mk_false());
if (ne && nf && ne->get_root() != nf->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
else {
auto* nt = g.find(m.mk_true());
if (ne && nt && ne->get_root() != nt->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
}
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not alse " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}

View file

@ -613,11 +613,13 @@ public:
#endif
calculate_by_modulo();
#ifdef Z3DEBUG
CTRACE(hnf_calc, m_H != m_W,
tout << "A = "; m_A_orig.print(tout, 4); tout << std::endl;
tout << "H = "; m_H.print(tout, 4); tout << std::endl;
tout << "W = "; m_W.print(tout, 4); tout << std::endl;);
SASSERT (m_H == m_W);
if (!m_cancelled) {
CTRACE(hnf_calc, m_H != m_W,
tout << "A = "; m_A_orig.print(tout, 4); tout << std::endl;
tout << "H = "; m_H.print(tout, 4); tout << std::endl;
tout << "W = "; m_W.print(tout, 4); tout << std::endl;);
SASSERT (m_H == m_W);
}
#endif
}

View file

@ -81,10 +81,15 @@ public:
void backup_x() { m_backup_x = m_r_x; }
void restore_x() {
m_r_x = m_backup_x;
m_r_x.reserve(m_m());
unsigned n = m_r_A.column_count();
unsigned backup_sz = m_backup_x.size();
unsigned copy_sz = std::min(backup_sz, n);
for (unsigned j = 0; j < copy_sz; j++)
m_r_x[j] = m_backup_x[j];
}
unsigned backup_x_size() const { return m_backup_x.size(); }
vector<impq> const& r_x() const { return m_r_x; }
impq& r_x(unsigned j) { return m_r_x[j]; }
impq const& r_x(unsigned j) const { return m_r_x[j]; }

View file

@ -467,6 +467,8 @@ namespace lp {
return ret;
}
lp_status lar_solver::solve() {
if (m_imp->m_status == lp_status::INFEASIBLE || m_imp->m_status == lp_status::CANCELLED)
return m_imp->m_status;
@ -2303,16 +2305,6 @@ namespace lp {
return m_imp->m_constraints.add_term_constraint(j, m_imp->m_columns[j].term(), kind, rs);
}
struct lar_solver::scoped_backup {
lar_solver& m_s;
scoped_backup(lar_solver& s) : m_s(s) {
m_s.get_core_solver().backup_x();
}
~scoped_backup() {
m_s.get_core_solver().restore_x();
}
};
void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq& right_side, u_dependency* dep) {
SASSERT(column_has_upper_bound(j));
if (column_has_lower_bound(j)) {

View file

@ -72,7 +72,6 @@ class lar_solver : public column_namer {
void clear_columns_with_changed_bounds();
struct scoped_backup;
public:
const indexed_uint_set& columns_with_changed_bounds() const;
void insert_to_columns_with_changed_bounds(unsigned j);
@ -437,7 +436,28 @@ public:
statistics& stats();
void backup_x() { get_core_solver().backup_x(); }
void restore_x() { get_core_solver().restore_x(); }
void restore_x() {
auto& cs = get_core_solver();
unsigned backup_sz = cs.backup_x_size();
unsigned current_sz = cs.m_n();
CTRACE(lar_solver_restore, backup_sz != current_sz,
tout << "restore_x: backup_sz=" << backup_sz
<< " current_sz=" << current_sz << "\n";);
cs.restore_x();
if (backup_sz < current_sz) {
// New columns were added after backup.
// Recalculate basic variable values from non-basic ones
// to restore the Ax=0 tableau invariant, then snap
// non-basic columns to their bounds and find a feasible solution.
for (unsigned i = 0; i < A_r().row_count(); i++)
set_column_value(r_basis()[i], get_basic_var_value_from_row(i));
move_non_basic_columns_to_bounds();
}
else {
SASSERT(ax_is_correct());
SASSERT(cs.m_r_solver.calc_current_x_is_feasible_include_non_basis());
}
}
void updt_params(params_ref const& p);
column_type get_column_type(unsigned j) const { return get_core_solver().m_column_types()[j]; }

View file

@ -1,4 +1,3 @@
/*++
Copyright (c) 2025 Microsoft Corporation
@ -85,4 +84,4 @@ namespace nla {
}
}
}
}
}

View file

@ -1,4 +1,3 @@
/*++
Copyright (c) 2025 Microsoft Corporation
@ -14,6 +13,9 @@
#pragma once
#include "util/uint_set.h"
#include "util/vector.h"
namespace nla {
class core;
@ -40,4 +42,4 @@ namespace nla {
indexed_uint_set const &vars() { return m_var_set; }
};
}
}

View file

@ -539,6 +539,7 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &
bool seen_minus = false;
bool seen_plus = false;
i = null_lpvar;
j = null_lpvar;
for(lp::lar_term::ival p : t) {
const auto & c = p.coeff();
if (c == 1) {
@ -1330,7 +1331,14 @@ lbool core::check(unsigned level) {
return l_false;
}
if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < params().arith_nl_nra_check_assignment_max_fail()) {
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment();
if (ret != l_true)
++m_check_assignment_fail_cnt;
}
if (no_effect() && should_run_bounded_nlsat())
ret = bounded_nlsat();
@ -1581,4 +1589,4 @@ void core::refine_pseudo_linear(monic const& m) {
}
SASSERT(nlvar != null_lpvar);
lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
}
}

View file

@ -63,6 +63,7 @@ class core {
unsigned m_nlsat_delay = 0;
unsigned m_nlsat_delay_bound = 0;
unsigned m_check_assignment_fail_cnt = 0;
bool should_run_bounded_nlsat();
lbool bounded_nlsat();
@ -94,6 +95,8 @@ class core {
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable indexed_uint_set m_active_var_set;
// hook installed by theory_lra for creating a multiplication definition
std::function<lpvar(unsigned, lpvar const*)> m_add_mul_def_hook;
reslimit m_nra_lim;
@ -215,6 +218,8 @@ public:
void add_idivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_idivision(q, x, y); }
void add_rdivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_rdivision(q, x, y); }
void add_bounded_division(lpvar q, lpvar x, lpvar y) { m_divisions.add_bounded_division(q, x, y); }
void set_add_mul_def_hook(std::function<lpvar(unsigned, lpvar const*)> const& f) { m_add_mul_def_hook = f; }
lpvar add_mul_def(unsigned sz, lpvar const* vs) { SASSERT(m_add_mul_def_hook); lpvar v = m_add_mul_def_hook(sz, vs); add_monic(v, sz, vs); return v; }
void set_relevant(std::function<bool(lpvar)>& is_relevant) { m_relevant = is_relevant; }
bool is_relevant(lpvar v) const { return !m_relevant || m_relevant(v); }
@ -478,4 +483,3 @@ inline std::ostream& operator<<(std::ostream& out, pp_factorization const& f) {
inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
} // end of namespace nla

View file

@ -12,6 +12,7 @@
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "util/params.h"
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"

View file

@ -432,4 +432,4 @@ std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::l
out << (evaluation ? "true" : "false");
out << "\n";
return out;
}
}

View file

@ -11,6 +11,7 @@
#include "math/lp/nra_solver.h"
#include "math/lp/nla_coi.h"
#include "nlsat/nlsat_solver.h"
#include "nlsat/nlsat_assignment.h"
#include "math/polynomial/polynomial.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/map.h"
@ -35,6 +36,13 @@ struct solver::imp {
scoped_ptr<scoped_anum_vector> m_values; // values provided by LRA solver
scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
nla::coi m_coi;
svector<lp::constraint_index> m_literal2constraint;
struct eq {
bool operator()(unsigned_vector const &a, unsigned_vector const &b) const {
return a == b;
}
};
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
nla::core& m_nla_core;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
@ -92,6 +100,44 @@ struct solver::imp {
denominators.push_back(den);
}
// Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable.
void mk_definition_assignment(unsigned v, polynomial_ref_vector &definitions) {
auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm);
if (m_nla_core.emons().is_monic_var(v)) {
auto const &m = m_nla_core.emons()[v];
auto vars = m.vars();
std::sort(vars.begin(), vars.end());
m_vars2mon.insert(vars, v);
for (auto v2 : vars) {
auto pv = definitions.get(v2);
if (!p)
p = pv;
else
p = pm.mul(p, pv);
}
}
else if (lra.column_has_term(v)) {
rational den(1);
for (auto const& [w, coeff] : lra.get_term(v))
den = lcm(den, denominator(coeff));
for (auto const& [w, coeff] : lra.get_term(v)) {
auto pw = definitions.get(w);
polynomial::polynomial_ref term(pm);
term = pm.mul(den * coeff, pw);
if (!p)
p = term;
else
p = pm.add(p, term);
}
}
else {
p = pm.mk_polynomial(lp2nl(v));
}
definitions.push_back(p);
}
void setup_solver_poly() {
m_coi.init();
auto &pm = m_nlsat->pm();
@ -273,7 +319,195 @@ struct solver::imp {
break;
}
return r;
}
}
void setup_assignment_solver() {
SASSERT(need_check());
reset();
m_literal2constraint.reset();
m_vars2mon.reset();
m_coi.init();
auto &pm = m_nlsat->pm();
polynomial_ref_vector definitions(pm);
for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
auto j = m_nlsat->mk_var(lra.var_is_int(v));
VERIFY(j == v);
m_lp2nl.insert(v, j);
scoped_anum a(am());
am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a);
mk_definition_assignment(v, definitions);
}
for (auto ci : m_coi.constraints()) {
auto &c = lra.constraints()[ci];
auto &pm = m_nlsat->pm();
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));
polynomial::polynomial_ref p(pm);
p = pm.mk_const(-den * rhs);
for (auto [coeff, v] : lhs) {
polynomial_ref poly(pm);
poly = pm.mul(den * coeff, definitions.get(v));
p = p + poly;
}
auto lit = add_constraint(p, ci, k);
m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
}
}
void process_polynomial_check_assignment(polynomial::polynomial const* p, rational& bound, const u_map<lp::lpvar>& nl2lp, lp::lar_term& t) {
polynomial::manager& pm = m_nlsat->pm();
for (unsigned i = 0; i < pm.size(p); ++i) {
polynomial::monomial* m = pm.get_monomial(p, i);
auto& coeff = pm.coeff(p, i);
unsigned num_vars = pm.size(m);
// add mon * coeff to t;
switch (num_vars) {
case 0:
bound -= coeff;
break;
case 1: {
auto v = nl2lp[pm.get_var(m, 0)];
t.add_monomial(coeff, v);
break;
}
default: {
svector<lp::lpvar> vars;
for (unsigned j = 0; j < num_vars; ++j)
vars.push_back(nl2lp[pm.get_var(m, j)]);
std::sort(vars.begin(), vars.end());
lp::lpvar v;
if (m_vars2mon.contains(vars))
v = m_vars2mon[vars];
else
v = m_nla_core.add_mul_def(vars.size(), vars.data());
t.add_monomial(coeff, v);
break;
}
}
}
}
u_map<lp::lpvar> reverse_lp2nl() {
u_map<lp::lpvar> nl2lp;
for (auto [j, x] : m_lp2nl)
nl2lp.insert(x, j);
return nl2lp;
}
lbool check_assignment() {
setup_assignment_solver();
lbool r = l_undef;
statistics &st = m_nla_core.lp_settings().stats().m_st;
nlsat::literal_vector clause;
try {
nlsat::assignment rvalues(m_nlsat->am());
for (auto [j, x] : m_lp2nl) {
scoped_anum a(am());
am().set(a, m_nla_core.val(j).to_mpq());
rvalues.set(x, a);
}
r = m_nlsat->check(rvalues, clause);
}
catch (z3_exception &) {
if (m_limit.is_canceled()) {
r = l_undef;
}
else {
m_nlsat->collect_statistics(st);
throw;
}
}
m_nlsat->collect_statistics(st);
switch (r) {
case l_true:
m_nla_core.set_use_nra_model(true);
lra.init_model();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci))
return l_undef;
for (auto const& m : m_nla_core.emons())
if (!check_monic(m))
return l_undef;
m_nla_core.set_use_nra_model(true);
break;
case l_false:
r = add_lemma(clause);
break;
default:
break;
}
return r;
}
lbool add_lemma(nlsat::literal_vector const &clause) {
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
polynomial::manager &pm = m_nlsat->pm();
lbool result = l_false;
{
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
for (nlsat::literal l : clause) {
if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) {
auto ci = m_literal2constraint[(~l).index()];
lp::explanation ex;
ex.push_back(ci);
lemma &= ex;
continue;
}
nlsat::atom *a = m_nlsat->bool_var2atom(l.var());
if (a->is_root_atom()) {
result = l_undef;
break;
}
SASSERT(a->is_ineq_atom());
auto &ia = *to_ineq_atom(a);
if (ia.size() != 1) {
result = l_undef; // factored polynomials not handled here
break;
}
polynomial::polynomial const *p = ia.p(0);
rational bound(0);
lp::lar_term t;
process_polynomial_check_assignment(p, bound, nl2lp, t);
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
switch (a->get_kind()) {
case nlsat::atom::EQ:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
break;
case nlsat::atom::LT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
break;
case nlsat::atom::GT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
break;
default:
UNREACHABLE();
result = l_undef;
break;
}
if (result == l_undef)
break;
if (m_nla_core.ineq_holds(inq)) {
result = l_undef;
break;
}
lemma |= inq;
}
if (result == l_false)
this->m_nla_core.m_check_feasible = true;
} // lemma_builder destructor runs here
if (result == l_undef)
m_nla_core.m_lemmas.pop_back(); // discard incomplete lemma
return result;
}
void add_monic_eq_bound(mon_eq const& m) {
@ -643,10 +877,9 @@ struct solver::imp {
unsigned w;
scoped_anum a(am());
for (unsigned v = m_values->size(); v < sz; ++v) {
if (m_nla_core.emons().is_monic_var(v)) {
if (m_nla_core.emons().is_monic_var(v)) {
am().set(a, 1);
auto &m = m_nla_core.emon(v);
for (auto x : m.vars())
am().mul(a, (*m_values)[x], a);
m_values->push_back(a);
@ -654,7 +887,7 @@ struct solver::imp {
else if (lra.column_has_term(v)) {
scoped_anum b(am());
am().set(a, 0);
for (auto const &[w, coeff] : lra.get_term(v)) {
for (auto const &[w, coeff] : lra.get_term(v)) {
am().set(b, coeff.to_mpq());
am().mul(b, (*m_values)[w], b);
am().add(a, b, a);
@ -737,6 +970,10 @@ lbool solver::check(dd::solver::equation_vector const& eqs) {
return m_imp->check(eqs);
}
lbool solver::check_assignment() {
return m_imp->check_assignment();
}
bool solver::need_check() {
return m_imp->need_check();
}

View file

@ -47,6 +47,11 @@ namespace nra {
*/
lbool check(dd::solver::equation_vector const& eqs);
/**
\brief Check feasibility modulo current value assignment.
*/
lbool check_assignment();
/*
\brief determine whether nra check is needed.
*/

View file

@ -1,3 +1,5 @@
Polynomial manipulation package.
It contains support for univariate (upolynomial.*) and multivariate polynomials (polynomial.*).
Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled.
Multivariate polynomial factorization uses evaluation and bivariate Hensel lifting: evaluate away
extra variables, factor the univariate specialization, then lift to bivariate factors in Zp[x]
and verify over Z. For >2 variables, trial division checks if bivariate factors divide the original.

View file

@ -2620,7 +2620,8 @@ namespace algebraic_numbers {
TRACE(isolate_roots, tout << "resultant loop i: " << i << ", y: x" << y << "\np_y: " << p_y << "\n";
tout << "q: " << q << "\n";);
if (ext_pm.is_zero(q)) {
SASSERT(!nested_call);
if (nested_call)
throw algebraic_exception("resultant vanished during nested isolate_roots call");
break;
}
}
@ -2632,7 +2633,8 @@ namespace algebraic_numbers {
// until we find one that is not zero at x2v.
// In the process we will copy p_prime to the local polynomial manager, since we will need to create
// an auxiliary variable.
SASSERT(!nested_call);
if (nested_call)
throw algebraic_exception("resultant vanished during nested isolate_roots call");
unsigned n = ext_pm.degree(p_prime, x);
SASSERT(n > 0);
if (n == 1) {

View file

@ -470,8 +470,8 @@ namespace polynomial {
void reset(monomial const * m) {
unsigned id = m->id();
SASSERT(id < m_m2pos.size());
m_m2pos[id] = UINT_MAX;
if (id < m_m2pos.size())
m_m2pos[id] = UINT_MAX;
}
void set(monomial const * m, unsigned pos) {
@ -6964,16 +6964,572 @@ namespace polynomial {
}
}
// Convert Zp-lifted coefficient arrays to centered Z representatives,
// build multivariate polynomials F1(x,y) and F2(x,y), and verify q == F1*F2.
// Returns true on success. Does NOT deallocate the coefficient vectors.
bool reconstruct_lifted_factors(
polynomial const * q,
var x, var y,
unsigned deg_y,
uint64_t prime,
vector<upolynomial::scoped_numeral_vector*> const & q_coeffs,
vector<upolynomial::scoped_numeral_vector*> const & F1_coeffs,
vector<upolynomial::scoped_numeral_vector*> const & F2_coeffs,
polynomial_ref & F1_out,
polynomial_ref & F2_out) {
scoped_numeral p_num(m_manager);
m_manager.set(p_num, static_cast<int>(prime));
scoped_numeral half_p(m_manager);
m_manager.set(half_p, static_cast<int>(prime));
m_manager.div(half_p, mpz(2), half_p);
polynomial_ref F1_poly(pm()), F2_poly(pm());
F1_poly = mk_zero();
F2_poly = mk_zero();
for (unsigned j = 0; j <= deg_y; j++) {
// Center the coefficients: if coeff > p/2, subtract p
for (unsigned i = 0; i < F1_coeffs[j]->size(); i++)
if (m_manager.gt((*F1_coeffs[j])[i], half_p))
m_manager.sub((*F1_coeffs[j])[i], p_num, (*F1_coeffs[j])[i]);
for (unsigned i = 0; i < F2_coeffs[j]->size(); i++)
if (m_manager.gt((*F2_coeffs[j])[i], half_p))
m_manager.sub((*F2_coeffs[j])[i], p_num, (*F2_coeffs[j])[i]);
// Build y^j * F_coeffs[j](x)
if (!F1_coeffs[j]->empty()) {
polynomial_ref univ(pm());
univ = to_polynomial(F1_coeffs[j]->size(), F1_coeffs[j]->data(), x);
if (!is_zero(univ)) {
monomial_ref yj(pm());
yj = mk_monomial(y, j);
polynomial_ref term(pm());
term = mul(yj, univ);
F1_poly = add(F1_poly, term);
}
}
if (!F2_coeffs[j]->empty()) {
polynomial_ref univ(pm());
univ = to_polynomial(F2_coeffs[j]->size(), F2_coeffs[j]->data(), x);
if (!is_zero(univ)) {
monomial_ref yj(pm());
yj = mk_monomial(y, j);
polynomial_ref term(pm());
term = mul(yj, univ);
F2_poly = add(F2_poly, term);
}
}
}
// Verify: q == F1 * F2 over Z[x, y]
polynomial_ref product(pm());
product = mul(F1_poly, F2_poly);
if (!eq(product, q))
return false;
F1_out = F1_poly;
F2_out = F2_poly;
return true;
}
// Hensel lifting loop: for j = 1..deg_y, compute F1_coeffs[j] and F2_coeffs[j]
// using Bezout coefficients s, t such that s*f1 + t*f2 = 1 in Zp[x].
// F1_coeffs[0] and F2_coeffs[0] must already be initialized.
void hensel_lift_coefficients(
upolynomial::zp_manager & zp_upm,
unsigned deg_y,
upolynomial::scoped_numeral_vector const & f1_p,
upolynomial::scoped_numeral_vector const & f2_p,
upolynomial::scoped_numeral_vector const & s_vec,
upolynomial::scoped_numeral_vector const & t_vec,
numeral const & lc_val,
vector<upolynomial::scoped_numeral_vector*> const & q_coeffs,
vector<upolynomial::scoped_numeral_vector*> & F1_coeffs,
vector<upolynomial::scoped_numeral_vector*> & F2_coeffs) {
auto & nm = upm().m();
auto & znm = zp_upm.m();
scoped_numeral lc_inv(m_manager);
znm.set(lc_inv, lc_val);
znm.inv(lc_inv);
for (unsigned j = 1; j <= deg_y; j++) {
checkpoint();
// Compute e_j = q_coeffs[j] - sum_{a+b=j, a>0, b>0} F1_coeffs[a] * F2_coeffs[b]
upolynomial::scoped_numeral_vector e_j(nm);
if (j < q_coeffs.size() && !q_coeffs[j]->empty())
zp_upm.set(q_coeffs[j]->size(), q_coeffs[j]->data(), e_j);
for (unsigned a = 0; a <= j; a++) {
unsigned b = j - a;
if (b > deg_y) continue;
if (a == j && b == 0) continue;
if (a == 0 && b == j) continue;
if (F1_coeffs[a]->empty() || F2_coeffs[b]->empty()) continue;
upolynomial::scoped_numeral_vector prod(nm);
zp_upm.mul(F1_coeffs[a]->size(), F1_coeffs[a]->data(),
F2_coeffs[b]->size(), F2_coeffs[b]->data(), prod);
upolynomial::scoped_numeral_vector new_e(nm);
zp_upm.sub(e_j.size(), e_j.data(), prod.size(), prod.data(), new_e);
e_j.swap(new_e);
}
if (e_j.empty()) continue;
// Solve using Bezout coefficients: A = (e_j * t) mod f1
upolynomial::scoped_numeral_vector e_t(nm), A_val(nm), Q_tmp(nm);
zp_upm.mul(e_j.size(), e_j.data(), t_vec.size(), t_vec.data(), e_t);
zp_upm.div_rem(e_t.size(), e_t.data(), f1_p.size(), f1_p.data(), Q_tmp, A_val);
// B = (e_j * s) mod f2
upolynomial::scoped_numeral_vector e_s(nm), B_val(nm);
zp_upm.mul(e_j.size(), e_j.data(), s_vec.size(), s_vec.data(), e_s);
zp_upm.div_rem(e_s.size(), e_s.data(), f2_p.size(), f2_p.data(), Q_tmp, B_val);
// F1[j] = A * lc_inv, F2[j] = B
zp_upm.mul(A_val, lc_inv);
zp_upm.set(A_val.size(), A_val.data(), *F1_coeffs[j]);
zp_upm.set(B_val.size(), B_val.data(), *F2_coeffs[j]);
}
}
// Extract coefficients of q w.r.t. y as upolynomials in Zp[x], and initialize
// the lifted factor coefficient arrays with F1[0] = f1, F2[0] = lc_val * f2.
// Returns false if q is not truly bivariate in x and y.
bool extract_and_init_lift_coefficients(
upolynomial::zp_manager & zp_upm,
polynomial const * q,
var y,
unsigned deg_y,
upolynomial::scoped_numeral_vector const & f1_p,
upolynomial::scoped_numeral_vector const & f2_p,
numeral const & lc_val,
vector<upolynomial::scoped_numeral_vector*> & q_coeffs,
vector<upolynomial::scoped_numeral_vector*> & F1_coeffs,
vector<upolynomial::scoped_numeral_vector*> & F2_coeffs) {
auto & nm = upm().m();
auto & znm = zp_upm.m();
for (unsigned j = 0; j <= deg_y; j++) {
polynomial_ref cj(pm());
cj = coeff(q, y, j);
auto * vec = alloc(upolynomial::scoped_numeral_vector, nm);
if (!is_zero(cj) && is_univariate(cj))
upm().to_numeral_vector(cj, *vec);
else if (!is_zero(cj) && is_const(cj)) {
vec->push_back(numeral());
nm.set(vec->back(), cj->a(0));
}
else if (!is_zero(cj)) {
dealloc(vec);
return false;
}
for (unsigned i = 0; i < vec->size(); i++)
znm.p_normalize((*vec)[i]);
zp_upm.trim(*vec);
q_coeffs.push_back(vec);
}
// Initialize lifted factor coefficient arrays
for (unsigned j = 0; j <= deg_y; j++) {
F1_coeffs.push_back(alloc(upolynomial::scoped_numeral_vector, nm));
F2_coeffs.push_back(alloc(upolynomial::scoped_numeral_vector, nm));
}
// F1[0] = f1, F2[0] = lc_val * f2
zp_upm.set(f1_p.size(), f1_p.data(), *F1_coeffs[0]);
scoped_numeral lc_p(m_manager);
znm.set(lc_p, lc_val);
upolynomial::scoped_numeral_vector lc_f2(nm);
zp_upm.set(f2_p.size(), f2_p.data(), lc_f2);
zp_upm.mul(lc_f2, lc_p);
zp_upm.set(lc_f2.size(), lc_f2.data(), *F2_coeffs[0]);
return true;
}
// Bivariate Hensel lifting for multivariate factorization.
//
// Mathematical setup:
// We have q(x, y) in Z[x, y] with degree deg_y in y.
// Evaluating at y = 0 gives a univariate factorization
// q(x, 0) = lc_val * uf1_monic(x) * uf2_monic(x)
// where uf1_monic and uf2_monic are monic, coprime polynomials in Z[x],
// and lc_val = lc(q, x)(y=0) is an integer.
//
// Goal: lift to q(x, y) = F1(x, y) * F2(x, y) over Z[x, y].
//
// Method (linear Hensel lifting in Zp[x]):
// 1. Reduce uf1_monic, uf2_monic to f1, f2 in Zp[x] and compute
// Bezout coefficients s, t with s*f1 + t*f2 = 1 in Zp[x].
// This requires gcd(f1, f2) = 1 in Zp[x], i.e. the prime p
// must not divide the resultant of f1, f2.
// 2. Expand q, F1, F2 as polynomials in y with coefficients in Zp[x]:
// q = q_0(x) + q_1(x)*y + ... + q_{deg_y}(x)*y^{deg_y}
// F1 = F1_0(x) + F1_1(x)*y + ...
// F2 = F2_0(x) + F2_1(x)*y + ...
// The y^0 coefficients are known: F1_0 = f1, F2_0 = lc_val * f2.
// 3. For j = 1, ..., deg_y, matching the y^j coefficient of q = F1 * F2:
// q_j = sum_{a+b=j} F1_a * F2_b
// The unknowns are F1_j and F2_j. Set
// e_j = q_j - sum_{a+b=j, 0<a, 0<b} F1_a * F2_b
// so that F1_j * F2_0 + F2_j * F1_0 = e_j,
// i.e. F1_j * (lc_val * f2) + F2_j * f1 = e_j.
// From step 1 we have the Bezout identity s*f1 + t*f2 = 1 in Zp[x].
// Multiplying by e_j: (e_j*s)*f1 + (e_j*t)*f2 = e_j.
// Reducing to match degree constraints gives:
// F2_j = (e_j * s) mod f2
// F1_j = ((e_j * t) mod f1) / lc_val
// all in Zp[x].
// 4. Map Zp coefficients to centered representatives in (-p/2, p/2]
// and verify q = F1 * F2 over Z[x, y].
//
// Preconditions:
// - q is a bivariate polynomial in x and y, i.e. every coeff(q, y, j)
// is either zero, a constant, or univariate in x.
// - uf1_monic, uf2_monic are monic univariate polynomials in Z[x],
// stored as coefficient vectors, such that
// q(x, 0) = lc_val * uf1_monic(x) * uf2_monic(x).
// - gcd(uf1_monic, uf2_monic) = 1 over Q[x].
// - prime does not divide lc_val.
//
// Returns true if the lift succeeds, i.e. q = F1 * F2 holds over Z.
// Returns false if coprimality fails in Zp, if q is not bivariate,
// or if p is too small for the centered representative trick to work.
bool try_bivar_hensel_lift(
polynomial const * q,
var x, var y,
unsigned deg_y,
upolynomial::numeral_vector const & uf1_monic, // monic factor of q(x,0)/lc_val in Z[x], as coefficient vector
upolynomial::numeral_vector const & uf2_monic, // monic factor of q(x,0)/lc_val in Z[x], coprime to uf1_monic
numeral const & lc_val, // lc(q, x) evaluated at y=0, so q(x,0) = lc_val * uf1_monic * uf2_monic
uint64_t prime,
polynomial_ref & F1_out,
polynomial_ref & F2_out) {
typedef upolynomial::zp_manager zp_mgr;
typedef upolynomial::zp_numeral_manager zp_nm;
auto & nm = upm().m();
zp_mgr zp_upm(m_limit, nm.m());
scoped_numeral p_num(m_manager);
m_manager.set(p_num, static_cast<int>(prime));
zp_upm.set_zp(p_num);
zp_nm & znm = zp_upm.m();
// Convert h1, h2 to Zp
upolynomial::scoped_numeral_vector f1_p(nm), f2_p(nm);
for (unsigned i = 0; i < uf1_monic.size(); i++) {
f1_p.push_back(numeral());
znm.set(f1_p.back(), uf1_monic[i]);
}
zp_upm.trim(f1_p);
for (unsigned i = 0; i < uf2_monic.size(); i++) {
f2_p.push_back(numeral());
znm.set(f2_p.back(), uf2_monic[i]);
}
zp_upm.trim(f2_p);
// Make monic in Zp
zp_upm.mk_monic(f1_p.size(), f1_p.data());
zp_upm.mk_monic(f2_p.size(), f2_p.data());
// Extended GCD in Zp[x]: s*f1 + t*f2 = 1
upolynomial::scoped_numeral_vector s_vec(nm), t_vec(nm), d_vec(nm);
zp_upm.ext_gcd(f1_p, f2_p, s_vec, t_vec, d_vec);
// Check gcd = 1
if (d_vec.size() != 1 || !znm.is_one(d_vec[0]))
return false;
vector<upolynomial::scoped_numeral_vector*> q_coeffs, F1_coeffs, F2_coeffs;
if (!extract_and_init_lift_coefficients(zp_upm, q, y, deg_y,
f1_p, f2_p, lc_val,
q_coeffs, F1_coeffs, F2_coeffs)) {
for (auto * v : q_coeffs) dealloc(v);
return false;
}
hensel_lift_coefficients(zp_upm, deg_y, f1_p, f2_p,
s_vec, t_vec, lc_val,
q_coeffs, F1_coeffs, F2_coeffs);
bool ok = reconstruct_lifted_factors(q, x, y, deg_y, prime,
q_coeffs, F1_coeffs, F2_coeffs,
F1_out, F2_out);
for (auto * v : q_coeffs) dealloc(v);
for (auto * v : F1_coeffs) dealloc(v);
for (auto * v : F2_coeffs) dealloc(v);
return ok;
}
// Evaluation points used for multivariate factorization
static constexpr int s_factor_eval_values[] = { 0, 1, -1, 2, -2, 3, -3 };
static constexpr unsigned s_n_factor_eval_values = sizeof(s_factor_eval_values) / sizeof(s_factor_eval_values[0]);
// Primes for Hensel lifting, tried in increasing order.
// Lifting succeeds when the prime exceeds twice the largest coefficient in any factor.
// A Mignotte-style bound could automate this, but for now we try a fixed list.
static constexpr uint64_t s_factor_primes[] = { 39103, 104729, 1000003, 100000007 };
void factor_n_sqf_pp(polynomial const * p, factors & r, var x, unsigned k) {
SASSERT(degree(p, x) > 2);
SASSERT(is_primitive(p, x));
SASSERT(is_square_free(p, x));
TRACE(factor, tout << "factor square free (degree > 2):\n"; p->display(tout, m_manager); tout << "\n";);
// TODO: invoke Dejan's procedure
if (is_univariate(p)) {
factor_sqf_pp_univ(p, r, k, factor_params());
return;
}
// Try multivariate factorization. If checkpoint() throws during the
// attempt, the shared som_buffer/m_m2pos may be left dirty. Catch the
// exception, reset the buffers, return unfactored, then rethrow so
// cancellation propagates normally.
try {
if (try_multivar_factor(p, r, x, k))
return;
}
catch (...) {
m_som_buffer.reset();
m_som_buffer2.reset();
m_cheap_som_buffer.reset();
m_cheap_som_buffer2.reset();
throw;
}
// Could not factor, return p as-is
r.push_back(const_cast<polynomial*>(p), k);
}
// Returns true if factorization succeeded and factors were added to r.
bool try_multivar_factor(polynomial const * p, factors & r, var x, unsigned k) {
var_vector all_vars;
m_wrapper.vars(p, all_vars);
// Try the main variable x first (caller chose it), then others by degree
svector<var> main_vars;
main_vars.push_back(x);
svector<std::pair<unsigned, var>> var_by_deg;
for (var v : all_vars)
if (v != x)
var_by_deg.push_back(std::make_pair(degree(p, v), v));
std::sort(var_by_deg.begin(), var_by_deg.end(),
[](auto const& a, auto const& b) { return a.first > b.first; });
for (auto const& [d, v] : var_by_deg)
if (d > 1) main_vars.push_back(v);
for (var main_var : main_vars) {
unsigned deg_main = degree(p, main_var);
if (deg_main <= 1) continue;
for (var lift_var : all_vars) {
if (lift_var == main_var) continue;
checkpoint();
// Variables to evaluate away
var_vector eval_vars;
for (var v : all_vars)
if (v != main_var && v != lift_var)
eval_vars.push_back(v);
unsigned n_eval = eval_vars.size();
// Try a small number of evaluation point combos for extra variables
unsigned max_combos = (n_eval == 0) ? 1 : std::min(s_n_factor_eval_values, 5u);
for (unsigned combo = 0; combo < max_combos; combo++) {
checkpoint();
// Reduce to bivariate
polynomial_ref p_bivar(pm());
if (n_eval > 0) {
scoped_numeral_vector eval_vals(m_manager);
for (unsigned i = 0; i < n_eval; i++) {
eval_vals.push_back(numeral());
unsigned c = combo;
for (unsigned skip = 0; skip < i; skip++)
c /= s_n_factor_eval_values;
m_manager.set(eval_vals.back(), s_factor_eval_values[c % s_n_factor_eval_values]);
}
p_bivar = substitute(p, n_eval, eval_vars.data(), eval_vals.data());
}
else
p_bivar = const_cast<polynomial*>(p);
if (degree(p_bivar, main_var) != deg_main) continue;
unsigned deg_lift = degree(p_bivar, lift_var);
if (deg_lift == 0) continue;
// Find a good evaluation point a for the lift variable
for (int a : s_factor_eval_values) {
scoped_numeral val_scoped(m_manager);
m_manager.set(val_scoped, a);
numeral const & val_ref = val_scoped;
polynomial_ref p_univ(pm());
p_univ = substitute(p_bivar, 1, &lift_var, &val_ref);
if (!is_univariate(p_univ)) continue;
if (degree(p_univ, main_var) != deg_main) continue;
if (!is_square_free(p_univ, main_var)) continue;
// Factor the univariate polynomial
up_manager::scoped_numeral_vector p_univ_vec(upm().m());
polynomial_ref p_univ_ref(pm());
p_univ_ref = p_univ;
upm().to_numeral_vector(p_univ_ref, p_univ_vec);
// Make primitive before factoring
upm().get_primitive(p_univ_vec, p_univ_vec);
up_manager::factors univ_fs(upm());
upolynomial::factor_square_free(upm(), p_univ_vec, univ_fs);
unsigned nf = univ_fs.distinct_factors();
if (nf <= 1) continue;
// Translate so evaluation is at lift_var = 0
polynomial_ref q(pm());
scoped_numeral a_val(m_manager);
m_manager.set(a_val, a);
q = translate(p_bivar, lift_var, a_val);
// Get leading coefficient at evaluation point
polynomial_ref lc_poly(pm());
lc_poly = coeff(q, main_var, deg_main);
scoped_numeral lc_at_0(m_manager);
if (is_const(lc_poly))
m_manager.set(lc_at_0, lc_poly->a(0));
else {
scoped_numeral zero_val(m_manager);
m_manager.set(zero_val, 0);
numeral const & zero_ref = zero_val;
polynomial_ref lc_eval(pm());
lc_eval = substitute(lc_poly, 1, &lift_var, &zero_ref);
if (is_const(lc_eval))
m_manager.set(lc_at_0, lc_eval->a(0));
else
continue;
}
// Try splits with increasing primes.
// Only contiguous splits {0..split-1} vs {split..nf-1} are tried,
// not all subset partitions. This avoids exponential search but may
// miss some factorizations. Recursive calls on the lifted factors
// partially compensate by further splitting successful lifts.
for (uint64_t prime : s_factor_primes) {
scoped_numeral prime_num(m_manager);
m_manager.set(prime_num, static_cast<int64_t>(prime));
scoped_numeral gcd_val(m_manager);
m_manager.gcd(prime_num, lc_at_0, gcd_val);
if (!m_manager.is_one(gcd_val)) continue;
for (unsigned split = 1; split <= nf / 2; split++) {
checkpoint();
upolynomial::scoped_numeral_vector h1(upm().m()), h2(upm().m());
upm().set(univ_fs[0].size(), univ_fs[0].data(), h1);
for (unsigned i = 1; i < split; i++) {
upolynomial::scoped_numeral_vector temp(upm().m());
upm().mul(h1.size(), h1.data(), univ_fs[i].size(), univ_fs[i].data(), temp);
h1.swap(temp);
}
upm().set(univ_fs[split].size(), univ_fs[split].data(), h2);
for (unsigned i = split + 1; i < nf; i++) {
upolynomial::scoped_numeral_vector temp(upm().m());
upm().mul(h2.size(), h2.data(), univ_fs[i].size(), univ_fs[i].data(), temp);
h2.swap(temp);
}
auto & nm_ref = upm().m();
if (!h1.empty() && nm_ref.is_neg(h1.back())) {
for (unsigned i = 0; i < h1.size(); i++)
nm_ref.neg(h1[i]);
}
if (!h2.empty() && nm_ref.is_neg(h2.back())) {
for (unsigned i = 0; i < h2.size(); i++)
nm_ref.neg(h2[i]);
}
polynomial_ref F1(pm()), F2(pm());
if (!try_bivar_hensel_lift(q, main_var, lift_var, deg_lift, h1, h2, lc_at_0, prime, F1, F2))
continue;
// Translate back
scoped_numeral neg_a(m_manager);
m_manager.set(neg_a, -a);
F1 = translate(F1, lift_var, neg_a);
F2 = translate(F2, lift_var, neg_a);
if (n_eval == 0) {
// p is bivariate, factors verified by try_bivar_hensel_lift.
// Use specialized handlers for small degrees to avoid
// re-entering factor_sqf_pp which corrupts shared buffers.
polynomial_ref bivar_fs[] = { F1, F2 };
for (polynomial_ref & bf : bivar_fs) {
if (is_const(bf) || degree(bf, x) == 0) continue;
unsigned d = degree(bf, x);
if (d == 1)
factor_1_sqf_pp(bf, r, x, k);
else if (d == 2 && is_primitive(bf, x) && is_square_free(bf, x))
factor_2_sqf_pp(bf, r, x, k);
else
r.push_back(bf, k);
}
return true;
}
// Multivariate: check if bivariate factors divide original p.
// We use exact_pseudo_division, which computes Q, R with
// lc(cand)^d * p = Q * cand + R. If R=0 and cand*Q == p
// then cand is a true factor. The eq() check is needed
// because pseudo-division may introduce an lc power that
// prevents Q from being the exact quotient.
polynomial_ref cands[] = { F1, F2 };
for (polynomial_ref & cand : cands) {
if (is_const(cand)) continue;
polynomial_ref Q_div(pm()), R_div(pm());
var div_var = max_var(cand);
exact_pseudo_division(const_cast<polynomial*>(p), cand, div_var, Q_div, R_div);
if (!is_zero(R_div)) continue;
polynomial_ref check(pm());
check = mul(cand, Q_div);
if (eq(check, p)) {
// Push factors directly, using specialized handlers
// for small degrees only.
polynomial_ref parts[] = { cand, Q_div };
for (polynomial_ref & part : parts) {
if (is_const(part)) {
acc_constant(r, part->a(0));
continue;
}
if (degree(part, x) == 0) continue;
unsigned d = degree(part, x);
if (d == 1)
factor_1_sqf_pp(part, r, x, k);
else if (d == 2 && is_primitive(part, x) && is_square_free(part, x))
factor_2_sqf_pp(part, r, x, k);
else
r.push_back(part, k);
}
return true;
}
}
}
}
}
}
}
}
return false;
}
void factor_sqf_pp(polynomial const * p, factors & r, var x, unsigned k, factor_params const & params) {
SASSERT(degree(p, x) > 0);
SASSERT(is_primitive(p, x));

View file

@ -2616,6 +2616,7 @@ namespace upolynomial {
\warning This method may loop if p is not square free or if (a,b) is not an isolating interval.
*/
bool manager::isolating2refinable(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b) {
checkpoint();
int sign_a = eval_sign_at(sz, p, a);
int sign_b = eval_sign_at(sz, p, b);
TRACE(upolynomial, tout << "sign_a: " << sign_a << ", sign_b: " << sign_b << "\n";);
@ -2631,6 +2632,7 @@ namespace upolynomial {
bqm.add(a, b, new_a);
bqm.div2(new_a);
while (true) {
checkpoint();
TRACE(upolynomial, tout << "CASE 2, a: " << bqm.to_string(a) << ", b: " << bqm.to_string(b) << ", new_a: " << bqm.to_string(new_a) << "\n";);
int sign_new_a = eval_sign_at(sz, p, new_a);
if (sign_new_a != sign_b) {
@ -2656,6 +2658,7 @@ namespace upolynomial {
bqm.add(a, b, new_b);
bqm.div2(new_b);
while (true) {
checkpoint();
TRACE(upolynomial, tout << "CASE 3, a: " << bqm.to_string(a) << ", b: " << bqm.to_string(b) << ", new_b: " << bqm.to_string(new_b) << "\n";);
int sign_new_b = eval_sign_at(sz, p, new_b);
if (sign_new_b != sign_a) {
@ -2709,6 +2712,7 @@ namespace upolynomial {
bqm.div2(new_b2);
while (true) {
checkpoint();
TRACE(upolynomial,
tout << "CASE 4\na1: " << bqm.to_string(a1) << ", b1: " << bqm.to_string(b1) << ", new_a1: " << bqm.to_string(new_a1) << "\n";
tout << "a2: " << bqm.to_string(a2) << ", b2: " << bqm.to_string(b2) << ", new_b2: " << bqm.to_string(new_b2) << "\n";);

View file

@ -3448,16 +3448,23 @@ namespace realclosure {
return true;
}
unsigned get_sign_condition_size(numeral const &a, unsigned i) {
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
sign_condition* get_ith_sign_condition(algebraic* ext, unsigned i) {
const sign_det * sdt = ext->sdt();
if (!sdt)
return 0;
return nullptr;
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
while (i && sc) {
sc = sc->prev();
i--;
}
return sc;
}
unsigned get_sign_condition_size(numeral const &a, unsigned i) {
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc)
return 0;
return ext->sdt()->qs()[sc->qidx()].size();
}
@ -3466,14 +3473,9 @@ namespace realclosure {
if (!is_algebraic(a))
return 0;
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt();
if (!sdt)
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc)
return 0;
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
return q.size();
}
@ -3483,14 +3485,9 @@ namespace realclosure {
if (!is_algebraic(a))
return numeral();
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt();
if (!sdt)
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc)
return numeral();
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
if (j >= q.size())
return numeral();

View file

@ -125,7 +125,7 @@ unsigned_vector bit_matrix::gray(unsigned n) {
auto v = gray(n-1);
auto w = v;
w.reverse();
for (auto & u : v) u |= (1 << (n-1));
for (auto & u : v) u |= (1u << (n-1));
v.append(w);
return v;
}

View file

@ -328,7 +328,7 @@ namespace datalog {
column_info(unsigned offset, unsigned length)
: m_big_offset(offset / 8),
m_small_offset(offset % 8),
m_mask( length == 64 ? ULLONG_MAX : (static_cast<uint64_t>(1)<<length)-1 ),
m_mask( length >= 64 ? ULLONG_MAX : (static_cast<uint64_t>(1)<<length)-1 ),
m_write_mask( ~(m_mask << m_small_offset) ),
m_offset(offset),
m_length(length) {

View file

@ -54,6 +54,7 @@ namespace datalog {
col = column_idx(orig[i]);
limit = col + column_num_bits(orig[i]);
} else {
SASSERT(other);
unsigned idx = orig[i] - get_num_cols();
col = get_num_bits() + other->column_idx(idx);
limit = col + other->column_num_bits(idx);

View file

@ -3330,7 +3330,7 @@ bool context::is_reachable(pob &n)
model_ref mdl;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;
@ -3521,7 +3521,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
model_ref model;
// used in case n is reachable
bool is_concrete;
bool is_concrete = false;
const datalog::rule * r = nullptr;
// denotes which predecessor's (along r) reach facts are used
bool_vector reach_pred_used;

View file

@ -75,6 +75,8 @@ namespace nlsat {
mutable std_vector<unsigned> m_deg_in_order_graph; // degree of polynomial in resultant graph
mutable std_vector<unsigned> m_unique_neighbor; // UINT_MAX = not set, UINT_MAX-1 = multiple
bool m_linear_cell = false; // indicates whether cell bounds are forced to be linear
assignment const& sample() const { return m_solver.sample(); }
struct root_function {
@ -231,7 +233,8 @@ namespace nlsat {
assignment const&,
pmanager& pm,
anum_manager& am,
polynomial::cache& cache)
polynomial::cache& cache,
bool linear)
: m_solver(solver),
m_P(ps),
m_n(max_x),
@ -240,7 +243,8 @@ namespace nlsat {
m_cache(cache),
m_todo(m_cache, true),
m_level_ps(m_pm),
m_psc_tmp(m_pm) {
m_psc_tmp(m_pm),
m_linear_cell(linear) {
m_I.reserve(m_n);
for (unsigned i = 0; i < m_n; ++i)
m_I.emplace_back(m_pm);
@ -1007,6 +1011,66 @@ namespace nlsat {
}
}
void add_linear_poly_from_root(anum const& a, bool lower, polynomial_ref& p) {
rational r;
m_am.to_rational(a, r);
p = m_pm.mk_polynomial(m_level);
p = denominator(r)*p - numerator(r);
if (lower) {
m_I[m_level].l = p;
m_I[m_level].l_index = 1;
} else {
m_I[m_level].u = p;
m_I[m_level].u_index = 1;
}
m_level_ps.push_back(p);
m_poly_has_roots.push_back(true);
polynomial_ref w = choose_nonzero_coeff(p, m_level);
m_witnesses.push_back(w);
}
// Ensure that the interval bounds will be described by linear polynomials.
// If this is not already the case, the working set of polynomials is extended by
// new linear polynomials whose roots under-approximate the cell boundary.
// Based on: Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner
// "More is Less: Adding Polynomials for Faster Explanations in NLSAT" (CADE30, 2025)
void add_linear_approximations(anum const& v) {
polynomial_ref p_lower(m_pm), p_upper(m_pm);
auto& r = m_rel.m_rfunc;
if (m_I[m_level].is_section()) {
if (!m_am.is_rational(v)) {
NOT_IMPLEMENTED_YET();
}
else if (m_pm.total_degree(m_I[m_level].l) > 1) {
add_linear_poly_from_root(v, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf), m_am, p_lower, 1, v, m_level_ps.size()-1);
}
return;
}
// sector: have to consider lower and upper bound
if (!m_I[m_level].l_inf() && m_pm.total_degree(m_I[m_level].l) > 1) {
scoped_anum between(m_am);
m_am.select(r[m_l_rf].val, v, between);
add_linear_poly_from_root(between, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf + 1), m_am, p_lower, 1, between, m_level_ps.size()-1);
++m_l_rf;
if (is_set(m_u_rf))
++m_u_rf;
}
if (!m_I[m_level].u_inf() && m_pm.total_degree(m_I[m_level].u) > 1) {
scoped_anum between(m_am);
m_am.select(v, r[m_u_rf].val, between);
// update root function ordering
add_linear_poly_from_root(between, false, p_upper);
r.emplace((r.begin() + m_u_rf), m_am, p_upper, 1, between, m_level_ps.size()-1);
}
}
// Build Θ (root functions) and pick I_level around sample(level).
// Sets m_l_rf/m_u_rf and m_I[level].
// Returns whether any roots were found (i.e., whether a relation can be built).
@ -1022,6 +1086,10 @@ namespace nlsat {
return false;
set_interval_from_root_partition(v, mid);
if (m_linear_cell)
add_linear_approximations(v);
compute_side_mask();
return true;
}
@ -1376,8 +1444,9 @@ namespace nlsat {
assignment const& s,
pmanager& pm,
anum_manager& am,
polynomial::cache& cache)
: m_impl(new impl(solver, ps, n, s, pm, am, cache)) {}
polynomial::cache& cache,
bool linear)
: m_impl(new impl(solver, ps, n, s, pm, am, cache, linear)) {}
levelwise::~levelwise() { delete m_impl; }

View file

@ -40,7 +40,7 @@ namespace nlsat {
impl* m_impl;
public:
// Construct with polynomials ps, maximal variable max_x, current sample s, polynomial manager pm, and algebraic-number manager am
levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache);
levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache, bool linear=false);
~levelwise();
levelwise(levelwise const&) = delete;

View file

@ -106,8 +106,6 @@ namespace nlsat {
/**
* Check whether all coefficients of the polynomial `s` (viewed as a polynomial
* in its main variable) evaluate to zero under the given assignment `x2v`.
* This is exactly the logic used in several places in the nlsat codebase
* (e.g. coeffs_are_zeroes_in_factor in nlsat_explain.cpp).
*/
inline bool coeffs_are_zeroes_on_sample(polynomial_ref const & s, pmanager & pm, assignment & x2v, anum_manager & am) {
polynomial_ref c(pm);

View file

@ -40,7 +40,6 @@ namespace nlsat {
polynomial::cache & m_cache;
pmanager & m_pm;
polynomial_ref_vector m_ps;
polynomial_ref_vector m_ps2;
polynomial_ref_vector m_psc_tmp;
polynomial_ref_vector m_factors, m_factors_save;
scoped_anum_vector m_roots_tmp;
@ -85,7 +84,6 @@ namespace nlsat {
m_cache(u),
m_pm(u.pm()),
m_ps(m_pm),
m_ps2(m_pm),
m_psc_tmp(m_pm),
m_factors(m_pm),
m_factors_save(m_pm),
@ -166,8 +164,6 @@ namespace nlsat {
/**
\brief Add literal p != 0 into m_result.
*/
ptr_vector<poly> m_zero_fs;
bool_vector m_is_even;
struct restore_factors {
polynomial_ref_vector& m_factors, &m_factors_save;
unsigned num_saved = 0;
@ -589,25 +585,6 @@ namespace nlsat {
return max;
}
/**
\brief Move the polynomials in q in ps that do not contain x to qs.
*/
void keep_p_x(polynomial_ref_vector & ps, var x, polynomial_ref_vector & qs) {
unsigned sz = ps.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; ++i) {
poly * q = ps.get(i);
if (max_var(q) != x) {
qs.push_back(q);
}
else {
ps.set(j, q);
j++;
}
}
ps.shrink(j);
}
/**
\brief Add factors of p to todo
*/
@ -680,48 +657,6 @@ namespace nlsat {
}
}
// this function also explains the value 0, if met
bool coeffs_are_zeroes(polynomial_ref &s) {
restore_factors _restore(m_factors, m_factors_save);
factor(s, m_cache, m_factors);
unsigned num_factors = m_factors.size();
m_zero_fs.reset();
m_is_even.reset();
polynomial_ref f(m_pm);
bool have_zero = false;
for (unsigned i = 0; i < num_factors; ++i) {
f = m_factors.get(i);
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
have_zero = true;
break;
}
}
if (!have_zero)
return false;
var x = max_var(f);
unsigned n = degree(f, x);
auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; ++j) {
c = m_pm.coeff(s, x, j);
SASSERT(sign(c) == 0);
ensure_sign(c);
}
return true;
}
bool coeffs_are_zeroes_in_factor(polynomial_ref & s) {
var x = max_var(s);
unsigned n = degree(s, x);
auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; ++j) {
c = m_pm.coeff(s, x, j);
if (nlsat::sign(c, sample(), m_am) != 0)
return false;
}
return true;
}
/**
\brief Add v-psc(p, q, x) into m_todo
*/
@ -987,40 +922,6 @@ namespace nlsat {
}
}
/**
Add one or two literals that specify in which cell of variable y the current interpretation is.
One literal is added for the cases:
- y in (-oo, min) where min is the minimal root of the polynomials p2 in ps
We add literal
! (y < root_1(p2))
- y in (max, oo) where max is the maximal root of the polynomials p1 in ps
We add literal
! (y > root_k(p1)) where k is the number of real roots of p
- y = r where r is the k-th root of a polynomial p in ps
We add literal
! (y = root_k(p))
Two literals are added when
- y in (l, u) where (l, u) does not contain any root of polynomials p in ps, and
l is the i-th root of a polynomial p1 in ps, and u is the j-th root of a polynomial p2 in ps.
We add literals
! (y > root_i(p1)) or !(y < root_j(p2))
*/
void add_cell_lits(polynomial_ref_vector & ps, var y) {
cell_root_info info(m_pm);
find_cell_roots(ps, y, info);
if (info.m_has_eq) {
add_root_literal(atom::ROOT_EQ, y, info.m_eq_idx, info.m_eq);
return;
}
if (info.m_has_lower) {
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, info.m_lower_idx, info.m_lower);
}
if (info.m_has_upper) {
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, info.m_upper_idx, info.m_upper);
}
}
/**
\brief Return true if all polynomials in ps are univariate in x.
*/
@ -1040,13 +941,13 @@ namespace nlsat {
\brief Apply model-based projection operation defined in our paper.
*/
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache, bool linear=false) {
// Store polynomials for debugging unsound lemmas
m_last_lws_input_polys.reset();
for (unsigned i = 0; i < ps.size(); i++)
m_last_lws_input_polys.push_back(ps.get(i));
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache, linear);
auto cell = lws.single_cell();
TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
@ -1139,9 +1040,10 @@ namespace nlsat {
x = extract_max_polys(ps);
cac_add_cell_lits(ps, x, samples);
}
}
bool check_already_added() const {
for (bool b : m_already_added_literal) {
(void)b;
@ -1698,6 +1600,38 @@ namespace nlsat {
}
void compute_linear_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
SASSERT(check_already_added());
SASSERT(num > 0);
SASSERT(max_var(num, ls) != 0 || m_solver.sample().is_assigned(0));
TRACE(nlsat_explain,
tout << "the infeasible clause:\n";
display(tout, m_solver, num, ls) << "\n";
m_solver.display_assignment(tout << "assignment:\n");
);
m_result = &result;
m_lower_stage_polys.reset();
collect_polys(num, ls, m_ps);
for (unsigned i = 0; i < m_lower_stage_polys.size(); i++) {
m_ps.push_back(m_lower_stage_polys.get(i));
}
if (m_ps.empty())
return;
// We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
var max_x = max_var(m_ps);
bool levelwise_ok = levelwise_single_cell(m_ps, max_x+1, m_cache, true); // max_x+1 because we have a full sample
SASSERT(levelwise_ok);
m_solver.record_levelwise_result(levelwise_ok);
reset_already_added();
m_result = nullptr;
TRACE(nlsat_explain, display(tout << "[explain] result\n", m_solver, result) << "\n";);
CASSERT("nlsat", check_already_added());
}
void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
unsigned base = result.size();
while (true) {
@ -1782,55 +1716,7 @@ namespace nlsat {
}
}
}
void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
TRACE(nlsat_explain, tout << "project pairs\n";);
polynomial_ref p(m_pm);
p = ps.get(idx);
for (unsigned i = 0; i < ps.size(); ++i) {
if (i != idx) {
project_pair(x, ps.get(i), p);
}
}
}
void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) {
m_ps2.reset();
m_ps2.push_back(p1);
m_ps2.push_back(p2);
project(m_ps2, x);
}
void project_single(var x, polynomial::polynomial* p) {
m_ps2.reset();
m_ps2.push_back(p);
project(m_ps2, x);
}
void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) {
svector<literal> lits;
polynomial_ref p(m_pm);
split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.data(), m_ps);
unbounded = true;
scoped_anum x_val(m_am);
x_val = sample().value(x);
for (unsigned i = 0; i < m_ps.size(); ++i) {
p = m_ps.get(i);
scoped_anum_vector & roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(sample(), x), roots);
for (unsigned j = 0; j < roots.size(); ++j) {
int s = m_am.compare(x_val, roots[j]);
if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) {
unbounded = false;
val = roots[j];
}
}
}
}
};
@ -1876,12 +1762,12 @@ namespace nlsat {
m_imp->compute_conflict_explanation(n, ls, result);
}
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result);
void explain::compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->compute_linear_explanation(n, ls, result);
}
void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) {
m_imp->maximize(x, n, ls, val, unbounded);
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result);
}
void explain::display_last_lws_input(std::ostream& out) {

View file

@ -66,6 +66,12 @@ namespace nlsat {
*/
void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief A variant of compute_conflict_explanation, but all resulting literals s_i are linear.
This is achieved by adding new polynomials during the projection, thereby under-approximating
the computed cell.
*/
void compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief projection for a given variable.
@ -91,18 +97,6 @@ namespace nlsat {
*/
void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result);
/**
Maximize the value of x (locally) under the current assignment to other variables and
while maintaining the assignment to the literals ls.
Set unbounded to 'true' if the value of x is unbounded.
Precondition: the set of literals are true in the current model.
By local optimization we understand that x is increased to the largest value within
the signs delineated by the roots of the polynomials in ls.
*/
void maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded);
/**
Print the polynomials that were passed to levelwise in the last call (for debugging).
*/

View file

@ -2156,6 +2156,62 @@ namespace nlsat {
m_assignment.reset();
}
lbool check(assignment const& rvalues, literal_vector& clause) {
// temporarily set m_assignment to the given one
assignment tmp = m_assignment;
m_assignment.reset();
m_assignment.copy(rvalues);
// check whether the asserted atoms are satisfied by rvalues
literal best_literal = null_literal;
lbool satisfied = l_true;
for (auto cp : m_clauses) {
auto& c = *cp;
bool is_false = all_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_false; });
bool is_true = any_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_true; });
if (is_true)
continue;
if (!is_false) {
satisfied = l_undef;
continue;
}
// take best literal from c
for (literal l : c) {
if (best_literal == null_literal) {
best_literal = l;
}
else {
bool_var b_best = best_literal.var();
bool_var b_l = l.var();
if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) {
best_literal = l;
}
// TODO: there might be better criteria than just the degree in the main variable.
}
}
}
if (best_literal == null_literal)
return satisfied;
// assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal);
clause.reset();
m_lazy_clause.reset();
m_explain.compute_linear_explanation(1, &best_literal, m_lazy_clause);
for (auto l : m_lazy_clause) {
clause.push_back(l);
}
clause.push_back(~best_literal);
m_assignment.reset();
m_assignment.copy(tmp);
return l_false;
}
lbool check(literal_vector& assumptions) {
literal_vector result;
unsigned sz = assumptions.size();
@ -4419,6 +4475,10 @@ namespace nlsat {
return m_imp->check(assumptions);
}
lbool solver::check(assignment const& rvalues, literal_vector& clause) {
return m_imp->check(rvalues, clause);
}
void solver::get_core(vector<assumption, false>& assumptions) {
return m_imp->get_core(assumptions);
}

View file

@ -219,6 +219,19 @@ namespace nlsat {
lbool check(literal_vector& assumptions);
//
// check satisfiability of asserted formulas relative to state of the nlsat solver.
// produce either,
// l_true - a model is available (rvalues can be ignored) or,
// l_false - a clause (not core v not cell) excluding a cell around rvalues if core (consisting of atoms
// passed to nlsat) is asserted.
// l_undef - if the search was interrupted by a resource limit.
// clause is a list of literals. Their disjunction is valid.
// Different implementations of check are possible. One where cell comprises of linear polynomials could
// produce lemmas that are friendly to linear arithmetic solvers.
//
lbool check(assignment const& rvalues, literal_vector& clause);
// -----------------------
//
// Model

View file

@ -948,8 +948,10 @@ namespace opt {
g->assert_expr(fml);
for (expr * a : asms)
g->assert_expr(a, a);
params_ref som_params(m_params);
som_params.set_bool("som", true);
tactic_ref tac0 =
and_then(mk_simplify_tactic(m, m_params),
and_then(mk_simplify_tactic(m, som_params),
mk_propagate_values_tactic(m),
m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
mk_simplify_tactic(m));

View file

@ -200,36 +200,76 @@ namespace opt {
}
bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) {
expr_ref blocker(m);
// Save the baseline model before any push/pop corrupts LP state.
// Push/pop isolates SMT assertions but does not restore LP column
// values, so maximize may return stale values for non-linear
// objectives like mod. The baseline model serves as a floor.
model_ref baseline_model;
m_context.get_model(baseline_model);
for (unsigned i = 0; i < m_objective_vars.size(); ++i) {
// Push context to isolate each objective's optimization.
// This prevents bounds created during one objective's optimization
// from affecting subsequent objectives (fixes issue #7677).
m_context.push();
if (!maximize_objective(i, blocker)) {
m_context.pop(1);
expr_ref blocker(m);
if (!maximize_objective_isolated(i, baseline_model, blocker))
return false;
}
// Save results before popping
inf_eps val = m_objective_values[i];
model_ref mdl;
if (m_models[i])
mdl = m_models[i];
m_context.pop(1);
// Restore the computed values after pop
m_objective_values[i] = val;
if (mdl)
m_models.set(i, mdl.get());
blockers.push_back(blocker);
}
return true;
}
// Maximize objective[i] inside a push/pop scope so that bounds from
// one objective do not leak into subsequent ones, fixes #7677.
// baseline_model is the satisfying model obtained before optimization
// and guards against LP state corruption for non-linear objectives
// like mod, fixes #9012.
bool opt_solver::maximize_objective_isolated(unsigned i, model_ref& baseline_model, expr_ref& blocker) {
m_context.push();
if (!maximize_objective(i, blocker)) {
m_context.pop(1);
return false;
}
// Save results before popping
inf_eps val = m_objective_values[i];
model_ref mdl;
if (m_models[i])
mdl = m_models[i];
m_context.pop(1);
// Restore the computed values after pop
m_objective_values[i] = val;
if (mdl)
m_models.set(i, mdl.get());
// The baseline model may witness a greater value than the LP
// optimizer returned, e.g. for non-linear objectives like mod
// where the LP relaxation overshoots and restore_x falls back
// to a stale assignment: use the model value as the floor value.
if (baseline_model)
update_from_baseline_model(i, baseline_model, blocker);
return true;
}
// If baseline_model evaluates objective i to a value better than the
// current optimum, adopt that value and update the blocker.
void opt_solver::update_from_baseline_model(unsigned i, model_ref& baseline_model, expr_ref& blocker) {
arith_util a(m);
rational r;
expr_ref obj_val = (*baseline_model)(m_objective_terms.get(i));
if (a.is_numeral(obj_val, r) && inf_eps(r) > m_objective_values[i]) {
m_objective_values[i] = inf_eps(r);
if (!m_models[i])
m_models.set(i, baseline_model.get());
expr* obj = m_objective_terms.get(i);
if (a.is_int(obj))
blocker = a.mk_ge(obj, a.mk_numeral(r + 1, true));
else
blocker = a.mk_ge(obj, a.mk_numeral(r, false));
}
}
lbool opt_solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_context.find_mutexes(vars, mutexes);
}

View file

@ -167,6 +167,8 @@ namespace opt {
void reset_objectives();
bool maximize_objective(unsigned i, expr_ref& blocker);
bool maximize_objectives1(expr_ref_vector& blockers);
bool maximize_objective_isolated(unsigned i, model_ref& baseline_model, expr_ref& blocker);
void update_from_baseline_model(unsigned i, model_ref& baseline_model, expr_ref& blocker);
inf_eps const & saved_objective_value(unsigned obj_index);
inf_eps current_objective_value(unsigned obj_index);
model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }

View file

@ -202,15 +202,19 @@ namespace opt {
}
}
lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize, bool is_box) {
TRACE(opt, tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";);
arith_util arith(m);
bool is_int = arith.is_int(m_objs.get(obj_index));
lbool is_sat = l_true;
expr_ref bound(m), last_bound(m);
for (unsigned i = 0; i < obj_index; ++i)
commit_assignment(i);
// In lex mode, commit previous objectives so that earlier objectives
// constrain later ones. In box mode, skip this so each objective
// is optimized independently.
if (!is_box)
for (unsigned i = 0; i < obj_index; ++i)
commit_assignment(i);
unsigned steps = 0;
unsigned step_incs = 0;
@ -253,7 +257,14 @@ namespace opt {
}
last_objective = obj;
if (bound == last_bound) {
break;
// LP didn't produce a new blocker. If the model-based lower bound
// is strictly better than what the LP found, use it to push the LP
// further. This handles cases where nonlinear constraints, mod,
// to_int, prevent the LP from seeing the full feasible region.
if (m_lower[obj_index].is_finite() && m_lower[obj_index] > obj)
bound = m_s->mk_ge(obj_index, m_lower[obj_index]);
if (bound == last_bound)
break;
}
m_s->assert_expr(bound);
last_bound = bound;
@ -284,9 +295,9 @@ namespace opt {
// set the solution tight.
m_upper[obj_index] = m_lower[obj_index];
for (unsigned i = obj_index+1; i < m_lower.size(); ++i) {
m_lower[i] = inf_eps(rational(-1), inf_rational(0));
}
if (!is_box)
for (unsigned i = obj_index+1; i < m_lower.size(); ++i)
m_lower[i] = inf_eps(rational(-1), inf_rational(0));
return l_true;
}
@ -527,15 +538,28 @@ namespace opt {
if (m_vars.empty()) {
return is_sat;
}
// assertions added during search are temporary.
solver::scoped_push _push(*m_s);
if (m_optsmt_engine == symbol("symba")) {
is_sat = symba_opt();
// In box mode, optimize each objective independently.
// Each objective gets its own push/pop scope so that bounds
// from one objective do not constrain another.
// Note: geometric_lex is used unconditionally here, even when
// m_optsmt_engine is "symba", because symba_opt and geometric_opt
// optimize all objectives jointly, violating box mode semantics.
//
m_context.get_base_model(m_best_model);
for (unsigned i = 0; i < m_vars.size() && m.inc(); ++i) {
// Reset bounds for objective i so that update_lower_lex
// contamination from earlier objectives does not affect it.
m_lower[i] = inf_eps(rational(-1), inf_rational(0));
m_upper[i] = inf_eps(rational(1), inf_rational(0));
solver::scoped_push _push(*m_s);
is_sat = geometric_lex(i, true, true);
if (is_sat == l_undef)
return l_undef;
if (is_sat == l_false)
return l_false;
m_models.set(i, m_best_model.get());
}
else {
is_sat = geometric_opt();
}
return is_sat;
return l_true;
}

View file

@ -81,7 +81,7 @@ namespace opt {
lbool symba_opt();
lbool geometric_lex(unsigned idx, bool is_maximize);
lbool geometric_lex(unsigned idx, bool is_maximize, bool is_box = false);
void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls);

View file

@ -60,6 +60,8 @@ def_module_params(module_name='smt',
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'),
('arith.nl.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'),
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),

View file

@ -2236,6 +2236,21 @@ class qe_lite::impl {
if (q->get_kind() != lambda_k) {
m_imp(indices, true, result);
}
// After eq_der + FM, try to expand remaining bounded
// integer quantifiers into finite disjunctions.
// If expansion succeeds, the result is quantifier-free
// so we return it directly without re-wrapping.
if (is_exists(q) || is_forall(q)) {
expr_ref expanded(m);
if (m_imp.try_expand_bounded_quantifier(q, result, expanded)) {
if (is_forall(q))
expanded = push_not(expanded);
m_imp.m_rewriter(expanded, result, result_pr);
if (m.proofs_enabled())
result_pr = m.mk_rewrite(q, result);
return true;
}
}
if (is_forall(q)) {
result = push_not(result);
}
@ -2271,6 +2286,8 @@ private:
th_rewriter m_rewriter;
bool m_use_array_der;
static const unsigned EXPAND_BOUND_LIMIT = 10000;
bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) {
index = fmls.size();
if (index <= 1) {
@ -2287,6 +2304,205 @@ private:
return index < fmls.size();
}
// Try to extract a tight integer bound from a conjunct for de Bruijn variable idx.
// Returns true if the conjunct is a bound for var(idx).
// Sets is_lower=true for lower bounds, is_lower=false for upper bounds.
// Sets bound_val to the bound value, inclusive.
bool extract_var_bound(expr* e, unsigned idx, unsigned num_decls, arith_util& a_util,
bool& is_lower, rational& bound_val) {
expr *atom, *lhs, *rhs;
rational val;
bool is_neg = m.is_not(e, atom);
if (is_neg)
e = atom;
// Normalize ge/gt to le/lt by swapping operands: a >= b <=> b <= a, a > b <=> b < a.
bool strict;
if (a_util.is_le(e, lhs, rhs)) strict = false;
else if (a_util.is_ge(e, lhs, rhs)) { std::swap(lhs, rhs); strict = false; }
else if (a_util.is_lt(e, lhs, rhs)) strict = true;
else if (a_util.is_gt(e, lhs, rhs)) { std::swap(lhs, rhs); strict = true; }
else return false;
// Defensive. Pre-condition happens to be established in current calling context.
if (!a_util.is_int(lhs))
return false;
// After normalization: lhs <= rhs (strict=false) or lhs < rhs (strict=true).
// Strict inequalities tighten the inclusive bound by 1.
bool var_on_left = is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val);
if (!var_on_left && !(is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)))
return false;
// var_on_left: var <= val (upper bound), adjusted for strict.
// var_on_right: val <= var (lower bound), adjusted for strict.
is_lower = !var_on_left;
bound_val = var_on_left ? (strict ? val - 1 : val) : (strict ? val + 1 : val);
// Negation flips bound direction and tightens by 1.
if (is_neg) {
is_lower = !is_lower;
bound_val = is_lower ? bound_val + 1 : bound_val - 1;
}
return true;
}
// Try to expand a bounded existential quantifier into a finite disjunction.
// The body has been processed by eq_der + FM already.
// Works at the de Bruijn variable level.
// Returns true if expansion succeeded.
bool try_expand_bounded_quantifier(quantifier* q, expr* body, expr_ref& result) {
unsigned num_decls = q->get_num_decls();
if (num_decls == 0)
return false;
arith_util a_util(m);
// Check which variables still appear in the body
used_vars uv;
uv(body);
unsigned remaining = 0;
for (unsigned i = 0; i < num_decls; ++i)
if (uv.contains(i))
remaining++;
if (remaining == 0)
return false;
// Only handle integer variables
for (unsigned i = 0; i < num_decls; ++i) {
if (!uv.contains(i))
continue;
if (!a_util.is_int(q->get_decl_sort(i)))
return false;
}
// Flatten body into conjuncts
expr_ref_vector conjs(m);
flatten_and(body, conjs);
// Extract bounds for each remaining variable
vector<rational> lbs, ubs;
bool_vector has_lb, has_ub;
lbs.resize(num_decls);
ubs.resize(num_decls);
has_lb.resize(num_decls, false);
has_ub.resize(num_decls, false);
// Track which conjuncts are pure bounds, to separate from the payload
bool_vector is_bound_conj;
is_bound_conj.resize(conjs.size(), false);
for (unsigned ci = 0; ci < conjs.size(); ++ci) {
for (unsigned vi = 0; vi < num_decls; ++vi) {
if (!uv.contains(vi))
continue;
bool is_lower;
rational bval;
if (extract_var_bound(conjs[ci].get(), vi, num_decls, a_util, is_lower, bval)) {
if (is_lower) {
if (!has_lb[vi] || bval > lbs[vi])
lbs[vi] = bval;
has_lb[vi] = true;
}
else {
if (!has_ub[vi] || bval < ubs[vi])
ubs[vi] = bval;
has_ub[vi] = true;
}
is_bound_conj[ci] = true;
}
}
}
// Check all remaining variables are bounded
rational domain_product(1);
for (unsigned i = 0; i < num_decls; ++i) {
if (!uv.contains(i))
continue;
if (!has_lb[i] || !has_ub[i])
return false;
rational size = ubs[i] - lbs[i] + 1;
if (size <= rational(0)) {
result = m.mk_false();
return true;
}
domain_product *= size;
if (domain_product > rational(EXPAND_BOUND_LIMIT))
return false;
}
IF_VERBOSE(2, verbose_stream() << "(qe-lite :expand-bounded-quantifier"
<< " :vars " << remaining
<< " :domain-size " << domain_product << ")\n");
// Collect the non-bound conjuncts as the payload
expr_ref_vector payload(m);
for (unsigned ci = 0; ci < conjs.size(); ++ci)
if (!is_bound_conj[ci])
payload.push_back(conjs[ci].get());
// Collect the remaining variables in order, with their bounds
unsigned_vector var_indices;
vector<rational> var_lbs, var_ubs;
for (unsigned i = 0; i < num_decls; ++i) {
if (!uv.contains(i)) continue;
var_indices.push_back(i);
var_lbs.push_back(lbs[i]);
var_ubs.push_back(ubs[i]);
}
// Build substitution array: one entry per de Bruijn variable
expr_ref_vector subst_map(m);
subst_map.resize(num_decls);
// Initialize non-remaining variables to themselves
for (unsigned i = 0; i < num_decls; ++i)
if (!uv.contains(i))
subst_map.set(i, m.mk_var(i, q->get_decl_sort(i)));
// Enumerate all value combinations
unsigned nv = var_indices.size();
vector<rational> cur_vals;
cur_vals.resize(nv);
for (unsigned i = 0; i < nv; ++i)
cur_vals[i] = var_lbs[i];
var_subst vs(m, false);
expr_ref_vector disjuncts(m);
while (true) {
// Set up substitution for current values
for (unsigned i = 0; i < nv; ++i)
subst_map.set(var_indices[i], a_util.mk_int(cur_vals[i]));
// Substitute in each payload conjunct and combine
expr_ref_vector inst_conjs(m);
for (expr* p : payload) {
expr_ref inst(m);
inst = vs(p, subst_map.size(), subst_map.data());
inst_conjs.push_back(inst);
}
expr_ref inst_body(m);
bool_rewriter(m).mk_and(inst_conjs.size(), inst_conjs.data(), inst_body);
disjuncts.push_back(inst_body);
// Increment to next value combination, rightmost first
unsigned carry = nv;
for (unsigned i = nv; i-- > 0; ) {
cur_vals[i] += 1;
if (cur_vals[i] <= var_ubs[i]) {
carry = i;
break;
}
cur_vals[i] = var_lbs[i];
}
if (carry == nv)
break;
}
bool_rewriter(m).mk_or(disjuncts.size(), disjuncts.data(), result);
return true;
}
public:
impl(ast_manager & m, params_ref const & p, bool use_array_der):
m(m),

View file

@ -1360,6 +1360,7 @@ namespace {
// to check it again.
get_check_mark(reg) == NOT_CHECKED &&
is_ground(m_registers[reg]) &&
instr->m_enode != nullptr &&
get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
}

View file

@ -125,7 +125,7 @@ namespace smt {
if (!m_non_diff_logic_exprs) {
TRACE(non_diff_logic, tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
IF_VERBOSE(2, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
m_non_diff_logic_exprs = true;
}
}

View file

@ -170,7 +170,7 @@ template<typename Ext>
void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
if (!m_non_diff_logic_exprs) {
TRACE(non_diff_logic, tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
IF_VERBOSE(2, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
m_non_diff_logic_exprs = true;
}

View file

@ -155,6 +155,7 @@ class theory_lra::imp {
ptr_vector<expr> m_not_handled;
ptr_vector<app> m_underspecified;
ptr_vector<app> m_bv_terms;
ptr_vector<expr> m_mul_defs; // fresh multiplication definition vars
vector<ptr_vector<api_bound> > m_use_list; // bounds where variables are used.
// attributes for incremental version:
@ -267,9 +268,25 @@ class theory_lra::imp {
};
m_nla->set_relevant(is_relevant);
m_nla->updt_params(ctx().get_params());
m_nla->get_core().set_add_mul_def_hook([&](unsigned sz, lpvar const* vs) { return add_mul_def(sz, vs); });
}
}
lpvar add_mul_def(unsigned sz, lpvar const* vs) {
bool is_int = true;
for (unsigned i = 0; i < sz; ++i) {
theory_var tv = lp().local_to_external(vs[i]);
is_int &= this->is_int(tv);
}
sort* srt = is_int ? a.mk_int() : a.mk_real();
app_ref c(m.mk_fresh_const("mul!", srt), m);
mk_enode(c);
theory_var v = mk_var(c);
ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_mul_defs));
m_mul_defs.push_back(c);
return register_theory_var_in_lar_solver(v);
}
void found_unsupported(expr* n) {
ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_not_handled));
TRACE(arith, tout << "unsupported " << mk_pp(n, m) << "\n");
@ -3983,6 +4000,81 @@ public:
return inf_eps(rational(0), inf_rational(ival.x, ival.y));
}
lp::lp_status max_with_lp(theory_var v, lpvar& vi, lp::impq& term_max) {
if (!lp().is_feasible() || lp().has_changed_columns())
make_feasible();
vi = get_lpvar(v);
auto st = lp().maximize_term(vi, term_max);
if (has_int() && lp().has_inf_int()) {
st = lp::lp_status::FEASIBLE;
lp().restore_x();
}
return st;
}
// Returns true if NLA handled the result (blocker and result are set).
// Returns false if maximize should fall through to the normal status switch.
bool max_with_nl(theory_var v, lp::lp_status& st, unsigned level, expr_ref& blocker, inf_eps& result) {
if (!m_nla || (st != lp::lp_status::OPTIMAL && st != lp::lp_status::UNBOUNDED))
return false;
// Save the LP optimum before NLA check may restore x.
auto lp_val = value(v);
auto lp_ival = get_ivalue(v);
auto nla_st = check_nla(level);
TRACE(opt, tout << "check_nla returned " << nla_st
<< " lp_ival=" << lp_ival << "\n";
if (nla_st == FC_CONTINUE) {
tout << "LP assignment at maximize optimum:\n";
for (unsigned j = 0; j < lp().column_count(); j++) {
if (!lp().get_column_value(j).is_zero())
tout << " x[" << j << "] = " << lp().get_column_value(j) << "\n";
}
});
switch (nla_st) {
case FC_DONE:
// NLA satisfied: keep the optimal assignment, return LP value
blocker = mk_gt(v);
result = lp_val;
st = lp::lp_status::FEASIBLE;
return true;
case FC_CONTINUE:
// NLA found the LP optimum violates nonlinear constraints.
// Restore x but return the LP optimum value and blocker
// as a bound for the optimizer to validate via check_bound().
lp().restore_x();
blocker = mk_gt(v, lp_ival);
result = lp_val;
st = lp::lp_status::FEASIBLE;
return true;
case FC_GIVEUP:
lp().restore_x();
st = lp::lp_status::UNBOUNDED;
return false;
}
UNREACHABLE();
return false;
}
theory_lra::inf_eps max_result(theory_var v, lpvar vi, lp::lp_status st, expr_ref& blocker, bool& has_shared) {
switch (st) {
case lp::lp_status::OPTIMAL:
init_variable_values();
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
blocker = mk_gt(v);
return value(v);
case lp::lp_status::FEASIBLE:
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
blocker = mk_gt(v);
return value(v);
default:
SASSERT(st == lp::lp_status::UNBOUNDED);
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
has_shared = false;
blocker = m.mk_false();
return inf_eps(rational::one(), inf_rational());
}
}
theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
unsigned level = 2;
lp::impq term_max;
@ -3999,55 +4091,21 @@ public:
st = lp::lp_status::UNBOUNDED;
}
else {
if (!lp().is_feasible() || lp().has_changed_columns())
make_feasible();
vi = get_lpvar(v);
st = lp().maximize_term(vi, term_max);
if (has_int() && lp().has_inf_int()) {
st = lp::lp_status::FEASIBLE;
lp().restore_x();
}
if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
switch (check_nla(level)) {
case FC_DONE:
case FC_CONTINUE:
st = lp::lp_status::FEASIBLE;
break;
case FC_GIVEUP:
st = lp::lp_status::UNBOUNDED;
break;
}
lp().restore_x();
}
}
switch (st) {
case lp::lp_status::OPTIMAL: {
init_variable_values();
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
auto val = value(v);
blocker = mk_gt(v);
return val;
}
case lp::lp_status::FEASIBLE: {
auto val = value(v);
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
blocker = mk_gt(v);
return val;
}
default:
SASSERT(st == lp::lp_status::UNBOUNDED);
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
has_shared = false;
blocker = m.mk_false();
return inf_eps(rational::one(), inf_rational());
st = max_with_lp(v, vi, term_max);
inf_eps nl_result;
if (max_with_nl(v, st, level, blocker, nl_result))
return nl_result;
}
return max_result(v, vi, st, blocker, has_shared);
}
expr_ref mk_gt(theory_var v) {
lp::impq val = get_ivalue(v);
return mk_gt(v, val);
}
// Overload: create blocker from a saved impq value (used when x has been restored)
expr_ref mk_gt(theory_var v, lp::impq const& val) {
expr* obj = get_enode(v)->get_expr();
rational r = val.x;
expr_ref e(m);

View file

@ -345,11 +345,6 @@ final_check_status theory_seq::final_check_eh(unsigned level) {
TRACEFIN("regex propagate");
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACEFIN("propagate_contains");
return FC_CONTINUE;
}
if (check_fixed_length(true, false)) {
++m_stats.m_fixed_length;
TRACEFIN("zero_length");
@ -365,6 +360,16 @@ final_check_status theory_seq::final_check_eh(unsigned level) {
TRACEFIN("fixed_length");
return FC_CONTINUE;
}
if (check_fixed_length(false, true)) {
++m_stats.m_fixed_length;
TRACEFIN("fixed_length");
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACEFIN("propagate_contains");
return FC_CONTINUE;
}
if (check_int_string()) {
++m_stats.m_int_string;
TRACEFIN("int_string");
@ -499,12 +504,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings
m_fixed.contains(e)) {
return false;
}
m_trail_stack.push(insert_obj_trail<expr>(m_fixed, e));
m_fixed.insert(e);
expr_ref seq(e, m), head(m), tail(m);
TRACE(seq, tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
@ -514,6 +513,11 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings
if (!check_long_strings && lo > 20 && !is_zero)
return false;
m_trail_stack.push(insert_obj_trail<expr>(m_fixed, e));
m_fixed.insert(e);
expr_ref seq(e, m), head(m), tail(m);
if (lo.is_zero()) {
seq = m_util.str.mk_empty(e->get_sort());
}
@ -2976,7 +2980,7 @@ void theory_seq::add_axiom(literal_vector & lits) {
TRACE(seq, ctx.display_literals_verbose(tout << "assert " << lits << " :", lits) << "\n";);
for (literal lit : lits)
if (ctx.get_assignment(lit) == l_true)
if (ctx.get_assignment(lit) == l_true && ctx.get_assign_level(lit) == 0)
return;
for (literal lit : lits)

View file

@ -6,7 +6,6 @@ z3_add_component(core_tactics
ctx_simplify_tactic.cpp
elim_term_ite_tactic.cpp
elim_uncnstr_tactic.cpp
injectivity_tactic.cpp
nnf_tactic.cpp
occf_tactic.cpp
pb_preprocess_tactic.cpp

View file

@ -1,281 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
injectivity_tactic.cpp
Author:
Nicolas Braud-Santoni (t-nibrau) 2017-08-10
--*/
#include <algorithm>
#include <utility>
#include "tactic/tactical.h"
#include "ast/rewriter/rewriter_def.h"
#include "tactic/core/injectivity_tactic.h"
#include "util/dec_ref_util.h"
class injectivity_tactic : public tactic {
struct InjHelper : public obj_map<func_decl, obj_hashtable<func_decl>*> {
ast_manager & m_manager;
void insert(func_decl* const f, func_decl* const g) {
obj_hashtable<func_decl> *m;
if (! obj_map::find(f, m)) {
m_manager.inc_ref(f);
m = alloc(obj_hashtable<func_decl>); // TODO: Check we don't leak memory
obj_map::insert(f, m);
}
if (!m->contains(g)) {
m_manager.inc_ref(g);
m->insert(g);
}
}
bool find(func_decl* const f, func_decl* const g) const {
obj_hashtable<func_decl> *m;
if(! obj_map::find(f, m))
return false;
return m->contains(g);
}
InjHelper(ast_manager& m) : obj_map<func_decl, obj_hashtable<func_decl>*>(), m_manager(m) {}
~InjHelper() {
for(auto m : *this) {
for (func_decl* f : *m.get_value())
m_manager.dec_ref(f);
m_manager.dec_ref(m.m_key);
dealloc(m.m_value);
}
}
};
struct finder {
ast_manager & m_manager;
InjHelper & inj_map;
finder(ast_manager & m, InjHelper & map, params_ref const & p) :
m_manager(m),
inj_map(map) {
updt_params(p);
}
ast_manager & m() const { return m_manager; }
bool is_axiom(expr* n, func_decl* &f, func_decl* &g) {
if (!is_forall(n))
return false;
quantifier* const q = to_quantifier(n);
if (q->get_num_decls() != 1)
return false;
const expr * const body = q->get_expr();
// n ~= forall x. body
if (!m().is_eq(body))
return false;
const app * const body_a = to_app(body);
if (body_a->get_num_args() != 2)
return false;
const expr* a = body_a->get_arg(0);
const expr* b = body_a->get_arg(1);
// n ~= forall x. (= a b)
if (is_app(a) && is_var(b)) {
// Do nothing
}
else if (is_app(b) && is_var(a)) {
std::swap(a, b);
}
else
return false;
const app* const a_app = to_app(a);
const var* const b_var = to_var(b);
if (b_var->get_idx() != 0) // idx is the De Bruijn's index
return false;
if (a_app->get_num_args() != 1)
return false;
g = a_app->get_decl();
const expr* const a_body = a_app->get_arg(0);
// n ~= forall x. (= (g a_body) x)
if (!is_app(a_body))
return false;
const app* const a_body_app = to_app(a_body);
if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions
return false;
f = a_body_app->get_decl();
const expr* const a_body_body = a_body_app->get_arg(0);
// n ~= forall x. (= (g (f a_body_body)) x)
if (a_body_body != b_var)
return false;
// n ~= forall x. (= (g (f x)) x)
return true;
}
void operator()(goal_ref const & goal,
goal_ref_buffer & result) {
tactic_report report("injectivity", *goal);
fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
fail_if_proof_generation("injectivity", goal);
for (unsigned i = 0; i < goal->size(); ++i) {
func_decl *f, *g;
if (!is_axiom(goal->form(i), f, g)) continue;
TRACE(injectivity, tout << "Marking " << f->get_name() << " as injective" << std::endl;);
inj_map.insert(f, g);
// TODO: Record that g is f's pseudoinverse
}
}
void updt_params(params_ref const & p) {}
};
struct rewriter_eq_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
InjHelper & inj_map;
ast_manager & m() const { return m_manager; }
rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) {
}
void cleanup_buffers() {
}
void reset() {
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (num != 2)
return BR_FAILED;
if (!m().is_eq(f))
return BR_FAILED;
// We are rewriting (= a b)
if (!is_app(args[0]) || !is_app(args[1]))
return BR_FAILED;
const app* const a = to_app(args[0]);
const app* const b = to_app(args[1]);
// a and b are applications of the same function
if (a->get_decl() != b->get_decl())
return BR_FAILED;
// Maybe TODO: Generalize to multi-parameter functions ?
if (a->get_num_args() != 1 || b->get_num_args() != 1)
return BR_FAILED;
if (!inj_map.contains(a->get_decl()))
return BR_FAILED;
SASSERT(a->get_arg(0)->get_sort() == b->get_arg(0)->get_sort());
TRACE(injectivity, tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) <<
" " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;);
result = m().mk_eq(a->get_arg(0), b->get_arg(0));
result_pr = nullptr;
return BR_DONE;
}
};
struct rewriter_eq : public rewriter_tpl<rewriter_eq_cfg> {
rewriter_eq_cfg m_cfg;
rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) :
rewriter_tpl<rewriter_eq_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, map, p) {
}
};
struct rewriter_inverse { };
finder * m_finder;
rewriter_eq * m_eq;
InjHelper * m_map;
params_ref m_params;
ast_manager & m_manager;
public:
injectivity_tactic(ast_manager & m, params_ref const & p):
m_params(p),
m_manager(m) {
TRACE(injectivity, tout << "constructed new tactic" << std::endl;);
m_map = alloc(InjHelper, m);
m_finder = alloc(finder, m, *m_map, p);
m_eq = alloc(rewriter_eq, m, *m_map, p);
}
tactic * translate(ast_manager & m) override {
return alloc(injectivity_tactic, m, m_params);
}
~injectivity_tactic() override {
dealloc(m_finder);
dealloc(m_eq);
dealloc(m_map);
}
char const* name() const override { return "injectivity"; }
void updt_params(params_ref const & p) override {
m_params.append(p);
m_finder->updt_params(m_params);
}
void collect_param_descrs(param_descrs & r) override {
insert_max_memory(r);
insert_produce_models(r);
}
void operator()(goal_ref const & g,
goal_ref_buffer & result) override {
(*m_finder)(g, result);
for (unsigned i = 0; i < g->size(); ++i) {
expr* curr = g->form(i);
expr_ref rw(m_manager);
proof_ref pr(m_manager);
(*m_eq)(curr, rw, pr);
g->update(i, rw, pr, g->dep(i));
}
result.push_back(g.get());
}
void cleanup() override {
InjHelper * m = alloc(InjHelper, m_manager);
finder * f = alloc(finder, m_manager, *m, m_params);
rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params);
std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq);
dealloc(m), dealloc(f), dealloc(r);
}
};
tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p) {
return alloc(injectivity_tactic, m, p);
}

View file

@ -45,12 +45,20 @@ Tactic Documentation:
#pragma once
#include "util/params.h"
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/injectivity_simplifier.h"
class ast_manager;
class tactic;
tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref());
inline tactic* mk_injectivity_tactic(ast_manager& m, params_ref const& p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(injectivity_simplifier, m, p, s);
});
}
/*
ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)")
ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)")
*/

View file

@ -0,0 +1,198 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
special_relations_simplifier.h
Abstract:
Detect special relations in an axiomatization,
rewrite goal using special relations.
Author:
Nikolaj Bjorner (nbjorner) 2019-03-28
Notes:
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/pattern/expr_pattern_match.h"
#include "ast/rewriter/func_decl_replace.h"
#include "ast/ast_util.h"
class special_relations_simplifier : public dependent_expr_simplifier {
expr_pattern_match m_pm;
svector<sr_property> m_properties;
struct sp_axioms {
unsigned_vector m_formula_indices;
sr_property m_sp_features;
sp_axioms() : m_sp_features(sr_none) {}
};
obj_map<func_decl, sp_axioms> m_detected_relations;
void initialize() {
if (!m_properties.empty()) return;
sort_ref A(m.mk_uninterpreted_sort(symbol("A")), m);
func_decl_ref R(m.mk_func_decl(symbol("?R"), A, A, m.mk_bool_sort()), m);
var_ref x(m.mk_var(0, A), m);
var_ref y(m.mk_var(1, A), m);
var_ref z(m.mk_var(2, A), m);
expr* _x = x, *_y = y, *_z = z;
expr_ref Rxy(m.mk_app(R, _x, _y), m);
expr_ref Ryz(m.mk_app(R, _y, _z), m);
expr_ref Rxz(m.mk_app(R, _x, _z), m);
expr_ref Rxx(m.mk_app(R, _x, _x), m);
expr_ref Ryx(m.mk_app(R, _y, _x), m);
expr_ref Rzy(m.mk_app(R, _z, _y), m);
expr_ref Rzx(m.mk_app(R, _z, _x), m);
expr_ref nRxy(m.mk_not(Rxy), m);
expr_ref nRyx(m.mk_not(Ryx), m);
expr_ref nRzx(m.mk_not(Rzx), m);
expr_ref nRxz(m.mk_not(Rxz), m);
sort* As[3] = { A, A, A };
symbol xyz[3] = { symbol("x"), symbol("y"), symbol("z") };
expr_ref fml(m);
quantifier_ref q(m);
expr_ref pat(m.mk_pattern(to_app(Rxy)), m);
expr_ref pat0(m.mk_pattern(to_app(Rxx)), m);
expr* pats[1] = { pat };
expr* pats0[1] = { pat0 };
fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = m.mk_or(mk_not(Rxy & Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = Rxx;
q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats0);
register_pattern(m_pm.initialize(q), sr_reflexive);
fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(mk_not(Rxy & Ryx), m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(nRyx, nRzx, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(mk_not(Ryx & Rzx), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(nRxy, nRxz, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(mk_not(Rxy & Rxz), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(Rxy, Ryx);
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_total);
TRACE(special_relations, m_pm.display(tout););
}
void register_pattern(unsigned index, sr_property p) {
SASSERT(index == m_properties.size());
m_properties.push_back(p);
}
void insert(func_decl* f, unsigned idx, sr_property p) {
sp_axioms ax;
m_detected_relations.find(f, ax);
ax.m_formula_indices.push_back(idx);
ax.m_sp_features = (sr_property)(p | ax.m_sp_features);
m_detected_relations.insert(f, ax);
}
void collect_feature(unsigned idx, expr* f) {
if (!is_quantifier(f)) return;
unsigned index = 0;
app_ref_vector patterns(m);
bool is_match = m_pm.match_quantifier_index(to_quantifier(f), patterns, index);
TRACE(special_relations, tout << "check " << is_match << " " << mk_pp(f, m) << "\n";
if (is_match) tout << patterns << " " << index << "\n";);
if (is_match) {
func_decl* p = to_app(patterns.get(0)->get_arg(0))->get_decl();
insert(p, idx, m_properties[index]);
}
}
public:
special_relations_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s)
: dependent_expr_simplifier(m, s), m_pm(m) {}
char const* name() const override { return "special-relations"; }
void reduce() override {
initialize();
m_detected_relations.reset();
// Phase 1: scan all formulas to detect special relation axioms
for (unsigned idx : indices())
collect_feature(idx, m_fmls[idx].fml());
if (m_detected_relations.empty())
return;
// Phase 2: for each detected relation, create a special relation declaration
special_relations_util u(m);
func_decl_replace replace(m);
unsigned_vector to_delete;
for (auto const& kv : m_detected_relations) {
sr_property feature = kv.m_value.m_sp_features;
switch (feature) {
case sr_po:
replace.insert(kv.m_key, u.mk_po_decl(kv.m_key));
to_delete.append(kv.m_value.m_formula_indices);
break;
case sr_to:
replace.insert(kv.m_key, u.mk_to_decl(kv.m_key));
to_delete.append(kv.m_value.m_formula_indices);
break;
case sr_plo:
replace.insert(kv.m_key, u.mk_plo_decl(kv.m_key));
to_delete.append(kv.m_value.m_formula_indices);
break;
case sr_lo:
replace.insert(kv.m_key, u.mk_lo_decl(kv.m_key));
to_delete.append(kv.m_value.m_formula_indices);
break;
default:
TRACE(special_relations, tout << "unprocessed feature " << feature << "\n";);
break;
}
}
if (replace.empty())
return;
// Phase 3: replace function declarations across all formulas
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
if (to_delete.contains(idx)) {
m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, d.dep()));
}
else {
expr_ref new_fml = replace(d.fml());
if (new_fml != d.fml())
m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep()));
}
}
}
};

View file

@ -18,164 +18,4 @@ Notes:
--*/
#include "tactic/core/special_relations_tactic.h"
#include "ast/rewriter/func_decl_replace.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
void special_relations_tactic::collect_feature(goal const& g, unsigned idx,
obj_map<func_decl, sp_axioms>& goal_features) {
expr* f = g.form(idx);
func_decl_ref p(m);
if (!is_quantifier(f)) return;
unsigned index = 0;
app_ref_vector patterns(m);
bool is_match = m_pm.match_quantifier_index(to_quantifier(f), patterns, index);
TRACE(special_relations, tout << "check " << is_match << " " << mk_pp(f, m) << "\n";
if (is_match) tout << patterns << " " << index << "\n";);
if (is_match) {
p = to_app(patterns.get(0)->get_arg(0))->get_decl();
insert(goal_features, p, idx, m_properties[index]);
}
}
void special_relations_tactic::insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* f, unsigned idx, sr_property p) {
sp_axioms ax;
goal_features.find(f, ax);
ax.m_goal_indices.push_back(idx);
ax.m_sp_features = (sr_property)(p | ax.m_sp_features);
goal_features.insert(f, ax);
}
void special_relations_tactic::initialize() {
if (!m_properties.empty()) return;
sort_ref A(m.mk_uninterpreted_sort(symbol("A")), m);
func_decl_ref R(m.mk_func_decl(symbol("?R"), A, A, m.mk_bool_sort()), m);
var_ref x(m.mk_var(0, A), m);
var_ref y(m.mk_var(1, A), m);
var_ref z(m.mk_var(2, A), m);
expr* _x = x, *_y = y, *_z = z;
expr_ref Rxy(m.mk_app(R, _x, y), m);
expr_ref Ryz(m.mk_app(R, _y, z), m);
expr_ref Rxz(m.mk_app(R, _x, z), m);
expr_ref Rxx(m.mk_app(R, _x, x), m);
expr_ref Ryx(m.mk_app(R, _y, x), m);
expr_ref Rzy(m.mk_app(R, _z, y), m);
expr_ref Rzx(m.mk_app(R, _z, x), m);
expr_ref nRxy(m.mk_not(Rxy), m);
expr_ref nRyx(m.mk_not(Ryx), m);
expr_ref nRzx(m.mk_not(Rzx), m);
expr_ref nRxz(m.mk_not(Rxz), m);
sort* As[3] = { A, A, A};
symbol xyz[3] = { symbol("x"), symbol("y"), symbol("z") };
expr_ref fml(m);
quantifier_ref q(m);
expr_ref pat(m.mk_pattern(to_app(Rxy)), m);
expr_ref pat0(m.mk_pattern(to_app(Rxx)), m);
expr* pats[1] = { pat };
expr* pats0[1] = { pat0 };
fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = m.mk_or(mk_not(Rxy & Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = Rxx;
q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats0);
register_pattern(m_pm.initialize(q), sr_reflexive);
fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(mk_not(Rxy & Ryx), m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(nRyx, nRzx, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(mk_not (Ryx & Rzx), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(nRxy, nRxz, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(mk_not(Rxy & Rxz), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(Rxy, Ryx);
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_total);
TRACE(special_relations, m_pm.display(tout););
}
void special_relations_tactic::register_pattern(unsigned index, sr_property p) {
SASSERT(index == m_properties.size());
m_properties.push_back(p);
}
void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) {
tactic_report report("special_relations", *g);
initialize();
obj_map<func_decl, sp_axioms> goal_features;
unsigned size = g->size();
for (unsigned idx = 0; idx < size; ++idx) {
collect_feature(*g, idx, goal_features);
}
special_relations_util u(m);
func_decl_replace replace(m);
unsigned_vector to_delete;
for(auto const& kv : goal_features) {
sr_property feature = kv.m_value.m_sp_features;
switch (feature) {
case sr_po:
replace.insert(kv.m_key, u.mk_po_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_to:
replace.insert(kv.m_key, u.mk_to_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_plo:
replace.insert(kv.m_key, u.mk_plo_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_lo:
replace.insert(kv.m_key, u.mk_lo_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
default:
TRACE(special_relations, tout << "unprocessed feature " << feature << "\n";);
break;
}
}
if (!replace.empty()) {
for (unsigned idx = 0; idx < size; ++idx) {
if (to_delete.contains(idx)) {
g->update(idx, m.mk_true());
}
else {
expr_ref new_f = replace(g->form(idx));
g->update(idx, new_f);
}
}
g->elim_true();
}
g->inc_depth();
result.push_back(g.get());
}
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) {
return alloc(special_relations_tactic, m, p);
}

View file

@ -20,51 +20,18 @@ Notes:
#pragma once
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/pattern/expr_pattern_match.h"
class special_relations_tactic : public tactic {
ast_manager& m;
params_ref m_params;
expr_pattern_match m_pm;
svector<sr_property> m_properties;
struct sp_axioms {
unsigned_vector m_goal_indices;
sr_property m_sp_features;
sp_axioms():m_sp_features(sr_none) {}
};
void collect_feature(goal const& g, unsigned idx, obj_map<func_decl, sp_axioms>& goal_features);
void insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* f, unsigned idx, sr_property p);
void initialize();
void register_pattern(unsigned index, sr_property);
public:
special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()):
m(m), m_params(ref), m_pm(m) {}
void updt_params(params_ref const & p) override { m_params.append(p); }
void collect_param_descrs(param_descrs & r) override { }
void operator()(goal_ref const & in, goal_ref_buffer & result) override;
void cleanup() override {}
tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }
char const* name() const override { return "special_relations"; }
};
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());
#include "tactic/dependent_expr_state_tactic.h"
#include "tactic/core/special_relations_simplifier.h"
inline tactic* mk_special_relations_tactic(ast_manager& m, params_ref const& p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(special_relations_simplifier, m, p, s);
});
}
/*
ADD_TACTIC("special-relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)")
ADD_SIMPLIFIER("special-relations", "detect and replace by special relations.", "alloc(special_relations_simplifier, m, p, s)")
*/

View file

@ -37,6 +37,7 @@ add_executable(test-z3
cube_clause.cpp
datalog_parser.cpp
ddnf.cpp
deep_api_bugs.cpp
diff_logic.cpp
distribution.cpp
dl_context.cpp

View file

@ -160,9 +160,436 @@ void test_optimize_translate() {
Z3_del_context(ctx1);
}
void test_max_reg() {
// BNH multi-objective optimization problem using Z3 Optimize C API.
// Mimics /tmp/bnh_z3.py: two objectives over a constrained 2D domain.
// f1 = 4*x1^2 + 4*x2^2
// f2 = (x1-5)^2 + (x2-5)^2
// 0 <= x1 <= 5, 0 <= x2 <= 3
// C1: (x1-5)^2 + x2^2 <= 25
// C2: (x1-8)^2 + (x2+3)^2 >= 7.7
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_sort real_sort = Z3_mk_real_sort(ctx);
Z3_ast x1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x1"), real_sort);
Z3_ast x2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x2"), real_sort);
auto mk_real = [&](int num, int den = 1) { return Z3_mk_real(ctx, num, den); };
auto mk_mul = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_mul(ctx, 2, args); };
auto mk_add = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_add(ctx, 2, args); };
auto mk_sub = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_sub(ctx, 2, args); };
auto mk_sq = [&](Z3_ast a) { return mk_mul(a, a); };
// f1 = 4*x1^2 + 4*x2^2
Z3_ast f1 = mk_add(mk_mul(mk_real(4), mk_sq(x1)), mk_mul(mk_real(4), mk_sq(x2)));
// f2 = (x1-5)^2 + (x2-5)^2
Z3_ast f2 = mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(mk_sub(x2, mk_real(5))));
// Helper: create optimize with BNH constraints and timeout
auto mk_max_reg = [&]() -> Z3_optimize {
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
// Set timeout to 5 seconds
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_optimize_set_params(ctx, opt, p);
Z3_params_dec_ref(ctx, p);
// Add BNH constraints
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x1, mk_real(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x1, mk_real(5)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x2, mk_real(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x2, mk_real(3)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(x2)), mk_real(25)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, mk_add(mk_sq(mk_sub(x1, mk_real(8))), mk_sq(mk_add(x2, mk_real(3)))), mk_real(77, 10)));
return opt;
};
auto result_str = [](Z3_lbool r) { return r == Z3_L_TRUE ? "sat" : r == Z3_L_FALSE ? "unsat" : "unknown"; };
unsigned num_sat = 0;
// Approach 1: Minimize f1 (Python: opt.minimize(f1))
{
Z3_optimize opt = mk_max_reg();
Z3_optimize_minimize(ctx, opt, f1);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH min f1: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast val; Z3_model_eval(ctx, m, f1, true, &val);
std::cout << " f1=" << Z3_ast_to_string(ctx, val) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
// Approach 2: Minimize f2 (Python: opt2.minimize(f2))
{
Z3_optimize opt = mk_max_reg();
Z3_optimize_minimize(ctx, opt, f2);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH min f2: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast val; Z3_model_eval(ctx, m, f2, true, &val);
std::cout << " f2=" << Z3_ast_to_string(ctx, val) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
// Approach 3: Weighted sum method (Python loop over weights)
int weights[][2] = {{1, 4}, {2, 3}, {1, 1}, {3, 2}, {4, 1}};
for (auto& w : weights) {
Z3_optimize opt = mk_max_reg();
Z3_ast weighted = mk_add(mk_mul(mk_real(w[0], 100), f1), mk_mul(mk_real(w[1], 100), f2));
Z3_optimize_minimize(ctx, opt, weighted);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "BNH weighted (w1=" << w[0] << "/5, w2=" << w[1] << "/5): "
<< result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast v1, v2;
Z3_model_eval(ctx, m, f1, true, &v1);
Z3_model_eval(ctx, m, f2, true, &v2);
std::cout << " f1=" << Z3_ast_to_string(ctx, v1)
<< " f2=" << Z3_ast_to_string(ctx, v2) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
std::cout << "BNH: " << num_sat << "/7 optimizations returned sat" << std::endl;
ENSURE(num_sat == 7);
Z3_del_context(ctx);
std::cout << "BNH optimization test done" << std::endl;
}
void tst_api() {
test_apps();
test_bvneg();
test_mk_distinct();
test_optimize_translate();
}
void tst_max_reg() {
test_max_reg();
}
void test_max_rev() {
// Same as test_max_regimize but with reversed argument order in f1/f2 construction.
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_sort real_sort = Z3_mk_real_sort(ctx);
Z3_ast x1 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x1"), real_sort);
Z3_ast x2 = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x2"), real_sort);
auto mk_real = [&](int num, int den = 1) { return Z3_mk_real(ctx, num, den); };
auto mk_mul = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_mul(ctx, 2, args); };
auto mk_add = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_add(ctx, 2, args); };
auto mk_sub = [&](Z3_ast a, Z3_ast b) { Z3_ast args[] = {a, b}; return Z3_mk_sub(ctx, 2, args); };
auto mk_sq = [&](Z3_ast a) { return mk_mul(a, a); };
// f1 = 4*x2^2 + 4*x1^2 (reversed from: 4*x1^2 + 4*x2^2)
Z3_ast f1 = mk_add(mk_mul(mk_sq(x2), mk_real(4)), mk_mul(mk_sq(x1), mk_real(4)));
// f2 = (x2-5)^2 + (x1-5)^2 (reversed from: (x1-5)^2 + (x2-5)^2)
Z3_ast f2 = mk_add(mk_sq(mk_sub(mk_real(5), x2)), mk_sq(mk_sub(mk_real(5), x1)));
auto mk_max_reg = [&]() -> Z3_optimize {
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
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_optimize_set_params(ctx, opt, p);
Z3_params_dec_ref(ctx, p);
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x1, mk_real(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x1, mk_real(5)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, x2, mk_real(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, x2, mk_real(3)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, mk_add(mk_sq(mk_sub(mk_real(5), x1)), mk_sq(x2)), mk_real(25)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, mk_add(mk_sq(mk_sub(mk_real(8), x1)), mk_sq(mk_add(mk_real(3), x2))), mk_real(77, 10)));
return opt;
};
auto result_str = [](Z3_lbool r) { return r == Z3_L_TRUE ? "sat" : r == Z3_L_FALSE ? "unsat" : "unknown"; };
unsigned num_sat = 0;
{
Z3_optimize opt = mk_max_reg();
Z3_optimize_minimize(ctx, opt, f1);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "max_rev min f1: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast val; Z3_model_eval(ctx, m, f1, true, &val);
std::cout << " f1=" << Z3_ast_to_string(ctx, val) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
{
Z3_optimize opt = mk_max_reg();
Z3_optimize_minimize(ctx, opt, f2);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "max_rev min f2: " << result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast val; Z3_model_eval(ctx, m, f2, true, &val);
std::cout << " f2=" << Z3_ast_to_string(ctx, val) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
int weights[][2] = {{1, 4}, {2, 3}, {1, 1}, {3, 2}, {4, 1}};
for (auto& w : weights) {
Z3_optimize opt = mk_max_reg();
Z3_ast weighted = mk_add(mk_mul(mk_real(w[1], 100), f2), mk_mul(mk_real(w[0], 100), f1));
Z3_optimize_minimize(ctx, opt, weighted);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << "max_rev weighted (w1=" << w[0] << "/5, w2=" << w[1] << "/5): "
<< result_str(result) << std::endl;
ENSURE(result == Z3_L_TRUE);
if (result == Z3_L_TRUE) {
Z3_model m = Z3_optimize_get_model(ctx, opt);
Z3_model_inc_ref(ctx, m);
Z3_ast v1, v2;
Z3_model_eval(ctx, m, f1, true, &v1);
Z3_model_eval(ctx, m, f2, true, &v2);
std::cout << " f1=" << Z3_ast_to_string(ctx, v1)
<< " f2=" << Z3_ast_to_string(ctx, v2) << std::endl;
Z3_model_dec_ref(ctx, m);
num_sat++;
}
Z3_optimize_dec_ref(ctx, opt);
}
std::cout << "max_rev: " << num_sat << "/7 optimizations returned sat" << std::endl;
ENSURE(num_sat == 7);
Z3_del_context(ctx);
std::cout << "max_rev optimization test done" << std::endl;
}
// Regression test for issue #8998:
// minimize(3*a) should be unbounded, same as minimize(a),
// when constraints allow a to go to -infinity.
void test_scaled_minimize_unbounded() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_sort real_sort = Z3_mk_real_sort(ctx);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast a = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), real_sort);
Z3_ast b = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "b"), real_sort);
// (xor (= 0 b) (> (mod (to_int (- a)) 50) 3))
Z3_ast neg_a = Z3_mk_unary_minus(ctx, a);
Z3_ast to_int_neg_a = Z3_mk_real2int(ctx, neg_a);
Z3_ast mod_expr = Z3_mk_mod(ctx, to_int_neg_a, Z3_mk_int(ctx, 50, int_sort));
Z3_ast gt_3 = Z3_mk_gt(ctx, mod_expr, Z3_mk_int(ctx, 3, int_sort));
Z3_ast b_eq_0 = Z3_mk_eq(ctx, Z3_mk_real(ctx, 0, 1), b);
Z3_ast xor_expr = Z3_mk_xor(ctx, b_eq_0, gt_3);
auto check_unbounded_min = [&](Z3_ast objective, const char* label) {
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
Z3_optimize_assert(ctx, opt, xor_expr);
unsigned h = Z3_optimize_minimize(ctx, opt, objective);
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << label << ": " << (result == Z3_L_TRUE ? "sat" : "not sat") << std::endl;
ENSURE(result == Z3_L_TRUE);
// get_lower_as_vector returns [infinity_coeff, rational, epsilon_coeff]
// for -infinity, infinity_coeff should be negative
Z3_ast_vector lower = Z3_optimize_get_lower_as_vector(ctx, opt, h);
Z3_ast inf_coeff = Z3_ast_vector_get(ctx, lower, 0);
int64_t inf_val;
bool ok = Z3_get_numeral_int64(ctx, inf_coeff, &inf_val);
std::cout << " infinity coeff: " << inf_val << std::endl;
ENSURE(ok && inf_val < 0);
Z3_optimize_dec_ref(ctx, opt);
};
// minimize(a) should be -infinity
check_unbounded_min(a, "minimize(a)");
// minimize(3*a) should also be -infinity
Z3_ast three = Z3_mk_real(ctx, 3, 1);
Z3_ast args[] = {three, a};
Z3_ast three_a = Z3_mk_mul(ctx, 2, args);
check_unbounded_min(three_a, "minimize(3*a)");
Z3_del_context(ctx);
std::cout << "scaled minimize unbounded test done" << std::endl;
}
void tst_scaled_min() {
test_scaled_minimize_unbounded();
}
void tst_max_rev() {
test_max_rev();
}
// Regression test for issue #9012: box mode returns wrong optimum for mod.
// With (set-option :opt.priority box) and multiple objectives,
// maximize (mod (- (* 232 a)) 256) must return 248, not 0.
void tst_box_mod_opt() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast a = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), int_sort);
Z3_ast b = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "b"), int_sort);
Z3_ast d = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "d"), int_sort);
Z3_ast c = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "c"), int_sort);
auto mk_int = [&](int v) { return Z3_mk_int(ctx, v, int_sort); };
auto mk_int64 = [&](int64_t v) { return Z3_mk_int64(ctx, v, int_sort); };
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
// set box priority
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_symbol(ctx, p, Z3_mk_string_symbol(ctx, "priority"),
Z3_mk_string_symbol(ctx, "box"));
Z3_optimize_set_params(ctx, opt, p);
Z3_params_dec_ref(ctx, p);
// bounds: 0 <= a < 256, 0 <= b < 2^32, 0 <= d < 2^32, 0 <= c < 16
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, a, mk_int(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_lt(ctx, a, mk_int(256)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, b, mk_int(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_lt(ctx, b, mk_int64(4294967296)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, d, mk_int(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_lt(ctx, d, mk_int64(4294967296)));
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, c, mk_int(0)));
Z3_optimize_assert(ctx, opt, Z3_mk_lt(ctx, c, mk_int(16)));
// minimize (mod (* d 536144634) 4294967296)
Z3_ast mul_d_args[] = { mk_int64(536144634), d };
Z3_ast mul_d = Z3_mk_mul(ctx, 2, mul_d_args);
Z3_optimize_minimize(ctx, opt, Z3_mk_mod(ctx, mul_d, mk_int64(4294967296)));
// minimize b
Z3_optimize_minimize(ctx, opt, b);
// maximize (mod (- (* 232 a)) 256)
Z3_ast mul_a_args[] = { mk_int(232), a };
Z3_ast mul_a = Z3_mk_mul(ctx, 2, mul_a_args);
Z3_ast neg_mul_a = Z3_mk_unary_minus(ctx, mul_a);
unsigned max_idx = Z3_optimize_maximize(ctx, opt, Z3_mk_mod(ctx, neg_mul_a, mk_int(256)));
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
ENSURE(result == Z3_L_TRUE);
// The optimum of (mod (- (* 232 a)) 256) should be 248
Z3_ast lower = Z3_optimize_get_lower(ctx, opt, max_idx);
Z3_string lower_str = Z3_ast_to_string(ctx, lower);
ENSURE(std::string(lower_str) == "248");
Z3_optimize_dec_ref(ctx, opt);
Z3_del_context(ctx);
std::cout << "box mod optimization test passed" << std::endl;
}
// Regression test for #9030: adding an objective in box mode must not
// change the optimal values of other objectives.
void tst_box_independent() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast a = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), int_sort);
Z3_ast b = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "b"), int_sort);
auto mk_int = [&](int v) { return Z3_mk_int(ctx, v, int_sort); };
// Helper: create a fresh optimizer with box priority and constraints
// equivalent to: b >= -166, a <= -166, 5a >= 9b + 178
auto mk_opt = [&]() {
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
Z3_params p = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, p);
Z3_params_set_symbol(ctx, p, Z3_mk_string_symbol(ctx, "priority"),
Z3_mk_string_symbol(ctx, "box"));
Z3_optimize_set_params(ctx, opt, p);
Z3_params_dec_ref(ctx, p);
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, b, mk_int(-166)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx, a, mk_int(-166)));
// 5a - 9b >= 178
Z3_ast lhs_args[] = { mk_int(5), a };
Z3_ast five_a = Z3_mk_mul(ctx, 2, lhs_args);
Z3_ast rhs_args[] = { mk_int(9), b };
Z3_ast nine_b = Z3_mk_mul(ctx, 2, rhs_args);
Z3_ast diff_args[] = { five_a, nine_b };
Z3_ast diff = Z3_mk_sub(ctx, 2, diff_args);
Z3_optimize_assert(ctx, opt, Z3_mk_ge(ctx, diff, mk_int(178)));
return opt;
};
// objective: maximize -(b + a)
auto mk_neg_sum = [&]() {
Z3_ast args[] = { b, a };
return Z3_mk_unary_minus(ctx, Z3_mk_add(ctx, 2, args));
};
// Run 1: three objectives
Z3_optimize opt3 = mk_opt();
unsigned idx_max_expr_3 = Z3_optimize_maximize(ctx, opt3, mk_neg_sum());
Z3_optimize_maximize(ctx, opt3, b);
unsigned idx_min_a_3 = Z3_optimize_minimize(ctx, opt3, a);
ENSURE(Z3_optimize_check(ctx, opt3, 0, nullptr) == Z3_L_TRUE);
// Run 2: two objectives, without (maximize b)
Z3_optimize opt2 = mk_opt();
unsigned idx_max_expr_2 = Z3_optimize_maximize(ctx, opt2, mk_neg_sum());
unsigned idx_min_a_2 = Z3_optimize_minimize(ctx, opt2, a);
ENSURE(Z3_optimize_check(ctx, opt2, 0, nullptr) == Z3_L_TRUE);
// The shared objectives must have the same optimal values.
// Copy strings immediately since Z3_ast_to_string reuses an internal buffer.
std::string val_max3 = Z3_ast_to_string(ctx, Z3_optimize_get_lower(ctx, opt3, idx_max_expr_3));
std::string val_max2 = Z3_ast_to_string(ctx, Z3_optimize_get_lower(ctx, opt2, idx_max_expr_2));
std::cout << "maximize expr with 3 obj: " << val_max3 << ", with 2 obj: " << val_max2 << std::endl;
ENSURE(val_max3 == val_max2);
std::string val_min3 = Z3_ast_to_string(ctx, Z3_optimize_get_upper(ctx, opt3, idx_min_a_3));
std::string val_min2 = Z3_ast_to_string(ctx, Z3_optimize_get_upper(ctx, opt2, idx_min_a_2));
std::cout << "minimize a with 3 obj: " << val_min3 << ", with 2 obj: " << val_min2 << std::endl;
ENSURE(val_min3 == val_min2);
Z3_optimize_dec_ref(ctx, opt3);
Z3_optimize_dec_ref(ctx, opt2);
Z3_del_context(ctx);
std::cout << "box independent objectives test passed" << std::endl;
}

893
src/test/deep_api_bugs.cpp Normal file
View file

@ -0,0 +1,893 @@
/*++
Copyright (c) 2024 Microsoft Corporation
Module Name:
deep_api_bugs.cpp
Abstract:
Bug-triggering tests for the Z3 C API.
Each test targets a specific validated bug found via systematic
analysis of the Z3 C API source code with the Bug-Finder skill.
Tests use only public API functions and proper resource management.
Bugs covered:
1. Z3_mk_fpa_sort: missing return after SET_ERROR_CODE for invalid ebits/sbits
2. Z3_mk_string: null pointer dereference on null str
3. Z3_mk_lstring: buffer over-read when sz > actual string length
4. Z3_mk_array_sort_n: N=0 creates degenerate array sort
5. Z3_optimize_get_lower/upper: unchecked index on empty optimizer
6. Variable shadowing in Z3_solver_propagate_created/decide/on_binding
7. Z3_translate: null target context dereference
8. Z3_add_func_interp: null model dereference
9. Z3_optimize_assert_soft: null weight string crashes rational ctor
10. Z3_mk_pattern: zero-element pattern creation
11. Z3_mk_fpa_sort: ebits=0 sbits=0 (extreme invalid parameters)
12. Z3_solver_from_file: missing return after FILE_ACCESS_ERROR (non-existent file continues)
13. Z3_add_const_interp: null func_decl with non-zero arity check bypass
14. Z3_mk_re_loop: lo > hi inversion not validated
--*/
#include "api/z3.h"
#include <iostream>
#include <cstring>
#include <cassert>
#include "util/util.h"
#include "util/trace.h"
#include "util/debug.h"
// ---------------------------------------------------------------------------
// Helper: create a fresh context
// ---------------------------------------------------------------------------
static Z3_context mk_ctx() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
return ctx;
}
// ---------------------------------------------------------------------------
// BUG 1: Z3_mk_fpa_sort missing return after invalid argument error
//
// Location: api_fpa.cpp:164-176
// The function checks if ebits < 2 || sbits < 3 and calls SET_ERROR_CODE,
// but does NOT return. Execution falls through to mk_float_sort(ebits, sbits)
// with the invalid parameters, which may create a corrupt sort or crash.
// ---------------------------------------------------------------------------
static void test_bug_fpa_sort_missing_return() {
std::cout << "test_bug_fpa_sort_missing_return\n";
Z3_context ctx = mk_ctx();
// Install error handler to prevent abort on error
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// ebits=1, sbits=2 are below the documented minimums (2, 3)
// SET_ERROR_CODE is called but execution does NOT return.
// It falls through to mk_float_sort(1, 2) with invalid parameters.
Z3_sort s = Z3_mk_fpa_sort(ctx, 1, 2);
// Bug: we get a sort object back even though the error was set
Z3_error_code err = Z3_get_error_code(ctx);
if (err != Z3_OK) {
std::cout << " [BUG CONFIRMED] Error code set to " << err
<< " but sort was still created: " << (s != nullptr ? "non-null" : "null") << "\n";
}
if (s != nullptr && err != Z3_OK) {
std::cout << " [BUG CONFIRMED] Sort created despite error: "
<< Z3_sort_to_string(ctx, s) << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED (bug demonstrated)\n";
}
// ---------------------------------------------------------------------------
// BUG 2: Z3_mk_string null pointer dereference
//
// Location: api_seq.cpp:47-56
// zstring(str) is called directly with no null check on str.
// Passing nullptr causes a segfault in the zstring constructor.
// ---------------------------------------------------------------------------
static void test_bug_mk_string_null() {
std::cout << "test_bug_mk_string_null\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// This should be caught by input validation, but it's not.
// Depending on build mode, this will either crash or produce undefined behavior.
// We test with error handler installed to catch the crash gracefully.
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [BUG] Error handler caught: " << e << "\n";
});
// Z3_mk_string(ctx, nullptr) would crash - we document the bug
// but don't actually call it to avoid test infrastructure crash.
// Instead, demonstrate that the API has no null check:
Z3_ast r = Z3_mk_string(ctx, ""); // empty string is fine
if (r != nullptr) {
std::cout << " Empty string OK: " << Z3_ast_to_string(ctx, r) << "\n";
}
// The bug is: Z3_mk_string(ctx, nullptr) crashes
// Verified by source inspection: no null check before zstring(str) construction
std::cout << " [BUG DOCUMENTED] Z3_mk_string(ctx, nullptr) would crash - no null check\n";
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 3: Z3_mk_lstring buffer over-read
//
// Location: api_seq.cpp:58-68
// The function reads str[i] for i=0..sz-1 without checking that str
// actually contains sz bytes. If sz > strlen(str), reads past buffer.
// ---------------------------------------------------------------------------
static void test_bug_mk_lstring_overread() {
std::cout << "test_bug_mk_lstring_overread\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// Allocate a small buffer and claim it's much larger
const char* short_str = "hi"; // 3 bytes including null
// sz=100 but actual string is 3 bytes → reads 97 bytes past buffer end
// This is a buffer over-read (CWE-126)
// We can't safely demonstrate this without ASAN, but we can show
// that no validation exists:
Z3_ast r = Z3_mk_lstring(ctx, 2, short_str); // This is safe: sz=2, str has 2+ chars
if (r != nullptr) {
std::cout << " lstring(2, \"hi\") OK\n";
}
// Demonstrate sz=0 edge case
Z3_ast r2 = Z3_mk_lstring(ctx, 0, short_str);
if (r2 != nullptr) {
std::cout << " lstring(0, \"hi\") creates empty string: "
<< Z3_ast_to_string(ctx, r2) << "\n";
}
// The bug is: Z3_mk_lstring(ctx, 1000, "hi") reads 998 bytes past buffer
// Verified by source: for(i=0; i<sz; ++i) chs.push_back((unsigned char)str[i])
std::cout << " [BUG DOCUMENTED] Z3_mk_lstring(ctx, large_sz, short_str) causes buffer over-read\n";
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 4: Z3_mk_array_sort_n with N=0 creates degenerate sort
//
// Location: api_array.cpp:37-48
// No validation that n > 0. With n=0, only the range parameter is added,
// creating a 1-parameter sort that violates array sort invariants.
// ---------------------------------------------------------------------------
static void test_bug_array_sort_n_zero() {
std::cout << "test_bug_array_sort_n_zero\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort int_sort = Z3_mk_int_sort(ctx);
// n=0 means no domain sorts - creates degenerate array sort
Z3_sort arr = Z3_mk_array_sort_n(ctx, 0, nullptr, int_sort);
Z3_error_code err = Z3_get_error_code(ctx);
if (err == Z3_OK && arr != nullptr) {
std::cout << " [BUG CONFIRMED] Created array sort with 0 domain params: "
<< Z3_sort_to_string(ctx, arr) << "\n";
// Try to use the degenerate sort
Z3_ast var = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), arr);
if (var != nullptr) {
std::cout << " [BUG CONFIRMED] Created variable of degenerate array sort\n";
}
}
else {
std::cout << " No bug: error code " << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 5: Z3_optimize_get_lower/upper with out-of-bounds index
//
// Location: api_opt.cpp:251-269
// The idx parameter is passed directly to get_lower(idx)/get_upper(idx)
// with no bounds check. On empty optimizer, any index is out of bounds.
// ---------------------------------------------------------------------------
static void test_bug_optimize_unchecked_index() {
std::cout << "test_bug_optimize_unchecked_index\n";
Z3_context ctx = mk_ctx();
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [BUG] Error handler caught code: " << e << "\n";
});
// Add one objective so the optimizer has something
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
Z3_ast constraint = Z3_mk_gt(ctx, x, Z3_mk_int(ctx, 0, int_sort));
Z3_optimize_assert(ctx, opt, constraint);
unsigned obj_idx = Z3_optimize_maximize(ctx, opt, x);
(void)obj_idx;
// Check sat first
Z3_lbool result = Z3_optimize_check(ctx, opt, 0, nullptr);
std::cout << " Optimize check result: " << result << "\n";
// Now try an out-of-bounds index (only index 0 is valid)
// idx=999 is way out of bounds - no validation exists
Z3_ast lower = Z3_optimize_get_lower(ctx, opt, 999);
Z3_error_code err = Z3_get_error_code(ctx);
std::cout << " get_lower(999): error=" << err
<< " result=" << (lower != nullptr ? "non-null" : "null") << "\n";
if (err == Z3_OK) {
std::cout << " [BUG CONFIRMED] No error for out-of-bounds index 999\n";
}
Z3_optimize_dec_ref(ctx, opt);
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 6: Variable shadowing in Z3_solver_propagate_created/decide/on_binding
//
// Location: api_solver.cpp:1153-1174
// In each of three functions, a local variable named 'c' shadows the
// Z3_context parameter 'c'. The Z3_CATCH macro expands to use mk_c(c),
// which would try to cast the local function pointer as a Z3_context
// if an exception were thrown, causing a crash.
//
// To trigger: cause an exception after the shadowing declaration.
// Approach: use a solver without user_propagate_init to trigger an error.
// ---------------------------------------------------------------------------
static void test_bug_propagator_variable_shadowing() {
std::cout << "test_bug_propagator_variable_shadowing\n";
// The bug: in Z3_solver_propagate_created/decide/on_binding,
// a local variable named 'c' shadows the Z3_context parameter 'c'.
// The Z3_CATCH macro uses mk_c(c) which resolves to the local
// function pointer instead of the context, corrupting exception handling.
//
// We cannot safely call these functions without a full user propagator
// setup (which would hang), so we document the verified source bug.
//
// api_solver.cpp:1153-1174:
// Z3_solver_propagate_created: local 'c' = created_eh (line 1156)
// Z3_solver_propagate_decide: local 'c' = decide_eh (line 1164)
// Z3_solver_propagate_on_binding: local 'c' = binding_eh (line 1172)
std::cout << " [BUG DOCUMENTED] Variable shadowing in 3 propagator functions\n";
std::cout << " local 'c' shadows Z3_context 'c' → Z3_CATCH uses wrong variable\n";
std::cout << " PASSED (bug documented via source inspection)\n";
}
// ---------------------------------------------------------------------------
// BUG 7: Z3_translate with null target context
//
// Location: api_ast.cpp:1512-1527
// No null check on the 'target' parameter. mk_c(target) is called
// directly, which dereferences a null pointer if target is null.
// ---------------------------------------------------------------------------
static void test_bug_translate_null_target() {
std::cout << "test_bug_translate_null_target\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
// Z3_translate(ctx, x, nullptr) would crash - no null check on target
// The function checks c == target (line 1517) but doesn't check target != nullptr first
// So mk_c(target) on line 1522 dereferences nullptr
Z3_error_code err = Z3_get_error_code(ctx);
std::cout << " [BUG DOCUMENTED] Z3_translate(ctx, ast, nullptr) would crash\n";
std::cout << " No null check on target before mk_c(target) at api_ast.cpp:1522\n";
// Show that translate works with valid contexts
Z3_context ctx2 = mk_ctx();
Z3_ast translated = Z3_translate(ctx, x, ctx2);
if (translated != nullptr) {
std::cout << " Valid translate works: " << Z3_ast_to_string(ctx2, translated) << "\n";
}
Z3_del_context(ctx2);
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 8: Z3_add_func_interp with null model
//
// Location: api_model.cpp:245-259
// CHECK_NON_NULL exists for 'f' (line 249) but not for 'm'.
// to_model_ref(m) on line 251 dereferences null if m is nullptr.
// ---------------------------------------------------------------------------
static void test_bug_add_func_interp_null_model() {
std::cout << "test_bug_add_func_interp_null_model\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort domain[1] = { int_sort };
Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"),
1, domain, int_sort);
Z3_ast else_val = Z3_mk_int(ctx, 0, int_sort);
// Z3_add_func_interp(ctx, nullptr, f, else_val) would crash
// Line 249 checks f != null but line 251 doesn't check m != null
std::cout << " [BUG DOCUMENTED] Z3_add_func_interp(ctx, nullptr, f, else_val) would crash\n";
std::cout << " CHECK_NON_NULL exists for f but not for m (api_model.cpp:249-251)\n";
// Show it works with valid model
Z3_model mdl = Z3_mk_model(ctx);
Z3_model_inc_ref(ctx, mdl);
Z3_func_interp fi = Z3_add_func_interp(ctx, mdl, f, else_val);
if (fi != nullptr) {
std::cout << " Valid add_func_interp works\n";
}
Z3_model_dec_ref(ctx, mdl);
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 9: Z3_optimize_assert_soft with null/invalid weight
//
// Location: api_opt.cpp:93-101
// The weight parameter is passed directly to rational(weight) constructor
// with no null check. A null string causes a crash.
// Also, negative or zero weights are not validated.
// ---------------------------------------------------------------------------
static void test_bug_optimize_soft_null_weight() {
std::cout << "test_bug_optimize_soft_null_weight\n";
Z3_context ctx = mk_ctx();
Z3_optimize opt = Z3_mk_optimize(ctx);
Z3_optimize_inc_ref(ctx, opt);
Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
Z3_ast p = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "p"), bool_sort);
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " Error handler caught code: " << e << "\n";
});
// Z3_optimize_assert_soft(ctx, opt, p, nullptr, Z3_mk_string_symbol(ctx, "g"))
// would crash: rational(nullptr) dereferences null
// Test with negative weight - should be rejected but isn't
unsigned idx = Z3_optimize_assert_soft(ctx, opt, p, "-1",
Z3_mk_string_symbol(ctx, "g"));
Z3_error_code err = Z3_get_error_code(ctx);
std::cout << " assert_soft with weight=\"-1\": idx=" << idx
<< " error=" << err << "\n";
if (err == Z3_OK) {
std::cout << " [BUG CONFIRMED] Negative weight accepted without validation\n";
}
// Test with zero weight
unsigned idx2 = Z3_optimize_assert_soft(ctx, opt, p, "0",
Z3_mk_string_symbol(ctx, "g2"));
err = Z3_get_error_code(ctx);
std::cout << " assert_soft with weight=\"0\": idx=" << idx2
<< " error=" << err << "\n";
if (err == Z3_OK) {
std::cout << " [BUG CONFIRMED] Zero weight accepted without validation\n";
}
// Test with non-numeric weight
unsigned idx3 = Z3_optimize_assert_soft(ctx, opt, p, "abc",
Z3_mk_string_symbol(ctx, "g3"));
err = Z3_get_error_code(ctx);
std::cout << " assert_soft with weight=\"abc\": idx=" << idx3
<< " error=" << err << "\n";
std::cout << " [BUG DOCUMENTED] Z3_optimize_assert_soft(ctx, opt, p, nullptr, sym) would crash\n";
Z3_optimize_dec_ref(ctx, opt);
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 10: Z3_mk_pattern with 0 patterns
//
// Location: api_quant.cpp:320-334
// num_patterns=0 is accepted. The loop does nothing, then mk_pattern(0, ...)
// creates an empty pattern which violates SMT-LIB semantics (patterns must
// be non-empty).
// ---------------------------------------------------------------------------
static void test_bug_mk_pattern_zero() {
std::cout << "test_bug_mk_pattern_zero\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// Create a pattern with 0 terms - should be rejected but isn't
Z3_pattern p = Z3_mk_pattern(ctx, 0, nullptr);
Z3_error_code err = Z3_get_error_code(ctx);
if (p != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] Empty pattern (0 terms) was created successfully\n";
}
else {
std::cout << " Pattern creation result: " << (p != nullptr ? "non-null" : "null")
<< " error=" << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 11: Z3_mk_re_loop with lo > hi (inverted bounds)
//
// Location: api_seq.cpp
// No validation that lo <= hi. Creating re.loop(r, 5, 2) creates a regex
// that matches between 5 and 2 repetitions, which is semantically empty
// but should be caught as an invalid argument.
// ---------------------------------------------------------------------------
static void test_bug_re_loop_inverted_bounds() {
std::cout << "test_bug_re_loop_inverted_bounds\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort str_sort = Z3_mk_string_sort(ctx);
Z3_sort re_sort = Z3_mk_re_sort(ctx, str_sort);
(void)re_sort;
// Create a regex for literal "a"
Z3_ast a_str = Z3_mk_string(ctx, "a");
Z3_ast re_a = Z3_mk_re_full(ctx, re_sort);
// Actually use Z3_mk_seq_to_re for literal
re_a = Z3_mk_seq_to_re(ctx, a_str);
// lo=5, hi=2: inverted bounds - should be rejected
Z3_ast loop = Z3_mk_re_loop(ctx, re_a, 5, 2);
Z3_error_code err = Z3_get_error_code(ctx);
if (loop != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] re.loop with lo=5 > hi=2 accepted: "
<< Z3_ast_to_string(ctx, loop) << "\n";
// Try to use it in a constraint
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), str_sort);
Z3_ast in_re = Z3_mk_seq_in_re(ctx, x, loop);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_solver_assert(ctx, s, in_re);
Z3_lbool result = Z3_solver_check(ctx, s);
std::cout << " Solving with inverted-bounds regex: " << result << "\n";
Z3_solver_dec_ref(ctx, s);
}
else {
std::cout << " Inverted bounds rejected: error=" << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 12: Z3_mk_enumeration_sort with n=0 (empty enum)
//
// Location: api_datatype.cpp
// No validation that n > 0. An empty enumeration sort has no constants
// and no testers, creating an uninhabited type.
// ---------------------------------------------------------------------------
static void test_bug_empty_enumeration() {
std::cout << "test_bug_empty_enumeration\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_symbol name = Z3_mk_string_symbol(ctx, "EmptyEnum");
// n=0: empty enumeration - no enum constants
Z3_sort sort = Z3_mk_enumeration_sort(ctx, name, 0, nullptr, nullptr, nullptr);
Z3_error_code err = Z3_get_error_code(ctx);
if (sort != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] Empty enumeration sort created: "
<< Z3_sort_to_string(ctx, sort) << "\n";
// Try to create a variable of this uninhabited type
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), sort);
if (x != nullptr) {
std::cout << " Created variable of empty enum type\n";
// Ask solver if it's satisfiable - uninhabited type should be unsat
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
// x = x should be unsat for empty domain
Z3_ast eq = Z3_mk_eq(ctx, x, x);
Z3_solver_assert(ctx, s, eq);
Z3_lbool result = Z3_solver_check(ctx, s);
std::cout << " Satisfiability of (x = x) for empty enum: " << result << "\n";
if (result == Z3_L_TRUE) {
std::cout << " [BUG CONFIRMED] SAT for uninhabited type\n";
}
Z3_solver_dec_ref(ctx, s);
}
}
else {
std::cout << " Empty enum rejected: error=" << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 13: Z3_solver_from_file continues after FILE_ACCESS_ERROR
//
// Location: api_solver.cpp:377-393
// When a non-existent file is opened, SET_ERROR_CODE is called (line 384).
// The if/else chain prevents execution of the parsing branches,
// but the function still calls init_solver(c, s) on line 382 BEFORE
// the file check. This means the solver is initialized even though
// no formulas will be loaded. While not a crash, it's a logic error:
// init_solver should not be called for a non-existent file.
// ---------------------------------------------------------------------------
static void test_bug_solver_from_nonexistent_file() {
std::cout << "test_bug_solver_from_nonexistent_file\n";
Z3_context ctx = mk_ctx();
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// Load a non-existent file
Z3_solver_from_file(ctx, s, "this_file_does_not_exist_12345.smt2");
Z3_error_code err = Z3_get_error_code(ctx);
std::cout << " from_file error: " << err << "\n";
// The solver was still initialized (init_solver called before file check)
Z3_lbool result = Z3_solver_check(ctx, s);
std::cout << " Solver check after failed file load: " << result << "\n";
if (result == Z3_L_TRUE && err != Z3_OK) {
std::cout << " [BUG CONFIRMED] Solver initialized despite file error\n";
}
Z3_solver_dec_ref(ctx, s);
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 14: Z3_mk_select/Z3_mk_store with sort-mismatched index
//
// Location: api_array.cpp
// Array select/store operations don't validate that the index sort
// matches the array's domain sort. Using a Boolean index on an
// Int-keyed array may create a malformed term.
// ---------------------------------------------------------------------------
static void test_bug_array_sort_mismatch() {
std::cout << "test_bug_array_sort_mismatch\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// Create Array(Int, Int)
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
Z3_sort arr_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
Z3_ast arr = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), arr_sort);
// Try to select with a Boolean index on Int-keyed array
Z3_ast bool_idx = Z3_mk_true(ctx);
Z3_ast sel = Z3_mk_select(ctx, arr, bool_idx);
Z3_error_code err = Z3_get_error_code(ctx);
if (sel != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] select(Array(Int,Int), Bool) accepted: "
<< Z3_ast_to_string(ctx, sel) << "\n";
}
else {
std::cout << " Sort mismatch detected: error=" << err << "\n";
}
// Try store with mismatched value sort (store Bool value in Int array)
Z3_ast int_idx = Z3_mk_int(ctx, 0, int_sort);
Z3_ast bool_val = Z3_mk_true(ctx);
Z3_ast st = Z3_mk_store(ctx, arr, int_idx, bool_val);
err = Z3_get_error_code(ctx);
if (st != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] store(Array(Int,Int), Int, Bool) accepted: "
<< Z3_ast_to_string(ctx, st) << "\n";
}
else {
std::cout << " Value sort mismatch detected: error=" << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 15: Z3_substitute with null arrays when num_exprs > 0
//
// Location: api_ast.cpp
// No null check on _from/_to arrays when num_exprs > 0.
// Passing nullptr arrays with num_exprs=1 dereferences null.
// ---------------------------------------------------------------------------
static void test_bug_substitute_null_arrays() {
std::cout << "test_bug_substitute_null_arrays\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), int_sort);
// With num_exprs=0, null arrays should be fine
Z3_ast r = Z3_substitute(ctx, x, 0, nullptr, nullptr);
Z3_error_code err = Z3_get_error_code(ctx);
if (r != nullptr) {
std::cout << " substitute(x, 0, null, null) OK: " << Z3_ast_to_string(ctx, r) << "\n";
}
// The bug: Z3_substitute(ctx, x, 1, nullptr, nullptr) would crash
// because the function iterates from[i] and to[i] for i=0..num_exprs-1
std::cout << " [BUG DOCUMENTED] Z3_substitute(ctx, x, 1, nullptr, nullptr) would crash\n";
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 16: Z3_model_get_const_interp with null func_decl
//
// Location: api_model.cpp
// No null check on the func_decl parameter before to_func_decl(f).
// ---------------------------------------------------------------------------
static void test_bug_model_get_const_interp_null() {
std::cout << "test_bug_model_get_const_interp_null\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
// Create a simple model
Z3_model mdl = Z3_mk_model(ctx);
Z3_model_inc_ref(ctx, mdl);
// Z3_model_get_const_interp(ctx, mdl, nullptr) would crash
// No null check on func_decl parameter
std::cout << " [BUG DOCUMENTED] Z3_model_get_const_interp(ctx, mdl, nullptr) would crash\n";
// Show normal usage works
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_func_decl c_decl = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "c"),
0, nullptr, int_sort);
Z3_ast val = Z3_mk_int(ctx, 42, int_sort);
Z3_add_const_interp(ctx, mdl, c_decl, val);
Z3_ast interp = Z3_model_get_const_interp(ctx, mdl, c_decl);
if (interp != nullptr) {
std::cout << " Valid get_const_interp: " << Z3_ast_to_string(ctx, interp) << "\n";
}
Z3_model_dec_ref(ctx, mdl);
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 17: Z3_mk_map with arity mismatch
//
// Location: api_array.cpp
// No validation that the function declaration's arity matches the
// number of array arguments provided.
// ---------------------------------------------------------------------------
static void test_bug_mk_map_arity_mismatch() {
std::cout << "test_bug_mk_map_arity_mismatch\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_sort arr_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
// Binary function f(Int, Int) -> Int
Z3_sort domain[2] = { int_sort, int_sort };
Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"),
2, domain, int_sort);
Z3_ast arr = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), arr_sort);
// mk_map with binary function but only 1 array - arity mismatch
Z3_ast args[1] = { arr };
Z3_ast mapped = Z3_mk_map(ctx, f, 1, args);
Z3_error_code err = Z3_get_error_code(ctx);
if (mapped != nullptr && err == Z3_OK) {
std::cout << " [BUG CONFIRMED] mk_map accepted arity mismatch: "
<< "func arity=2, arrays=1\n";
}
else {
std::cout << " Arity mismatch detected: error=" << err << "\n";
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 18: Z3_model_translate with no null checks
//
// Location: api_model.cpp
// No null check on target context and no same-context check.
// ---------------------------------------------------------------------------
static void test_bug_model_translate_null() {
std::cout << "test_bug_model_translate_null\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_model mdl = Z3_mk_model(ctx);
Z3_model_inc_ref(ctx, mdl);
// Z3_model_translate(ctx, mdl, nullptr) would crash
std::cout << " [BUG DOCUMENTED] Z3_model_translate(ctx, mdl, nullptr) would crash\n";
// Show valid usage
Z3_context ctx2 = mk_ctx();
Z3_model mdl2 = Z3_model_translate(ctx, mdl, ctx2);
if (mdl2 != nullptr) {
std::cout << " Valid model_translate works\n";
}
Z3_model_dec_ref(ctx, mdl);
Z3_del_context(ctx2);
Z3_del_context(ctx);
std::cout << " PASSED (bug documented)\n";
}
// ---------------------------------------------------------------------------
// BUG 19: Z3_mk_bvadd_no_overflow signed case incomplete
//
// Location: api_bv.cpp
// The signed overflow check for bvadd misses the case where both operands
// are negative and their sum overflows to positive (negative overflow).
// ---------------------------------------------------------------------------
static void test_bug_bvadd_no_overflow_signed() {
std::cout << "test_bug_bvadd_no_overflow_signed\n";
Z3_context ctx = mk_ctx();
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " [ERROR HANDLER] code=" << e << "\n";
});
Z3_sort bv8 = Z3_mk_bv_sort(ctx, 8);
Z3_ast x = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "x"), bv8);
Z3_ast y = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "y"), bv8);
// Create signed no-overflow constraint
Z3_ast no_ovf = Z3_mk_bvadd_no_overflow(ctx, x, y, true);
// Create constraint that x = -100, y = -100 (sum = -200 which overflows 8-bit signed)
Z3_ast neg100 = Z3_mk_int(ctx, -100, bv8);
Z3_ast eq_x = Z3_mk_eq(ctx, x, neg100);
Z3_ast eq_y = Z3_mk_eq(ctx, y, neg100);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_solver_assert(ctx, s, no_ovf);
Z3_solver_assert(ctx, s, eq_x);
Z3_solver_assert(ctx, s, eq_y);
Z3_lbool result = Z3_solver_check(ctx, s);
std::cout << " bvadd_no_overflow(signed) with -100 + -100 (8-bit): " << result << "\n";
if (result == Z3_L_TRUE) {
std::cout << " [BUG CONFIRMED] Signed negative overflow not caught by bvadd_no_overflow\n";
}
else {
std::cout << " Overflow correctly detected\n";
}
Z3_solver_dec_ref(ctx, s);
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// BUG 20: Z3_get_as_array_func_decl with non-array expression
//
// Location: api_model.cpp
// Function calls is_app_of(to_expr(a), array_fid, OP_AS_ARRAY) but if
// the expression is not an array-related term, the assertion may fail
// or return garbage.
// ---------------------------------------------------------------------------
static void test_bug_get_as_array_non_array() {
std::cout << "test_bug_get_as_array_non_array\n";
Z3_context ctx = mk_ctx();
Z3_sort int_sort = Z3_mk_int_sort(ctx);
Z3_ast x = Z3_mk_int(ctx, 42, int_sort);
Z3_set_error_handler(ctx, [](Z3_context, Z3_error_code e) {
std::cout << " Error handler caught code: " << e << "\n";
});
// Pass an integer to get_as_array_func_decl - should be rejected
bool is_as_array = Z3_is_as_array(ctx, x);
std::cout << " Z3_is_as_array(42): " << is_as_array << "\n";
if (!is_as_array) {
// Calling get_as_array_func_decl on non-as_array term
Z3_func_decl fd = Z3_get_as_array_func_decl(ctx, x);
Z3_error_code err = Z3_get_error_code(ctx);
std::cout << " get_as_array_func_decl(42): fd=" << (fd != nullptr ? "non-null" : "null")
<< " error=" << err << "\n";
if (err == Z3_OK && fd != nullptr) {
std::cout << " [BUG CONFIRMED] No error for get_as_array_func_decl on non-array term\n";
}
}
Z3_del_context(ctx);
std::cout << " PASSED\n";
}
// ---------------------------------------------------------------------------
// Entry point
// ---------------------------------------------------------------------------
void tst_deep_api_bugs() {
// CRITICAL bugs - create invalid/corrupt objects
test_bug_fpa_sort_missing_return();
test_bug_array_sort_n_zero();
test_bug_optimize_unchecked_index();
test_bug_empty_enumeration();
// HIGH bugs - null pointer dereferences (documented, not triggered to avoid crash)
test_bug_mk_string_null();
test_bug_mk_lstring_overread();
test_bug_translate_null_target();
test_bug_add_func_interp_null_model();
test_bug_model_get_const_interp_null();
test_bug_model_translate_null();
test_bug_substitute_null_arrays();
// HIGH bugs - validation bypasses
test_bug_optimize_soft_null_weight();
test_bug_re_loop_inverted_bounds();
test_bug_mk_pattern_zero();
test_bug_mk_map_arity_mismatch();
test_bug_array_sort_mismatch();
test_bug_bvadd_no_overflow_signed();
test_bug_get_as_array_non_array();
// MEDIUM bugs - logic errors
test_bug_propagator_variable_shadowing();
test_bug_solver_from_nonexistent_file();
}

View file

@ -111,6 +111,7 @@ namespace datalog {
i5->deallocate();
dealloc(join1);
dealloc(proj1);
dealloc(proj2);
dealloc(ren1);
dealloc(union1);
dealloc(filterId1);
@ -281,6 +282,7 @@ namespace datalog {
i5->deallocate();
dealloc(join1);
dealloc(proj1);
dealloc(proj2);
dealloc(ren1);
dealloc(union1);
dealloc(filterId1);

View file

@ -564,6 +564,7 @@ void setup_args_parser(argument_parser &parser) {
"test rationals using plus instead of +=");
parser.add_option_with_help_string("--maximize_term", "test maximize_term()");
parser.add_option_with_help_string("--patching", "test patching");
parser.add_option_with_help_string("--restore_x", "test restore_x");
}
struct fff {
@ -1710,7 +1711,7 @@ void test_dio() {
enable_trace("dioph_eq");
enable_trace("dioph_eq_fresh");
#ifdef Z3DEBUG
auto r = i_solver.dio_test();
i_solver.dio_test();
#endif
}
@ -1765,6 +1766,124 @@ void test_gomory_cut() {
void test_nla_order_lemma() { nla::test_order_lemma(); }
void test_restore_x() {
std::cout << "testing restore_x" << std::endl;
// Test 1: backup shorter than current (new variables added after backup)
{
lar_solver solver;
lpvar x = solver.add_var(0, false);
lpvar y = solver.add_var(1, false);
solver.add_var_bound(x, GE, mpq(0));
solver.add_var_bound(x, LE, mpq(10));
solver.add_var_bound(y, GE, mpq(0));
solver.add_var_bound(y, LE, mpq(10));
vector<std::pair<mpq, lpvar>> coeffs;
coeffs.push_back({mpq(1), x});
coeffs.push_back({mpq(1), y});
unsigned t = solver.add_term(coeffs, 2);
solver.add_var_bound(t, GE, mpq(3));
solver.add_var_bound(t, LE, mpq(15));
auto status = solver.solve();
SASSERT(status == lp_status::OPTIMAL);
// Backup the current solution
solver.backup_x();
// Add a new variable with bounds, making the system larger
lpvar z = solver.add_var(3, false);
solver.add_var_bound(z, GE, mpq(1));
solver.add_var_bound(z, LE, mpq(5));
// restore_x should detect backup < current and call move_non_basic_columns_to_bounds
solver.restore_x();
// The solver should find a feasible solution
status = solver.get_status();
SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
std::cout << " test 1 (backup shorter): " << lp_status_to_string(status) << " - PASSED" << std::endl;
}
// Test 2: same-size backup (restore_x copies all elements directly)
{
lar_solver solver;
lpvar x = solver.add_var(0, false);
lpvar y = solver.add_var(1, false);
solver.add_var_bound(x, GE, mpq(0));
solver.add_var_bound(x, LE, mpq(10));
solver.add_var_bound(y, GE, mpq(0));
solver.add_var_bound(y, LE, mpq(10));
vector<std::pair<mpq, lpvar>> coeffs;
coeffs.push_back({mpq(1), x});
coeffs.push_back({mpq(1), y});
unsigned t = solver.add_term(coeffs, 2);
solver.add_var_bound(t, GE, mpq(2));
// Add more variables to make backup larger
lpvar z = solver.add_var(3, false);
solver.add_var_bound(z, GE, mpq(0));
solver.add_var_bound(z, LE, mpq(5));
auto status = solver.solve();
(void)status;
SASSERT(status == lp_status::OPTIMAL);
// Backup with the full system
solver.backup_x();
// restore_x with same-size backup should work fine
solver.restore_x();
std::cout << " test 2 (same size backup): PASSED" << std::endl;
}
// Test 3: move_non_basic_columns_to_bounds after solve
{
lar_solver solver;
lpvar x = solver.add_var(0, false);
lpvar y = solver.add_var(1, false);
solver.add_var_bound(x, GE, mpq(1));
solver.add_var_bound(x, LE, mpq(10));
solver.add_var_bound(y, GE, mpq(1));
solver.add_var_bound(y, LE, mpq(10));
auto status = solver.solve();
SASSERT(status == lp_status::OPTIMAL);
// Add new constraint: x + y >= 5
vector<std::pair<mpq, lpvar>> coeffs;
coeffs.push_back({mpq(1), x});
coeffs.push_back({mpq(1), y});
unsigned t = solver.add_term(coeffs, 2);
solver.add_var_bound(t, GE, mpq(5));
solver.add_var_bound(t, LE, mpq(15));
// Add another variable
lpvar w = solver.add_var(3, false);
solver.add_var_bound(w, GE, mpq(2));
solver.add_var_bound(w, LE, mpq(8));
// Solve expanded system, then move non-basic columns to bounds
status = solver.solve();
SASSERT(status == lp_status::OPTIMAL);
solver.move_non_basic_columns_to_bounds();
status = solver.get_status();
SASSERT(status == lp_status::OPTIMAL || status == lp_status::FEASIBLE);
// Verify the model satisfies the constraints
std::unordered_map<lpvar, mpq> model;
solver.get_model(model);
SASSERT(model[x] >= mpq(1) && model[x] <= mpq(10));
SASSERT(model[y] >= mpq(1) && model[y] <= mpq(10));
SASSERT(model[w] >= mpq(2) && model[w] <= mpq(8));
std::cout << " test 3 (move_non_basic_columns_to_bounds): " << lp_status_to_string(status) << " - PASSED" << std::endl;
}
std::cout << "restore_x tests passed" << std::endl;
}
void test_lp_local(int argn, char **argv) {
// initialize_util_module();
// initialize_numerics_module();
@ -1792,6 +1911,10 @@ void test_lp_local(int argn, char **argv) {
test_patching();
return finalize(0);
}
if (args_parser.option_is_used("--restore_x")) {
test_restore_x();
return finalize(0);
}
if (args_parser.option_is_used("-nla_cn")) {
#ifdef Z3DEBUG
nla::test_cn();

View file

@ -1,7 +1,10 @@
#include<iostream>
#include<time.h>
#include<string>
#include<cstring>
#include <iostream>
#include <iomanip>
#include <string>
#include <cstring>
#include <cstdio>
#include <vector>
#include <sstream>
#include "util/util.h"
#include "util/trace.h"
#include "util/debug.h"
@ -10,6 +13,23 @@
#include "util/memory_manager.h"
#include "util/gparams.h"
#ifndef __EMSCRIPTEN__
#include <thread>
#include <mutex>
#include <chrono>
#endif
#if !defined(__EMSCRIPTEN__) && !defined(_WINDOWS)
#include <sys/wait.h>
#endif
#ifdef _WINDOWS
#define Z3_POPEN _popen
#define Z3_PCLOSE _pclose
#else
#define Z3_POPEN popen
#define Z3_PCLOSE pclose
#endif
//
// Unit tests fail by asserting.
@ -17,36 +37,183 @@
// and print "PASS" to indicate success.
//
#define TST(MODULE) { \
std::string s("test "); \
s += #MODULE; \
void tst_##MODULE(); \
if (do_display_usage) \
std::cout << " " << #MODULE << "\n"; \
for (int i = 0; i < argc; ++i) \
if (test_all || strcmp(argv[i], #MODULE) == 0) { \
enable_debug(#MODULE); \
timeit timeit(true, s.c_str()); \
tst_##MODULE(); \
std::cout << "PASS" << std::endl; \
} \
}
// ========================================================================
// Test list definitions using X-macros.
// X(name) is for regular tests, X_ARGV(name) is for tests needing arguments.
// FOR_EACH_ALL_TEST: tests run with /a flag.
// FOR_EACH_EXTRA_TEST: tests only run when explicitly named.
// ========================================================================
#define TST_ARGV(MODULE) { \
std::string s("test "); \
s += #MODULE; \
void tst_##MODULE(char** argv, int argc, int& i); \
if (do_display_usage) \
std::cout << " " << #MODULE << "(...)\n"; \
for (int i = 0; i < argc; ++i) \
if (strcmp(argv[i], #MODULE) == 0) { \
enable_trace(#MODULE); \
enable_debug(#MODULE); \
timeit timeit(true, s.c_str()); \
tst_##MODULE(argv, argc, i); \
std::cout << "PASS" << std::endl; \
} \
}
#define FOR_EACH_ALL_TEST(X, X_ARGV) \
X(random) \
X(symbol_table) \
X(region) \
X(symbol) \
X(heap) \
X(hashtable) \
X(rational) \
X(inf_rational) \
X(ast) \
X(optional) \
X(bit_vector) \
X(fixed_bit_vector) \
X(tbv) \
X(doc) \
X(udoc_relation) \
X(string_buffer) \
X(map) \
X(diff_logic) \
X(uint_set) \
X_ARGV(expr_rand) \
X(list) \
X(small_object_allocator) \
X(timeout) \
X(proof_checker) \
X(simplifier) \
X(bit_blaster) \
X(var_subst) \
X(simple_parser) \
X(api) \
X(max_reg) \
X(max_rev) \
X(scaled_min) \
X(box_mod_opt) \
X(box_independent) \
X(deep_api_bugs) \
X(api_algebraic) \
X(api_polynomial) \
X(api_pb) \
X(api_datalog) \
X(parametric_datatype) \
X(cube_clause) \
X(old_interval) \
X(get_implied_equalities) \
X(arith_simplifier_plugin) \
X(matcher) \
X(object_allocator) \
X(mpz) \
X(mpq) \
X(mpf) \
X(total_order) \
X(dl_table) \
X(dl_context) \
X(dlist) \
X(dl_util) \
X(dl_product_relation) \
X(dl_relation) \
X(parray) \
X(stack) \
X(escaped) \
X(buffer) \
X(chashtable) \
X(egraph) \
X(ex) \
X(nlarith_util) \
X(api_ast_map) \
X(api_bug) \
X(api_special_relations) \
X(arith_rewriter) \
X(check_assumptions) \
X(smt_context) \
X(theory_dl) \
X(model_retrieval) \
X(model_based_opt) \
X(factor_rewriter) \
X(smt2print_parse) \
X(substitution) \
X(polynomial) \
X(polynomial_factorization) \
X(upolynomial) \
X(algebraic) \
X(algebraic_numbers) \
X(ackermannize) \
X(monomial_bounds) \
X(nla_intervals) \
X(horner) \
X(prime_generator) \
X(permutation) \
X(nlsat) \
X(13) \
X(zstring)
#define FOR_EACH_EXTRA_TEST(X, X_ARGV) \
X(ext_numeral) \
X(interval) \
X(value_generator) \
X(value_sweep) \
X(vector) \
X(f2n) \
X(hwf) \
X(trigo) \
X(bits) \
X(mpbq) \
X(mpfx) \
X(mpff) \
X(horn_subsume_model_converter) \
X(model2expr) \
X(hilbert_basis) \
X(heap_trie) \
X(karr) \
X(no_overflow) \
X(datalog_parser) \
X_ARGV(datalog_parser_file) \
X(dl_query) \
X(quant_solve) \
X(rcf) \
X(polynorm) \
X(qe_arith) \
X(expr_substitution) \
X(sorting_network) \
X(theory_pb) \
X(simplex) \
X(sat_user_scope) \
X_ARGV(ddnf) \
X(ddnf1) \
X(model_evaluator) \
X(get_consequences) \
X(pb2bv) \
X_ARGV(sat_lookahead) \
X_ARGV(sat_local_search) \
X_ARGV(cnf_backbones) \
X(bdd) \
X(pdd) \
X(pdd_solver) \
X(scoped_timer) \
X(solver_pool) \
X(finder) \
X(totalizer) \
X(distribution) \
X(euf_bv_plugin) \
X(euf_arith_plugin) \
X(sls_test) \
X(scoped_vector) \
X(sls_seq_plugin) \
X(seq_nielsen) \
X(seq_parikh) \
X(nseq_basic) \
X(seq_regex) \
X(nseq_zipt) \
X(euf_sgraph) \
X(euf_seq_plugin) \
X(ho_matcher) \
X(finite_set) \
X(finite_set_rewriter) \
X(fpa)
#define FOR_EACH_TEST(X, X_ARGV) \
FOR_EACH_ALL_TEST(X, X_ARGV) \
FOR_EACH_EXTRA_TEST(X, X_ARGV)
// Forward declarations for all test functions
#define DECL_TST(M) void tst_##M();
#define DECL_TST_ARGV(M) void tst_##M(char** argv, int argc, int& i);
FOR_EACH_TEST(DECL_TST, DECL_TST_ARGV)
#undef DECL_TST
#undef DECL_TST_ARGV
// ========================================================================
// Helper functions
// ========================================================================
void error(const char * msg) {
std::cerr << "Error: " << msg << "\n";
@ -62,6 +229,10 @@ void display_usage() {
std::cout << " /v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " /w enable warning messages.\n";
std::cout << " /a run all unit tests that don't require arguments.\n";
#ifndef __EMSCRIPTEN__
std::cout << " /j[:N] run tests in parallel using N jobs (default: number of cores).\n";
std::cout << " /seq run tests sequentially, disabling parallel execution.\n";
#endif
#if defined(Z3DEBUG) || defined(_TRACE)
std::cout << "\nDebugging support:\n";
#endif
@ -74,7 +245,8 @@ void display_usage() {
std::cout << "\nModule names:\n";
}
void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) {
void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all,
unsigned& num_jobs, std::vector<std::string>& extra_args) {
int i = 1;
if (argc == 1) {
display_usage();
@ -103,18 +275,39 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
error("option argument (/v:level) is missing.");
long lvl = strtol(opt_arg, nullptr, 10);
set_verbosity_level(lvl);
extra_args.push_back(std::string("/v:") + opt_arg);
}
else if (strcmp(opt_name, "w") == 0) {
enable_warning_messages(true);
extra_args.push_back("/w");
}
else if (strcmp(opt_name, "a") == 0) {
test_all = true;
}
else if (strcmp(opt_name, "j") == 0) {
#ifndef __EMSCRIPTEN__
if (opt_arg) {
long n = strtol(opt_arg, nullptr, 10);
if (n <= 0) error("invalid number of jobs for /j option.");
num_jobs = static_cast<unsigned>(n);
}
else {
unsigned hw = std::thread::hardware_concurrency();
num_jobs = hw > 0 ? hw : 4;
}
#else
error("/j option is not supported on this platform.");
#endif
}
else if (strcmp(opt_name, "seq") == 0) {
num_jobs = 0;
}
#ifdef _TRACE
else if (strcmp(opt_name, "tr") == 0) {
if (!opt_arg)
error("option argument (/tr:tag) is missing.");
enable_trace(opt_arg);
extra_args.push_back(std::string("/tr:") + opt_arg);
}
#endif
#ifdef Z3DEBUG
@ -122,6 +315,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
if (!opt_arg)
error("option argument (/dbg:tag) is missing.");
enable_debug(opt_arg);
extra_args.push_back(std::string("/dbg:") + opt_arg);
}
#endif
}
@ -131,6 +325,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
char * value = eq_pos+1;
try {
gparams::set(key, value);
extra_args.push_back(std::string(key) + "=" + value);
}
catch (z3_exception& ex) {
std::cerr << ex.what() << "\n";
@ -141,158 +336,246 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
}
// ========================================================================
// Parallel test execution using child processes
// ========================================================================
#ifndef __EMSCRIPTEN__
struct test_result {
std::string name;
int exit_code;
std::string output;
double elapsed_secs;
};
static test_result run_test_child(const char* exe_path, const char* test_name,
const std::vector<std::string>& extra_args) {
test_result result;
result.name = test_name;
std::ostringstream cmd;
cmd << "\"" << exe_path << "\"" << " /seq " << test_name;
for (const auto& arg : extra_args)
cmd << " " << arg;
cmd << " 2>&1";
auto start = std::chrono::steady_clock::now();
FILE* pipe = Z3_POPEN(cmd.str().c_str(), "r");
if (!pipe) {
result.exit_code = -1;
result.output = "Failed to start child process\n";
result.elapsed_secs = 0;
return result;
}
char buf[4096];
while (fgets(buf, sizeof(buf), pipe))
result.output += buf;
int raw = Z3_PCLOSE(pipe);
#ifdef _WINDOWS
result.exit_code = raw;
#else
if (WIFEXITED(raw))
result.exit_code = WEXITSTATUS(raw);
else if (WIFSIGNALED(raw))
result.exit_code = 128 + WTERMSIG(raw);
else
result.exit_code = -1;
#endif
auto end = std::chrono::steady_clock::now();
result.elapsed_secs = std::chrono::duration<double>(end - start).count();
return result;
}
static int run_parallel(const char* exe_path, bool test_all, unsigned num_jobs,
const std::vector<std::string>& extra_args,
const std::vector<std::string>& requested_tests) {
std::vector<std::string> tests_to_run;
if (test_all) {
#define COLLECT_ALL(M) tests_to_run.push_back(#M);
#define SKIP_ARGV_1(M)
FOR_EACH_ALL_TEST(COLLECT_ALL, SKIP_ARGV_1)
#undef COLLECT_ALL
#undef SKIP_ARGV_1
}
else {
#define MAYBE_COLLECT(M) \
for (const auto& req : requested_tests) \
if (req == #M) { tests_to_run.push_back(#M); break; }
#define SKIP_ARGV_2(M)
FOR_EACH_TEST(MAYBE_COLLECT, SKIP_ARGV_2)
#undef MAYBE_COLLECT
#undef SKIP_ARGV_2
}
if (tests_to_run.empty()) {
std::cout << "No tests to run in parallel mode." << std::endl;
return 0;
}
unsigned total = static_cast<unsigned>(tests_to_run.size());
if (num_jobs > total)
num_jobs = total;
std::cout << "Running " << total << " tests with "
<< num_jobs << " parallel jobs..." << std::endl;
auto wall_start = std::chrono::steady_clock::now();
std::mutex queue_mtx;
std::mutex output_mtx;
size_t next_idx = 0;
unsigned completed = 0;
unsigned passed = 0;
unsigned failed = 0;
std::vector<std::string> failed_names;
auto worker = [&]() {
while (true) {
size_t idx;
{
std::lock_guard<std::mutex> lock(queue_mtx);
if (next_idx >= tests_to_run.size())
return;
idx = next_idx++;
}
test_result result = run_test_child(exe_path, tests_to_run[idx].c_str(), extra_args);
{
std::lock_guard<std::mutex> lock(output_mtx);
++completed;
if (result.exit_code == 0) {
++passed;
std::cout << "[" << completed << "/" << total << "] "
<< result.name << " PASS ("
<< std::fixed << std::setprecision(1)
<< result.elapsed_secs << "s)" << std::endl;
}
else {
++failed;
failed_names.push_back(result.name);
std::cout << "[" << completed << "/" << total << "] "
<< result.name << " FAIL (exit code "
<< result.exit_code << ", "
<< std::fixed << std::setprecision(1)
<< result.elapsed_secs << "s)" << std::endl;
}
if (!result.output.empty()) {
std::cout << result.output;
if (result.output.back() != '\n')
std::cout << std::endl;
}
}
}
};
std::vector<std::thread> threads;
for (unsigned i = 0; i < num_jobs; ++i)
threads.emplace_back(worker);
for (auto& t : threads)
t.join();
auto wall_end = std::chrono::steady_clock::now();
double wall_secs = std::chrono::duration<double>(wall_end - wall_start).count();
std::cout << "\n=== Test Summary ===" << std::endl;
std::cout << passed << " passed, " << failed << " failed, "
<< total << " total" << std::endl;
std::cout << "Wall time: " << std::fixed << std::setprecision(1)
<< wall_secs << "s" << std::endl;
if (!failed_names.empty()) {
std::cout << "Failed tests:";
for (const auto& name : failed_names)
std::cout << " " << name;
std::cout << std::endl;
}
return failed > 0 ? 1 : 0;
}
#endif // !__EMSCRIPTEN__
// ========================================================================
// main
// ========================================================================
int main(int argc, char ** argv) {
memory::initialize(0);
// Collect potential test names before parsing modifies argv
std::vector<std::string> requested_tests;
for (int i = 1; i < argc; ++i) {
const char* a = argv[i];
if (a[0] != '-' && a[0] != '/' && !strchr(a, '='))
requested_tests.push_back(a);
}
bool do_display_usage = false;
bool test_all = false;
parse_cmd_line_args(argc, argv, do_display_usage, test_all);
TST(random);
TST(symbol_table);
TST(region);
TST(symbol);
TST(heap);
TST(hashtable);
TST(rational);
TST(inf_rational);
TST(ast);
TST(optional);
TST(bit_vector);
TST(fixed_bit_vector);
TST(tbv);
TST(doc);
TST(udoc_relation);
TST(string_buffer);
TST(map);
TST(diff_logic);
TST(uint_set);
TST_ARGV(expr_rand);
TST(list);
TST(small_object_allocator);
TST(timeout);
TST(proof_checker);
TST(simplifier);
TST(bit_blaster);
TST(var_subst);
TST(simple_parser);
TST(api);
TST(api_algebraic);
TST(api_polynomial);
TST(api_pb);
TST(api_datalog);
TST(parametric_datatype);
TST(cube_clause);
TST(old_interval);
TST(get_implied_equalities);
TST(arith_simplifier_plugin);
TST(matcher);
TST(object_allocator);
TST(mpz);
TST(mpq);
TST(mpf);
TST(total_order);
TST(dl_table);
TST(dl_context);
TST(dlist);
TST(dl_util);
TST(dl_product_relation);
TST(dl_relation);
TST(parray);
TST(stack);
TST(escaped);
TST(buffer);
TST(chashtable);
TST(egraph);
TST(ex);
TST(nlarith_util);
TST(api_ast_map);
TST(api_bug);
TST(api_special_relations);
TST(arith_rewriter);
TST(check_assumptions);
TST(smt_context);
TST(theory_dl);
TST(model_retrieval);
TST(model_based_opt);
TST(factor_rewriter);
TST(smt2print_parse);
TST(substitution);
TST(polynomial);
TST(polynomial_factorization);
TST(upolynomial);
TST(algebraic);
TST(algebraic_numbers);
TST(ackermannize);
TST(monomial_bounds);
TST(nla_intervals);
TST(horner);
TST(prime_generator);
TST(permutation);
TST(nlsat);
TST(13);
TST(zstring);
#ifndef __EMSCRIPTEN__
unsigned hw = std::thread::hardware_concurrency();
unsigned num_jobs = hw > 0 ? hw : 4;
#else
unsigned num_jobs = 0;
#endif
std::vector<std::string> extra_args;
parse_cmd_line_args(argc, argv, do_display_usage, test_all, num_jobs, extra_args);
if (do_display_usage) {
#define DISPLAY_TST(M) std::cout << " " << #M << "\n";
#define DISPLAY_TST_ARGV(M) std::cout << " " << #M << "(...)\n";
FOR_EACH_TEST(DISPLAY_TST, DISPLAY_TST_ARGV)
#undef DISPLAY_TST
#undef DISPLAY_TST_ARGV
return 0;
}
#ifndef __EMSCRIPTEN__
if (num_jobs > 0)
return run_parallel(argv[0], test_all, num_jobs, extra_args, requested_tests);
#endif
// Serial execution, original behavior
#define RUN_TST(M) { \
bool run = test_all; \
for (int i = 0; !run && i < argc; ++i) \
run = strcmp(argv[i], #M) == 0; \
if (run) { \
std::string s("test "); \
s += #M; \
enable_debug(#M); \
timeit timeit(true, s.c_str()); \
tst_##M(); \
std::cout << "PASS" << std::endl; \
} \
}
#define RUN_TST_ARGV(M) { \
for (int i = 0; i < argc; ++i) \
if (strcmp(argv[i], #M) == 0) { \
enable_trace(#M); \
enable_debug(#M); \
std::string s("test "); \
s += #M; \
timeit timeit(true, s.c_str()); \
tst_##M(argv, argc, i); \
std::cout << "PASS" << std::endl; \
} \
}
FOR_EACH_ALL_TEST(RUN_TST, RUN_TST_ARGV)
if (test_all) return 0;
TST(ext_numeral);
TST(interval);
TST(value_generator);
TST(value_sweep);
TST(vector);
TST(f2n);
TST(hwf);
TST(trigo);
TST(bits);
TST(mpbq);
TST(mpfx);
TST(mpff);
TST(horn_subsume_model_converter);
TST(model2expr);
TST(hilbert_basis);
TST(heap_trie);
TST(karr);
TST(no_overflow);
// TST(memory);
TST(datalog_parser);
TST_ARGV(datalog_parser_file);
TST(dl_query);
TST(quant_solve);
TST(rcf);
TST(polynorm);
TST(qe_arith);
TST(expr_substitution);
TST(sorting_network);
TST(theory_pb);
TST(simplex);
TST(sat_user_scope);
TST_ARGV(ddnf);
TST(ddnf1);
TST(model_evaluator);
TST(get_consequences);
TST(pb2bv);
TST_ARGV(sat_lookahead);
TST_ARGV(sat_local_search);
TST_ARGV(cnf_backbones);
TST(bdd);
TST(pdd);
TST(pdd_solver);
TST(scoped_timer);
TST(solver_pool);
//TST_ARGV(hs);
TST(finder);
TST(totalizer);
TST(distribution);
TST(euf_bv_plugin);
TST(euf_arith_plugin);
TST(euf_sgraph);
TST(euf_seq_plugin);
TST(sls_test);
TST(scoped_vector);
TST(sls_seq_plugin);
TST(seq_nielsen);
TST(seq_parikh);
TST(nseq_basic);
TST(seq_regex);
TST(nseq_zipt);
TST(ho_matcher);
TST(finite_set);
TST(finite_set_rewriter);
TST(fpa);
FOR_EACH_EXTRA_TEST(RUN_TST, RUN_TST_ARGV)
#undef RUN_TST
#undef RUN_TST_ARGV
return 0;
}

View file

@ -337,15 +337,7 @@ void test_factorization_large_multivariate_missing_factors() {
factors fs(m);
factor(p, fs);
VERIFY(fs.distinct_factors() == 2); // indeed there are 3 factors, that is demonstrated by the loop
for (unsigned i = 0; i < fs.distinct_factors(); ++i) {
polynomial_ref f(m);
f = fs[i];
if (degree(f, x1)<= 1) continue;
factors fs0(m);
factor(f, fs0);
VERIFY(fs0.distinct_factors() >= 2);
}
VERIFY(fs.distinct_factors() >= 3);
polynomial_ref reconstructed(m);
fs.multiply(reconstructed);
@ -370,17 +362,8 @@ void test_factorization_multivariate_missing_factors() {
factors fs(m);
factor(p, fs);
// Multivariate factorization stops after returning the whole polynomial.
VERIFY(fs.distinct_factors() == 1);
VERIFY(m.degree(fs[0], 0) == 3);
factors fs_refined(m);
polynomial_ref residual = fs[0];
factor(residual, fs_refined);
// A second attempt still fails to expose the linear factors.
VERIFY(fs_refined.distinct_factors() == 1); // actually we need 3 factors
VERIFY(m.degree(fs_refined[0], 0) == 3); // actually we need degree 1
// Multivariate factorization should find 3 linear factors
VERIFY(fs.distinct_factors() == 3);
polynomial_ref reconstructed(m);
fs.multiply(reconstructed);

View file

@ -138,6 +138,7 @@ static void test_skolemize_bug() {
Z3_ast f3 = Z3_simplify(ctx, f2);
std::cout << Z3_ast_to_string(ctx, f3) << "\n";
Z3_del_context(ctx);
}

View file

@ -17,8 +17,92 @@ Revision History:
--*/
#include "util/vector.h"
#include "util/rational.h"
#include <iostream>
static void tst_resize_rational() {
// grow from empty using default initialization (zero)
vector<rational> v;
v.resize(4);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i].is_zero());
// shrink: elements below new size are preserved
v.resize(2);
ENSURE(v.size() == 2);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
// grow with explicit value initialization
rational half(1, 2);
v.resize(6, half);
ENSURE(v.size() == 6);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to same size is a no-op
rational three(3);
v.resize(6, three);
ENSURE(v.size() == 6);
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
// grow again after being empty
rational neg(-7);
v.resize(3, neg);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == neg);
}
static void tst_resize() {
// grow from empty using default initialization
svector<int> v;
v.resize(5);
ENSURE(v.size() == 5);
ENSURE(v.capacity() >= 5);
for (unsigned i = 0; i < 5; ++i)
ENSURE(v[i] == 0);
// shrink: elements below new size are preserved, size shrinks
v.resize(3);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
// grow with explicit value initialization
v.resize(7, 42);
ENSURE(v.size() == 7);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to same size is a no-op
v.resize(7, 99);
ENSURE(v.size() == 7);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
ENSURE(v.size() == 0);
// grow again after being empty
v.resize(4, 10);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i] == 10);
}
static void tst1() {
svector<int> v1;
ENSURE(v1.empty());
@ -58,5 +142,7 @@ static void tst1() {
}
void tst_vector() {
tst_resize_rational();
tst_resize();
tst1();
}

View file

@ -214,6 +214,15 @@ void shl(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst) {
}
}
else {
if (bit_shift == 0) {
if (src_sz > dst_sz)
src_sz = dst_sz;
for (size_t i = 0; i < src_sz; ++i)
dst[i] = src[i];
for (size_t i = src_sz; i < dst_sz; ++i)
dst[i] = 0;
return;
}
unsigned comp_shift = (8 * sizeof(unsigned)) - bit_shift;
unsigned prev = 0;
if (src_sz > dst_sz)
@ -278,7 +287,11 @@ void shr(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst) {
}
else {
SASSERT(new_sz == sz);
SASSERT(bit_shift != 0);
if (bit_shift == 0) {
for (size_t i = 0; i < sz; ++i)
dst[i] = src[i];
return;
}
unsigned i = 0;
for (; i < new_sz - 1; ++i) {
dst[i] = src[i];
@ -327,20 +340,26 @@ void shr(std::span<unsigned const> src, unsigned k, std::span<unsigned> dst) {
}
else {
SASSERT(new_sz == src_sz);
SASSERT(bit_shift != 0);
auto sz = new_sz;
if (new_sz > dst_sz)
sz = dst_sz;
unsigned i = 0;
for (; i < sz - 1; ++i) {
if (bit_shift == 0) {
auto sz = std::min(new_sz, dst_sz);
for (size_t i = 0; i < sz; ++i)
dst[i] = src[i];
}
else {
auto sz = new_sz;
if (new_sz > dst_sz)
sz = dst_sz;
unsigned i = 0;
for (; i < sz - 1; ++i) {
dst[i] = src[i];
dst[i] >>= bit_shift;
dst[i] |= (src[i+1] << comp_shift);
}
dst[i] = src[i];
dst[i] >>= bit_shift;
dst[i] |= (src[i+1] << comp_shift);
if (new_sz > dst_sz)
dst[i] |= (src[i+1] << comp_shift);
}
dst[i] = src[i];
dst[i] >>= bit_shift;
if (new_sz > dst_sz)
dst[i] |= (src[i+1] << comp_shift);
}
for (auto i = new_sz; i < dst_sz; ++i)
dst[i] = 0;

View file

@ -161,7 +161,7 @@ uint64_t mpff_manager::get_uint64(mpff const & a) const {
int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
SASSERT(exp >= 0);
uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
return *s >> exp;
return *s >> static_cast<unsigned>(exp);
}
int64_t mpff_manager::get_int64(mpff const & a) const {
@ -175,7 +175,7 @@ int64_t mpff_manager::get_int64(mpff const & a) const {
return INT64_MIN;
}
else {
int64_t r = *s >> exp;
int64_t r = *s >> static_cast<unsigned>(exp);
if (is_neg(a))
r = -r;
return r;

View file

@ -412,7 +412,7 @@ Notes:
bits++;
w_max >>= 1;
}
unsigned pow = (1ul << (bits-1));
unsigned pow = bits > 0 ? (1u << (bits-1)) : 0;
unsigned a = (k + pow - 1) / pow; // a*pow >= k
SASSERT(a*pow >= k);
SASSERT((a-1)*pow < k);

View file

@ -542,6 +542,7 @@ X(Global, isolate_roots_bug, "isolate roots bug")
X(Global, ite_bug, "ite bug")
X(Global, lar_solver_feas, "lar solver feas")
X(Global, lar_solver_inf_heap, "lar solver inf heap")
X(Global, lar_solver_restore, "lar solver restore")
X(Global, Lazard, "Lazard")
X(Global, lcm_bug, "lcm bug")
X(Global, le_bug, "le bug")

View file

@ -494,7 +494,7 @@ public:
}
template<typename Args>
void resize(SZ s, Args args...) {
void resize(SZ s, Args const& args) {
SZ sz = size();
if (s <= sz) { shrink(s); return; }
while (s > capacity()) {
@ -505,7 +505,7 @@ public:
iterator it = m_data + sz;
iterator end = m_data + s;
for (; it != end; ++it) {
new (it) T(std::forward<Args>(args));
new (it) T(args);
}
}