reach: simpler encoding when right is an observation

bnediction · Mar 6, 2024 · 9367d4a · 9367d4a
1 parent 40d74bf
commit 9367d4a
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/bonesis/asp_encoding.py b/bonesis/asp_encoding.py
@@ -525,8 +525,9 @@ def encode_reach(self, cfg1, right, mutant=None,
             f":- {pred}({Y},N,V), ext({Z},N,-V), not ext({Z},N,V)",
         ] + self.apply_mutant_to_mcfg(mutant, Z)
         if not monotone:
+            compl = f"cfg({Y},N,-V)" if pred == "cfg" else f"not obs({Y},N,V)"
             rules += [
-            f"{{ext({Z},N,V)}} :- eval({Z},N,V), {pred}({Y},N,-V)"
+                f"{{ext({Z},N,V)}} :- eval({Z},N,V), {compl}"
             ]
         if isinstance(max_changes, int) and max_changes > 0:
             rules += [