From 1cd86e73f91b5198621e77b0320d9424a787e311 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Nov 2021 12:05:40 +0100
Subject: [PATCH] [qed] forking sigma
---
src/plugins/qed/logic.mli | 1 +
src/plugins/qed/term.ml | 6 ++++++
src/plugins/wp/Lang.mli | 1 +
3 files changed, 8 insertions(+)
diff --git a/src/plugins/qed/logic.mli b/src/plugins/qed/logic.mli
index 9fc9da00920..cf4f9df3ffe 100644
--- a/src/plugins/qed/logic.mli
+++ b/src/plugins/qed/logic.mli
@@ -332,6 +332,7 @@ sig
sig
type t = sigma
val create : ?pool:pool -> unit -> t
+ val copy : sigma -> sigma
val fresh : t -> tau -> var
val find : t -> term -> term
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 1809bf71702..aa7fc81b4b7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2225,6 +2225,12 @@ struct
filter = [] ;
}
+ let copy sigma = {
+ pool = POOL.create ~copy:sigma.pool () ;
+ shared = sigma.shared ;
+ filter = sigma.filter ;
+ }
+
let validate fn e =
if not (lc_closed e) then
begin
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index dc8cd859a31..4e10985cd28 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -376,6 +376,7 @@ sig
module Subst :
sig
+ val copy : sigma -> sigma
val find : sigma -> term -> term
val add : sigma -> term -> term -> unit
val add_map : sigma -> term Tmap.t -> unit
--
GitLab