From be9f17cd486aab1c9e10bf13de1d7d992903d9a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20R=C3=BCmmer?= Date: Sat, 14 Sep 2024 09:23:51 +0200 Subject: [PATCH] some comments --- src/main/scala/lazabs/horn/symex/Symex.scala | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/main/scala/lazabs/horn/symex/Symex.scala b/src/main/scala/lazabs/horn/symex/Symex.scala index a7799a0a..79f85cbc 100644 --- a/src/main/scala/lazabs/horn/symex/Symex.scala +++ b/src/main/scala/lazabs/horn/symex/Symex.scala @@ -86,6 +86,9 @@ abstract class Symex[CC](iClauses: Iterable[CC])( // Note that the prover must be manually shut down for clean-up. implicit val prover: SimpleAPI = SimpleAPI.spawn prover.addTheories(theories) + + // TODO: keeping preds as a set is problematic, it will introduced + // non-determinism. Turn the preds field into a Seq[Predicate]? prover.addRelations(preds) // Keeps track of all the terms and adds new symbols to the prover @@ -123,6 +126,7 @@ abstract class Symex[CC](iClauses: Iterable[CC])( (rel, normClauses.filter(_._1.head._1 == rel).map(_._1)) }).toMap + // TODO: this block will not have any effect? for (pred <- preds) { normClauses.filter(