z3/src/math/lp/horner.cpp

/*++
  Copyright (c) 2017 Microsoft Corporation

  Module Name:

  <name>

  Abstract:

  <abstract>

  Author:
  Nikolaj Bjorner (nbjorner)
  Lev Nachmanson (levnach)

  Revision History:


  --*/

#include "math/lp/horner.h"
#include "math/lp/nla_core.h"
#include "math/lp/lp_utils.h"
#include "math/lp/cross_nested.h"

namespace nla {
typedef intervals::interval interv;
horner::horner(core * c, intervals * i) : common(c, i), m_row_sum(m_nex_creator), m_fixed_as_scalars(false) {}

template <typename T>
bool horner::row_has_monomial_to_refine(const T& row) const {
    for (const auto& p : row) {
        if (c().m_to_refine.contains(p.var()))
            return true;
    }
    return false;
}

// Returns true if the row has at least two monomials sharing a variable
template <typename T>
bool horner::row_is_interesting(const T& row) const {
    TRACE("nla_solver_details", m_core->print_term(row, tout););
    if (row.size() > m_core->m_nla_settings.horner_row_length_limit()) {
        TRACE("nla_solver_details", tout << "disregard\n";);
        return false;
    }
    SASSERT(row_has_monomial_to_refine(row));
    c().clear_active_var_set();
    for (const auto& p : row) {
        lpvar j = p.var();
        if (!c().is_monic_var(j))
            continue;
        auto & m = c().emons()[j];
        
        for (lpvar k : m.vars()) {
            if (c().active_var_set_contains(k))
                return true;
        }
        for (lpvar k : m.vars()) {
            c().insert_to_active_var_set(k);
        }
    }
    return false;
}

bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
    TRACE("nla_horner", tout << "e = " << *e << "\n";);
    cn.run(e);
    return cn.done();
}

template <typename T> 
bool horner::lemmas_on_row(const T& row) {
    cross_nested cn(
        [this](const nex* n) { return m_intervals->check_nex(n,  m_fixed_as_scalars? get_fixed_vars_dep_from_row(c().m_lar_solver.A_r().m_rows[m_row_index], m_intervals->dep_manager()) : nullptr); },
        [this](unsigned j)   { return c().var_is_fixed(j); },
        [this]() { return c().random(); }, m_nex_creator);

    SASSERT (row_is_interesting(row));
    c().clear_and_resize_active_var_set();
    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars, nullptr);
    set_active_vars_weights(); // without this call the comparisons will be incorrect
    nex* e =  m_nex_creator.simplify(m_row_sum.mk());
    TRACE("nla_horner", tout << "e = " << * e << "\n";);
    if (e->get_degree() < 2)
        return false;
    if (!e->is_sum())
        return false;
    
    return lemmas_on_expr(cn, to_sum(e));
}

void horner::horner_lemmas() {
    if (!c().m_nla_settings.run_horner()) {
        TRACE("nla_solver", tout << "not generating horner lemmas\n";);
        return;
    }
    c().lp_settings().stats().m_horner_calls++;
    const auto& matrix = c().m_lar_solver.A_r();
    // choose only rows that depend on m_to_refine variables
    std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set
    for (lpvar j : c().m_to_refine) {
        for (auto & s : matrix.m_columns[j])
            rows_to_check.insert(s.var());
    }
    c().clear_and_resize_active_var_set();
    svector<unsigned> rows;
    for (unsigned i : rows_to_check) {
        if (row_is_interesting(matrix.m_rows[i]))
            rows.push_back(i);
    }

    unsigned r = c().random();
    unsigned sz = rows.size();
    for (unsigned i = 0; i < sz; i++) {
        m_row_index = rows[(i + r) % sz];
        if (lemmas_on_row(matrix.m_rows[m_row_index])) {
            c().lp_settings().stats().m_horner_conflicts++;
            break;
        }
    }
}
}