From cc07e93dc46cfbc9ee5c808b6bc1acd1697294e9 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 16:43:05 +0100
Subject: [PATCH] Add function to substitute variables
---
src/lib/CoAlgFormula.ml | 78 ++++++++++++++++++++++++++++++++++++++++
src/lib/CoAlgFormula.mli | 1 +
2 files changed, 79 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 36d851e..eee1f9e 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -2124,6 +2124,84 @@ let rec hc_formula hcF f =
| EU _ ->
raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+(* Replace the Variable name in f with formula formula
+ hc_replace foo φ ψ => ψ[foo |-> φ]
+ *)
+let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
+ let func = hc_replace hcF name formula in
+ let gennew = HcFormula.hashcons hcF in
+ match f.HC.node with
+ | HCTRUE
+ | HCFALSE
+ | HCAP _
+ | HCNOT _
+ | HCCONST _
+ | HCCONSTN _ -> f
+ | HCVAR s ->
+ if compare s name == 0
+ then formula
+ else f
+ | HCAT (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCAT(s, nf1))
+ | HCOR (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
+ | HCAND (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
+ | HCEX (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCEX(s, nf1))
+ | HCAX (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCAX(s, nf1))
+ | HCENFORCES (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
+ | HCALLOWS (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
+ | HCMORETHAN (n, s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
+ | HCMAXEXCEPT (n, s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
+ | HCATLEASTPROB (p, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
+ | HCLESSPROBFAIL (p, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
+ | HCID f1 ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCID(nf1))
+ | HCNORM (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
+ | HCNORMN (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
+ | HCCHC (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
+ | HCFUS (first, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCFUS(first, nf1))
+ | HCMU (var, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMU(var, nf1))
+ | HCNU (var, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCNU(var, nf1))
+
+
(** An instantiation of a hash table (of the standard library)
for hash-consed formulae. The test for equality
and computing the hash value is done in constant time.
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index a00a530..43f294e 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -164,5 +164,6 @@ and hcFormula_node =
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
val hc_formula : HcFormula.t -> formula -> hcFormula
+val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
module HcFHt : (Hashtbl.S with type key = hcFormula)
--
GitLab