From 9b6bdd74b2727da82077515da616823d06120e47 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 15:14:54 +0100
Subject: [PATCH] unfold fixpoints when creating new Cores
---
src/lib/CoAlgReasoner.ml | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 034d6f2..77d68df 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -476,6 +476,23 @@ let newCore sort bs =
assert (okay1);
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
assert (okay2)
+ | MuF
+ | NuF ->
+ (*
+ Dest of a fixpoint is it's unfolded version. This adds just
+ an simple forward implication that could be optimised out
+ though not without nontrivial transformation of code
+
+ f = μ X . φ |---> lf
+ φ[X |-> f] |---> lf1
+
+ Then adding lf -> lf1 to minisat
+ *)
+ let f1 = lfGetDest1 sort f in
+ addClauses f1;
+ let lf1 = fhtMustFind fht f1 in
+ let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
+ assert (okay1);
| _ -> ()
(* case 2.(c)
We don't need to do anything except adding f to the fht
--
GitLab