Substituting Function Symbols without providing Interpretations

[cvick32]

Substituting Function Symbols without providing Interpretations

[mikand]

Hi @cvick32,

indeed it should work: there is nothing special about Read or Write, they are terms for the substituter.

What is the behavior of pysmt? does it crash?
Can you provide a full example to reproduce the bug?

[cvick32]

Here's a python file that fails to substitute a term like one that I had above:

from pysmt.shortcuts import Function, Symbol, Implies, Not, Iff, Equals
from pysmt.typing import BOOL, INT, _TypeDecl, FunctionType, PySMTType


arr = _TypeDecl("Arr-Id-Bool", 0)
arr_type = PySMTType(arr, "Arr-Id-Bool")
ReadType = FunctionType(BOOL, [arr_type, INT])
WriteType = FunctionType(arr_type, [arr_type, INT, BOOL])
Read = Symbol(f"ReadArr-Id-Bool", ReadType)
Write = Symbol(f"WriteArr-Id-Bool", WriteType)

V = Symbol("V", BOOL)
L = Symbol("L", INT)
Z = Symbol("Z", INT)

Arr1 = Symbol("Arr1", arr_type)


lhs = Read(Write(Arr1, L, V), Z)
rhs = Read(Arr1, Z)

phi = Read(Write(Arr1, L, V), Z)

assert phi.substitute({lhs: rhs}) == rhs, "Assert Fails"

I would expect for phi to match lhs as they are syntactically equivalent, but the assert fails for me.

[cvick32]

Hey @mikand, just wanted to check in and make sure this script has the same behavior for you.