Added C++ interface and test for lp_polynomial_constraint_evaluate_subs

and added missing `Value(int)` constructor.

Author: Ovascos

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);

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);

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(),

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());

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);
+}