mirror of
https://github.com/Z3Prover/z3
synced 2026-06-09 02:20:57 +00:00
70e88e56fa
The `m_normalized_terms_to_columns` map in `lar_solver` uses a `term_comparer` that delegates to `lar_term::operator==`, which intentionally returns `false` (with comment "take care not to create identical terms"). This makes `fetch_normalized_term_column` unable to find any term, rendering the Horner module's `interval_from_term` bounds-recovery path dead code. History: `lar_term::operator==` returning `false` has been present since the original "merge LRA" commit (911b24784, 2018). The `m_normalized_terms_to_columns` lookup was added later (dfe0e856,c95f66e0, Aug 2019) as "toward fetching existing terms intervals from lar_solver". The initial code had `lp_assert(find == end)` on registration (always true with broken ==) and `lp_assert(find != end)` on deregister (always false). The very next commit (207c1c50, one day later) removed both asserts, replacing them with soft checks. The `term_comparer` struct delegating to `operator==` was introduced during a later PIMPL refactor (b375faa77). Fix: Replace the `term_comparer` implementation with a structural comparison that checks size and then verifies each coefficient-variable pair via `coeffs().find_core()`. This is localized to the `m_normalized_terms_to_columns` map and does not change `lar_term::operator==`, preserving its intentional semantics elsewhere. Validated: on a QF_UFNIA benchmark, `interval_from_term` lookups go from 0/573 successful to 34/573 successful. Unit test added for the `fetch_normalized_term_column` round-trip. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
292 lines
No EOL
8.7 KiB
C++
292 lines
No EOL
8.7 KiB
C++
/*++
|
|
Copyright (c) 2024 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
nla_intervals.cpp
|
|
|
|
Abstract:
|
|
|
|
Tests for NLA interval propagation functionality
|
|
|
|
Author:
|
|
|
|
Test Coverage Improvement
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
|
|
#include "math/lp/nla_intervals.h"
|
|
#include "math/lp/nla_core.h"
|
|
#include "math/lp/lar_solver.h"
|
|
#include "util/rational.h"
|
|
#include "util/rlimit.h"
|
|
#include <iostream>
|
|
|
|
namespace nla {
|
|
|
|
void test_nla_intervals_basic() {
|
|
std::cout << "test_nla_intervals_basic\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables with known intervals
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar y = s.add_var(1, true);
|
|
lpvar xy = s.add_var(2, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial xy = x * y
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
nla_solver.add_monic(xy, vars.size(), vars.begin());
|
|
|
|
// Set bounds: x in [1, 3], y in [2, 4]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(1));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(3));
|
|
s.add_var_bound(y, lp::lconstraint_kind::GE, rational(2));
|
|
s.add_var_bound(y, lp::lconstraint_kind::LE, rational(4));
|
|
|
|
// Test basic intervals: xy should be in [2, 12]
|
|
VERIFY(true); // This is a placeholder since actual interval computation requires more setup
|
|
}
|
|
|
|
void test_nla_intervals_negative() {
|
|
std::cout << "test_nla_intervals_negative\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables with negative intervals
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar y = s.add_var(1, true);
|
|
lpvar xy = s.add_var(2, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial xy = x * y
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
nla_solver.add_monic(xy, vars.size(), vars.begin());
|
|
|
|
// Set bounds: x in [-3, -1], y in [2, 4]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(-3));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(-1));
|
|
s.add_var_bound(y, lp::lconstraint_kind::GE, rational(2));
|
|
s.add_var_bound(y, lp::lconstraint_kind::LE, rational(4));
|
|
|
|
// Expected: xy in [-12, -2] since x*y with x∈[-3,-1], y∈[2,4] gives xy∈[-12,-2]
|
|
VERIFY(true); // Placeholder
|
|
}
|
|
|
|
void test_nla_intervals_zero_crossing() {
|
|
std::cout << "test_nla_intervals_zero_crossing\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables where one interval crosses zero
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar y = s.add_var(1, true);
|
|
lpvar xy = s.add_var(2, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial xy = x * y
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
nla_solver.add_monic(xy, vars.size(), vars.begin());
|
|
|
|
// Set bounds: x in [-2, 3], y in [1, 4]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(-2));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(3));
|
|
s.add_var_bound(y, lp::lconstraint_kind::GE, rational(1));
|
|
s.add_var_bound(y, lp::lconstraint_kind::LE, rational(4));
|
|
|
|
// Expected: xy in [-8, 12] since x*y with x∈[-2,3], y∈[1,4] gives xy∈[-8,12]
|
|
VERIFY(true); // Placeholder
|
|
}
|
|
|
|
void test_nla_intervals_power() {
|
|
std::cout << "test_nla_intervals_power\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables for power operations
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar x_squared = s.add_var(1, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial x_squared = x * x
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(x);
|
|
nla_solver.add_monic(x_squared, vars.size(), vars.begin());
|
|
|
|
// Set bounds: x in [-3, 2]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(-3));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(2));
|
|
|
|
// Expected: x^2 in [0, 9] since x^2 with x∈[-3,2] gives x^2∈[0,9]
|
|
VERIFY(true); // Placeholder
|
|
}
|
|
|
|
void test_nla_intervals_mixed_signs() {
|
|
std::cout << "test_nla_intervals_mixed_signs\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables for three-way product
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar y = s.add_var(1, true);
|
|
lpvar z = s.add_var(2, true);
|
|
lpvar xyz = s.add_var(3, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial xyz = x * y * z
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
vars.push_back(z);
|
|
nla_solver.add_monic(xyz, vars.size(), vars.begin());
|
|
|
|
// Set bounds: x in [-1, 1], y in [-2, 2], z in [1, 3]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(-1));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(1));
|
|
s.add_var_bound(y, lp::lconstraint_kind::GE, rational(-2));
|
|
s.add_var_bound(y, lp::lconstraint_kind::LE, rational(2));
|
|
s.add_var_bound(z, lp::lconstraint_kind::GE, rational(1));
|
|
s.add_var_bound(z, lp::lconstraint_kind::LE, rational(3));
|
|
|
|
// Expected: xyz in [-6, 6] since x*y*z with given intervals
|
|
VERIFY(true); // Placeholder
|
|
}
|
|
|
|
void test_nla_intervals_fractional() {
|
|
std::cout << "test_nla_intervals_fractional\n";
|
|
|
|
reslimit rl;
|
|
params_ref p;
|
|
lp::lar_solver s;
|
|
|
|
// Create variables for fractional bounds
|
|
lpvar x = s.add_var(0, true);
|
|
lpvar y = s.add_var(1, true);
|
|
lpvar xy = s.add_var(2, true);
|
|
|
|
nla::core nla_solver(s, p, rl);
|
|
|
|
// Create monomial xy = x * y
|
|
vector<lpvar> vars;
|
|
vars.push_back(x);
|
|
vars.push_back(y);
|
|
nla_solver.add_monic(xy, vars.size(), vars.begin());
|
|
|
|
// Set fractional bounds: x in [0.5, 1.5], y in [2.5, 3.5]
|
|
s.add_var_bound(x, lp::lconstraint_kind::GE, rational(1, 2));
|
|
s.add_var_bound(x, lp::lconstraint_kind::LE, rational(3, 2));
|
|
s.add_var_bound(y, lp::lconstraint_kind::GE, rational(5, 2));
|
|
s.add_var_bound(y, lp::lconstraint_kind::LE, rational(7, 2));
|
|
|
|
// Expected: xy in [1.25, 5.25] since x*y with given fractional intervals
|
|
VERIFY(true); // Placeholder
|
|
}
|
|
|
|
void test_fetch_normalized_term_column() {
|
|
std::cout << "test_fetch_normalized_term_column\n";
|
|
|
|
lp::lar_solver s;
|
|
|
|
// Create some variables
|
|
lpvar x = s.add_var(0, true); // j0
|
|
lpvar y = s.add_var(1, true); // j1
|
|
lpvar z = s.add_var(2, true); // j2
|
|
|
|
// Add a term t = 2*x + 3*y and register it
|
|
lp::lar_term t;
|
|
t.add_monomial(rational(2), x);
|
|
t.add_monomial(rational(3), y);
|
|
s.add_term(t.coeffs_as_vector(), UINT_MAX);
|
|
s.register_existing_terms();
|
|
|
|
// Now build the same term independently and look it up
|
|
lp::lar_term query;
|
|
query.add_monomial(rational(2), x);
|
|
query.add_monomial(rational(3), y);
|
|
lp::mpq a;
|
|
lp::lar_term norm_query = query.get_normalized_by_min_var(a);
|
|
|
|
std::pair<lp::mpq, lpvar> result;
|
|
bool found = s.fetch_normalized_term_column(norm_query, result);
|
|
VERIFY(found);
|
|
std::cout << " round-trip lookup: " << (found ? "PASS" : "FAIL") << "\n";
|
|
|
|
// Build query with variables added in reverse order
|
|
lp::lar_term query_rev;
|
|
query_rev.add_monomial(rational(3), y);
|
|
query_rev.add_monomial(rational(2), x);
|
|
lp::lar_term norm_rev = query_rev.get_normalized_by_min_var(a);
|
|
|
|
bool found_rev = s.fetch_normalized_term_column(norm_rev, result);
|
|
VERIFY(found_rev);
|
|
std::cout << " reverse-order lookup: " << (found_rev ? "PASS" : "FAIL") << "\n";
|
|
|
|
// Test a 3-variable term: x - y + 5*z
|
|
lp::lar_term t2;
|
|
t2.add_monomial(rational(1), x);
|
|
t2.add_monomial(rational(-1), y);
|
|
t2.add_monomial(rational(5), z);
|
|
s.add_term(t2.coeffs_as_vector(), UINT_MAX);
|
|
s.register_existing_terms();
|
|
|
|
lp::lar_term query2;
|
|
query2.add_monomial(rational(1), x);
|
|
query2.add_monomial(rational(-1), y);
|
|
query2.add_monomial(rational(5), z);
|
|
lp::lar_term norm2 = query2.get_normalized_by_min_var(a);
|
|
|
|
found = s.fetch_normalized_term_column(norm2, result);
|
|
VERIFY(found);
|
|
std::cout << " 3-variable term lookup: " << (found ? "PASS" : "FAIL") << "\n";
|
|
|
|
// Test that a non-registered term is NOT found
|
|
lp::lar_term query3;
|
|
query3.add_monomial(rational(7), x);
|
|
query3.add_monomial(rational(11), y);
|
|
lp::lar_term norm3 = query3.get_normalized_by_min_var(a);
|
|
|
|
bool found_missing = s.fetch_normalized_term_column(norm3, result);
|
|
VERIFY(!found_missing);
|
|
std::cout << " non-existent term not found: " << (!found_missing ? "PASS" : "FAIL") << "\n";
|
|
}
|
|
|
|
void test_nla_intervals() {
|
|
test_nla_intervals_basic();
|
|
test_nla_intervals_negative();
|
|
test_nla_intervals_zero_crossing();
|
|
test_nla_intervals_power();
|
|
test_nla_intervals_mixed_signs();
|
|
test_nla_intervals_fractional();
|
|
test_fetch_normalized_term_column();
|
|
}
|
|
|
|
} // namespace nla
|
|
|
|
void tst_nla_intervals() {
|
|
nla::test_nla_intervals();
|
|
} |