Re: soot-dev: SAT solver problem

[Ondrej Lhotak <olhotak@sable.mcgill.ca>]

On Tue, Sep 21, 2004 at 04:53:10PM +0200, Richard Stahl wrote:
> Hello,
> 
> while trying to compile the development version i have got the following 
> error:
> 
>      [apply] Attemptimg to extract unsat core.
>      [apply] ZExtract: UnSAT Core Extractor
>      [apply] Copyright Princeton University, 2003-2004. All Right Reserved.
>      [apply] jeddc: SAT solver couldn't assign physical domains.
>      [apply] 1 error.
> 
> BUILD FAILED
> .../java/soot-dev/build.xml:386: apply returned: 1
> 
> I have downloaded zchaff from official page, version Chaff II.
> 
> What am I doing wrong? Has anybody had a similar problem? Please, help!

The quickest way to get Soot compiled, provided you haven't changed any
.jedd files, is to use that .java versions of all the .jedd files that
are included with Soot in the Subversion repository, in the directory
soot/generated/jedd. Subversion sometimes messes up the modification
times of these files, making ant want to re-generate them. To prevent
ant from trying to re-generate them, you can touch them with the
command:

find soot/generated/jedd -name '*.jedd' | xargs touch

As to why Jedd is failing to compile the .jedd files for you, the two
most likely reasons are that either zchaff is not correctly compiled,
installed, or referenced from the ant.settings file, or that the version
of zchaff that you have has once again changed its output format and
confused Jedd. The easiest way to diagnose this is to look in your /tmp
directory for a recent file with the name domainassing<number>.cnf,
where <number> is some number, and run zchaff on that file. If it fails,
hopefully it will give some error message indicating what's wrong.

Ondrej

> 
> 
> Thank you very much.
> 
> Kind regards,
> Richard
>