other
(in-package "CGEN")
other
(include-book "basis")
other
(include-book "type")
other
(include-book "simple-graph-array")
other
(include-book "cgen-state")
other
(defrec cs% (defdata-type spilled-types eq-constraint range member-constraint additional-constraints) nil)
cs%-pfunction
(defun cs%-p (v) (declare (xargs :guard t)) (case-match v (('cs% dt st eqc int mem ac) (and (possible-defdata-type-p dt) (possible-defdata-type-list-p st) (or (pseudo-termp eqc) (eq 'empty-eq-constraint eqc)) (tau-intervalp int) (pseudo-termp mem) (pseudo-term-listp ac)))))
|is (symbol . cs%)|function
(defun |is (symbol . cs%)| (v) (declare (xargs :guard t)) (case-match v ((x . y) (and (symbolp x) (cs%-p y)))))
symbol-cs%-alistpfunction
(defun symbol-cs%-alistp (vs) (declare (xargs :guard t)) (if (consp vs) (and (|is (symbol . cs%)| (car vs)) (symbol-cs%-alistp (cdr vs))) nil))
other
(def put-additional-constraints. (vs term v-cs%-alst.) (decl :sig ((symbol-list pseudo-term symbol-cs%-alist) -> symbol-cs%-alist) :doc "put term in alist for all keys in vs") (if (endp vs) v-cs%-alst. (b* (((cons v cs%) (assoc-eq (car vs) v-cs%-alst.)) (cs% (change cs% additional-constraints (cons term (access cs% additional-constraints))))) (put-additional-constraints. (cdr vs) term (put-assoc-eq v cs% v-cs%-alst.)))))
other
(def insert-before-key (key entry alist) (decl :sig ((symbol entry symbol-alist) -> symbol-alist) :doc "insert entry before key in alist") (if (endp alist) nil (if (eq key (caar alist)) (cons entry alist) (cons (car alist) (insert-before-key key entry (cdr alist))))))
other
(def put-var-eq-constraint. (v1 v2 vl wrld v-cs%-alst.) (decl :sig ((symbol symbol vl plist-world symbol-cs%-alist) -> symbol-cs%-alist) :doc "put variable equality constraint in alist for key v") (declare (xargs :verify-guards nil)) (b* (((when (eql v1 v2)) v-cs%-alst.) ((cons & cs1%) (assoc-eq v1 v-cs%-alst.)) ((cons & cs2%) (assoc-eq v2 v-cs%-alst.)) (dt1 (access cs% cs1% :defdata-type)) (dt2 (access cs% cs2% :defdata-type)) (m (table-alist 'type-metadata-table wrld)) (a (table-alist 'type-alias-table wrld)) (p1 (predicate-name dt1 a m)) (p2 (predicate-name dt2 a m)) ((mv v other-v cs% other-cs%) (if (subtype-p p2 p1 wrld) (mv v1 v2 cs1% cs2%) (mv v2 v1 cs2% cs1%))) (eqc (access cs% cs% :eq-constraint)) (other-eqc (access cs% other-cs% :eq-constraint)) ((when (eq other-v eqc)) v-cs%-alst.) ((when (eq v other-eqc)) v-cs%-alst.) (- (cw? (and (verbose-stats-flag vl) (not (eq 'empty-eq-constraint eqc))) "CEgen/Note: Overwriting (variable) eq-constraint for ~x0 with ~x1~|" v other-v)) (cs% (change cs% eq-constraint other-v)) (v-cs%-alst. (put-assoc-eq v cs% v-cs%-alst.))) (insert-before-key v (cons other-v other-cs%) (remove1-assoc-eq other-v v-cs%-alst.))))
other
(def put-eq-constraint. (v term vl v-cs%-alst.) (decl :sig ((symbol pseudo-term vl symbol-cs%-alist) -> symbol-cs%-alist) :doc "put eq-constraint term in alist for key v") (b* (((cons & cs%) (assoc-eq v v-cs%-alst.)) (eqc (access cs% eq-constraint)) (- (cw? (and (verbose-stats-flag vl) (not (eq 'empty-eq-constraint eqc))) "CEgen/Note: Overwriting eq-constraint for ~x0 with ~x1~|" v term)) (cs% (change cs% eq-constraint term))) (put-assoc-eq v cs% v-cs%-alst.)))
other
(def put-member-constraint. (v term vl v-cs%-alst.) (decl :sig ((symbol pseudo-term vl symbol-cs%-alist) -> symbol-cs%-alist) :doc "put member-constraint term in alist for key v") (b* (((cons & cs%) (assoc-eq v v-cs%-alst.)) (memc (access cs% member-constraint)) (- (cw? (and (verbose-stats-flag vl) (not (equal 'empty-mem-constraint memc))) "CEgen/Note: Overwriting member-constraint for ~x0 with ~x1~|" v term)) (cs% (change cs% member-constraint term))) (put-assoc-eq v cs% v-cs%-alst.)))
other
(def put-defdata-type. (v typ vl v-cs%-alst.) (decl :sig ((symbol possible-defdata-type-p fixnum symbol-cs%-alist) -> symbol-cs%-alist) :doc "put defdata type typ in alist for key v") (b* (((cons & cs%) (assoc-eq v v-cs%-alst.)) (dt (access cs% defdata-type)) (- (cw? (and (verbose-stats-flag vl) (not (eq 'all dt))) "CEgen/Note: Overwriting defdata type for ~x0. ~x1 -> ~x2~|" v dt typ)) (cs% (change cs% defdata-type typ))) (put-assoc-eq v cs% v-cs%-alst.)))
process-return-lastfunction
(defun process-return-last (term) (declare (xargs :mode :logic :guard (pseudo-termp term))) (case-match term (('return-last . x) (process-return-last (car (last x)))) (& term)))
other
(defs (v-cs%-alist-from-term. (term vl wrld ans.)
(decl :sig ((pseudo-term fixnum
plist-world
symbol-cs%-alist) ->
symbol-cs%-alist)
:doc "helper to collect-constraints")
(declare (xargs :verify-guards nil))
(f* ((add-constraints... nil
(put-additional-constraints. fvars
term
ans.)) (add-eq/mem-constraint... (t1)
(if (membership-relationp r wrld)
(put-member-constraint. x
t1
vl
ans.)
(add-eq-constraint... t1)))
(add-eq-constraint... (t1)
(if (equivalence-relationp r wrld)
(if (symbolp t1)
(put-var-eq-constraint. x
t1
vl
wrld
ans.)
(put-eq-constraint. x
t1
vl
ans.))
(add-constraints...))))
(b* ((fvars (all-vars term)))
(case-match term
(('quote c) (declare (ignore c)) ans.)
((p (f . &)) (declare (ignore p f))
(add-constraints...))
(('not x) (put-eq-constraint. x ''nil vl ans.))
((p x) (declare (ignore p x))
(b* ((term (expand-lambda term)) (term (remove-guard-holders-weak term t))
((list p x) term)
(tname (is-type-predicate p wrld))
((cons & cs%) (assoc-eq x ans.))
(- (cw? (system-debug-flag vl)
"~| x: ~x0, ans.: ~x1, cs%: ~x2, P: ~x3, tname: ~x4~|"
x
ans.
cs%
p
tname))
(curr-typ (access cs% defdata-type))
(smaller-typ (meet tname curr-typ vl wrld)))
(if tname
(if (not (eq smaller-typ curr-typ))
(put-defdata-type. x
smaller-typ
vl
ans.)
ans.)
(add-constraints...))))
((r (f . &) (g . &)) (declare (ignore r f g))
(add-constraints...))
((r x ('quote c)) (add-eq/mem-constraint... (kwote c)))
((r ('quote c) x) (add-eq-constraint... (kwote c)))
((r x (f . args)) (add-eq/mem-constraint... (cons-term f args)))
((r (f . args) x) (add-eq-constraint... (cons-term f args)))
((r x y) (add-eq/mem-constraint... y))
(& (add-constraints...)))))))
other
(def v-cs%-alist-from-terms. (terms vl wrld ans.) (decl :sig ((pseudo-term-listp fixnum plist-worldp symbol-cs%-alist) -> symbol-cs%-alist) :doc "helper to collect-constraints%") (declare (xargs :verify-guards nil)) (if (endp terms) ans. (v-cs%-alist-from-terms. (cdr terms) vl wrld (v-cs%-alist-from-term. (car terms) vl wrld ans.))))
other
(def put-range-constraint. (v int v-cs%-alst.) (decl :sig ((symbolp tau-intervalp symbol-cs%-alistp) -> symbol-cs%-alistp) :doc "put interval int in alist for key v") (b* (((cons & cs%) (assoc-eq v v-cs%-alst.)) (cs% (change cs% range int))) (put-assoc-eq v cs% v-cs%-alst.)))
other
(def range-is-alias-p (interval type wrld) (decl :sig ((non-empty-non-universal-interval-p symbolp plist-worldp) -> boolean) :doc "is interval an alias of type?") (declare (xargs :verify-guards nil)) (b* ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi)) (lo-rel (access tau-interval interval :lo-rel)) (hi-rel (access tau-interval interval :hi-rel)) (m (table-alist 'type-metadata-table wrld)) (a (table-alist 'type-alias-table wrld)) (p (predicate-name type a m))) (case (access tau-interval interval :domain) (integerp (or (and (subtype-p p 'natp wrld) (equal lo 0) (null hi)) (and (subtype-p p 'posp wrld) (equal lo 1) (null hi)) (and (subtype-p p 'negp wrld) (null lo) (equal hi -1)))) (otherwise (or (and (subtype-p p 'positive-rationalp wrld) lo-rel (null hi) (equal lo 0)) (and (subtype-p p 'negative-rationalp wrld) hi-rel (null lo) (equal hi 0)))))))
other
(verify-termination empty-tau-intervalp)
singleton-tau-intervalpfunction
(defun singleton-tau-intervalp (interval) (b* ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi)) (lo-rel (access tau-interval interval :lo-rel)) (hi-rel (access tau-interval interval :hi-rel))) (and (access tau-interval interval :domain) (singleton-tau-intervalp lo-rel lo hi-rel hi))))
non-empty-non-universal-interval-pfunction
(defun non-empty-non-universal-interval-p (interval) (and interval (tau-intervalp interval) (access tau-interval interval :domain) (or (rationalp (access tau-interval interval :lo)) (rationalp (access tau-interval interval :hi))) (b* ((lo (access tau-interval interval :lo)) (hi (access tau-interval interval :hi)) (lo-rel (access tau-interval interval :lo-rel)) (hi-rel (access tau-interval interval :hi-rel))) (and (not (empty-tau-intervalp lo-rel lo hi-rel hi)) (not (singleton-tau-intervalp lo-rel lo hi-rel hi))))))
other
(def assimilate-apriori-type-information
(vs vt-dlist
tau-interval-alist
vl
wrld
ans.)
(decl :sig ((symbol-list symbol-doublet-list
alist
symbol-alist
fixnum
plist-world
symbol-cs%-alist) ->
symbol-cs%-alist)
:doc "overwrite into v-cs%-alst. the type information in type-alist/tau-interval-alist.
Put defdata symbol types into defdata-type field, but put constants
into eq-constraint field and put interval into range constraint field")
(declare (xargs :verify-guards nil))
(if (endp vs)
ans.
(b* ((x (car vs)) (prior-types-entry (assoc-eq x vt-dlist))
(- (cw? (and (verbose-stats-flag vl)
(consp prior-types-entry)
(consp (cdr prior-types-entry))
(not (null (cddr prior-types-entry))))
"~|CEgen/Warning: Ignoring rest of union types ~x0 ~|"
(cddr prior-types-entry)))
(typ-given (if (and (consp prior-types-entry)
(consp (cdr prior-types-entry)))
(cadr prior-types-entry)
'all))
((when (possible-constant-value-p typ-given)) (assimilate-apriori-type-information (cdr vs)
vt-dlist
tau-interval-alist
vl
wrld
(put-eq-constraint. x
typ-given
vl
ans.)))
(int-entry (assoc-eq x tau-interval-alist))
(int (cdr int-entry))
((when (singleton-tau-intervalp int)) (assimilate-apriori-type-information (cdr vs)
vt-dlist
tau-interval-alist
vl
wrld
(put-eq-constraint. x
(kwote (access tau-interval int :lo))
vl
ans.)))
((cons & cs%) (assoc-eq x ans.))
(curr-typ (access cs% defdata-type))
(final-typ (meet curr-typ
typ-given
vl
wrld))
(ans. (if (and (non-empty-non-universal-interval-p int)
(not (range-is-alias-p int
final-typ
wrld)))
(put-range-constraint. x int ans.)
ans.)))
(assimilate-apriori-type-information (cdr vs)
vt-dlist
tau-interval-alist
vl
wrld
(put-defdata-type. x
final-typ
vl
ans.)))))
other
(def-const *empty-cs%* (make cs% :defdata-type 'all :spilled-types 'nil :eq-constraint 'empty-eq-constraint :range (make-tau-interval nil nil nil nil nil) :member-constraint 'empty-mem-constraint :additional-constraints 'nil))
other
(def collect-constraints%
(hyps ordered-vars
top-vt-dlist
type-alist
tau-interval-alist
vl
wrld)
(decl :sig ((pseudo-term-listp symbol-listp
symbol-doublet-listp
alistp
symbol-alistp
fixnum
plist-worldp) ->
symbol-cs%-alist)
:doc "
* Synopsis
For each free variable compute/infer both the simple defdata types
and additional constraints on it.
* Input
hyps is a usually a list of hypotheses of the conjecture under query
and is a term-listp. ordered-vars is the free variables of hyps, but in the
variable dependency order as computed from the dependency graphs of hyps.
type-alist is the ACL2 context.
top-vt-dlist is meet of top-level dumb type inference and ACL2 type-alist info.
tau-interval-alist is the range type information inferred by Tau.
* Output
An alist mapping free variables to cs% record
")
(declare (xargs :verify-guards nil))
(f* ((unconstrained-v-cs%-alst (xs)
(pairlis$ xs
(make-list (len xs)
:initial-element *empty-cs%*))))
(b* ((v-cs%-alst (unconstrained-v-cs%-alst ordered-vars)) (v-cs%-alst (assimilate-apriori-type-information ordered-vars
top-vt-dlist
tau-interval-alist
vl
wrld
v-cs%-alst))
(context-hyps (reify-type-alist-hyps type-alist))
(hyps+ (filter-terms-with-vars (union-equal context-hyps hyps)
ordered-vars)))
(v-cs%-alist-from-terms. hyps+
vl
wrld
v-cs%-alst))))
other
(program)
other
(set-state-ok t)
other
(set-ignore-ok t)
one-way-unifyfunction
(defun one-way-unify (pat pattern-x given given-x) "do match but make sure pattern-x is matched with given-x" (b* (((mv ans alist) (one-way-unify pat given)) ((unless (eq (get1 pattern-x alist) given-x)) (list nil nil))) (list ans alist)))
other
(mutual-recursion (defun innermost-subterm-one-way-unify (pat pat-x term x acc) (cond ((variablep term) acc) ((fquotep term) acc) (t (b* (((list ans alist) (one-way-unify pat pat-x term x))) (cond (ans (innermost-subterm-one-way-unify-lst pat pat-x (fargs term) x (list ans alist))) (t (innermost-subterm-one-way-unify-lst pat pat-x (fargs term) x acc))))))) (defun innermost-subterm-one-way-unify-lst (pat pat-x terms x acc) (cond ((null terms) acc) (t (b* (((list ans alist) (innermost-subterm-one-way-unify pat pat-x (car terms) x acc))) (cond (ans (innermost-subterm-one-way-unify-lst pat pat-x (cdr terms) x (list ans alist))) (t (innermost-subterm-one-way-unify-lst pat pat-x (cdr terms) x acc))))))))
other
(include-book "tools/templates" :dir :system)
sublis-varfunction
(defun sublis-var (sigma term) (sublis-var sigma term))
filter-splice-entriesfunction
(defun filter-splice-entries (replace-alist) (if (endp replace-alist) 'nil (b* (((cons key val) (car replace-alist))) (if (equal "@" (subseq (symbol-name key) 0 1)) (cons (car replace-alist) (filter-splice-entries (cdr replace-alist))) (filter-splice-entries (cdr replace-alist))))))
remove1-assoc-eq-lstfunction
(defun remove1-assoc-eq-lst (xs alist) (if (endp xs) alist (remove1-assoc-eq-lst (cdr xs) (remove1-assoc-eq (car xs) alist))))
eval-meta-replacefunction
(defun eval-meta-replace (mc usigma vl wrld) (b* (((unless (consp mc)) (mv nil nil)) (mc (listlis (strip-cars mc) (sublis-var-lst usigma (strip-cadrs mc)))) (vars (strip-cars mc)) ((mv erp replace-alist) (trans-my-ev-w `(let ,CGEN::MC (declare (ignorable ,@CGEN::VARS)) ,(CGEN::MAKE-VAR-VALUE-CONS-BINDINGS CGEN::VARS 'NIL)) 'eval-meta-replace wrld nil)) (splice-alist (filter-splice-entries replace-alist)) (atom-alist (remove1-assoc-eq-lst (strip-cars splice-alist) replace-alist)) ((when erp) (prog2$ (cw? (debug-flag vl) "~| Error in evaluating meta-replace ~x0 given sigma ~x1~%" mc usigma) (mv nil nil)))) (mv atom-alist splice-alist)))
match-constraint1function
(defun match-constraint1 (constraint-rule given-c x vl wrld) "does given-C match with this constraint-rule with a variable renaming for x" (declare (ignorable vl)) (b* ((pattern-c (get1 :constraint constraint-rule)) (pattern-x (get1 :constraint-variable constraint-rule)) ((list yesp usigma) (if (eq :subterm-match (get1 :match-type constraint-rule)) (innermost-subterm-one-way-unify pattern-c pattern-x given-c x (list nil nil)) (one-way-unify pattern-c pattern-x given-c x))) ((unless yesp) nil) (- (cw? (debug-flag vl) "~| Match successful: ~x0 ~%" usigma)) (meta-precondition (get1 :meta-precondition constraint-rule)) (vars (strip-cars usigma)) (letb (listlis vars (kwote-lst (strip-cdrs usigma)))) ((mv erp okp) (trans-my-ev-w `(let ,CGEN::LETB (declare (ignorable ,@CGEN::VARS)) ,CGEN::META-PRECONDITION) 'match-constraint1 wrld nil)) ((unless (and (not erp) okp)) nil) (rule-form (get1 :rule constraint-rule)) (rule-form-instance (sublis-var usigma rule-form)) (mc (get1 :meta-replace constraint-rule)) ((mv atom-alist splice-alist) (eval-meta-replace mc usigma vl wrld)) (rule-form-instance-renamed (let ((str-alist `((,(SYMBOL-NAME CGEN::PATTERN-X) . ,(SYMBOL-NAME CGEN::X))))) (template-subst rule-form-instance :str-alist str-alist :atom-alist atom-alist :splice-alist splice-alist :pkg-sym x)))) rule-form-instance-renamed))
record-pfunction
(defun record-p (type wrld) (b* ((type-entry (get1 type (type-metadata-table wrld))) (pdef (get1 :prettyified-def type-entry))) (and (consp pdef) (equal (car pdef) 'record))))
expand-recordfunction
(defun expand-record (x type wrld) (b* ((type-entry (get1 type (type-metadata-table wrld))) (ndef (get1 :normalized-def type-entry)) (conx (car ndef)) (fields (strip-cars (cdr ndef))) (ftypes (strip-cdrs (cdr ndef))) (new-names (modify-symbol-lst (string-append (symbol-name x) ".") fields "" (symbol-package-name x))) (m (table-alist 'type-metadata-table wrld)) (a (table-alist 'type-alias-table wrld)) (fpreds (predicate-names ftypes a m)) (pred-calls (listlis fpreds new-names))) (mv (cons conx new-names) pred-calls)))
other
(defloop match-constraint/loop (constraint-rules c x vl wrld) "return first matched" (for ((crule in constraint-rules)) (thereis (match-constraint1 crule c x vl wrld))))
match-constraintfunction
(defun match-constraint (x type c vl wrld) (b* ((m (type-metadata-table wrld)) (a (table-alist 'type-alias-table wrld)) ((unless (predicate-name type a m)) nil) (constraint-rules (get2 type :constraint-rules m))) (match-constraint/loop constraint-rules c x vl wrld)))
other
(include-book "propagate")
other
(include-book "misc/bash" :dir :system)
other
(mutual-recursion (defun refine-enum-shape1 (x type constraints vl state rtermb new-hyps) "Infer a more specialized ACL2 expression for x:type given additional constraints on x. If no more constraints return rtermB, new-hyps else pick c from constraints iterate over trigger-constraints t stored for type till one finds a 'match' (i.e. c (subterm) matches t and satisfies the trigger's condition) from rule-action, get specialized exp for x and new-hyps on introduced variables store exp for x in rtermB, new-hyps++ get type-bindings for all introduced variables constraints' := simplify x=exp + new-hyps ++ constraints for each (x' type') in type-bindings refine-enum-shape(x', type', constraints' on x', rtermB, new-hyps) " (if (endp constraints) (value (list rtermb new-hyps)) (b* ((c (car constraints)) (rule (match-constraint x type c vl (w state))) ((unless rule) (refine-enum-shape1 x type (cdr constraints) vl state rtermb new-hyps)) (`(implies ,CGEN::HYP (equal ,CGEN::VAR ,CGEN::REFINED-EXP)) rule) (rule-hyps (if (eq (car hyp) 'and) (cdr hyp) (list hyp))) ((unless (and (variablep var) (equal var x))) (prog2$ (cw? (verbose-stats-flag vl) "Cgen/refine-enum-shape1:: Expected ~x0 to be an elim rule for var ~x1" rule x) (mv t (list rtermb new-hyps) state))) ((when (intersection-eq (list x) (all-vars refined-exp))) (prog2$ (cw? (verbose-stats-flag vl) "Cgen/refine-enum-shape1:: An Invariant broke!! ~x0 should not occur in ~x1." x refined-exp) (mv t (list rtermb new-hyps) state))) (new-hyps (union-equal rule-hyps new-hyps)) (rtermb (acons x refined-exp rtermb)) (var-type-dlist (dumb-type-alist-infer rule-hyps (all-vars-lst rule-hyps) vl (w state))) ((er constraints~) (simplify-term-lst (subst-var-lst refined-exp x (cdr constraints)) rule-hyps 'nil state))) (refine-enum-shapes1 var-type-dlist constraints~ vl state rtermb new-hyps)))) (defun refine-enum-shapes1 (var-type-dlist constraints vl state rtermb new-hyps) (if (endp var-type-dlist) (value (list rtermb new-hyps)) (b* (((list x type) (car var-type-dlist)) ((er (list rtermb1 new-hyps1)) (if (record-p type (w state)) (b* (((mv rec-expansion rec-field-hyps) (expand-record x type (w state)))) (value (list (acons x rec-expansion 'nil) rec-field-hyps))) (refine-enum-shape1 x type constraints vl state 'nil 'nil))) (rtermb (union-equal rtermb1 rtermb)) (new-hyps (union-equal new-hyps1 new-hyps))) (refine-enum-shapes1 (cdr var-type-dlist) constraints vl state rtermb new-hyps)))))
other
(mutual-recursion (defun expand-term-under-bindings (term b) (cond ((variablep term) (if (assoc-eq term b) (expand-term-under-bindings (cdr (assoc-eq term b)) (remove1-assoc-eq term b)) term)) ((fquotep term) term) (t (cons (ffn-symb term) (expand-terms-under-bindings (fargs term) b))))) (defun expand-terms-under-bindings (terms b) (if (endp terms) 'nil (cons (expand-term-under-bindings (car terms) b) (expand-terms-under-bindings (cdr terms) b)))))
other
(defloop contains-var (x terms) "filter terms that contain variable x" (for ((term in terms)) (append (and (member-eq x (all-vars term)) (list term)))))
other
(defloop remove-terms-with-vars (terms xs) "remove terms with variables in xs" (for ((term in terms)) (append (and (not (intersection-eq xs (all-vars term))) (list term)))))
refine-enum-shapefunction
(defun refine-enum-shape (var type constraints vl state) "Infer a more specialized (refined) ACL2 expression for x:type given additional constraints on x." (b* (((er ans) (refine-enum-shape1 var type constraints vl state 'nil 'nil)) ((list rtermb additional-hyps) ans) ((when (null rtermb)) (value (list 'nil 'nil))) (refined-term (expand-term-under-bindings var rtermb)) (elimed-vars (strip-cars rtermb)) (additional-hyps (remove-terms-with-vars additional-hyps elimed-vars)) (new-vars (all-vars-lst additional-hyps)) (vars-in-refined-term (all-vars refined-term)) (- (cw? (debug-flag vl) "vars-in-additional-hyps: ~x0 and vars-in-refined-term: ~x1" new-vars vars-in-refined-term)) (- (assert$ (subsetp-eq vars-in-refined-term new-vars) nil))) (value (list refined-term additional-hyps))))