mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
enable test_tangent_lemma_reg
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
30d35488d8
commit
9c8d5ddffb
|
@ -165,8 +165,9 @@ rational core::product_value(const unsigned_vector & m) const {
|
|||
// return true iff the monic value is equal to the product of the values of the factors
|
||||
bool core::check_monic(const monic& m) const {
|
||||
SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int());
|
||||
TRACE("nla_solver", print_monic_with_vars(m, tout) << '\n';);
|
||||
return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
|
||||
bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
|
||||
CTRACE("nla_solver", !ret, print_monic(m, tout) << '\n';);
|
||||
return ret;
|
||||
}
|
||||
|
||||
void core::explain(const monic& m, lp::explanation& exp) const {
|
||||
|
@ -1257,7 +1258,7 @@ bool core::done() const {
|
|||
}
|
||||
|
||||
lbool core::incremental_linearization(bool constraint_derived) {
|
||||
TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout););
|
||||
TRACE("nla_solver_details", print_terms(tout); m_lar_solver.print_constraints(tout););
|
||||
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
|
||||
TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";);
|
||||
if (search_level == 0) {
|
||||
|
|
|
@ -2,7 +2,7 @@ add_executable(lp_tst
|
|||
EXCLUDE_FROM_ALL
|
||||
lp_main.cpp lp.cpp nla_solver_test.cpp $<TARGET_OBJECTS:util>
|
||||
$<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat>
|
||||
$<TARGET_OBJECTS:lp> $<TARGET_OBJECTS:grobner>
|
||||
$<TARGET_OBJECTS:lp> $<TARGET_OBJECTS:grobner> $<TARGET_OBJECTS:simplex>
|
||||
$<TARGET_OBJECTS:interval> $<TARGET_OBJECTS:dd> $<TARGET_OBJECTS:ast>)
|
||||
target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
|
||||
target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
|
||||
|
|
|
@ -718,26 +718,18 @@ void test_monotone_lemma() {
|
|||
}
|
||||
|
||||
void test_tangent_lemma_reg() {
|
||||
/*
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, ab = 10;
|
||||
unsigned a = s.number_of_vars();
|
||||
unsigned b = a + 1;
|
||||
unsigned ab = b + 1;
|
||||
|
||||
lpvar lp_a = s.add_named_var(a, true, "a");
|
||||
lpvar lp_b = s.add_named_var(b, true, "b");
|
||||
// lpvar lp_c = s.add_named_var(c, true, "c");
|
||||
// lpvar lp_d = s.add_named_var(d, true, "d");
|
||||
// lpvar lp_e = s.add_named_var(e, true, "e");
|
||||
// lpvar lp_f = s.add_named_var(f, true, "f");
|
||||
// lpvar lp_i = s.add_named_var(i, true, "i");
|
||||
// lpvar lp_j = s.add_named_var(j, true, "j");
|
||||
lpvar lp_ab = s.add_named_var(ab, true, "ab");
|
||||
int sign = 1;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
sign *= -1;
|
||||
s_set_column_value(s, j, sign * rational((j + 2) * (j + 2)));
|
||||
}
|
||||
|
||||
s_set_column_value(s, lp_a, rational(3));
|
||||
s_set_column_value(s, lp_b, rational(4));
|
||||
s_set_column_value(s, lp_ab, rational(11));
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
|
@ -745,13 +737,11 @@ void test_tangent_lemma_reg() {
|
|||
vector<unsigned> vec;
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_b);
|
||||
int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
|
||||
nla.add_monic(lp_ab, vec.size(), vec.begin());
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
*/
|
||||
}
|
||||
|
||||
void test_tangent_lemma_equiv() {
|
||||
|
|
Loading…
Reference in a new issue