mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

share some equalities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-19 15:58:17 -06:00
parent 9179deb746
commit c816d45a7d
4 changed files with 43 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/cmd_context/basic_cmds.cpp
View file

@ -872,22 +872,9 @@ public:
void execute(cmd_context & ctx) override {
ast_manager& m = ctx.m();
qe::interpolator mbi(m);
expr_ref a(m_a, m);
expr_ref b(m_b, m);
expr_ref itp(m);
solver_factory& sf = ctx.get_solver_factory();
params_ref p;
solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
sA->assert_expr(a);
sB->assert_expr(b);
qe::uflia_mbi pA(sA.get(), sNotA.get());
qe::prop_mbi_plugin pB(sB.get());
pA.set_shared(a, b);
pB.set_shared(a, b);
lbool res = mbi.pogo(pA, pB, itp);
ctx.regular_stream() << res << " " << itp << "\n";
lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
ctx.regular_stream() << itp << "\n";
}
};