search

stp / stp

Simple Theorem Prover, an efficient SMT solver for bitvectors
https://stp.github.io/
Other
501 stars 128 forks source link

Improve commutativity/associativity reasoning for addition #444

Open aytey opened 2 years ago

aytey commented 2 years ago

For this file:

(set-logic QF_BV)
(declare-const __T1 (_ BitVec 5))
(declare-const __ (_ BitVec 6))
(declare-const _T1 (_ BitVec 3))
(declare-const __T (_ BitVec 6))
(declare-const T1 (_ BitVec 3))
(declare-const T (_ BitVec 7))
(declare-const _T (_ BitVec 1))
(assert
  (let
    ((?x25 ((_ zero_extend 24) ((_ zero_extend 1) ((_ zero_extend 1) __T)))))
    (bvslt
      (_ bv111 32)
      (bvadd
        ((_ zero_extend 24) ((_ zero_extend 4) ((_ zero_extend 1) T1)))
        (bvadd
          ((_ zero_extend 24) ((_ zero_extend 1) T))
          ?x25
          (
            (_ zero_extend 24)
            ((_ zero_extend 1) ((_ zero_extend 1) ((_ zero_extend 1) __T1))))
          ((_ zero_extend 24) ((_ zero_extend 4) ((_ zero_extend 1) _T1)))
          ((_ zero_extend 24) ((_ zero_extend 1) ((_ zero_extend 1) __))))))))
(assert
  (let
    (
      (?x1088
        (bvadd
          ((_ zero_extend 24) ((_ zero_extend 7) _T))
          ((_ zero_extend 24) ((_ zero_extend 1) ((_ zero_extend 1) __))))))
    (bvsge
      (_ bv111 32)
      (bvadd
        (bvadd
          ((_ zero_extend 24) ((_ zero_extend 4) ((_ zero_extend 1) T1)))
          (
            (_ zero_extend 24)
            ((_ zero_extend 1) ((_ zero_extend 1) ((_ zero_extend 1) __T1)))))
        ?x1088
        ((_ zero_extend 24) ((_ zero_extend 4) ((_ zero_extend 1) _T1)))
        ((_ zero_extend 24) ((_ zero_extend 1) ((_ zero_extend 1) __T)))
        (bvadd
          ((_ zero_extend 24) ((_ zero_extend 7) _T))
          ((_ zero_extend 24) ((_ zero_extend 1) T)))))))
(check-sat)

STP as submitted to SMTCOMP 2022 times-out:

/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

This file was reduced with ddSMT from:

cvc5 (https://github.com/cvc5/cvc5/commit/cc80711) is almost instantaneous on this file:

/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
TrevorHansen commented 2 years ago

Thanks @aytey,

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.