Add function to substitute variables

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.

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)