search

j5b / ps-pc

Automatically exported from code.google.com/p/ps-pc
GNU General Public License v3.0
0 stars 0 forks source link

foldExists error #14

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. findPOM [Exists "R" (Or (Atom "A") (Atom "D")),Exists "R" (Or (Atom "A") 
(Neg (Atom "D")))] [Atom "A",Forall "R" (Forall "R" (Or (Atom "A") (Neg (Atom 
"B"))))]

What is the expected output? What do you see instead?
I expect a good model, I've got a satanic model, where R(1,3) is true but there 
is no 3 inside the model

Please use labels and text to provide additional information.
There seems to be a problem with Exists "R" (Or (Atom "A") (Atom "D")) and 
Exists "R" (Or (Atom "A") (Neg (Atom "D")))

Original issue reported on code.google.com by mparusinski@gmail.com on 7 Dec 2010 at 2:48

GoogleCodeExporter commented 9 years ago 
After Sagie and I changed a few things today, we get a really nice model for 
your example (i.e. I think we exorcised the reason for the satanic model). We 
get:

  Left ([1,2],[("A",[1,2])],[("R",[(1,2)])])

Original comment by jannis.bulian@gmail.com on 7 Dec 2010 at 9:48