Skip to content

multiset_solver cannot even solve trivial goals

I am not sure what goals multiset_solver is supposed to be able to handle, but so far it has solved zero of the goals I tried it on. Here is a rather simple example that only requires reasoning up to A/C:

  net_phys, net_ghost : gmultiset val
  m : val
-----------------------------------------
{[m]} ⊎ net_ghost ∖ {[m]} ⊎ net_phys = net_ghost ∖ {[m]} ⊎ (net_phys ⊎ {[m]})
Edited by Ralf Jung