mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #6637

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-22 08:49:33 +01:00
parent 53ca65a62e
commit 2683a2d6ed
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_divisions.cpp
View file

@ -58,10 +58,11 @@ namespace nla {
auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val, auto monotonicity1 = [&](auto x1, auto& x1val, auto y1, auto& y1val, auto& q1, auto& q1val,
auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) { auto x2, auto& x2val, auto y2, auto& y2val, auto& q2, auto& q2val) {
if (y1val >= y2val && y2val > 0 && x1val <= x2val && q1val > q2val) { if (y1val >= y2val && y2val > 0 && 0 <= x1val && x1val <= x2val && q1val > q2val) {
new_lemma lemma(c, "y1 >= y2 > 0 & x1 <= x2 => x1/y1 <= x2/y2"); new_lemma lemma(c, "y1 >= y2 > 0 & 0 <= x1 <= x2 => x1/y1 <= x2/y2");
lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0); lemma |= ineq(term(y1, rational(-1), y2), llc::LT, 0);
lemma |= ineq(y2, llc::LE, 0); lemma |= ineq(y2, llc::LE, 0);
lemma |= ineq(x1, llc::LT, 0);
lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0); lemma |= ineq(term(x1, rational(-1), x2), llc::GT, 0);
lemma |= ineq(term(q1, rational(-1), q2), llc::LE, 0); lemma |= ineq(term(q1, rational(-1), q2), llc::LE, 0);
return true; return true;

2
src/sat/smt/euf_proof_checker.h
View file

@ -35,7 +35,7 @@ namespace euf {
virtual bool check(app* jst) = 0; virtual bool check(app* jst) = 0;
virtual expr_ref_vector clause(app* jst) = 0; virtual expr_ref_vector clause(app* jst) = 0;
virtual void register_plugins(theory_checker& pc) = 0; virtual void register_plugins(theory_checker& pc) = 0;
virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.reset(); v.append(this->clause(jst)); return false; } virtual bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) { v.append(this->clause(jst)); return false; }
}; };
class theory_checker { class theory_checker {