From f02f4a91ef7be83109c5adaf6a2560141f1e6500 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 16 Aug 2021 17:18:55 +0200
Subject: [PATCH] [Quant] In pp pairs watch only parent1
---
src_colibri2/theories/quantifier/InvertedPath.ml | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index ed3ea87c7..a49905985 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -179,12 +179,7 @@ let insert_pattern d (trigger : Trigger.t) =
| Pattern.Var v ->
let pairs = Expr.Term.Var.M.find_def [] v.var pp_vars in
let pairs =
- List.filter
- (fun pp ->
- (* improvement: possible to limit to just parent1 since only one
- path is needed by pairs *)
- F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
- pairs
+ List.filter (fun pp -> F_Pos.equal fp pp.PP.parent1) pairs
in
let ips = List.map (fun pp -> HPP.find pp_ips d pp) pairs in
let ip = create (Egraph.context d) in
--
GitLab