Open GoogleCodeExporter opened 9 years ago
Hi: Similar tricks to A4 would have to be done to make solution enumeration
work.
In A4, we created 2 special tasks SimpleTask1 and SimpleTask2
for doing solution solving and doing solution enumeration in subJVM.
In A4E, solution solving in subJVM works, but solution enumeration in subJVM
doesn't
work.
That's because the current A4E way is that once a solution is solved
by the subJVM, then the solution is written to XML and then read-back from XML.
But the read-back instance is not associated with a live SAT solver.
(The live SAT solver is still alive in the subJVM, but it's out of reach from
parent JVM)
Live SAT solver is needed to perform solution enumeration.
Please take a look at A4's SimpleTask2 and we can then discuss later
on how to apply the same approach to A4E.
Sincerely
Felix Chang
Alloy4 Lead Developer
Original comment by felix2...@gmail.com
on 8 Dec 2008 at 9:20
Felix,
Thanks for pointing me to the right direction.
I will take a look at it this week and let you know if I have some problems to
adapt
it to A4E.
Daniel
Original comment by daniel.l...@gmail.com
on 8 Dec 2008 at 9:33
That feature need to be implemented if possible for release 0.3.0.
Please check SimpleTask2 class in A4.
Original comment by daniel.l...@gmail.com
on 19 May 2011 at 8:53
We should have time this year to fix that issue.
Original comment by daniel.l...@gmail.com
on 17 Apr 2012 at 6:46
Original issue reported on code.google.com by
daniel.l...@gmail.com
on 8 Dec 2008 at 7:59