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

[shigoel]

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)