Formulae for Scalable Chain; some fixes and improvements

logics/rsltl.py

@@ -3,8 +3,7 @@ from enum import Enum
 
 from logics.bags import *
 
-rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not t_globally t_finally t_next t_until t_release')
-
+rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not l_implies t_globally t_finally t_next t_until t_release')
 
 class Formula_rsLTL(object):
     
@@ -35,6 +34,8 @@ class Formula_rsLTL(object):
             return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )"
         if self.f_type == rsLTL_form_type.l_or:
             return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )"
+        if self.f_type == rsLTL_form_type.l_implies:
+            return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )"
         if self.f_type == rsLTL_form_type.t_until:
             return "( " + repr(self.left_operand) + " U[" + repr(self.sub_operand) + "]" + repr(self.right_operand) + " )"
         if self.f_type == rsLTL_form_type.t_release:
@@ -68,6 +69,10 @@ class Formula_rsLTL(object):
     def f_R(cls, sub, arg_L, arg_R):
         return cls(rsLTL_form_type.t_release, L_oper = arg_L, R_oper = arg_R, sub_oper = sub)
         
+    @classmethod
+    def f_Implies(cls, arg_L, arg_R):
+        return cls(rsLTL_form_type.l_implies, L_oper = arg_L, R_oper = arg_R)
+        
     def __and__(self, other):
         return Formula_rsLTL(rsLTL_form_type.l_and, L_oper = self, R_oper = other)
     

logics/rsltl_encoder.py

@@ -1,5 +1,8 @@
 from logics.rsltl import *
 
+def simplify(x):
+    return x
+
 class rsLTL_Encoder(object):
     """Class for encoding rsLTL formulae for a given smt_checker instance"""
         
@@ -10,8 +13,20 @@ class rsLTL_Encoder(object):
         self.rs = smt_checker.rs
         self.loop_position = smt_checker.loop_position
         
+        self.init_ncalls()
+        
+    def init_ncalls(self):
+        self.ncalls_encode = 0
+        self.ncalls_encode_approx = 0
+        
+    def get_ncalls(self):
+        return (self.ncalls_encode, self.ncalls_encode_approx)
+        
     def encode_bag(self, bag_formula, level, context=False):
-                
+
+        if not bag_formula:
+            raise RuntimeError("bag_formula is None")
+
         if bag_formula.f_type == BagDesc_oper.entity:
             entity_id = self.rs.get_entity_id(bag_formula.entity)
             if context:
@@ -56,6 +71,8 @@ class rsLTL_Encoder(object):
       
     def encode(self, formula, level, bound):
         
+        self.ncalls_encode += 1
+        
         if not isinstance(formula, Formula_rsLTL):
             raise NotImplementedError("Unsupported formula type: " + str(type(formula)))
         
@@ -76,20 +93,26 @@ class rsLTL_Encoder(object):
             return And(
                     self.encode(formula.left_operand, level, bound), 
                     self.encode(formula.right_operand, level, bound)
-                )
+            )
 
         elif formula.f_type == rsLTL_form_type.l_or:
             return Or(
                     self.encode(formula.left_operand, level, bound), 
                     self.encode(formula.right_operand, level, bound)
-                )
+            )
 
+        elif formula.f_type == rsLTL_form_type.l_implies:
+            return Implies(
+                    self.encode(formula.left_operand, level, bound), 
+                    self.encode(formula.right_operand, level, bound)
+            )
+            
         elif formula.f_type == rsLTL_form_type.t_next:
             if level < bound:
                 enc = And(
                         self.encode(formula.left_operand, level + 1, bound), 
                         self.encode_bag_ctx(formula.sub_operand, level)
-                    )
+                )
             else: 
                 # level == bound
                 enc = False
@@ -107,22 +130,22 @@ class rsLTL_Encoder(object):
                         self.encode(formula.left_operand, level, bound),
                         self.encode_bag_ctx(formula.sub_operand, level),
                         self.encode(formula, level + 1, bound)
-                    )
+                )
             else:
                 # level == bound
                 enc_loops = False
                 for loop_level in range(1, bound+1):
                     enc_loops = Or(enc_loops, 
-                            And(
-                                self.loop_position == loop_level,
-                                self.encode_approx(formula, loop_level, bound),
-                            )
+                        And(
+                            self.loop_position == loop_level,
+                            self.encode_approx(formula, loop_level, bound),
                         )
-                enc = And(
-                        self.encode(formula.left_operand, bound, bound),
-                        enc_loops, 
-                        self.encode_bag_ctx(formula.sub_operand, level)
                     )
+                enc = And(
+                    self.encode(formula.left_operand, bound, bound),
+                    enc_loops, 
+                    self.encode_bag_ctx(formula.sub_operand, level)
+                )
                 enc = simplify(enc)  
 
             return enc
@@ -218,6 +241,9 @@ class rsLTL_Encoder(object):
         
         Used by encode()
         """
+        
+        self.ncalls_encode_approx += 1
+        
         if formula.f_type == rsLTL_form_type.t_until:
             if level < bound:
                 enc = Or(