mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #6969

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-29 17:43:14 -07:00
parent 9d57bdd2ef
commit 589024aa1c
2 changed files with 20 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/math/lp/nla_grobner.cpp
View file

@ -199,14 +199,22 @@ namespace nla {
// IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n"); // IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
term t; term t;
rational lc(1);
auto ql = q;
while (!ql.is_val()) {
lc = lcm(lc, denominator(ql.hi().val()));
ql = q.lo();
}
lc = lcm(denominator(ql.val()), lc);
while (!q.is_val()) { while (!q.is_val()) {
t.add_monomial(q.hi().val(), q.var()); t.add_monomial(lc*q.hi().val(), q.var());
q = q.lo(); q = q.lo();
} }
vector<ineq> ineqs; vector<ineq> ineqs;
for (auto v : vars) for (auto v : vars)
ineqs.push_back(ineq(v, llc::EQ, rational::zero())); ineqs.push_back(ineq(v, llc::EQ, rational::zero()));
ineqs.push_back(ineq(t, llc::EQ, -q.val())); ineqs.push_back(ineq(t, llc::EQ, -lc*q.val()));
for (auto const& i : ineqs) for (auto const& i : ineqs)
if (c().ineq_holds(i)) if (c().ineq_holds(i))
return false; return false;

17
src/smt/theory_lra.cpp
View file

@ -589,11 +589,15 @@ class theory_lra::imp {
void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) { void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";); TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";);
ctx().mk_th_axiom(get_id(), l1, l2, num_params, params); // static unsigned num_bin = 0;
// std::cout << "binary " << (num_bin++) << "\n";
ctx().mk_th_lemma(get_id(), l1, l2, num_params, params);
} }
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) { void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; ctx().display_literals_smt2(tout, 3, lits); tout << "\n";); TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; ctx().display_literals_smt2(tout, 3, lits); tout << "\n";);
static unsigned num_ter = 0;
std::cout << "ternary " << (num_ter++) << "\n";
ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params); ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params);
} }
@ -3342,7 +3346,7 @@ public:
// The lemmas can come in batches // The lemmas can come in batches
// and the same literal can appear in several lemmas in a batch: it becomes l_true // and the same literal can appear in several lemmas in a batch: it becomes l_true
// in earlier processing, but it was not so when the lemma was produced // in earlier processing, but it was not so when the lemma was produced
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data()); ctx().mk_th_lemma(get_id(), m_core.size(), m_core.data());
} }
} }
@ -3703,17 +3707,16 @@ public:
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) { app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
expr_ref_vector args(m); expr_ref_vector args(m);
for (auto const& kv : coeffs) { for (auto const& [w, coeff] : coeffs) {
theory_var w = kv.m_key;
expr* o = get_enode(w)->get_expr(); expr* o = get_enode(w)->get_expr();
if (kv.m_value.is_zero()) { if (coeff.is_zero()) {
// continue // continue
} }
else if (kv.m_value.is_one()) { else if (coeff.is_one()) {
args.push_back(o); args.push_back(o);
} }
else { else {
args.push_back(a.mk_mul(a.mk_numeral(kv.m_value, is_int), o)); args.push_back(a.mk_mul(a.mk_numeral(coeff, is_int), o));
} }
} }
if (!offset.is_zero()) { if (!offset.is_zero()) {