mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fixes for mixed case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
9c8d5ddffb
commit
fd1e0e4d80
|
|
@ -13,7 +13,7 @@ def_module_params('nla',
|
|||
('grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'),
|
||||
('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'),
|
||||
('grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
|
||||
('gr_q', UINT, 8, 'grobner\'s quota'),
|
||||
('gr_q', UINT, 10, 'grobner\'s quota'),
|
||||
('grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only')
|
||||
))
|
||||
|
||||
|
|
|
|||
|
|
@ -21,14 +21,200 @@
|
|||
#include "math/lp/nla_core.h"
|
||||
|
||||
namespace nla {
|
||||
template <typename T> rational tangents::val(T const& t) const { return m_core->val(t); }
|
||||
|
||||
tangents::tangents(core * c) : common(c, nullptr) {}
|
||||
struct imp {
|
||||
point m_a;
|
||||
point m_b;
|
||||
point m_xy;
|
||||
bool m_a_is_ok;
|
||||
bool m_b_is_ok;
|
||||
rational m_correct_v;
|
||||
// "below" means that the incorrect value is less than the correct one, that is m_v < m_correct_v
|
||||
bool m_below;
|
||||
rational m_v; // the monomial value
|
||||
lpvar m_j; // the monic variable
|
||||
const monic& m_m;
|
||||
const factor& m_x;
|
||||
const factor& m_y;
|
||||
lpvar m_jx;
|
||||
lpvar m_jy;
|
||||
tangents& m_tang;
|
||||
imp(point xy,
|
||||
const rational& v,
|
||||
lpvar j, // the monic variable
|
||||
const monic& m,
|
||||
const factor& x,
|
||||
const factor& y,
|
||||
tangents& tang) : m_xy(xy),
|
||||
m_correct_v(xy.x * xy.y),
|
||||
m_below(v < m_correct_v),
|
||||
m_v(v),
|
||||
m_j(tang.var(m)),
|
||||
m_m(m),
|
||||
m_x(x),
|
||||
m_y(y),
|
||||
m_jx(tang.var(x)),
|
||||
m_jy(tang.var(y)),
|
||||
m_tang(tang) {}
|
||||
|
||||
|
||||
std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std::ostream& out) const {
|
||||
return out << "(" << a << ", " << b << ")";
|
||||
}
|
||||
core & c() { return m_tang.c(); }
|
||||
|
||||
void generate_explanations_of_tang_lemma(lp::explanation& exp) {
|
||||
// here we repeat the same explanation for each lemma
|
||||
c().explain(m_m, exp);
|
||||
c().explain(m_x, exp);
|
||||
c().explain(m_y, exp);
|
||||
}
|
||||
void generate_simple_tangent_lemma(const monic& m, const factorization&);
|
||||
void tangent_lemma_on_bf() {
|
||||
get_tang_points();
|
||||
TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(tout) << std::endl;);
|
||||
generate_two_tang_lines();
|
||||
if (m_a_is_ok)
|
||||
generate_tang_plane(m_a);
|
||||
if (m_b_is_ok)
|
||||
generate_tang_plane(m_b);
|
||||
}
|
||||
|
||||
|
||||
void generate_tang_plane(const point & pl) {
|
||||
c().add_empty_lemma();
|
||||
c().negate_relation(m_jx, pl.x);
|
||||
c().negate_relation(m_jy, pl.y);
|
||||
#if Z3DEBUG
|
||||
int mult_sign = nla::rat_sign(pl.x - c().val(m_jx))*nla::rat_sign(pl.y - c().val(m_jy));
|
||||
SASSERT((mult_sign == 1) == m_below);
|
||||
// If "mult_sign is 1" then (a - x)(b-y) > 0 and ab - bx - ay + xy > 0
|
||||
// or -ab + bx + ay < xy or -ay - bx + xy > -ab
|
||||
// val(j) stands for xy. So, finally we have -ay - bx + j > - ab
|
||||
#endif
|
||||
|
||||
lp::lar_term t;
|
||||
t.add_monomial(- pl.x, m_jy);
|
||||
t.add_monomial(- pl.y, m_jx);
|
||||
t.add_var(m_j);
|
||||
c().mk_ineq(t, m_below? llc::GT : llc::LT, - pl.x*pl.y);
|
||||
}
|
||||
|
||||
void generate_two_tang_lines() {
|
||||
m_tang.add_empty_lemma();
|
||||
c().mk_ineq(m_jx, llc::NE, m_xy.x);
|
||||
c().mk_ineq(m_j, - m_xy.x, m_jy, llc::EQ);
|
||||
|
||||
m_tang.add_empty_lemma();
|
||||
c().mk_ineq(m_jy, llc::NE, m_xy.y);
|
||||
c().mk_ineq(m_j, - m_xy.y, m_jx, llc::EQ);
|
||||
}
|
||||
// Get two planes tangent to surface z = xy, one at point a, and another at point b, creating a cut
|
||||
void get_initial_tang_points() {
|
||||
const rational& x = m_xy.x;
|
||||
const rational& y = m_xy.y;
|
||||
if (!m_below){
|
||||
m_a = point(x - rational(1), y + rational(1));
|
||||
m_b = point(x + rational(1), y - rational(1));
|
||||
}
|
||||
else {
|
||||
// denote x = xy.x and y = xy.y, and vx, vy - the value of x and y.
|
||||
// we have val(xy) < vx*y + vy*x - vx*vy = pl(x, y);
|
||||
// The plane with delta (1, 1) is (vx + 1)y + (vy + 1)x - (vx + 1)(vy + 1) =
|
||||
// vx*y + vy*x - vx*vy + y + x - xv*vy - vx - vy - 1 = pl(x, y) - 1
|
||||
// For integers the last expression is greater than or equal to val(xy) when x = vx and y = vy.
|
||||
// If x <= vx+1 and y <= vy+1 then (vx+1-x)*(vy+1-y) > 0, that creates a cut
|
||||
// - (vx + 1)y - (vy + 1)x + xy > - (vx+1)*(vx+1)
|
||||
m_a = point(x - rational(1), y - rational(1));
|
||||
m_b = point(x + rational(1), y + rational(1));
|
||||
}
|
||||
}
|
||||
|
||||
void push_tang_point(point & a) {
|
||||
int steps = 10;
|
||||
point del = a - m_xy;
|
||||
while (steps--) {
|
||||
del *= rational(2);
|
||||
point na = m_xy + del;
|
||||
TRACE("nla_solver_tp", tout << "del = " << del << std::endl;);
|
||||
if (!plane_is_correct_cut(na)) {
|
||||
TRACE("nla_solver_tp", tout << "exit";tout << std::endl;);
|
||||
return;
|
||||
}
|
||||
a = na;
|
||||
}
|
||||
}
|
||||
|
||||
bool pull_tang_point(point & a ) {
|
||||
if (plane_is_correct_cut(a))
|
||||
return true;
|
||||
point del = a - m_xy;
|
||||
unsigned steps = 10;
|
||||
while (steps--) {
|
||||
del /= rational(2);
|
||||
point na = m_xy + del;
|
||||
TRACE("nla_solver_tp", tout << "del = " << del << std::endl;);
|
||||
if (plane_is_correct_cut(na)) {
|
||||
a = na;
|
||||
TRACE("nla_solver_tp", tout << "exit";tout << std::endl;);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
rational tang_plane(const point& a) const {
|
||||
return a.x * m_xy.y + a.y * m_xy.x - a.x * a.y;
|
||||
}
|
||||
|
||||
void get_tang_points() {
|
||||
get_initial_tang_points();
|
||||
TRACE("nla_solver", tout << "xy = " << m_xy << ", correct val = " << m_correct_v;
|
||||
tout << "\ntang points:"; print_tangent_domain(tout);tout << std::endl;);
|
||||
bool all_ints = m_v.is_int() && m_xy.x.is_int() && m_xy.y.is_int();
|
||||
if (!all_ints) {
|
||||
m_a_is_ok = pull_tang_point(m_a);
|
||||
m_b_is_ok = pull_tang_point(m_b);
|
||||
} else {
|
||||
m_a_is_ok = m_b_is_ok = true;
|
||||
}
|
||||
if (m_a_is_ok) {
|
||||
push_tang_point(m_a);
|
||||
TRACE("nla_solver", tout << "pushed a = " << m_a << std::endl;);
|
||||
}
|
||||
if (m_b_is_ok) {
|
||||
push_tang_point(m_b);
|
||||
TRACE("nla_solver", tout << "pushed b = " << m_b << std::endl;);
|
||||
}
|
||||
TRACE("nla_solver",
|
||||
if (m_a_is_ok) { tout << "tang_plane(a) = " << tang_plane(m_a) << " , val = " << m_v; }
|
||||
if (m_b_is_ok) { tout << "\ntang_plane(b) = " << tang_plane(m_b) << " , val = " << m_v << std::endl;});
|
||||
}
|
||||
|
||||
std::ostream& print_tangent_domain(std::ostream& out) {
|
||||
if (m_a_is_ok && m_b_is_ok) {
|
||||
out << "(" << m_a << ", " << m_b << ")";
|
||||
} else if (m_a_is_ok) {
|
||||
out << m_a;
|
||||
}
|
||||
else if (m_b_is_ok) {
|
||||
out << m_b;
|
||||
} else {
|
||||
out << "no a, no b";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
bool plane_is_correct_cut(const point& plane) const {
|
||||
TRACE("nla_solver", tout << "plane = " << plane << "\n";
|
||||
tout << "tang_plane() = " << tang_plane(plane) << ", v = " << m_v << ", correct_v = " << m_correct_v << "\n";);
|
||||
SASSERT((m_below && m_v < m_correct_v) ||
|
||||
((!m_below) && m_v > m_correct_v));
|
||||
rational sign = m_below? rational(1) : rational(-1);
|
||||
rational px = tang_plane(plane);
|
||||
return ((m_correct_v - px)*sign).is_pos() && !((px - m_v)*sign).is_neg();
|
||||
}
|
||||
};
|
||||
|
||||
tangents::tangents(core * c) : common(c, nullptr) {}
|
||||
|
||||
void tangents::tangent_lemma() {
|
||||
if (!c().m_nla_settings.run_tangents()) {
|
||||
TRACE("nla_solver", tout << "not generating tangent lemmas\n";);
|
||||
|
|
@ -37,7 +223,28 @@ void tangents::tangent_lemma() {
|
|||
factorization bf(nullptr);
|
||||
const monic* m;
|
||||
if (c().find_bfc_to_refine(m, bf)) {
|
||||
tangent_lemma_bf(*m, bf);
|
||||
unsigned lemmas_size_was = c().m_lemma_vec->size();
|
||||
unsigned j = m->var();
|
||||
imp i(point(val(bf[0]), val(bf[1])),
|
||||
c().val(j),
|
||||
j,
|
||||
*m,
|
||||
bf[0],
|
||||
bf[1],
|
||||
*this);
|
||||
i.tangent_lemma_on_bf();
|
||||
if (!bf.is_mon()) {
|
||||
lp::explanation expl;
|
||||
generate_explanations_of_tang_lemma(*m, bf, expl);
|
||||
for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++) {
|
||||
auto &l = ((*c().m_lemma_vec)[i]);
|
||||
l.expl().add(expl);
|
||||
}
|
||||
}
|
||||
TRACE("nla_solver",
|
||||
for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++)
|
||||
c().print_specific_lemma((*c().m_lemma_vec)[i], tout); );
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -48,134 +255,4 @@ void tangents::generate_explanations_of_tang_lemma(const monic& rm, const factor
|
|||
c().explain(bf[1], exp);
|
||||
}
|
||||
|
||||
void tangents::generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j) {
|
||||
lpvar jx = var(x);
|
||||
lpvar jy = var(y);
|
||||
add_empty_lemma();
|
||||
c().negate_relation(jx, a);
|
||||
c().negate_relation(jy, b);
|
||||
#if Z3DEBUG
|
||||
int mult_sign = nla::rat_sign(a - val(jx))*nla::rat_sign(b - val(jy));
|
||||
SASSERT((mult_sign == 1) == below);
|
||||
// If "mult_sign is 1" then (a - x)(b-y) > 0 and ab - bx - ay + xy > 0
|
||||
// or -ab + bx + ay < xy or -ay - bx + xy > -ab
|
||||
// val(j) stands for xy. So, finally we have -ay - bx + j > - ab
|
||||
#endif
|
||||
|
||||
lp::lar_term t;
|
||||
t.add_monomial(-a, jy);
|
||||
t.add_monomial(-b, jx);
|
||||
t.add_var(j);
|
||||
c().mk_ineq(t, below? llc::GT : llc::LT, - a*b);
|
||||
}
|
||||
|
||||
void tangents::tangent_lemma_bf(const monic& m, const factorization& bf){
|
||||
point a, b;
|
||||
point xy (val(bf[0]), val(bf[1]));
|
||||
rational correct_mult_val = xy.x * xy.y;
|
||||
lpvar j =m.var();
|
||||
SASSERT(canonize_sign(bf) == canonize_sign(m));
|
||||
rational v = val(j);
|
||||
bool below = v < correct_mult_val;
|
||||
TRACE("nla_solver", tout << "below = " << below << std::endl; );
|
||||
get_tang_points(a, b, below, v, xy);
|
||||
TRACE("nla_solver", tout << "tang domain = "; print_tangent_domain(a, b, tout); tout << std::endl;);
|
||||
unsigned lemmas_size_was = c().m_lemma_vec->size();
|
||||
rational sign(1);
|
||||
generate_two_tang_lines(bf, xy, j);
|
||||
generate_tang_plane(a.x, a.y, bf[0], bf[1], below, j);
|
||||
generate_tang_plane(b.x, b.y, bf[0], bf[1], below, j);
|
||||
|
||||
if (!bf.is_mon()) {
|
||||
lp::explanation expl;
|
||||
generate_explanations_of_tang_lemma(m, bf, expl);
|
||||
for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++) {
|
||||
auto &l = ((*c().m_lemma_vec)[i]);
|
||||
l.expl().add(expl);
|
||||
}
|
||||
}
|
||||
TRACE("nla_solver",
|
||||
for (unsigned i = lemmas_size_was; i < c().m_lemma_vec->size(); i++)
|
||||
c().print_specific_lemma((*c().m_lemma_vec)[i], tout); );
|
||||
}
|
||||
|
||||
|
||||
void tangents::generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j) {
|
||||
add_empty_lemma();
|
||||
c().mk_ineq(var(bf[0]), llc::NE, xy.x);
|
||||
c().mk_ineq(j, - xy.x, var(bf[1]), llc::EQ);
|
||||
|
||||
add_empty_lemma();
|
||||
c().mk_ineq(var(bf[1]), llc::NE, xy.y);
|
||||
c().mk_ineq(j, - xy.y, var(bf[0]), llc::EQ);
|
||||
}
|
||||
|
||||
// Get two planes tangent to surface z = xy, one at point a, and another at point b.
|
||||
// One can show that these planes still create a cut.
|
||||
void tangents::get_initial_tang_points(point &a, point &b, const point& xy,
|
||||
bool below) const {
|
||||
const rational& x = xy.x;
|
||||
const rational& y = xy.y;
|
||||
if (!below){
|
||||
a = point(x - rational(1), y + rational(1));
|
||||
b = point(x + rational(1), y - rational(1));
|
||||
}
|
||||
else {
|
||||
a = point(x - rational(1), y - rational(1));
|
||||
b = point(x + rational(1), y + rational(1));
|
||||
}
|
||||
}
|
||||
|
||||
void tangents::push_tang_point(point &a, const point& xy, bool below, const rational& correct_val, const rational& val) const {
|
||||
SASSERT(correct_val == xy.x * xy.y);
|
||||
int steps = 10;
|
||||
point del = a - xy;
|
||||
while (steps--) {
|
||||
del *= rational(2);
|
||||
point na = xy + del;
|
||||
TRACE("nla_solver_tp", tout << "del = " << del << std::endl;);
|
||||
if (!plane_is_correct_cut(na, xy, correct_val, val, below)) {
|
||||
TRACE("nla_solver_tp", tout << "exit";tout << std::endl;);
|
||||
return;
|
||||
}
|
||||
a = na;
|
||||
}
|
||||
}
|
||||
|
||||
void tangents::push_tang_points(point &a, point &b, const point& xy, bool below, const rational& correct_val, const rational& val) const {
|
||||
push_tang_point(a, xy, below, correct_val, val);
|
||||
push_tang_point(b, xy, below, correct_val, val);
|
||||
}
|
||||
|
||||
rational tangents::tang_plane(const point& a, const point& x) const {
|
||||
return a.x * x.y + a.y * x.x - a.x * a.y;
|
||||
}
|
||||
|
||||
bool tangents:: plane_is_correct_cut(const point& plane,
|
||||
const point& xy,
|
||||
const rational & correct_val,
|
||||
const rational & val,
|
||||
bool below) const {
|
||||
SASSERT(correct_val == xy.x * xy.y);
|
||||
if (below && val > correct_val) return false;
|
||||
rational sign = below? rational(1) : rational(-1);
|
||||
rational px = tang_plane(plane, xy);
|
||||
return ((correct_val - px)*sign).is_pos() && !((px - val)*sign).is_neg();
|
||||
|
||||
}
|
||||
|
||||
// "below" means that the val is below the surface xy
|
||||
void tangents::get_tang_points(point &a, point &b, bool below, const rational& val,
|
||||
const point& xy) const {
|
||||
get_initial_tang_points(a, b, xy, below);
|
||||
auto correct_val = xy.x * xy.y;
|
||||
TRACE("nla_solver", tout << "xy = " << xy << ", correct val = " << xy.x * xy.y;
|
||||
tout << "\ntang points:"; print_tangent_domain(a, b, tout);tout << std::endl;);
|
||||
TRACE("nla_solver", tout << "tang_plane(a, xy) = " << tang_plane(a, xy) << " , val = " << val;
|
||||
tout << "\ntang_plane(b, xy) = " << tang_plane(b, xy); tout << std::endl;);
|
||||
SASSERT(plane_is_correct_cut(a, xy, correct_val, val, below));
|
||||
SASSERT(plane_is_correct_cut(b, xy, correct_val, val, below));
|
||||
push_tang_points(a, b, xy, below, correct_val, val);
|
||||
TRACE("nla_solver", tout << "pushed a = " << a << "\npushed b = " << b << std::endl;);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,6 +35,11 @@ struct point {
|
|||
y *= a;
|
||||
return *this;
|
||||
}
|
||||
inline point& operator/=(rational a) {
|
||||
x /= a;
|
||||
y /= a;
|
||||
return *this;
|
||||
}
|
||||
inline point operator+(const point& b) const {
|
||||
return point(x + b.x, y + b.y);
|
||||
}
|
||||
|
|
@ -47,37 +52,9 @@ struct point {
|
|||
inline std::ostream& operator<<(std::ostream& out, point const& a) { return out << "(" << a.x << ", " << a.y << ")"; }
|
||||
|
||||
|
||||
class tangents : common {
|
||||
public:
|
||||
struct tangents : common {
|
||||
tangents(core *core);
|
||||
void tangent_lemma();
|
||||
private:
|
||||
lpvar find_binomial_to_refine();
|
||||
void generate_explanations_of_tang_lemma(const monic& m, const factorization& bf, lp::explanation& exp);
|
||||
void generate_simple_tangent_lemma(const monic& m, const factorization&);
|
||||
void tangent_lemma_bf(const monic& m,const factorization& bf);
|
||||
void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j);
|
||||
|
||||
void generate_two_tang_lines(const factorization & bf, const point& xy, lpvar j);
|
||||
// Get two planes tangent to surface z = xy, one at point a, and another at point b.
|
||||
// One can show that these planes still create a cut.
|
||||
void get_initial_tang_points(point &a, point &b, const point& xy, bool below) const;
|
||||
|
||||
void push_tang_point(point &a, const point& xy, bool below, const rational& correct_val, const rational& val) const;
|
||||
|
||||
void push_tang_points(point &a, point &b, const point& xy, bool below, const rational& correct_val, const rational& val) const;
|
||||
|
||||
rational tang_plane(const point& a, const point& x) const;
|
||||
void get_tang_points(point &a, point &b, bool below, const rational& val, const point& xy) const;
|
||||
std::ostream& print_point(const point &a, std::ostream& out) const;
|
||||
std::ostream& print_tangent_domain(const point &a, const point &b, std::ostream& out) const;
|
||||
// "below" means that the val is below the surface xy
|
||||
bool plane_is_correct_cut(const point& plane,
|
||||
const point& xy,
|
||||
const rational & correct_val,
|
||||
const rational & val,
|
||||
bool below) const;
|
||||
template <typename T> rational val(T const& t) const;
|
||||
template <typename T> lpvar var(T const& t) const { return t.var(); }
|
||||
void tangent_lemma();
|
||||
void generate_explanations_of_tang_lemma(const monic& rm, const factorization& bf, lp::explanation& exp);
|
||||
}; // end of tangents
|
||||
}
|
||||
} // end of namespace
|
||||
|
|
|
|||
|
|
@ -1735,19 +1735,36 @@ public:
|
|||
bool is_int = offset.is_int();
|
||||
u_map<rational> coeffs;
|
||||
term2coeffs(term, coeffs);
|
||||
TRACE("arith",
|
||||
lp().print_term(term, tout << "term: ") << "\n";
|
||||
for (auto const& kv : coeffs) {
|
||||
tout << "v" << kv.m_key << " * " << kv.m_value << "\n";
|
||||
TRACE("arith",
|
||||
{
|
||||
bool all_ints = true;
|
||||
lp().print_term(term, tout << "term: ") << "\n";
|
||||
for (auto const& kv : coeffs) {
|
||||
if (kv.m_value.is_int() == false)
|
||||
all_ints = false;
|
||||
tout << "v" << kv.m_key << " * " << kv.m_value << "\n";
|
||||
}
|
||||
tout << offset << "\n";
|
||||
if (all_ints) {
|
||||
rational g(0);
|
||||
for (auto const& kv : coeffs) {
|
||||
g = gcd(g, kv.m_value);
|
||||
}
|
||||
tout << "gcd: " << g << "\n";
|
||||
}
|
||||
}
|
||||
tout << offset << "\n";
|
||||
rational g(0);
|
||||
for (auto const& kv : coeffs) {
|
||||
g = gcd(g, kv.m_value);
|
||||
}
|
||||
tout << "gcd: " << g << "\n";
|
||||
);
|
||||
bool all_ints = true;
|
||||
if (is_int) {
|
||||
for (auto const& kv : coeffs) {
|
||||
if (kv.m_value.is_int() == false) {
|
||||
all_ints = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (is_int && all_ints) {
|
||||
// 3x + 6y >= 5 -> x + 3y >= 5/3, then x + 3y >= 2
|
||||
// 3x + 6y <= 5 -> x + 3y <= 1
|
||||
|
||||
|
|
|
|||
|
|
@ -717,6 +717,34 @@ void test_monotone_lemma() {
|
|||
*/
|
||||
}
|
||||
|
||||
void test_tangent_lemma_rat() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
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, false, "b");
|
||||
lpvar lp_ab = s.add_named_var(ab, false, "ab");
|
||||
s_set_column_value(s, lp_a, rational(3));
|
||||
s_set_column_value(s, lp_b, rational(4));
|
||||
rational v = rational(12) + rational (1)/rational(7);
|
||||
s_set_column_value(s, lp_ab, v);
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// create monomial ab
|
||||
vector<unsigned> vec;
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_b);
|
||||
nla.add_monic(lp_ab, vec.size(), vec.begin());
|
||||
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
void test_tangent_lemma_reg() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
|
|
@ -793,7 +821,8 @@ void test_tangent_lemma_equiv() {
|
|||
|
||||
|
||||
void test_tangent_lemma() {
|
||||
test_tangent_lemma_reg();
|
||||
test_tangent_lemma_rat();
|
||||
test_tangent_lemma_reg();
|
||||
test_tangent_lemma_equiv();
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue