From 7eb1affc7b6a7f14a59809285aeb954f89918afa Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Dec 2019 13:04:45 -0800 Subject: [PATCH] after rebasing with Z3Prover Signed-off-by: Lev Nachmanson --- src/math/interval/dep_intervals.cpp | 2 +- src/math/interval/dep_intervals.h | 24 ++++++++++++------------ src/math/lp/nla_settings.h | 2 +- src/smt/theory_lra.cpp | 3 +-- src/tactic/smtlogics/qfnia_tactic.cpp | 13 ++++++------- 5 files changed, 21 insertions(+), 23 deletions(-) diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp index e236223e6..fd4379954 100644 --- a/src/math/interval/dep_intervals.cpp +++ b/src/math/interval/dep_intervals.cpp @@ -172,7 +172,7 @@ template dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) { interval b; if (with_deps == wd) { - interval_deps combine_rule; + interval_deps_combine_rule combine_rule; m_imanager.power(a, n, b, combine_rule); combine_deps(a, combine_rule, b); } diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index 77269ce00..5a7521b53 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -54,14 +54,14 @@ private: u_dependency* m_upper_dep; // justification for the upper bound }; - void add_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { - i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_deps); - i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_deps); + void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { + i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine); + i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine); } - void add_deps(interval const& a, interval_deps const& deps, interval& i) const { - i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_deps); - i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_deps); + void add_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const { + i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine); + i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine); } @@ -103,7 +103,7 @@ private: im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} private: - u_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const { + u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { u_dependency* dep = nullptr; if (dep_in_lower1(bd)) { dep = m_dep_manager.mk_join(dep, a.m_lower_dep); @@ -120,7 +120,7 @@ private: return dep; } - u_dependency* mk_dependency(interval const& a, bound_deps bd) const { + u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { u_dependency* dep = nullptr; if (dep_in_lower1(bd)) { dep = m_dep_manager.mk_join(dep, a.m_lower_dep); @@ -148,15 +148,15 @@ private: template void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const; - void mul(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.mul(a, b, c, deps); } - void add(const interval& a, const interval& b, interval& c, interval_deps& deps) { m_imanager.add(a, b, c, deps); } + void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); } + void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } - void combine_deps(interval const& a, interval const& b, interval_deps const& deps, interval& i) const { + void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { SASSERT(&a != &i && &b != &i); m_config.add_deps(a, b, deps, i); } - void combine_deps(interval const& a, interval_deps const& deps, interval& i) const { + void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const { SASSERT(&a != &i); m_config.add_deps(a, deps, i); } diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index d00df150b..772589a2d 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -44,7 +44,7 @@ public: m_grobner_frequency(5), m_grobner_eqs_threshold(512), m_grobner_row_length_limit(10), - m_grobner_expr_size_limit(20) + m_grobner_expr_size_limit(50) {} unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index aa0e33119..89341a7f1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -32,7 +32,6 @@ #include "util/cancel_eh.h" #include "util/scoped_timer.h" #include "util/nat_set.h" -#include "util/lp/nra_solver.h" #include "ast/ast_pp.h" #include "model/numeral_factory.h" #include "smt/smt_theory.h" @@ -1079,7 +1078,7 @@ public: void apply_sort_cnstr(enode* n, sort*) { if (!th.is_attached_to_var(n)) { theory_var v = mk_var(n->get_owner(), false); - get_var_index(v); + register_theory_var_in_lar_solver(v); } } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 4d318eec6..f8335a279 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -117,13 +117,12 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_report_verbose_tactic("(qfnia-tactic)", 10), - mk_qfnia_premable(m, p), - // or_else(mk_qfnia_sat_solver(m, p), - // try_for(mk_qfnia_smt_solver(m, p), 2000), - // mk_qfnia_nlsat_solver(m, p), - - mk_qfnia_smt_solver(m, p)) - // ) + mk_qfnia_preamble(m, p), + or_else(mk_qfnia_sat_solver(m, p), + try_for(mk_qfnia_smt_solver(m, p), 2000), + mk_qfnia_nlsat_solver(m, p), + mk_qfnia_smt_solver(m, p)) + ) ; }