mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

after rebasing with Z3Prover

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-19 13:04:45 -08:00
parent 0039b68ca3
commit 7eb1affc7b
5 changed files with 21 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/interval/dep_intervals.cpp
View file

@ -172,7 +172,7 @@ template <e_with_deps wd>
dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) { dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) {
interval b; interval b;
if (with_deps == wd) { if (with_deps == wd) {
interval_deps combine_rule; interval_deps_combine_rule combine_rule;
m_imanager.power(a, n, b, combine_rule); m_imanager.power(a, n, b, combine_rule);
combine_deps(a, combine_rule, b); combine_deps(a, combine_rule, b);
} }

24
src/math/interval/dep_intervals.h
View file

@ -54,14 +54,14 @@ private:
u_dependency* m_upper_dep; // justification for the upper bound 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 { 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_deps); 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_deps); 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 { 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_deps); 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_deps); 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) {} im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {}
private: 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; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
@ -120,7 +120,7 @@ private:
return dep; 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; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
@ -148,15 +148,15 @@ private:
template <enum with_deps_t wd> template <enum with_deps_t wd>
void update_upper_for_intersection(const interval& a, const interval& b, interval& i) const; 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 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& deps) { m_imanager.add(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); SASSERT(&a != &i && &b != &i);
m_config.add_deps(a, b, deps, 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); SASSERT(&a != &i);
m_config.add_deps(a, deps, i); m_config.add_deps(a, deps, i);
} }

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

@ -44,7 +44,7 @@ public:
m_grobner_frequency(5), m_grobner_frequency(5),
m_grobner_eqs_threshold(512), m_grobner_eqs_threshold(512),
m_grobner_row_length_limit(10), 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; } unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; }

3
src/smt/theory_lra.cpp
View file

@ -32,7 +32,6 @@
#include "util/cancel_eh.h" #include "util/cancel_eh.h"
#include "util/scoped_timer.h" #include "util/scoped_timer.h"
#include "util/nat_set.h" #include "util/nat_set.h"
#include "util/lp/nra_solver.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "model/numeral_factory.h" #include "model/numeral_factory.h"
#include "smt/smt_theory.h" #include "smt/smt_theory.h"
@ -1079,7 +1078,7 @@ public:
void apply_sort_cnstr(enode* n, sort*) { void apply_sort_cnstr(enode* n, sort*) {
if (!th.is_attached_to_var(n)) { if (!th.is_attached_to_var(n)) {
theory_var v = mk_var(n->get_owner(), false); theory_var v = mk_var(n->get_owner(), false);
get_var_index(v); register_theory_var_in_lar_solver(v);
} }
} }

13
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -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) { tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
return and_then( return and_then(
mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_report_verbose_tactic("(qfnia-tactic)", 10),
mk_qfnia_premable(m, p), mk_qfnia_preamble(m, p),
// or_else(mk_qfnia_sat_solver(m, p), or_else(mk_qfnia_sat_solver(m, p),
// try_for(mk_qfnia_smt_solver(m, p), 2000), try_for(mk_qfnia_smt_solver(m, p), 2000),
// mk_qfnia_nlsat_solver(m, p), mk_qfnia_nlsat_solver(m, p),
mk_qfnia_smt_solver(m, p))
mk_qfnia_smt_solver(m, p)) )
// )
; ;
} }