mcmas.logic

  1"""
  2mcmas.logic.
  3"""
  4
  5import sympy
  6from pydantic_core import core_schema
  7from sympy import Eq as _Eq
  8
  9# from sympy.logic.boolalg import BooleanFunction
 10from sympy.printing.str import StrPrinter
 11
 12# from sympy import And, Or, Not, Eq, Lt, Gt
 13# from sympy.abc import *
 14# from sympy.printing.str import StrPrinter
 15
 16
 17class Function(sympy.Function):
 18    """
 19    
 20    """
 21
 22
 23class And(Function):
 24    """
 25    
 26    """
 27
 28    def __str__(self):
 29        """
 30        
 31        """
 32        return " and ".join([str(x) for x in self._sorted_args])
 33
 34
 35class Or(Function):
 36    """
 37    
 38    """
 39
 40    def __str__(self):
 41        """
 42        
 43        """
 44        return " or ".join([str(x) for x in self._sorted_args])
 45
 46
 47class Grouping(Function):
 48    """
 49    
 50    """
 51
 52    def __str__(self):
 53        """
 54        
 55        """
 56        tmp = " ".join([str(x) for x in self._sorted_args])
 57        return f"({tmp})"
 58
 59
 60class If(Function):
 61    """
 62    
 63    """
 64
 65    def __str__(self):
 66        """
 67        
 68        """
 69        if len(self._sorted_args) == 1:
 70            return f"if {self._sorted_args[0]}"
 71        else:
 72            assert len(self._sorted_args) == 2, "multiclause if not supported yet"
 73            return f"{self._sorted_args[0]} if {self._sorted_args[1]}"
 74
 75
 76class Eq(_Eq):
 77    """
 78    
 79    """
 80
 81    def __str__(expr):
 82        """
 83        
 84        """
 85        return f"{expr.lhs}={expr.rhs}"
 86
 87
 88Equal = Eq
 89
 90from mcmas import util
 91
 92LOGGER = util.get_logger(__name__)
 93
 94
 95class Symbol(sympy.core.symbol.Symbol):
 96    """
 97    
 98    """
 99
100    def __getitem__(self, key):
101        """
102        
103        """
104        if isinstance(key, (str,)):
105            return [self.__class__(k) for k in key.split(" ")]
106        else:
107            raise NotImplementedError()
108
109    @classmethod
110    def __get_pydantic_core_schema__(
111        cls,
112        source_type,  # noqa
113        handler,  # noqa
114    ) -> core_schema.CoreSchema:
115        """
116        Return a Pydantic core schema for Symbol validation.
117
118        This schema accepts: 1. Existing Symbol instances (passthrough)
119        2. String names to create new Symbols 3. Dictionaries with
120        'name' and optional symbol properties
121        """
122
123        def validate_symbol(value) -> "Symbol":
124            """
125            Validate and convert input to Symbol.
126            """
127            if isinstance(value, sympy.core.symbol.Symbol):
128                # If it's already a Symbol, return as-is (or convert to our class)
129                if isinstance(value, cls):
130                    return value
131                else:
132                    # Convert base Symbol to our extended Symbol
133                    return cls(value.name, **value.assumptions0)
134            elif isinstance(value, str):
135                # Create Symbol from string name
136                return cls(value)
137            elif isinstance(value, dict):
138                # Create Symbol from dictionary
139                if "name" not in value:
140                    raise ValueError("Dictionary must contain 'name' field")
141                name = value["name"]
142                # Extract symbol assumptions (like real=True, positive=True, etc.)
143                assumptions = {k: v for k, v in value.items() if k != "name"}
144                return cls(name, **assumptions)
145            else:
146                raise ValueError(
147                    f"Cannot convert {type(value).__name__} to Symbol. "
148                    f"Expected Symbol, str, or dict with 'name' field."
149                )
150
151        # Create the core schema (simplified version without custom serialization)
152        return core_schema.no_info_plain_validator_function(validate_symbol)
153
154    def __matmul__(self, other):
155        """
156        
157        """
158        return Eq(self, other)
159
160    def __eq__(self, other):
161        """
162        
163        """
164        LOGGER.critical(f"[{self},{other}]")
165        # return f"{self}={other}"
166        if isinstance(other, str):
167            # Compare with symbol name
168            return self.name == other
169        elif isinstance(other, (int, float)):
170            return False  # Symbols typically don't equal numbers
171        return super().__eq__(other)
172
173    def __ne__(self, other):
174        """
175        
176        """
177        return not self.__eq__(other)
178
179    def __hash__(self):
180        """
181        
182        """
183        # Maintain the parent's hash behavior
184        return super().__hash__()
185
186    def __and__(self, other):
187        """
188        
189        """
190        return self.__class__(f"{self.name} and {other}")
191
192    def __or__(self, other):
193        """
194        
195        """
196        return self.__class__(f"{self.name} or {other}")
197
198    def __rshift__(self, other):
199        """
200        
201        """
202        # return If(self, other)
203        return self.__class__(f"{self.name} if {other}")
204
205    def __imul__(self, other):
206        """
207        
208        """
209        return self.__class__(f"{self.name}={other}")
210
211    def __add__(self, other):
212        """
213        
214        """
215        return self.__class__(f"{self.name}+{other}")
216
217    def __lt__(self, other):
218        """
219        
220        """
221        return self.__class__(f"{self.name}<{other}")
222
223    def __lte__(self, other):
224        """
225        
226        """
227        return self.__class__(f"{self.name}<={other}")
228
229    def __gt__(self, other):
230        """
231        
232        """
233        return self.__class__(f"{self.name}>{other}")
234
235    def __gte__(self, other):
236        return self.__class__(f"{self.name}>={other}")
237
238    def __call__(self, other):
239        return self.__class__(f"{self.name}({other})")
240
241    def __getattribute__(self, name):
242        """
243        
244        """
245        try:
246            attr = super().__getattribute__(name)
247            # If it exists and is callable, return it
248            if callable(attr):
249                return attr
250            # If it exists and is not callable, return it
251            return attr
252        except AttributeError:
253            # Only create new symbols for names that don't exist as attributes
254            # and don't start with underscore (to avoid internal methods)
255            if not name.startswith("_"):
256                current_name = super().__getattribute__("name")
257                if current_name:
258                    new_name = f"{current_name}.{name}"
259                else:
260                    new_name = f"{name}"
261                return self.__class__(new_name)
262            # If it starts with underscore, re-raise the AttributeError
263            raise
264
265
266class CustomStrPrinter(StrPrinter):
267    """
268    
269    """
270
271    def _print_Equality(self, expr):
272        """
273        
274        """
275        return f"{expr.lhs}={expr.rhs}"
276
277
278printer = CustomStrPrinter()
279sympy2ispl = printer.doprint
280
281symbols = Symbol("")
282types = Symbol("")
283types.bool = types.boolean = types.boolean
284true = symbols.true
285false = symbols.false
286Environment = symbols.Environment
287
288# Temporal Operators / CTL
289# EF φ	There exists a path where eventually φ holds
290# AF φ	On all paths, eventually φ holds (φ is inevitable)
291# EG φ	There exists a path where φ holds forever
292# AG φ	On all paths, φ holds globally (φ is always true)
293AF = symbols.AF
294AG = symbols.AG
295EF = symbols.EF
296EG = symbols.EG
297
298# Epistemic	Operators
299# K(i, φ)	Agent i knows φ
300# CK(G, φ)  Group Knowledge; φ is common knowledge in group G
301K = symbols.K
302CK = symbols.CK
303
304# ATL <<G >>F φ	Group G can enforce φ eventually
305from .complexity import analyzer  # noqa