Keep names in smtlib2 format

[weaversa]

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 replacing s# 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).

sawscript> prove (offline_smtlib2 "names") {{ (\myName1 myName2 -> myName1 == myName2) : Integer -> Integer -> Bit }}
[Valid]
sawscript> :q
$ more names.prove0.smt2
; Automatically created by SBV on 2021-03-21 17:50:06.252006 UTC
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic ALL) ; has unbounded values, using catch-all.
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
; --- skolem constants ---
(declare-fun s0 () Int) ; tracks user variable "x0"
(declare-fun s1 () Int) ; tracks user variable "x1"
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s2 () Bool (= s0 s1))
(define-fun s3 () Bool (not s2))
(assert s3)
(check-sat)

[weaversa]

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)

[brianhuffman]

The code that chooses the "user" variable names for SBV is in the saw-core-sbv package, functions newVars and nextId:

saw-script/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

Lines 675 to 698 in 7b8c134

	nextId :: StateT Int IO String
	nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s))
	unzipMap :: Map k (a, b) -> (Map k a, Map k b)
	unzipMap m = (fmap fst m, fmap snd m)
	newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue)
	newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s)
	newVars FOTInt = nextId <&> \s-> (IntegerLabel s, vInteger <$> existsSInteger s)
	newVars (FOTIntMod n) = nextId <&> \s-> (IntegerLabel s, VIntMod n <$> existsSInteger s)
	newVars (FOTVec n FOTBit) =
	if n == 0
	then nextId <&> \s-> (WordLabel s, return (vWord (literalSWord 0 0)))
	else nextId <&> \s-> (WordLabel s, vWord <$> existsSWord s (fromIntegral n))
	newVars (FOTVec n tp) = do
	(labels, vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVars tp)
	return (VecLabel labels, VVector <$> traverse (fmap ready) vals)
	newVars (FOTArray{}) = fail "FOTArray unimplemented for backend"
	newVars (FOTTuple ts) = do
	(labels, vals) <- V.unzip <$> traverse newVars (V.fromList ts)
	return (TupleLabel labels, vTuple <$> traverse (fmap ready) (V.toList vals))
	newVars (FOTRec tm) = do
	(labels, vals) <- unzipMap <$> (traverse newVars tm :: StateT Int IO (Map FieldName (Labeler, Symbolic SValue)))
	return (RecLabel labels, vRecord <$> traverse (fmap ready) (vals :: (Map FieldName (Symbolic SValue))))

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:

• When there is no lambda-bound variable name present, we'll still have to make up names sometimes.
• When the lambda-bound variable has a compound type, we'll have to generate a bunch of names with suffixes for all of its basic components.

Anyway, I think this is a good idea, and we should go ahead and try to implement it.

[brianhuffman]

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.

[brianhuffman]

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.

[weaversa]

May I suggest a prefix of s## rather than x## so the names also track with the smtlib names?

[brianhuffman]

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.)

[weaversa]

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.