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

Build fix for eee96ec: create mbp::def w/ brace initialization

Browse source 
eee96ec removed the explicit constructor for mbp_plugin.h's struct def.
Change qe_mbp.cpp and q_mbi.cpp to use brace initialization.
This commit is contained in:
Jevin Sweval 2025-02-16 13:06:36 -05:00
parent a703cf81b1
commit d7ffd67e68
No known key found for this signature in database
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/qe/qe_mbp.cpp
View file

@ -487,7 +487,7 @@ public:
val = model(var); val = model(var);
sub.insert(var, val); sub.insert(var, val);
if (defs) if (defs)
defs->push_back(mbp::def(expr_ref(var, m), val)); defs->push_back(mbp::def{expr_ref(var, m), val});
unsigned j = 0; unsigned j = 0;
for (expr* f : fmls) { for (expr* f : fmls) {
sub(f, tmp); sub(f, tmp);

4
src/sat/smt/q_mbi.cpp
View file

@ -367,7 +367,7 @@ namespace q {
TRACE("euf", tout << "replaced model value " << term << "\nfrom\n" << val << "\n"); TRACE("euf", tout << "replaced model value " << term << "\nfrom\n" << val << "\n");
rep.insert(v, term); rep.insert(v, term);
if (ctx.use_drat()) if (ctx.use_drat())
m_defs.push_back(mbp::def(expr_ref(v, m), term)); m_defs.push_back(mbp::def{expr_ref(v, m), term});
eqs.push_back(m.mk_eq(v, val)); eqs.push_back(m.mk_eq(v, val));
} }
rep(fmls); rep(fmls);
@ -569,7 +569,7 @@ namespace q {
for (unsigned i = 0; i < binding.size(); ++i) { for (unsigned i = 0; i < binding.size(); ++i) {
expr_ref v(qb.vars.get(i), m); expr_ref v(qb.vars.get(i), m);
expr_ref t(binding.get(i), m); expr_ref t(binding.get(i), m);
m_defs.push_back(mbp::def(v, t)); m_defs.push_back(mbp::def{v, t});
} }
} }
add_instantiation(q, body); add_instantiation(q, body);