[Soot-list] JEDD Unsatisfied Core

[Ondrej Lhotak]

On Tue, Oct 23, 2007 at 03:50:25PM +0100, Richard Warburton wrote:
> The 2004 paper on JEDD states that I can extract information about the
> unsatisfied core in a manner that will allow me to infer where the
> physical domain assignment conflicts are.  Unfortunately I can't find
> documentation that tells me how I actually do it.  I have looked in "A
> brief user's guide to JEDD" and the paper, but I don't understand.
> The zchaff website was also lacking in documentation on this matter.
> It would be most helpful if someone could explain what the steps are
> to identify this information.

When zChaff tells the Jedd translator that the SAT instance is
unsatisfiable, the Jedd translator automatically invokes the "zcore"
script to get zChaff to compute an unsatisfiable core. The Jedd
translator automatically interprets the resulting core, and gives you an
error message in terms of the attributes and line numbers in the Jedd
source.

If this is not happening, most likely the problem is related to the
zcore script. The zcore script that I use contains:

#!/bin/sh
$HOME/zChaff/zverify_df $1 $2 -core
mv unsat_core.cnf $3

This is for zChaff 2004.5.13. The commands needed to extract the core
may be different in other versions of zChaff.

>   Richard Warburton
> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>