mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix model converter to include negation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-27 17:50:51 -08:00
parent f009dfcc00
commit b5ff4602e9
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/generic_model_converter.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include "ast/ast_util.h"
#include "ast/occurs.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/generic_model_converter.h"
#include "model/model_v2_pp.h"
#include "model/model_evaluator.h"
@ -160,7 +161,10 @@ expr_ref generic_model_converter::simplify_def(entry const& e) {
expr_ref result2 = e.m_def;
rep.apply_substitution(c, m.mk_true(), result1);
rep.apply_substitution(c, m.mk_false(), result2);
return expr_ref(m.mk_and(m.mk_or(c, result2), m.mk_or(m.mk_not(c), result1)), m);
th_rewriter rw(m);
expr_ref result(m.mk_and(m.mk_implies(result2, c), m.mk_implies(c, result1)), m);
rw(result);
return result;
}
else {
return expr_ref(m.mk_eq(c, e.m_def), m);