language: add support for ObservationVar on left of nonreach operator

Author: pauleve

bonesis/asp_encoding.py

@@ -535,18 +535,28 @@ def encode_reach(self, cfg1, right, mutant=None,
             ]
         return rules
 
-    def encode_nonreach(self, cfg1, right, mutant=None, bounded="auto"):
+    def encode_nonreach(self, left, right, mutant=None, bounded="auto"):
         self.load_template_eval()
         Z = self.fresh_atom("nonreach")
-        X = clingo_encode(cfg1.name)
+        X = clingo_encode(left.name)
         Y = clingo_encode(right.name)
         if isinstance(right, ConfigurationVar):
             pred = "cfg"
         elif isinstance(right, ObservationVar):
             pred = "obs"
         else:
             raise NotImplementedError
-        rules = [
+
+        rules = []
+
+        if isinstance(left, ObservationVar):
+            satcfg = self.saturating_configuration(free=f"not obs({X},N,_)",
+                                                   fixed=f"obs({X},N,V)")
+            condition = self.make_saturation_condition(satcfg)
+            rules.append(f"{condition} :- nr_ok({Z})")
+            X = satcfg
+
+        rules += [
             f"mcfg(({Z},1..K),N,V) :- reach_steps({Z},K), cfg({X},N,V)",
             f"ext(({Z},I),N,V) :- eval(({Z},I),N,V), not locked(({Z},I),N)",
 

bonesis/language.py

@@ -222,6 +222,7 @@ def __hash__(self):
         return hash((self.__class__.__name__,self.name))
 
 @allreach_operator
+@nonreach_operator
 class ObservationVar(BonesisVar):
     def __init__(self, arg):
         if isinstance(arg, dict):
@@ -477,6 +478,11 @@ def __init__(self, left, right):
         if isinstance(right, fixed):
             self.predicate_name = "final_nonreach"
         super().__init__(left, right)
+    @classmethod
+    def left_arg(celf, arg):
+        if isinstance(arg, ObservationVar):
+            return arg
+        return super().left_arg(arg)
 
 @language_api
 class final_nonreach(nonreach):