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

add stubs to the nla_grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-04 12:27:05 -07:00
parent d08d381115
commit bfcfc517fe
7 changed files with 53 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/CMakeLists.txt
View file

@ -29,6 +29,7 @@ z3_add_component(lp
nla_basics_lemmas.cpp
nla_common.cpp
nla_core.cpp
nla_grobner.cpp
nla_intervals.cpp
nla_monotone_lemmas.cpp
nla_order_lemmas.cpp

2
src/math/lp/nex.h
View file

@ -56,7 +56,7 @@ public:
return false;
default:
return true;
}
}
}
bool is_sum() const { return type() == expr_type::SUM; }

33
src/math/lp/nla_core.cpp
View file

@ -30,6 +30,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_order(this),
m_monotone(this),
m_horner(this),
m_grobner(this),
m_emons(m_evars),
m_reslim(lim)
{}
@ -1249,24 +1250,18 @@ bool core::conflict_found() const {
bool core::done() const {
return m_lemma_vec->size() >= 10 || conflict_found();
}
lbool core::inner_check(bool derived) {
if (derived && (lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0))
m_horner.horner_lemmas();
if (done()) {
return l_false;
}
lbool core::incremental_linearization(bool constraint_derived) {
TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout););
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";);
if (search_level == 0) {
m_basics.basic_lemma(derived);
m_basics.basic_lemma(constraint_derived);
if (!m_lemma_vec->empty())
return l_false;
}
if (derived) continue;
TRACE("nla_solver", tout << "passed derived and basic lemmas\n";);
if (constraint_derived) continue;
TRACE("nla_solver", tout << "passed constraint_derived and basic lemmas\n";);
SASSERT(elists_are_consistent(true));
if (search_level == 1) {
m_order.order_lemma();
@ -1277,6 +1272,20 @@ lbool core::inner_check(bool derived) {
}
return m_lemma_vec->empty()? l_undef : l_false;
}
// constraint_derived is set to true when we do not use the model values to
// obtain the lemmas
lbool core::inner_check(bool constraint_derived) {
if (constraint_derived) {
if (need_to_call_horner())
m_horner.horner_lemmas();
else if (need_to_call_grobner())
m_grobner.grobner_lemmas();
if (done()) {
return l_false;
}
}
return incremental_linearization(constraint_derived);
}
bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
bool first = true;

11
src/math/lp/nla_core.h
View file

@ -29,6 +29,7 @@
#include "math/lp/nla_settings.h"
#include "math/lp/nex.h"
#include "math/lp/horner.h"
#include "math/lp/nla_grobner.h"
namespace nla {
template <typename A, typename B>
@ -76,19 +77,19 @@ public:
bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
};
class core {
public:
var_eqs<emonomials> m_evars;
lp::lar_solver& m_lar_solver;
vector<lemma> * m_lemma_vec;
lp::int_set m_to_refine;
lp::int_set m_to_refine;
tangents m_tangents;
basics m_basics;
order m_order;
monotone m_monotone;
horner m_horner;
nla_settings m_settings;
nla_grobner m_grobner;
private:
emonomials m_emons;
svector<lpvar> m_add_buffer;
@ -124,6 +125,12 @@ public:
lpvar var(const factor& f) const { return f.var(); }
bool need_to_call_horner() const { return lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0; }
bool need_to_call_grobner() const { return lp_settings().st().m_nla_calls % m_settings.grobner_frequency() == 0; }
lbool incremental_linearization(bool);
svector<lpvar> sorted_rvars(const factor& f) const;
bool done() const;

4
src/math/lp/nla_params.pyg
View file

@ -5,7 +5,9 @@ def_module_params('nla',
('tangents', BOOL, True, 'run tangent lemmas'),
('horner', BOOL, True, 'run horner\'s heuristic'),
('horner_frequency', UINT, 4, 'horner\'s call frequency'),
('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value')
('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
('grobner', BOOL, True, 'run grobner\'s heuristic'),
('grobner_frequency', UINT, 5, 'grobner\'s call frequency')
))

19
src/math/lp/nla_settings.h
View file

@ -21,18 +21,23 @@ Revision History:
#pragma once
namespace nla {
class nla_settings {
bool m_run_order;
bool m_run_tangents;
bool m_run_horner;
bool m_run_order;
bool m_run_tangents;
bool m_run_horner;
// how often to call the horner heuristic
unsigned m_horner_frequency;
unsigned m_horner_row_length_limit;
bool m_run_grobner;
unsigned m_grobner_frequency;
public:
nla_settings() : m_run_order(true),
m_run_tangents(true),
m_run_horner(true),
m_horner_frequency(4),
m_horner_row_length_limit(10)
m_horner_row_length_limit(10),
m_run_grobner(true),
m_grobner_frequency(5)
{}
bool run_order() const { return m_run_order; }
@ -48,5 +53,11 @@ public:
unsigned& horner_frequency() { return m_horner_frequency; }
unsigned horner_row_length_limit() const { return m_horner_row_length_limit; }
unsigned& horner_row_length_limit() { return m_horner_row_length_limit; }
bool run_grobner() const { return m_run_grobner; }
bool& run_grobner() { return m_run_grobner; }
unsigned grobner_frequency() const { return m_grobner_frequency; }
unsigned& grobner_frequency() { return m_grobner_frequency; }
};
}

4
src/smt/theory_lra.cpp
View file

@ -452,7 +452,9 @@ class theory_lra::imp {
m_nla->get_core()->m_settings.run_tangents() = nla.tangents();
m_nla->get_core()->m_settings.run_horner() = nla.horner();
m_nla->get_core()->m_settings.horner_frequency() = nla.horner_frequency();
m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit();
m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit();
m_nla->get_core()->m_settings.grobner_frequency() = nla.grobner_frequency();
m_nla->get_core()->m_settings.run_grobner() = nla.grobner();
}
}