From 804a431c518205dfc086ada828409a9715075afe Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 3 Nov 2025 14:09:07 -0800 Subject: [PATCH 1/4] fixes provided by SMT-RAT --- include/polynomial.h | 10 ++++++++ src/polynomial/polynomial.c | 47 +++++++++++++++++++++++++++++++++---- src/variable/variable_db.c | 2 ++ 3 files changed, 54 insertions(+), 5 deletions(-) diff --git a/include/polynomial.h b/include/polynomial.h index 58604ec3..e3e2fa4a 100644 --- a/include/polynomial.h +++ b/include/polynomial.h @@ -109,6 +109,11 @@ void lp_polynomial_lc_constant(const lp_polynomial_t* A, lp_integer_t *out); /** Get the context of the given polynomial */ const lp_polynomial_context_t* lp_polynomial_get_context(const lp_polynomial_t* A); +/** Sets the context of a polynomial. + * Warning: variable DB indexes are not checked. + */ +void lp_polynomial_set_context(lp_polynomial_t* A, const lp_polynomial_context_t* ctx); + /** Returns all the variables (it will not clear the output list vars) */ void lp_polynomial_get_variables(const lp_polynomial_t* A, lp_variable_list_t* vars); @@ -375,6 +380,11 @@ lp_polynomial_t* lp_polynomial_constraint_explain_infer_bounds(const lp_polynomi */ int lp_polynomial_constraint_evaluate(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* M); +/** Substitutes the polynomial with M and checks the sign of the resulting real number. + * If M does not fully evaluate A to a real, -1 is returned. + */ +int lp_polynomial_constraint_evaluate_subs(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* M); + /** * Given a polynomial constraint over an integer ring Zp, evaluate its truth value. * sgn_condition must either be (== 0) or (!= 0) and M must assign to Zp. diff --git a/src/polynomial/polynomial.c b/src/polynomial/polynomial.c index 4e65889e..d2c17522 100644 --- a/src/polynomial/polynomial.c +++ b/src/polynomial/polynomial.c @@ -1177,6 +1177,18 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t lp_value_construct_none(&x_value_backup); } + lp_polynomial_t* B = lp_polynomial_new(A->ctx); + { + coefficient_t A_rat; + lp_integer_t multiplier; + integer_construct(&multiplier); + coefficient_construct(A->ctx, &A_rat); + coefficient_evaluate_rationals(A->ctx, &A->data, M, &A_rat, &multiplier); + coefficient_swap(&B->data, &A_rat); + coefficient_destruct(&A_rat); + integer_destruct(&multiplier); + } + size_t i; lp_polynomial_t** factors = 0; @@ -1190,11 +1202,13 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t // Get the reduced polynomial lp_polynomial_t A_r; lp_polynomial_construct(&A_r, A->ctx); - lp_polynomial_reductum_m(&A_r, A, M); - assert(x == lp_polynomial_top_variable(A)); - - // Get the square-free factorization - lp_polynomial_factor_square_free(&A_r, &factors, &multiplicities, &factors_size); + if (x == lp_polynomial_top_variable(B)) { + lp_polynomial_reductum_m(&A_r, B, M); + assert(x == lp_polynomial_top_variable(B)); + // Get the square-free factorization + lp_polynomial_factor_square_free(&A_r, &factors, &multiplicities, &factors_size); + } + lp_polynomial_delete(B); // Count the max number of roots size_t total_degree = 0; @@ -2134,6 +2148,29 @@ int lp_polynomial_constraint_evaluate(const lp_polynomial_t* A, lp_sign_conditio return lp_sign_condition_consistent(sgn_condition, p_sign); } +int lp_polynomial_constraint_evaluate_subs(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* M) { + coefficient_t A_rat; + lp_integer_t multiplier; + + lp_polynomial_external_clean(A); + assert(A->ctx->K == lp_Z); + + integer_construct(&multiplier); + coefficient_construct(A->ctx, &A_rat); + coefficient_evaluate_rationals(A->ctx, &A->data, M, &A_rat, &multiplier); + integer_destruct(&multiplier); + + int res = -1; + if (A_rat.type == COEFFICIENT_NUMERIC) { + int sgn = integer_sgn(lp_Z, &A_rat.value.num); + res = lp_sign_condition_consistent(sgn_condition, sgn); + assert(res >= 0); + } + + coefficient_destruct(&A_rat); + return res; +} + int lp_polynomial_constraint_evaluate_Zp(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* m) { lp_polynomial_external_clean(A); diff --git a/src/variable/variable_db.c b/src/variable/variable_db.c index 60f3df4c..33866c47 100644 --- a/src/variable/variable_db.c +++ b/src/variable/variable_db.c @@ -63,9 +63,11 @@ void lp_variable_db_add_variable(lp_variable_db_t* var_db, lp_variable_t var, co assert(var_db); while (var >= var_db->capacity) { lp_variable_db_resize(var_db, 2*var_db->capacity); + var_db->size = var_db->capacity < var ? var_db->capacity : var; } assert(var_db->variable_names[var] == 0); var_db->variable_names[var] = strdup(name); + var_db->size = var_db->size < var ? var : var_db->size; } void lp_variable_db_construct(lp_variable_db_t* var_db) { From b974645c459f2b5f0a547fa557204ecace538105 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 4 Nov 2025 11:05:13 -0800 Subject: [PATCH 2/4] code updates --- src/polynomial/polynomial.c | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/src/polynomial/polynomial.c b/src/polynomial/polynomial.c index d2c17522..497c914e 100644 --- a/src/polynomial/polynomial.c +++ b/src/polynomial/polynomial.c @@ -1177,17 +1177,13 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t lp_value_construct_none(&x_value_backup); } - lp_polynomial_t* B = lp_polynomial_new(A->ctx); - { - coefficient_t A_rat; - lp_integer_t multiplier; - integer_construct(&multiplier); - coefficient_construct(A->ctx, &A_rat); - coefficient_evaluate_rationals(A->ctx, &A->data, M, &A_rat, &multiplier); - coefficient_swap(&B->data, &A_rat); - coefficient_destruct(&A_rat); - integer_destruct(&multiplier); - } + lp_polynomial_t B; + lp_polynomial_construct(&B, A->ctx); + + lp_integer_t multiplier; + integer_construct(&multiplier); + coefficient_evaluate_rationals(A->ctx, &A->data, M, &B.data, &multiplier); + integer_destruct(&multiplier); size_t i; @@ -1202,13 +1198,12 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t // Get the reduced polynomial lp_polynomial_t A_r; lp_polynomial_construct(&A_r, A->ctx); - if (x == lp_polynomial_top_variable(B)) { - lp_polynomial_reductum_m(&A_r, B, M); - assert(x == lp_polynomial_top_variable(B)); + if (x == lp_polynomial_top_variable(&B)) { + lp_polynomial_reductum_m(&A_r, &B, M); + assert(x == lp_polynomial_top_variable(&B)); // Get the square-free factorization lp_polynomial_factor_square_free(&A_r, &factors, &multiplicities, &factors_size); } - lp_polynomial_delete(B); // Count the max number of roots size_t total_degree = 0; @@ -1311,6 +1306,7 @@ void lp_polynomial_roots_isolate(const lp_polynomial_t* A, const lp_assignment_t free(roots_tmp); lp_value_destruct(&x_value_backup); lp_polynomial_destruct(&A_r); + lp_polynomial_destruct(&B); } lp_feasibility_set_t* lp_polynomial_constraint_get_feasible_set(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, int negated, const lp_assignment_t* M) { From 962119881130e280d57f153e3aaeb606bb1ad536 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 4 Nov 2025 11:06:11 -0800 Subject: [PATCH 3/4] update comment --- include/polynomial.h | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/include/polynomial.h b/include/polynomial.h index e3e2fa4a..36f1a9f6 100644 --- a/include/polynomial.h +++ b/include/polynomial.h @@ -109,8 +109,9 @@ void lp_polynomial_lc_constant(const lp_polynomial_t* A, lp_integer_t *out); /** Get the context of the given polynomial */ const lp_polynomial_context_t* lp_polynomial_get_context(const lp_polynomial_t* A); -/** Sets the context of a polynomial. - * Warning: variable DB indexes are not checked. +/** + * Sets the context of a polynomial. + * Warning: variable DB indexes are not checked. Use with caution. */ void lp_polynomial_set_context(lp_polynomial_t* A, const lp_polynomial_context_t* ctx); @@ -380,8 +381,9 @@ lp_polynomial_t* lp_polynomial_constraint_explain_infer_bounds(const lp_polynomi */ int lp_polynomial_constraint_evaluate(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* M); -/** Substitutes the polynomial with M and checks the sign of the resulting real number. - * If M does not fully evaluate A to a real, -1 is returned. +/** + * Substitutes the polynomial with M and checks the sign of the resulting real number. + * If M does not fully evaluate A to a real, -1 is returned. */ int lp_polynomial_constraint_evaluate_subs(const lp_polynomial_t* A, lp_sign_condition_t sgn_condition, const lp_assignment_t* M); From 4e2b911250a9d06f6838cfbd6fc1ffd7e0749fb5 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 12 Nov 2025 11:54:59 -0800 Subject: [PATCH 4/4] Added C++ interface and test for lp_polynomial_constraint_evaluate_subs and added missing `Value(int)` constructor. --- include/polyxx/polynomial.h | 9 +++++-- include/polyxx/value.h | 2 ++ src/polyxx/polynomial.cpp | 5 ++++ src/polyxx/value.cpp | 1 + test/polyxx/test_polynomial.cpp | 46 +++++++++++++++++++++++++++++++++ 5 files changed, 61 insertions(+), 2 deletions(-) diff --git a/include/polyxx/polynomial.h b/include/polyxx/polynomial.h index d18ee579..3018bd51 100644 --- a/include/polyxx/polynomial.h +++ b/include/polyxx/polynomial.h @@ -117,8 +117,8 @@ namespace poly { * assignment. */ bool is_assigned_over_assignment(const Polynomial& p, const Assignment& a); /** Evaluates p over a given assignment and returns an univariate polynomial. - * Assumes that a assigns all variable in p but the top variable. - * Assumes that a assigns to integer only. */ + * Assumes that 'a' assigns all variable in p but the top variable. + * Assumes that 'a' assigns to integer only. */ UPolynomial to_univariate(const Polynomial& p, const Assignment& a); /** Compute the sign of a polynomial over an assignment. */ int sgn(const Polynomial& p, const Assignment& a); @@ -127,6 +127,11 @@ namespace poly { /** Evaluate a polynomial constraint over an assignment. */ bool evaluate_constraint(const Polynomial& p, const Assignment& a, SignCondition sc); + /** Checks if a polynomial constraint is fully evaluated over assignment. + * Returns -1 if 'a' does not fully evaluate the constraint. + * Otherwise, returns true if the constraint holds under 'a'. */ + int evaluate_constraint_subs(const Polynomial& p, const Assignment& a, + SignCondition sc); /** Evaluate a polynomial over an interval assignment. The result is only an * approximation. */ Interval evaluate(const Polynomial& p, const IntervalAssignment& a); diff --git a/include/polyxx/value.h b/include/polyxx/value.h index 4534b516..17376846 100644 --- a/include/polyxx/value.h +++ b/include/polyxx/value.h @@ -29,6 +29,8 @@ namespace poly { /** Construct a none value. */ Value(); /** Construct from a native integer. */ + Value(int i); + /** Construct from a native integer. */ Value(long i); /** Copy from the given Value. */ Value(const Value& val); diff --git a/src/polyxx/polynomial.cpp b/src/polyxx/polynomial.cpp index 3dc4e40e..3c7f8c99 100644 --- a/src/polyxx/polynomial.cpp +++ b/src/polyxx/polynomial.cpp @@ -165,6 +165,11 @@ namespace poly { return lp_polynomial_constraint_evaluate( p.get_internal(), to_sign_condition(sc), a.get_internal()); } + int evaluate_constraint_subs(const Polynomial& p, const Assignment& a, + SignCondition sc) { + return lp_polynomial_constraint_evaluate_subs( + p.get_internal(), to_sign_condition(sc), a.get_internal()); + } Interval evaluate(const Polynomial& p, const IntervalAssignment& a) { Interval res; lp_polynomial_interval_value(p.get_internal(), a.get_internal(), diff --git a/src/polyxx/value.cpp b/src/polyxx/value.cpp index a4ac1d4c..e56a71e7 100644 --- a/src/polyxx/value.cpp +++ b/src/polyxx/value.cpp @@ -13,6 +13,7 @@ namespace poly { } Value::Value() { lp_value_construct_none(&mValue); } + Value::Value(int i) { lp_value_construct_int(get_internal(), i); } Value::Value(long i) { lp_value_construct_int(get_internal(), i); } Value::Value(const Value& val) { lp_value_construct_copy(get_internal(), val.get_internal()); diff --git a/test/polyxx/test_polynomial.cpp b/test/polyxx/test_polynomial.cpp index b116f442..c7aec516 100644 --- a/test/polyxx/test_polynomial.cpp +++ b/test/polyxx/test_polynomial.cpp @@ -100,3 +100,49 @@ TEST_CASE("polynomial::constructor") { CHECK(p_cp == p_cp_a); CHECK(ptr == p_mv_a.get_internal()); } + +TEST_CASE("polynomial::evaluate") { + Variable x("x"); + Variable y("y"); + Polynomial p1 = 1 * pow(x, 6) + 2 * pow(x, 5) + 3 * y - 1; + Polynomial p2 = 1 * y * pow(x + 1, 4); + + // full assignment + Assignment a; + a.set(x, -1); + a.set(y, 2); + CHECK(a.has(x)); + CHECK(a.has(y)); + + CHECK(evaluate(p1, a) == Value(4)); + CHECK(evaluate_constraint(p1, a, SignCondition::GE) == true); + CHECK(evaluate_constraint(p1, a, SignCondition::LT) == false); + CHECK(evaluate_constraint(p1, a, SignCondition::EQ) == false); + CHECK(evaluate_constraint_subs(p1, a, SignCondition::GE) == 1); + CHECK(evaluate_constraint_subs(p1, a, SignCondition::LT) == 0); + CHECK(evaluate_constraint_subs(p1, a, SignCondition::EQ) == 0); + + CHECK(evaluate(p2, a) == Value(0)); + CHECK(evaluate_constraint(p2, a, SignCondition::GE) == true); + CHECK(evaluate_constraint(p2, a, SignCondition::LT) == false); + CHECK(evaluate_constraint(p2, a, SignCondition::EQ) == true); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::GE) == 1); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::LT) == 0); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::EQ) == 1); + + // partial assignment + a.unset(y); + CHECK(a.has(x)); + CHECK(!a.has(y)); + + CHECK(evaluate_constraint_subs(p1, a, SignCondition::GE) == -1); + CHECK(evaluate_constraint_subs(p1, a, SignCondition::LT) == -1); + CHECK(evaluate_constraint_subs(p1, a, SignCondition::EQ) == -1); + + CHECK(evaluate_constraint(p2, a, SignCondition::GE) == true); + CHECK(evaluate_constraint(p2, a, SignCondition::LT) == false); + CHECK(evaluate_constraint(p2, a, SignCondition::EQ) == true); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::GE) == 1); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::LT) == 0); + CHECK(evaluate_constraint_subs(p2, a, SignCondition::EQ) == 1); +}