Satlink-parse-variable-line
- Signature
(satlink-parse-variable-line x n xl saw-zero-p env$)
→
(mv error saw-zero-p env$)
- Arguments
- x — String we're processing.
Guard (stringp x).
- n — Current position in x.
Guard (natp n).
- xl — Pre-computed length of x.
Guard (equal xl (length x)).
- saw-zero-p — Have we seen a 0 yet?.
Guard (booleanp saw-zero-p).
- env$ — Satisfying assignment we're populating.
- Returns
- error — True if there is an error parsing this line.
- saw-zero-p — Did we ever see 0? (checked later).
- env$ — Updated satisfying assignment.
Definitions and Theorems
Function: satlink-parse-variable-line
(defun satlink-parse-variable-line (x n xl saw-zero-p env$)
(declare (xargs :stobjs (env$)))
(declare (xargs :guard (and (stringp x)
(natp n)
(booleanp saw-zero-p)
(equal xl (length x)))))
(declare (xargs :guard (<= n xl)))
(let ((__function__ 'satlink-parse-variable-line))
(declare (ignorable __function__))
(b*
((n (satlink-skip-ws x n xl))
((when (mbe :logic (zp (- (nfix xl) n))
:exec (int= xl n)))
(mv nil saw-zero-p env$))
(minus-p (eql (char x n) #\-))
(n (if minus-p (+ n 1) n))
((when (int= xl n))
(cw
"SATLINK: Error parsing variable line: ends with minus? ~s0~%"
x)
(mv t saw-zero-p env$))
((mv val len)
(str::parse-nat-from-string x 0 0 n xl))
((when (zp len))
(cw "SATLINK: Error parsing variable line: ~s0~%"
x)
(mv t saw-zero-p env$))
((when (and (zp val) saw-zero-p))
(cw "SATLINK: Error: saw zero multiple times: ~s0~%"
x)
(mv t saw-zero-p env$))
(saw-zero-p (or saw-zero-p (zp val)))
(index (1- val))
(env$ (cond ((zp val) env$)
((< index (bits-length env$))
(set-bit index (if minus-p 0 1) env$))
(t env$))))
(satlink-parse-variable-line x (+ n len)
xl saw-zero-p env$))))
