other
(in-package "ACL2")
polys-from-type-setfunction
(defun polys-from-type-set (term force-flag dwp type-alist ens wrld ttree) (if (good-pot-varp term) (mv-let (ts ts-ttree) (type-set term force-flag dwp type-alist ens wrld ttree nil nil) (cond ((ts-subsetp ts *ts-zero*) (list (add-linear-terms :rhs term (base-poly ts-ttree '<= t nil)) (add-linear-terms :lhs term (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-one*) (list (add-linear-terms :lhs *1* :rhs term (base-poly ts-ttree '<= t nil)) (add-linear-terms :lhs term :rhs *1* (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-bit*) (list (add-linear-terms :lhs *0* :rhs term (base-poly ts-ttree '<= t nil)) (add-linear-terms :lhs term :rhs *1* (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-integer>1*) (list (add-linear-terms :lhs *2* :rhs term (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-positive-integer*) (list (add-linear-terms :lhs *1* :rhs term (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-negative-integer*) (list (add-linear-terms :lhs term :rhs ''-1 (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-positive-rational*) (list (add-linear-terms :rhs term (base-poly ts-ttree '< t nil)))) ((ts-subsetp ts *ts-negative-rational*) (list (add-linear-terms :lhs term (base-poly ts-ttree '< t nil)))) ((ts-subsetp ts *ts-non-negative-rational*) (list (add-linear-terms :rhs term (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts *ts-non-positive-rational*) (list (add-linear-terms :lhs term (base-poly ts-ttree '<= t nil)))) ((ts-subsetp ts (ts-union *ts-non-positive-rational* *ts-one*)) (list (add-linear-terms :lhs term :rhs *1* (base-poly ts-ttree '<= t nil)))) (t nil))) (er hard 'inverse-polys "A presumptive pot-label, ~x0, has turned out to be illegitimate. ~ If possible, please send a script reproducing this error ~ to the authors of ACL2." term)))
add-type-set-polysfunction
(defun add-type-set-polys (var-lst new-pot-lst old-pot-lst already-noted-vars pt nonlinearp type-alist ens force-flg wrld) (cond ((null var-lst) (let ((new-var-lst (changed-pot-vars new-pot-lst old-pot-lst already-noted-vars))) (if new-var-lst (add-type-set-polys new-var-lst new-pot-lst new-pot-lst new-var-lst pt nonlinearp type-alist ens force-flg wrld) (mv nil new-pot-lst)))) (t (mv-let (contradictionp new-new-pot-lst) (add-polys0 (polys-from-type-set (car var-lst) force-flg nil type-alist ens wrld nil) new-pot-lst pt nonlinearp t) (cond (contradictionp (mv contradictionp nil)) (t (add-type-set-polys (cdr var-lst) new-new-pot-lst old-pot-lst already-noted-vars pt nonlinearp type-alist ens force-flg wrld)))))))
add-polynomial-inequalitiesfunction
(defun add-polynomial-inequalities (lst pot-lst pt nonlinearp type-alist ens force-flg wrld) (mv-let (contradictionp new-pot-lst) (add-polys0 lst pot-lst pt nonlinearp t) (cond (contradictionp (mv contradictionp nil)) (t (let ((changed-pot-vars (changed-pot-vars new-pot-lst pot-lst nil))) (add-type-set-polys changed-pot-vars new-pot-lst new-pot-lst changed-pot-vars pt nonlinearp type-alist ens force-flg wrld))))))
add-polysfunction
(defun add-polys (lst pot-lst pt nonlinearp type-alist ens force-flg wrld) (add-polynomial-inequalities lst pot-lst pt nonlinearp type-alist ens force-flg wrld))
eval-ground-subexpressions1mutual-recursion
(mutual-recursion (defun eval-ground-subexpressions1 (term ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((or (variablep term) (fquotep term) (eq (ffn-symb term) 'hide)) (mv nil term ttree memo)) ((flambda-applicationp term) (let ((lam (ffn-symb term))) (mv-let (flg args ttree memo) (eval-ground-subexpressions1-lst (fargs term) ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((all-quoteps args) (mv-let (flg val ttree memo) (eval-ground-subexpressions1 (sublis-var (pairlis$ (lambda-formals (ffn-symb term)) args) (lambda-body lam)) ens wrld safe-mode gc-off ttree hands-off-fns memo) (declare (ignore flg)) (mv t val ttree memo))) (t (mv-let (flg-body body ttree memo) (eval-ground-subexpressions1 (lambda-body lam) ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((or flg flg-body) (mv t (fcons-term (if flg-body (make-lambda (lambda-formals lam) body) lam) args) ttree memo)) (t (mv nil term ttree memo))))))))) ((eq (ffn-symb term) 'if) (mv-let (flg1 arg1 ttree memo) (eval-ground-subexpressions1 (fargn term 1) ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((quotep arg1) (if (cadr arg1) (mv-let (flg2 arg2 ttree memo) (eval-ground-subexpressions1 (fargn term 2) ens wrld safe-mode gc-off ttree hands-off-fns memo) (declare (ignore flg2)) (mv t arg2 ttree memo)) (mv-let (flg3 arg3 ttree memo) (eval-ground-subexpressions1 (fargn term 3) ens wrld safe-mode gc-off ttree hands-off-fns memo) (declare (ignore flg3)) (mv t arg3 ttree memo)))) (t (mv-let (flg2 arg2 ttree memo) (eval-ground-subexpressions1 (fargn term 2) ens wrld safe-mode gc-off ttree hands-off-fns memo) (mv-let (flg3 arg3 ttree memo) (eval-ground-subexpressions1 (fargn term 3) ens wrld safe-mode gc-off ttree hands-off-fns memo) (mv (or flg1 flg2 flg3) (if (or flg2 flg3) (if (equal arg2 arg3) arg2 (fcons-term* 'if arg1 arg2 arg3)) (if flg1 (fcons-term 'if (cons arg1 (cdr (fargs term)))) term)) ttree memo))))))) (t (let ((pair (assoc-equal term memo))) (cond (pair (mv t (or (cdr pair) term) ttree memo)) (t (mv-let (flg args ttree memo) (eval-ground-subexpressions1-lst (fargs term) ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((and (logicp (ffn-symb term) wrld) (all-quoteps args) (enabled-xfnp (ffn-symb term) ens wrld) (not (member-eq (ffn-symb term) hands-off-fns)) (not (getpropc (ffn-symb term) 'constrainedp nil wrld))) (mv-let (erp val) (pstk (ev-fncall-w (ffn-symb term) (strip-cadrs args) wrld nil safe-mode gc-off t nil)) (cond (erp (cond (flg (let ((new-term (cons-term (ffn-symb term) args))) (mv t new-term ttree (acons term new-term memo)))) (t (mv nil term ttree (acons term nil memo))))) (t (let ((kwote-val (kwote val))) (mv t kwote-val (push-lemma (fn-rune-nume (ffn-symb term) nil t wrld) ttree) (acons term kwote-val memo))))))) (flg (mv t (cons-term (ffn-symb term) args) ttree memo)) (t (mv nil term ttree memo)))))))))) (defun eval-ground-subexpressions1-lst (lst ens wrld safe-mode gc-off ttree hands-off-fns memo) (cond ((null lst) (mv nil nil ttree memo)) (t (mv-let (flg1 x ttree memo) (eval-ground-subexpressions1 (car lst) ens wrld safe-mode gc-off ttree hands-off-fns memo) (mv-let (flg2 y ttree memo) (eval-ground-subexpressions1-lst (cdr lst) ens wrld safe-mode gc-off ttree hands-off-fns memo) (mv (or flg1 flg2) (if (or flg1 flg2) (cons x y) lst) ttree memo)))))))
eval-ground-subexpressionsfunction
(defun eval-ground-subexpressions (term ens wrld state ttree) (mv-let (flg x ttree memo) (eval-ground-subexpressions1 term ens wrld (f-get-global 'safe-mode state) (gc-off state) ttree nil nil) (declare (ignore memo)) (mv flg x ttree)))
eval-ground-subexpressions-lstfunction
(defun eval-ground-subexpressions-lst (lst ens wrld state ttree) (mv-let (flg x ttree memo) (eval-ground-subexpressions1-lst lst ens wrld (f-get-global 'safe-mode state) (gc-off state) ttree nil nil) (declare (ignore memo)) (mv flg x ttree)))
poly-setfunction
(defun poly-set (op poly1 poly2) (cond ((eq op 'and) (cond ((or (eq poly1 nil) (silly-polyp poly1)) (cond ((silly-polyp poly2) nil) (t (list (list poly2))))) ((silly-polyp poly2) (list (list poly1))) (t (list (list poly1 poly2))))) ((or (silly-polyp poly1) (silly-polyp poly2)) nil) ((impossible-polyp poly1) (list (list (change poly poly2 :ttree (cons-tag-trees (access poly poly1 :ttree) (access poly poly2 :ttree)) :parents (marry-parents (access poly poly1 :parents) (access poly poly2 :parents)))))) ((impossible-polyp poly2) (list (list (change poly poly1 :ttree (cons-tag-trees (access poly poly1 :ttree) (access poly poly2 :ttree)) :parents (marry-parents (access poly poly1 :parents) (access poly poly2 :parents)))))) (t (list (list poly1) (list poly2)))))
linearize1function
(defun linearize1 (term positivep type-alist ens force-flg wrld ttree state) (mv-let (flg temp ttree) (eval-ground-subexpressions term ens wrld state ttree) (declare (ignore flg)) (mv-let (not-flg atm) (strip-not temp) (let ((positivep (if not-flg (not positivep) positivep))) (cond ((inequalityp atm) (let ((lhs (fargn atm 1)) (rhs (fargn atm 2))) (mv-let (ts-lhs ts-ttree) (type-set lhs force-flg nil type-alist ens wrld ttree nil nil) (mv-let (ts-rhs ts-ttree) (type-set rhs force-flg nil type-alist ens wrld ts-ttree nil nil) (if positivep (cond ((and (ts-integerp ts-lhs) (ts-integerp ts-rhs)) (poly-set 'and nil (add-linear-terms :lhs lhs :lhs *1* :rhs rhs (base-poly ts-ttree '<= t nil)))) (t (poly-set 'and nil (add-linear-terms :lhs lhs :rhs rhs (let ((rationalp-flg (and (ts-real/rationalp ts-lhs) (ts-real/rationalp ts-rhs)))) (base-poly0 (if rationalp-flg ts-ttree ttree) (collect-parents ttree) '< rationalp-flg nil)))))) (poly-set 'and nil (add-linear-terms :lhs rhs :rhs lhs (let ((rationalp-flg (and (ts-real/rationalp ts-lhs) (ts-real/rationalp ts-rhs)))) (base-poly0 (if rationalp-flg ts-ttree ttree) (collect-parents ttree) '<= rationalp-flg nil))))))))) ((equalityp atm) (let ((lhs (fargn atm 1)) (rhs (fargn atm 2))) (mv-let (ts-lhs ts-ttree) (type-set lhs force-flg nil type-alist ens wrld ttree nil nil) (mv-let (ts-rhs ts-ttree) (type-set rhs force-flg nil type-alist ens wrld ts-ttree nil nil) (cond ((and (ts-disjointp ts-lhs *ts-acl2-number*) (ts-disjointp ts-rhs *ts-acl2-number*)) nil) (positivep (let ((rationalp-flg (and (ts-real/rationalp ts-lhs) (ts-real/rationalp ts-rhs)))) (poly-set 'and (add-linear-terms :lhs lhs :rhs rhs (base-poly0 (if rationalp-flg ts-ttree ttree) (collect-parents ttree) '<= rationalp-flg t)) (add-linear-terms :lhs rhs :rhs lhs (base-poly0 (if rationalp-flg ts-ttree ttree) (collect-parents ttree) '<= rationalp-flg t))))) ((and (ts-subsetp ts-lhs *ts-integer*) (ts-subsetp ts-rhs *ts-integer*)) (poly-set 'or (add-linear-terms :lhs lhs :lhs *1* :rhs rhs (base-poly ts-ttree '<= t nil)) (add-linear-terms :lhs rhs :lhs *1* :rhs lhs (base-poly ts-ttree '<= t nil)))) ((if (ts-subsetp ts-lhs *ts-acl2-number*) (or (ts-subsetp ts-rhs *ts-acl2-number*) (ts-disjointp ts-lhs *ts-zero*)) (and (ts-subsetp ts-rhs *ts-acl2-number*) (ts-disjointp ts-rhs *ts-zero*))) (let ((rationalp-flg (and (ts-real/rationalp ts-lhs) (ts-real/rationalp ts-rhs)))) (poly-set 'or (add-linear-terms :lhs lhs :rhs rhs (base-poly ts-ttree '< rationalp-flg nil)) (add-linear-terms :lhs rhs :rhs lhs (base-poly ts-ttree '< rationalp-flg nil))))) ((and (ts-acl2-numberp ts-lhs) force-flg (ts-intersectp ts-rhs *ts-acl2-number*)) (mv-let (flg new-ttree) (add-linear-assumption term `(acl2-numberp ,RHS) type-alist ens (immediate-forcep nil ens) force-flg wrld ts-ttree) (cond ((and (not (eq flg :failed)) (not (eq flg :known-false))) (poly-set 'or (add-linear-terms :lhs lhs :rhs rhs (base-poly new-ttree '< nil nil)) (add-linear-terms :lhs rhs :rhs lhs (base-poly new-ttree '< nil nil)))) (t nil)))) ((and (ts-acl2-numberp ts-rhs) force-flg (ts-intersectp ts-lhs *ts-acl2-number*)) (mv-let (flg new-ttree) (add-linear-assumption term `(acl2-numberp ,LHS) type-alist ens (immediate-forcep nil ens) force-flg wrld ts-ttree) (cond ((and (not (eq flg :failed)) (not (eq flg :known-false))) (poly-set 'or (add-linear-terms :lhs lhs :rhs rhs (base-poly new-ttree '< nil nil)) (add-linear-terms :lhs rhs :rhs lhs (base-poly new-ttree '< nil nil)))) (t nil)))) (t nil)))))) ((quotep atm) (if positivep (if (equal atm *nil*) (poly-set 'and nil (impossible-poly ttree)) nil) (if (not (equal atm *nil*)) (poly-set 'and nil (impossible-poly ttree)) nil))) (t nil))))))
linearizefunction
(defun linearize (term positivep type-alist ens force-flg wrld ttree state) (let ((temp (linearize1 term positivep type-alist ens force-flg wrld ttree state))) (cond ((null temp) nil) ((null (cdr temp)) (list (normalize-poly-lst (car temp)))) (t (list (normalize-poly-lst (car temp)) (normalize-poly-lst (cadr temp)))))))
linearize-lst1function
(defun linearize-lst1 (term-lst ttrees positivep type-alist ens force-flg wrld state poly-lst split-lst) (cond ((null term-lst) (mv (reverse poly-lst) (reverse split-lst))) (t (let ((lst (linearize (car term-lst) positivep type-alist ens force-flg wrld (car ttrees) state))) (cond ((null lst) (linearize-lst1 (cdr term-lst) (cdr ttrees) positivep type-alist ens force-flg wrld state poly-lst split-lst)) ((null (cdr lst)) (linearize-lst1 (cdr term-lst) (cdr ttrees) positivep type-alist ens force-flg wrld state (revappend (car lst) poly-lst) split-lst)) (t (linearize-lst1 (cdr term-lst) (cdr ttrees) positivep type-alist ens force-flg wrld state poly-lst (cons lst split-lst))))))))
linearize-lstfunction
(defun linearize-lst (term-lst ttrees positivep type-alist ens force-flg wrld state) (linearize-lst1 term-lst ttrees positivep type-alist ens force-flg wrld state nil nil))