mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
shortcut negation
This commit is contained in:
parent
f3fc6a50f3
commit
7ddfc54250
|
@ -19,6 +19,7 @@ Notes:
|
|||
|
||||
#include "util/ref_util.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "tactic/goal.h"
|
||||
#include "sat/smt/atom2bool_var.h"
|
||||
|
||||
|
@ -27,7 +28,7 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
|
|||
sat::literal l(static_cast<sat::bool_var>(kv.m_value), false);
|
||||
lit2expr.set(l.index(), kv.m_key);
|
||||
l.neg();
|
||||
lit2expr.set(l.index(), m().mk_not(kv.m_key));
|
||||
lit2expr.set(l.index(), mk_not(m(), kv.m_key));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -218,7 +218,7 @@ struct sat2goal::imp {
|
|||
}
|
||||
sat::literal lit(l.var(), false);
|
||||
m_lit2expr.set(lit.index(), aux);
|
||||
m_lit2expr.set((~lit).index(), m.mk_not(aux));
|
||||
m_lit2expr.set((~lit).index(), mk_not(m, aux));
|
||||
}
|
||||
return m_lit2expr.get(l.index());
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue