mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

install importlib-resources for ubuntu doc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-04 10:30:12 -08:00
parent 17913f3ec8
commit f7415bb677
3 changed files with 23 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/release.yml
View file

@ -133,6 +133,7 @@ stages:
pool:
vmImage: "ubuntu-latest"
steps:
- script: pip3 install importlib-resources
- script: sudo apt-get install ocaml opam libgmp-dev
- script: opam init -y
- script: eval `opam config env`; opam install zarith ocamlfind -y

10
src/math/lp/nla_grobner.cpp
View file

@ -399,7 +399,7 @@ namespace nla {
for (auto eq : m_solver.equations())
if (propagate_linear_equations(*eq))
++changed;
#if 0
#if 1
for (auto eq : m_solver.equations())
if (check_missed_bound(*eq))
return true;
@ -419,15 +419,15 @@ namespace nla {
if (vars.empty())
di.add(coeff, i);
else {
di.set_value(t, rational::one());
di.set_value(t, coeff);
for (auto v : vars) {
set_var_interval(v, s);
di.mul<dd::w_dep::with_deps>(coeff, s, s);
di.add<dd::w_dep::with_deps>(t, s, t);
di.mul<dd::w_dep::with_deps>(t, s, t);
}
if (m_mon2var.find(vars) != m_mon2var.end()) {
auto v = m_mon2var.find(vars)->second;
set_var_interval(v, u);
di.mul<dd::w_dep::with_deps>(coeff, u, u);
di.intersect<dd::w_dep::with_deps>(t, u, t);
}
di.add<dd::w_dep::with_deps>(i, t, i);
@ -435,6 +435,8 @@ namespace nla {
}
if (!di.separated_from_zero(i))
return false;
// m_solver.display(verbose_stream() << "missed bound\n", e);
// exit(1);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
new_lemma lemma(m_core, "pdd");
lemma &= e;

29
src/sat/smt/array_axioms.cpp
View file

@ -409,6 +409,11 @@ namespace array {
def1 = a.mk_default(store);
def2 = a.mk_default(store->get_arg(0));
prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
euf::enode* ndef1 = e_internalize(def1);
euf::enode* ndef2 = e_internalize(def2);
if (has_unitary_domain(store)) {
def2 = store->get_arg(num_args - 1);
}
@ -417,8 +422,8 @@ namespace array {
// let A = store(B, i, v)
//
// Add:
// default(A) = ite(epsilon1 = i, v, default(B))
// A[diag(i)] = B[diag(i)]
// default(A) = A[epsilon]
// default(B) = B[epsilon]
//
expr_ref_vector eqs(m);
expr_ref_vector args1(m), args2(m);
@ -428,22 +433,20 @@ namespace array {
for (unsigned i = 1; i + 1 < num_args; ++i) {
expr* arg = store->get_arg(i);
sort* srt = arg->get_sort();
auto ep = mk_epsilon(srt);
eqs.push_back(m.mk_eq(ep.first, arg));
args1.push_back(m.mk_app(ep.second, arg));
args2.push_back(m.mk_app(ep.second, arg));
auto [ep, d] = mk_epsilon(srt);
eqs.push_back(m.mk_eq(ep, arg));
args1.push_back(ep);
args2.push_back(ep);
}
expr_ref eq(m.mk_and(eqs), m);
def2 = m.mk_ite(eq, store->get_arg(num_args - 1), def2);
app_ref sel1(m), sel2(m);
sel1 = a.mk_select(args1);
sel2 = a.mk_select(args2);
prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2);
if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
prop = true;
return
ctx.propagate(e_internalize(sel1), ndef1, array_axiom()) ||
ctx.propagate(e_internalize(sel2), ndef2, array_axiom());
}
prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
// default(A) == default(B)
if (ctx.propagate(ndef1, ndef2, array_axiom()))
prop = true;
return prop;
}