Project wouldn't compile with latest version of nlambda
Closed this issue · 6 comments
Hello! I am trying to experiment with your package, and it wouldn't compile when built with the latest version of NLambda.
It seems that szynwelski/nlambda@47d81e0 renamed the identifier NominalType to Nominal for the whole NLambda project. After I replaced all instances of NominalType by Nominal in the Haskell files in nominal-lstar, I was able to compile nominal-lstar without issues.
Thanks! I have replaced all those instances.
It compiles, but it seems that NLambda cannot parse the output of Z3 anymore. Do you have similar issues?
Hmmm, I am not super familiar with NLambda and what it uses Z3 for, but I am currently running cabal bench in nominal-lstar without any visible errors.
I cannot run the benchmarks for some reason (Unsupported OS/architecture/compiler in gauge). So I am not sure what the benchmarks do if something goes wrong (in this case a parsing error).
Which version of z3 do you have?
I am using Z3 version 4.12.1, cabal version 3.6.2, GHC version 9.2.7.
Here is a section of output from cabal-bench when I run it:
benchmarking NomLStarC/Fifo/4 ... 1. Making it closed
Not closed
newrows = {[Get a₁] : for a₁ ∊ 𝔸}
1. Making it closed
2. Making it consistent
Automaton {states = {{}, {[]}}, alphabet = {Put a₁ : for a₁ ∊ 𝔸, Get a₁ : for a₁ ∊ 𝔸}, delta = {({},Put a₁,{}) : for a₁ ∊ 𝔸, ({},Get a₁,{}) : for a₁ ∊ 𝔸, ({[]},Put a₁,{[]}) : for a₁ ∊ 𝔸, ({[]},Get a₁,{}) : for a₁ ∊ 𝔸}, initialStates = {{[]}}, finalStates = {{[]}}}
3. Equivalent?
No
Using ce: {[Put a₁,Get a₁] : for a₁ ∊ 𝔸}
1. Making it closed
Not closed
newrows = {[Put a₁] : for a₁ ∊ 𝔸}
1. Making it closed
2. Making it consistent
Automaton {states = {{}, {[], [Put a₁,Get a₁], [Get a₁]} : for a₁ ∊ 𝔸, {[], [Put a₁,Get a₁] : for a₁ ∊ 𝔸}}, alphabet = {Put a₁ : for a₁ ∊ 𝔸, Get a₁ : for a₁ ∊ 𝔸}, delta = {({},Put a₁,{}) : for a₁ ∊ 𝔸, ({},Get a₁,{}) : for a₁ ∊ 𝔸, ({[], [Put a₁,Get a₁], [Get a₁]},Put a₂,{[], [Put a₁,Get a₁], [Get b₁] : b₁ = a₁ ∧ ((a₁ = a₁ ∧ a₂ = a₁) ∨ (a₁ = a₁ ∧ a₂ ≠ a₁)) for b₁ ∊ 𝔸}) : for a₁,a₂ ∊ 𝔸, ({[], [Put a₁,Get a₁], [Get a₁]},Get a₂,{[] : a₁ = a₂, [Put b₁,Get b₁] : a₁ = a₂ for b₁ ∊ 𝔸}) : for a₁,a₂ ∊ 𝔸, ({[], [Put a₁,Get a₁] : for a₁ ∊ 𝔸},Put b₁,{[], [Put b₁,Get b₁], [Get b₁]}) : for b₁ ∊ 𝔸, ({[], [Put a₁,Get a₁] : for a₁ ∊ 𝔸},Get b₁,{}) : for b₁ ∊ 𝔸}, initialStates = {{[], [Put a₁,Get a₁] : for a₁ ∊ 𝔸}}, finalStates = {{[], [Put a₁,Get a₁], [Get a₁]} : for a₁ ∊ 𝔸, {[], [Put a₁,Get a₁] : for a₁ ∊ 𝔸}}}
3. Equivalent?
No
Using ce: {[Put a₁,Put a₂,Get a₁,Get a₂] : for a₁,a₂ ∊ 𝔸}
1. Making it closed
Not closed
newrows = {[Put a₁,Put a₂] : for a₁,a₂ ∊ 𝔸}
1. Making it closed
Not closed
newrows = {[Put a₁,Put a₂,Put a₃] : for a₁,a₂,a₃ ∊ 𝔸, [Put a₁,Put a₂,Get a₃] : (a₁ = a₃ ∨ (a₁ = a₃ ∧ a₂ = a₃) ∨ (a₁ = a₃ ∧ a₂ = b₁) ∨ (a₁ = a₃ ∧ a₂ ≠ a₃)) ∧ (a₁ ≠ a₃ ∨ (a₂ = b₁ ∧ (a₁ ≠ a₃ ∨ a₂ ≠ b₁)) ∨ ((a₂ = a₃ ∨ a₁ ≠ a₃) ∧ (a₁ ≠ a₃ ∨ a₂ ≠ a₃))) for a₁,a₂,a₃ ∊ 𝔸}
1. Making it closed
Not closed
newrows = {[Put a₁,Put a₂,Put a₃,Put a₄] : for a₁,a₂,a₃,a₄ ∊ 𝔸, [Put a₁,Put a₂,Put a₃,Get a₄] : (a₁ = a₄ ∨ (a₁ = a₄ ∧ a₃ = a₄) ∨ (a₁ = a₄ ∧ a₃ ≠ a₄) ∨ (a₁ = a₄ ∧ (a₂ = a₃ ∨ (a₁ = a₂ ∧ a₁ = a₃) ∨ (a₂ ≠ a₃ ∧ (a₂ = a₃ ∨ (a₁ = a₂ ∧ a₂ = a₃)) ∧ (a₁ ≠ a₂ ∨ a₂ ≠ a₃)) ∨ (a₂ ≠ a₃ ∧ (a₁ ≠ a₂ ∨ a₂ ≠ a₃))))) ∧ (a₁ ≠ a₄ ∨ (a₂ = a₃ ∧ (a₁ ≠ a₄ ∨ a₂ ≠ a₃)) ∨ (a₂ ≠ a₃ ∧ ((a₁ = a₄ ∧ a₂ = a₃) ∨ (a₁ = a₄ ∧ a₂ = a₃ ∧ ((a₂ ≠ a₃ ∧ (a₂ = a₃ ∨ (a₂ = a₃ ∧ a₂ = a₄)) ∧ (a₂ ≠ a₃ ∨ a₂ ≠ a₄)) ∨ (a₂ ≠ a₃ ∧ (a₂ ≠ a₃ ∨ a₂ ≠ a₄)))) ∨ (a₁ = a₄ ∧ a₂ = a₄ ∧ a₃ = a₄))) ∨ ((a₃ = a₄ ∨ a₁ ≠ a₄) ∧ (a₁ ≠ a₄ ∨ a₃ ≠ a₄)) ∨ ((a₃ = a₄ ∨ a₂ ≠ a₄) ∧ (a₂ ≠ a₃ ∨ a₃ ≠ a₄) ∧ ((a₁ = a₄ ∧ a₂ = a₃ ∧ a₃ = a₄) ∨ (a₁ = a₄ ∧ a₂ = a₄ ∧ a₃ = a₄) ∨ (a₁ = a₄ ∧ a₂ = a₄ ∧ ((a₂ ≠ a₃ ∧ (a₂ = a₃ ∨ (a₂ = a₃ ∧ a₂ = a₄)) ∧ (a₂ ≠ a₃ ∨ a₂ ≠ a₄)) ∨ (a₂ ≠ a₃ ∧ (a₂ ≠ a₃ ∨ a₂ ≠ a₄)))))) ∨ ((a₁ ≠ a₄ ∨ a₂ ≠ a₃) ∧ (a₁ ≠ a₄ ∨ a₂ ≠ a₄ ∨ a₃ ≠ a₄) ∧ (a₁ ≠ a₄ ∨ ((a₂ = a₃ ∨ (a₂ = a₃ ∧ a₂ = a₄)) ∧ (a₂ = a₃ ∨ (a₂ = a₃ ∧ a₂ = a₄) ∨ (a₂ ≠ a₃ ∧ (a₂ ≠ a₃ ∨ a₂ ≠ a₄))))))) for a₁,a₂,a₃,a₄ ∊ 𝔸, [Put a₁,Put a₂,Get a₃] : (a₁ = a₃ ∨ (a₁ = a₃ ∧ a₂ = a₃) ∨ (a₁ = a₃ ∧ a₂ = b₁) ∨ (a₁ = a₃ ∧ a₂ ≠ a₃)) ∧ (a₁ ≠ a₃ ∨ (a₂ = b₁ ∧ (a₁ ≠ a₃ ∨ a₂ ≠ b₁)) ∨ ((a₂ = a₃ ∨ a₁ ≠ a₃) ∧ (a₁ ≠ a₃ ∨ a₂ ≠ a₃))) for a₁,a₂,a₃ ∊ 𝔸, [Put a₁,Put a₂,Get a₃,Put a₄] : (a₁ = a₃ ∨ (a₁ = a₃ ∧ a₂ = a₃) ∨ (a₁ = a₃ ∧ a₂ = a₄) ∨ (a₁ = a₃ ∧ a₂ ≠ a₃)) ∧ (a₁ = a₃ ∨ (a₁ = a₃ ∧ a₂ = a₄)) ∧ (a₁ ≠ a₃ ∨ (a₂ = a₄ ∧ (a₁ ≠ a₃ ∨ a₂ ≠ a₄)) ∨ ((a₂ = a₃ ∨ a₁ ≠ a₃) ∧ (a₁ ≠ a₃ ∨ a₂ ≠ a₃))) for a₁,a₂,a₃,a₄ ∊ 𝔸}
1. Making it closed
2. Making it consistent
Okay that seems to work fine indeed (and we have the same version of z3). Maybe the parsing issue only occurs in the interactive parts.