mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

create a test for order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-22 10:24:50 -08:00 • committed by Lev Nachmanson
parent ea02231ef8
commit 979593e2f1
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/lp/nla_solver.cpp
View file

@ -2310,6 +2310,7 @@ void solver::test_monotone_lemma() {
// set f == j + 1 // set f == j + 1
s.set_column_value(lp_f, s.get_column_value(lp_j) + rational(1)); s.set_column_value(lp_f, s.get_column_value(lp_j) + rational(1));
// set the values of ab, ef, cd, and ij correctly // set the values of ab, ef, cd, and ij correctly
s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab)); s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab));
s.set_column_value(lp_cd, nla.m_imp->mon_value_by_vars(mon_cd)); s.set_column_value(lp_cd, nla.m_imp->mon_value_by_vars(mon_cd));
s.set_column_value(lp_ij, nla.m_imp->mon_value_by_vars(mon_ij)); s.set_column_value(lp_ij, nla.m_imp->mon_value_by_vars(mon_ij));
@ -2319,9 +2320,7 @@ void solver::test_monotone_lemma() {
vector<ineq> lemma; vector<ineq> lemma;
lp::explanation exp; lp::explanation exp;
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false); SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(std::cout << "lemma: "); nla.m_imp->print_lemma(std::cout << "lemma: ");
} }