search

leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
73 stars 12 forks source link

Feature Request: Allow users to map suitable Lean functions to corresponding SMT functions #12

Open shigoel opened 10 months ago

shigoel commented 10 months ago

Solvers are sensitive to encoding, and for certain problems, it would help if the user could dictate whether the Lean functions in their conjecture should be mapped to a corresponding SMT function. Here is an illustrative example:

import Std.Data.BitVec
import Auto

set_option auto.smt true
set_option auto.smt.trust true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true
set_option trace.auto.smt.model true
set_option trace.auto.smt.proof false

def prop (a1 a2 b1 b2 : Std.BitVec 64) : Bool :=
  Std.BitVec.ule (a2 - b1) (b2 - b1) &&
  Std.BitVec.ule (a1 - b1) (a2 - b1)

set_option auto.smt.timeout 200 -- seconds
set_option trace.auto.smt.printCommands true in
set_option auto.smt.savepath "/tmp/prop_transitive.smt2" in
theorem prop_transitive
  (h1 : prop a1 a2 b1 b2)
  (h2 : prop b1 b2 c1 c2) :
  prop a1 a2 c1 c2 := by
  revert h1 h2
  auto d[prop] --- times out

Auto inlines prop, which adversely affects the SMT solving time. On the other hand, z3 can solve this problem in ~10s in my hand-written SMT file below, where prop appears as an SMT function.

(set-logic ALL)
(set-option :interactive-mode true)

(declare-const a1 (_ BitVec 64))
(declare-const a2 (_ BitVec 64))
(declare-const b1 (_ BitVec 64))
(declare-const b2 (_ BitVec 64))
(declare-const c1 (_ BitVec 64))
(declare-const c2 (_ BitVec 64))

(define-fun prop ((a1 (_ BitVec 64))
                  (a2 (_ BitVec 64))
                  (b1 (_ BitVec 64))
                  (b2 (_ BitVec 64)))
  Bool  
  (and (bvule (bvadd a2 (bvneg b1)) (bvadd b2 (bvneg b1)))
       (bvule (bvadd a1 (bvneg b1)) (bvadd a2 (bvneg b1)))))

;; Preferred solver: z3 (~10s)

;; prop_transitive
(assert (not
         (=> (and (prop a1 a2 b1 b2)
                  (prop b1 b2 c1 c2))
             (prop a1 a2 c1 c2))))

(check-sat)