mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

code review of tangent lemmas (#94)

Browse source 
* code reviewing order lemmas

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* code review monotonity

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* cr tangent

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* cr tangent

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-20 13:49:20 -07:00 • committed by Lev Nachmanson
parent c97a6dd7cb
commit c327f8799b
2 changed files with 17 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/util/lp/nla_tangent_lemmas.cpp
View file

@ -24,15 +24,12 @@ namespace nla {
template <typename T> rational tangents::vvr(T const& t) const { return m_core->vvr(t); } template <typename T> rational tangents::vvr(T const& t) const { return m_core->vvr(t); }
tangents::tangents(core * c) : common(c) {} tangents::tangents(core * c) : common(c) {}
std::ostream& tangents::print_point(const point &a, std::ostream& out) const {
out << "(" << a.x << ", " << a.y << ")";
return out;
}
std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std::ostream& out) const { std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std::ostream& out) const {
out << "("; print_point(a, out); out << ", "; print_point(b, out); out << ")"; return out << "(" << a << ", " << b << ")";
return out;
} }
void tangents::generate_simple_tangent_lemma(const smon* rm) { void tangents::generate_simple_tangent_lemma(const smon* rm) {
if (rm->size() != 2) if (rm->size() != 2)
return; return;
@ -172,7 +169,7 @@ void tangents::push_tang_point(point &a, const point& xy, bool below, const rati
while (steps--) { while (steps--) {
del *= rational(2); del *= rational(2);
point na = xy + del; point na = xy + del;
TRACE("nla_solver", tout << "del = "; print_point(del, tout); tout << std::endl;); TRACE("nla_solver", tout << "del = " << del << std::endl;);
if (!plane_is_correct_cut(na, xy, correct_val, val, below)) { if (!plane_is_correct_cut(na, xy, correct_val, val, below)) {
TRACE("nla_solver_tp", tout << "exit";tout << std::endl;); TRACE("nla_solver_tp", tout << "exit";tout << std::endl;);
return; return;
@ -208,14 +205,14 @@ void tangents::get_tang_points(point &a, point &b, bool below, const rational& v
const point& xy) const { const point& xy) const {
get_initial_tang_points(a, b, xy, below); get_initial_tang_points(a, b, xy, below);
auto correct_val = xy.x * xy.y; auto correct_val = xy.x * xy.y;
TRACE("nla_solver", tout << "xy = "; print_point(xy, tout); tout << ", 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;); 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; 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;); 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(a, xy, correct_val, val, below));
SASSERT(plane_is_correct_cut(b, 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); push_tang_points(a, b, xy, below, correct_val, val);
TRACE("nla_solver", tout << "pushed a = "; print_point(a, tout); tout << "\npushed b = "; print_point(b, tout); tout << std::endl;); TRACE("nla_solver", tout << "pushed a = " << a << "\npushed b = " << b << std::endl;);
} }
} }

11
src/util/lp/nla_tangent_lemmas.h
View file

@ -25,7 +25,7 @@
namespace nla { namespace nla {
class core; class core;
struct tangents: common {
struct point { struct point {
rational x; rational x;
rational y; rational y;
@ -45,12 +45,17 @@ struct tangents: common {
} }
}; };
inline std::ostream& operator<<(std::ostream& out, point const& a) { return out << "(" << a.x << ", " << a.y << ")"; }
class tangents : common {
public:
tangents(core *core); tangents(core *core);
void tangent_lemma();
private:
void generate_simple_tangent_lemma(const smon* rm); void generate_simple_tangent_lemma(const smon* rm);
void tangent_lemma();
void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp); void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp);
void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm); void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm);