You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
/usr/bin/time -vvv ./stp reduced.smt2
Timed Out.
Command being timed: "./stp reduced.smt2"
User time (seconds): 11.04
System time (seconds): 0.00
Percent of CPU this job got: 100%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.04
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 5180
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 722
Voluntary context switches: 1
Involuntary context switches: 11
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
/usr/bin/time -vvv ./cvc5-Linux-2022-08-08-cc80711 reduced.smt2
unsat
Command being timed: "./cvc5-Linux-2022-08-08-cc80711 reduced.smt2"
User time (seconds): 0.00
System time (seconds): 0.00
Percent of CPU this job got: 100%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.00
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 15860
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 564
Voluntary context switches: 1
Involuntary context switches: 0
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
The text was updated successfully, but these errors were encountered:
This problem is solved easily with some commutativity/associativity reasoning. STP solves it in about 20ms with --flattening=1 .
Unfortunately, the current implementation of flattening slows down other problems, so I've not enabled it by default.
If anyone else wants to investigate, that'd be great. Currently, it's about my 15th highest priority, so it'll be a while before I look at it.
Trev.
TrevorHansen
changed the title
Performance issue on QF_BV query (missing rewrite?)
Improve commutativity/associativity reasoning for addition
Aug 11, 2022
For this file:
STP as submitted to SMTCOMP 2022 times-out:
This file was reduced with ddSMT from:
cvc5 (cvc5/cvc5@cc80711) is almost instantaneous on this file:
The text was updated successfully, but these errors were encountered: