search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
131 stars 33 forks source link

Profiler doesn't work as expected with CDCL solver #348

Closed iguerNL closed 4 years ago

iguerNL commented 4 years ago

Some asserts are failing, like below:

alt-ergo string_fixed.ads_131_14_postcondition_1__modified.why --profiling 1
GTimer      : Global timer
Steps       : Number of Steps
Case splits : Number of Case Splits
Mod.        : Current active module
Module Id   : Each call to a module is tagged with a fresh Id
ilvl        : Current Instantiaton level
#i rnds     : Number of intantiation rounds
#insts      : Number of generated instances
i/r         : AVG number of generated instances per instantiation rounds
dlvl        : Current Decision level
#decs       : Number of decisions
T-asm       : Number of calls to Theory.assume
T/d         : Number of Theory.assume after last decision
T-qr        : Number of calls to Theory.query
B-R         : Number of reduced clauses by Boolean propagation
B-E         : Number of eliminated clauses by Boolean propagation
T-R         : Number of reduced clauses by Theory propagation
T-E         : Number of eliminated clauses by Theory propagation
B-!         : Number of direct Boolean conflicts
T-!         : Number of direct Theory conflicts
B>!         : Number of Boolean conflicts deduced by BCP
T>!         : Number of Theory conflicts deduced by BCP
M>!         : Number of Mix conflicts deduced by BCP
SAT         : Time spent in SAT module(s)
Matching    : Time spent in Matching module(s)
CC          : Time spent in CC module(s)
Arith       : Time spent in Arith module(s)
Arrays      : Time spent in Arrays module(s)
Sum         : Time spent in Sum module(s)
Records     : Time spent in Records module(s)
AC          : Time spent in AC module(s)
Total       : Time spent in 'supervised' module(s)
|-----------|--------------|--------------|-------|----------|------|--------|--------|--------|------|------|------|------|---------------|------|------|------|------|-----|-----|-----|-----|-----|
|GTimer     |Steps         |Case splits   |Mod.   |Module Id |ilvl  |#i rnds |#insts  |i/r     |dlvl  |#decs |T-asm |T/d   |T-qr           |B-R   |B-E   |T-R   |T-E   |B-!  |T-!  |B>!  |T>!  |M>!  |
|-----------|--------------|--------------|-------|----------|------|--------|--------|--------|------|------|------|------|---------------|------|------|------|------|-----|-----|-----|-----|-----|
|0.942109   |0      ~0/s   |0      ~0/s   |None   |0         |0     |0       |0       |0       |0     |0     |0     |0     |0              |0     |0     |0     |0     |0    |0    |0    |0    |0    |
|1.901804   |0      ~0/s   |0      ~0/s   |None   |0         |0     |0       |0       |0       |0     |0     |0     |0     |0              |0     |0     |0     |0     |0    |0    |0    |0    |0    |
|3.701421   |5424   ~1465/s|0      ~0/s   |UF     |143307    |0     |0       |0       |0       |0     |0     |137   |137   |17440          |88    |14    |0     |0     |0    |0    |0    |0    |0    |
|4.565358   |11324  ~2480/s|0      ~0/s   |UF     |267997    |0     |0       |0       |0       |0     |0     |137   |137   |19221          |88    |14    |0     |0     |0    |0    |0    |0    |0    |
|5.437266   |17139  ~3152/s|0      ~0/s   |CC     |391721    |0     |0       |0       |0       |0     |0     |137   |137   |20966          |88    |14    |0     |0     |0    |0    |0    |0    |0    |
|6.285338   |19493  ~3101/s|0      ~0/s   |Match  |529941    |1     |1       |11      |11      |2640  |2640  |154   |1     |26482          |7930  |10484 |0     |0     |0    |0    |0    |0    |0    |
Fatal error: exception File "src/lib/structures/profiling.ml", line 224, characters 2-8: Assertion failed
iguerNL commented 4 years ago

This was rather due to isse: https://github.com/OCamlPro/alt-ergo/issues/349