search

cvc5 / cvc5-projects

1 stars 0 forks source link

A bitvector VC we'd like to see solved #463

Open florianschanda opened 6 years ago

florianschanda commented 6 years ago

Hi,

One of our tests contains this VC and I was wondering of you could do something about it :)

(set-info :smt-lib-version 2.6)
(set-logic QF_BV)

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

(assert
  (not
   (= (bvmul (bvadd x y) (bvadd x y))
      (bvadd (bvmul x x) (bvmul y (bvadd (bvmul #x00000002 x) y))))))
(check-sat)
mpreiner commented 6 years ago

How often do these patterns occur in your tests? I'll have a look if we can add some normalization for these kind of problems since this can be solved by rewriting.

florianschanda commented 6 years ago

This specific one, twice - in our testsuite. But these kind of identities might pop up in users code as well. And, since its re-writing it doesn't sound like it would cause regressions?

I'll send you the rest of the VCs for this specific test as its reasonably full of this kind of stuff.

florianschanda commented 6 years ago

Also, if it helps; I think Z3 is doing this via re-writes too - so they either thought its a good idea in general or they has some user need.

florianschanda commented 6 years ago

In my bag of benchmarks https://github.com/florianschanda/smtlib_schanda/commit/0af22cba9381077175a886cecb085b0176ee25d4, the following VCs are from this test (all in directory spark_2014_all):

UFBVDTLIRA/QA31-008von_neumann_redone___p32.adb_100_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_100_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_100_64_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_102_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_102_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_104_34_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_104_34_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_104_46_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_106_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_106_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_108_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_108_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_108_47_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_110_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_110_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_112_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_112_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_113_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_113_33_loop_invariant_init2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_113_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_113_33_loop_invariant_preserv2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_113_89_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_114_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_114_33_loop_invariant_init2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_114_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_114_33_loop_invariant_preserv2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_114_57_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_116_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_116_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_116_33_loop_invariant_preserv2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_116_33_loop_invariant_preserv3.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_123_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_123_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_123_41_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_125_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_125_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_125_33_loop_invariant_preserv2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_125_51_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_128_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_129_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_130_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_130_42_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_131_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_131_22_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_132_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_133_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_134_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_135_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_136_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_137_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_139_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_13_31_range_check.smt2 UFBVDTLIRA/QA31-008__von_neumannredonep32.adb_140_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_148_29_range_check.smt2 UFBVDTLIRA/QA31-008von_neumannredonep32.adb_21_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone___p32.adb_21_22_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_58_22_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_67_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_67_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_71_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_71_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_72_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_72_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_73_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_73_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_76_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_76_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_76_40_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_76_40_precondition2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_77_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_77_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_77_34_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_77_34_precondition2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_79_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_79_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_80_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_80_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_80_54_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_80_54_precondition2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_82_25_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_82_25_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_82_39_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_82_39_precondition2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_88_28_assert.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_88_28_assert2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_88_53_precondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_88_53_precondition2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_92_23_division_check.smt2 UFBVDTLIRA/QA31-008__von_neumannredonep32.adb_92_23_division_check2.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.adb_96_10_loop_variant.smt2 UFBVDTLIRA/QA31-008von_neumannredonep32.adb_98_33_loop_invariant_init.smt2 UFBVDTLIRA/QA31-008von_neumann_redone___p32.adb_98_33_loop_invariant_preserv.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.ads_20_14_postcondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.ads_24_19_postcondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.ads_24_20_postcondition.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.ads_24_20_postcondition3.smt2 UFBVDTLIRA/QA31-008von_neumann_redone_p32.ads_27_19_postcondition2.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert10.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert3.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert4.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert5.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert6.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert7.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert8.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.adb_21_22_assert9.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.ads_37_19_postcondition.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.ads_37_19_postcondition2.smt2 UFBVDTNIRA/QA31-008von_neumann_redone_p32.ads_37_46_overflow_check.smt2 UFBVDTNIRA/QA31-008__von_neumannredonep32.ads_40_41_overflow_check.smt2

The one I mentioned here is a stripped down version of QA31-008__von_neumann_redone___p32.adb_21_22_assert.smt2

ajreynol commented 2 years ago

Moving to projects, as this is "performance".