mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

enable unsat core extraction in nlsat_tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-11-01 17:57:28 +01:00
parent 84172302a2
commit 305e080239
9 changed files with 46 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/tactic/sat_tactic.cpp
View file

@ -73,14 +73,15 @@ class sat_tactic : public tactic {
if (r == l_false) {
expr_dependency * lcore = 0;
if (produce_core) {
sat::literal_vector const& core = m_solver.get_core();
sat::literal_vector const& ucore = m_solver.get_core();
u_map<expr*> asm2dep;
mk_asm2dep(dep2asm, asm2dep);
for (unsigned i = 0; i < core.size(); ++i) {
sat::literal lit = core[i];
for (unsigned i = 0; i < ucore.size(); ++i) {
sat::literal lit = ucore[i];
expr* dep = asm2dep.find(lit.index());
lcore = m.mk_join(lcore, m.mk_leaf(dep));
}
core = lcore;
}
g->assert_expr(m.mk_false(), 0, lcore);
}