[Cryptominisat-devel] I need a bit of help debugging CryptoMiniSat
vegard.nossum at gmail.com
Mer 19 Jan 18:14:38 CET 2011
On 19 January 2011 14:13, Vegard Nossum <vegard.nossum at gmail.com> wrote:
> On 19 January 2011 12:22, Mate Soos <soos.mate at gmail.com> wrote:
> Here's my best tip for the moment: Try to find a minimal test-case
> that exhibits the bad behaviour.
> So for example, in this case, I would create a new file (with a new
> main()) and copy some of the relevant classes, for example Clause and
> Lit. Also copy Solver::propNormalClause() and make it a regular
> function that you can call from main() with some dummy arguments --
> make sure you can reproduce the bug in this "controlled" environment
> (i.e. not using the full solver).
> From this point you should still be able to remove a lot of things,
> like unused functions, etc. When you have the minimal test-case it
> should be pretty easy to tell whether it's a code bug or a gcc bug. At
> least you have eliminated a lot of things and somebody could finally
> say: "Ah, but strict aliasing makes GCC cache the value of c in a
> register because it cannot possibly [...]"
> I'll give it a try too :-)
I created a new Main.cpp which defines a new class Solver2, which is
MUCH smaller than the regular Solver. It uses Var, Lit, vec, and
ClauseAllocator from the other files, so the next step is to eliminate
those as well. So you see this new file also demonstrates the same
problem, but with a much simpler program now. This is the output:
$ for o in 0 3; do echo -n "-O$o: "; g++ -Wall -O$o -ISolver -Imtl
-IMTRand -o test Main.cpp Solver/ClauseAllocator.cpp && ./test; done
Will try to isolate it further.
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Taille: 2741 octets
Desc: non disponible
More information about the Cryptominisat-devel