From 97b37ae5a18bec9ee0db6b60268e136098a697a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 6 Feb 2023 11:18:04 +0100
Subject: [PATCH] [Simplex] add comment about the reason of a restriction
---
colibri2/theories/LRA/simplex.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/colibri2/theories/LRA/simplex.ml b/colibri2/theories/LRA/simplex.ml
index af6b211b6..3673a8f9e 100644
--- a/colibri2/theories/LRA/simplex.ml
+++ b/colibri2/theories/LRA/simplex.ml
@@ -177,6 +177,8 @@ let make_equations d (eqs, vars) n =
let sign = Dom_product.SolveSign.get_repr d n in
match (abs, sign) with
| Some abs, Some sign ->
+ (* The restriction is not for soundness, any node can be added as
+ equation using {!addition} since it uses the domains of the node *)
Debug.dprintf6 debug "[Simplex] %a: %a --- %a" Node.pp n Product.pp abs
Sign_product.pp sign;
if Sign_product.(equal one sign) then
--
GitLab