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

debug output with the variable that is fixed and its value

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-27 00:52:26 -07:00
parent 2297b0334b
commit 9033b826f4
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_arith_nl.h
View file

@ -765,10 +765,8 @@ typename theory_arith<Ext>::numeral theory_arith<Ext>::get_monomial_fixed_var_pr
template<typename Ext>
expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg);
if (!is_fixed(_var))
for (expr* arg : *to_app(m)) {
if (!is_fixed(expr2var(arg)))
return arg;
}
return nullptr;
@ -780,7 +778,7 @@ expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
TRACE("non_linear", tout << "checking whether v" << v << " became linear...\n";);
TRACE("non_linear_verbose", tout << "checking whether v" << v << " became linear...\n";);
if (m_data[v].m_nl_propagated)
return false; // already propagated this monomial.
expr * m = var2expr(v);
@ -819,6 +817,11 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
ctx.mark_as_relevant(rhs);
}
TRACE("non_linear_bug", tout << "enode: " << ctx.get_enode(rhs) << " enode_id: " << ctx.get_enode(rhs)->get_owner_id() << "\n";);
IF_VERBOSE(3,
for (auto* arg : *to_app(m))
if (is_fixed(expr2var(arg)))
verbose_stream() << mk_pp(arg, get_manager()) << " = " << -k << "\n");
theory_var new_v = expr2var(rhs);
SASSERT(new_v != null_theory_var);
new_lower = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
@ -906,7 +909,7 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
return false;
if (!reflection_enabled())
return false;
TRACE("non_linear", tout << "propagating linear monomials...\n";);
TRACE("non_linear_verbose", tout << "propagating linear monomials...\n";);
bool p = false;
// CMW: m_nl_monomials can grow during this loop, so
// don't use iterators.