Closed weaversa closed 3 years ago
Same request for the w4
variants (offline_w4_unint_z3
, etc.). In these cases the comment is gone, so perhaps a comment could be added?
(set-option :produce-models true)
; :1:0
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(define-fun x!0 () Bool (= x0 x1))
(define-fun x!1 () Bool (not x!0))
(assert x!1)
(check-sat)
(exit)
The code that chooses the "user" variable names for SBV is in the saw-core-sbv
package, functions newVars
and nextId
:
https://github.com/GaloisInc/saw-script/blob/7b8c134a1a2fad07620af1f17b246d3012744e80/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs#L675-L698
Right now, function newVars
generates these variables and their names based only on the type. We could probably modify this function to also take a suggested name along with the type, with a couple of caveats:
Anyway, I think this is a good idea, and we should go ahead and try to implement it.
One thing we'll need to worry about when generating these names: We need to ensure that all the names we use are distinct; otherwise we might have problems trying to obtain counterexample models. This means that we will need to have an operation for "freshening" a name, generating a unique variant in the case that a desired name is already in use.
With #1279, we can now do an offline_smtlib2
command like prove (offline_smtlib2 "foobar") {{ \(xs:[8][8]) ys -> xs + ys == ys + xs }}
, and we get a generated .smt2
file like this:
; Automatically created by SBV on 2021-04-29 11:52:27.996824 PDT
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 8)) ; tracks user variable "x0_xs.0"
(declare-fun s1 () (_ BitVec 8)) ; tracks user variable "x1_xs.1"
(declare-fun s2 () (_ BitVec 8)) ; tracks user variable "x2_xs.2"
(declare-fun s3 () (_ BitVec 8)) ; tracks user variable "x3_xs.3"
(declare-fun s4 () (_ BitVec 8)) ; tracks user variable "x4_xs.4"
(declare-fun s5 () (_ BitVec 8)) ; tracks user variable "x5_xs.5"
(declare-fun s6 () (_ BitVec 8)) ; tracks user variable "x6_xs.6"
(declare-fun s7 () (_ BitVec 8)) ; tracks user variable "x7_xs.7"
(declare-fun s8 () (_ BitVec 8)) ; tracks user variable "x8_ys.0"
(declare-fun s9 () (_ BitVec 8)) ; tracks user variable "x9_ys.1"
(declare-fun s10 () (_ BitVec 8)) ; tracks user variable "x10_ys.2"
(declare-fun s11 () (_ BitVec 8)) ; tracks user variable "x11_ys.3"
(declare-fun s12 () (_ BitVec 8)) ; tracks user variable "x12_ys.4"
(declare-fun s13 () (_ BitVec 8)) ; tracks user variable "x13_ys.5"
(declare-fun s14 () (_ BitVec 8)) ; tracks user variable "x14_ys.6"
(declare-fun s15 () (_ BitVec 8)) ; tracks user variable "x15_ys.7"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s16 () (_ BitVec 8) (bvadd s0 s8))
(define-fun s17 () (_ BitVec 8) (bvadd s1 s9))
(define-fun s18 () (_ BitVec 8) (bvadd s2 s10))
(define-fun s19 () (_ BitVec 8) (bvadd s3 s11))
(define-fun s20 () (_ BitVec 8) (bvadd s4 s12))
(define-fun s21 () (_ BitVec 8) (bvadd s5 s13))
(define-fun s22 () (_ BitVec 8) (bvadd s6 s14))
(define-fun s23 () (_ BitVec 8) (bvadd s7 s15))
(assert false)
(check-sat)
So I just kept the sequentially-numbered x##
as a prefix (to ensure uniqueness of names), and then concatenate that with the actual user-provided variable name, plus dot-separated suffixes to indicate array/tuple/record elements.
May I suggest a prefix of s##
rather than x##
so the names also track with the smtlib names?
Sure, we could change from x
to s
[EDIT: I've now done that], but SBV doesn't actually give us any control over what actual smtlib names are used. They might stay in sync if we're lucky, but we can't guarantee that. (I think SBV also uses names from the same unique name supply for things like constant tables, so the names would probably get out of sync when you use certain features or operations.)
I see. If it's not possible to ensure the mapping is accurate, its probably better not to try -- a partial solution would likely confuse.
It would be nice (for offline solving) if the offline format (smtlib2) kept variable names. Instead it references them with
x#
in a comment that says , for example; tracks user variable "x0"
. Can the comment also include the user-provided variable name? I'm ambivalent to replacings#
with the actual variable name. The comment is good enough for me, so long as the format of the string is reliable (for parsing by some other tool).