building-blocks

(defun arg1
  (x)
  (declare (xargs :guard t))
  (if (and (consp x) (consp (cdr x)))
    (cadr x)
    nil))

(defun arg2
  (x)
  (declare (xargs :guard t))
  (if (and (consp x) (consp (cdr x)) (consp (cddr x)))
    (caddr x)
    nil))

(defun constant-p
  (x)
  (declare (xargs :guard t))
  (and (quotep x) (consp (cdr x))))

(defun numeric-constant-p
  (x)
  (declare (xargs :guard t))
  (and (quotep x) (consp (cdr x)) (acl2-numberp (unquote x))))

(defun integer-constant-p
  (x)
  (declare (xargs :guard t))
  (and (quotep x) (consp (cdr x)) (integerp (unquote x))))

(defun rational-constant-p
  (x)
  (declare (xargs :guard t))
  (and (quotep x) (consp (cdr x)) (rationalp (unquote x))))

(defun power-of-2-measure
  (x)
  (declare (xargs :guard (and (real/rationalp x) (not (equal x 0)))))
  (cond ((or (not (real/rationalp x)) (<= x 0)) 0)
    ((< x 1) (cons (cons 1 1) (floor (/ x) 1)))
    (t (floor x 1))))

(defun power-of-2-helper
  (x)
  (declare (xargs :guard t :measure (power-of-2-measure x)))
  (cond ((or (not (real/rationalp x)) (<= x 0)) 0)
    ((< x 1) (+ -1 (power-of-2-helper (* 2 x))))
    ((<= 2 x) (+ 1 (power-of-2-helper (* 1/2 x))))
    ((equal x 1) 0)
    (t 0)))

(defun power-of-2-generalized
  (x)
  (declare (xargs :guard t))
  (cond ((not (rational-constant-p x)) nil)
    ((< 0 (unquote x)) (let ((c (power-of-2-helper (unquote x))))
        (if (equal (expt 2 c) (unquote x))
          c
          nil)))
    ((< (unquote x) 0) (let ((c (power-of-2-helper (- (unquote x)))))
        (if (equal (expt 2 c) (- (unquote x)))
          c
          nil)))
    (t nil)))

(defun power-of-2
  (x)
  (declare (xargs :guard t))
  (cond ((not (integer-constant-p x)) nil)
    ((< 1 (unquote x)) (let ((c (power-of-2-helper (unquote x))))
        (if (equal (expt 2 c) (unquote x))
          c
          nil)))
    ((< (unquote x) -1) (let ((c (power-of-2-helper (- (unquote x)))))
        (if (equal (expt 2 c) (- (unquote x)))
          c
          nil)))
    (t nil)))

(defun power-of-2-minus-1
  (x)
  (declare (xargs :guard t))
  (cond ((not (integer-constant-p x)) nil)
    ((< 0 (unquote x)) (let ((c (power-of-2-helper (+ 1 (unquote x)))))
        (if (equal (expt 2 c) (+ 1 (unquote x)))
          c
          nil)))
    (t nil)))

(defun rewriting-goal-literal
  (x mfc state)
  (declare (xargs :guard t))
  (declare (ignore x state))
  (null (mfc-ancestors mfc)))

(defun term-equal
  (term1 term2)
  (declare (xargs :guard t))
  (if (equal (fn-symb term1) 'equal)
    (and (equal (fn-symb term2) 'equal)
      (or (and (equal (arg1 term1) (arg1 term2))
          (equal (arg2 term1) (arg2 term2)))
        (and (equal (arg1 term1) (arg2 term2))
          (equal (arg2 term1) (arg1 term2)))))
    (equal term1 term2)))

(defun rewriting-hypothesis-1
  (term ancestors)
  (declare (xargs :guard t))
  (if (and (consp ancestors) (consp (car ancestors)))
    (let ((hyp (caar ancestors)))
      (cond ((term-equal term hyp) 'positive)
        ((and (eq (fn-symb hyp) 'not) (term-equal term (arg1 hyp))) 'negative)
        (t nil)))
    nil))

(defun rewriting-hypothesis
  (term mfc state)
  (declare (ignore state))
  (rewriting-hypothesis-1 term (mfc-ancestors mfc)))

(defun present-in-hyps
  (term goal)
  (declare (xargs :guard t))
  (cond ((atom goal) nil)
    ((atom (cdr goal)) nil)
    ((term-equal term (car goal)) 'positive)
    ((and (eq (fn-symb (car goal)) 'not)
       (term-equal term (arg1 (car goal)))) 'negative)
    (t (present-in-hyps term (cdr goal)))))

(defun present-in-goal-1
  (term goal)
  (declare (xargs :guard t))
  (cond ((atom goal) nil)
    ((term-equal term (car goal)) 'positive)
    ((and (eq (fn-symb (car goal)) 'not)
       (term-equal term (arg1 (car goal)))) 'negative)
    (t (present-in-goal-1 term (cdr goal)))))

(defun present-in-goal
  (term mfc state)
  (declare (ignore state))
  (present-in-goal-1 term (mfc-clause mfc)))

(defun negate-match
  (match)
  (declare (xargs :guard t))
  (cond ((variablep match) `(unary-- ,MATCH))
    ((numeric-constant-p match) (kwote (- (unquote match))))
    ((eq (ffn-symb match) 'unary--) (arg1 match))
    ((and (eq (ffn-symb match) 'binary-*)
       (numeric-constant-p (arg1 match))) `(binary-* ,(KWOTE (- (UNQUOTE (ARG1 MATCH)))) ,(ARG2 MATCH)))
    ((eq (ffn-symb match) 'binary-+) `(binary-+ ,(NEGATE-MATCH (ARG1 MATCH))
        ,(NEGATE-MATCH (ARG2 MATCH))))
    (t `(unary-- ,MATCH))))

(defun invert-match
  (match)
  (declare (xargs :guard t))
  (cond ((variablep match) `(unary-/ ,MATCH))
    ((numeric-constant-p match) (if (eql (unquote match) 0)
        (kwote 0)
        (kwote (/ (unquote match)))))
    ((eq (ffn-symb match) 'unary-/) (arg1 match))
    ((eq (ffn-symb match) 'unary--) `(unary-- ,(INVERT-MATCH (ARG1 MATCH))))
    ((eq (ffn-symb match) 'binary-*) `(binary-* ,(INVERT-MATCH (ARG1 MATCH))
        ,(INVERT-MATCH (ARG2 MATCH))))
    ((eq (ffn-symb match) 'expt) `(expt ,(ARG1 MATCH) ,(NEGATE-MATCH (ARG2 MATCH))))
    (t `(unary-/ ,MATCH))))

(defun proveably-integer
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(integerp ,X) alist t t mfc state) *t*))

(defun proveably-rational
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(rationalp ,X) alist t t mfc state) *t*))

(defun proveably-real/rational
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(rationalp ,X) alist t t mfc state) *t*))

(defun proveably-acl2-numberp
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(acl2-numberp ,X) alist t t mfc state) *t*))

(defun proveably-non-zero1
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(not (equal (fix ,X) '0)) alist t t mfc state)
    *t*))

(defun proveably-non-zero
  (x alist mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) (proveably-non-zero1 x alist mfc state))
    ((fquotep x) (and (numeric-constant-p x) (not (equal x ''0))))
    ((eq (ffn-symb x) 'if) nil)
    (t (proveably-non-zero1 x alist mfc state))))

(defun proveably-non-zero-rational1
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(not (equal (rfix ,X) '0)) alist t t mfc state)
    *t*))

(defun proveably-non-zero-rational
  (x alist mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) (proveably-non-zero-rational1 x alist mfc state))
    ((fquotep x) (and (rational-constant-p x) (not (equal x ''0))))
    ((eq (ffn-symb x) 'if) nil)
    (t (proveably-non-zero-rational1 x alist mfc state))))

(defun proveably-non-zero-real/rational1
  (x alist mfc state)
  (declare (xargs :guard t))
  (equal (mfc-rw+ `(not (equal (rfix ,X) '0)) alist t t mfc state)
    *t*))

(defun proveably-non-zero-real/rational
  (x alist mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) (proveably-non-zero-real/rational1 x alist mfc state))
    ((fquotep x) (and (rational-constant-p x) (not (equal x ''0))))
    ((eq (ffn-symb x) 'if) nil)
    (t (proveably-non-zero-real/rational1 x alist mfc state))))

(defun stable-under-rewriting
  (x bin-op mfc state)
  (declare (xargs :guard (symbolp bin-op))
    (ignore bin-op))
  (let ((rewritten-term (mfc-rw+ `(fix x) `((x . ,X)) '? nil mfc state)))
    (equal rewritten-term x)))

(defun stable-under-rewriting-sums
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) (stable-under-rewriting x 'binary-+ mfc state))
    ((fquotep x) t)
    ((member-eq (ffn-symb x) '(if binary-+)) nil)
    (t (stable-under-rewriting x 'binary-+ mfc state))))

(defun stable-under-rewriting-products
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) (stable-under-rewriting x 'binary-* mfc state))
    ((fquotep x) t)
    ((member-eq (ffn-symb x) '(if binary-*)) nil)
    (t (stable-under-rewriting x 'binary-* mfc state))))

(defun in-term-order-+
  (x mfc state)
  (declare (xargs :mode :program))
  (declare (ignorable mfc))
  (if (equal (fn-symb x) 'binary-+)
    (if (equal (fn-symb (arg2 x)) 'binary-+)
      (and (term-order+ (arg1 x)
          (arg1 (arg2 x))
          (invisible-fns '(binary-+)
            (invisible-fns-table (w state))
            t))
        (in-term-order-+ (arg2 x) mfc state))
      (term-order+ (arg1 x)
        (arg2 x)
        (invisible-fns '(binary-+)
          (invisible-fns-table (w state))
          t)))
    t))

(defun in-term-order-*
  (x mfc state)
  (declare (xargs :mode :program))
  (declare (ignorable mfc))
  (if (equal (fn-symb x) 'binary-*)
    (if (equal (fn-symb (arg2 x)) 'binary-*)
      (and (term-order+ (arg1 x)
          (arg1 (arg2 x))
          (invisible-fns '(binary-*)
            (invisible-fns-table (w state))
            t))
        (in-term-order-* (arg2 x) mfc state))
      (term-order+ (arg1 x)
        (arg2 x)
        (invisible-fns '(binary-*)
          (invisible-fns-table (w state))
          t)))
    t))

(defun in-term-order
  (x mfc state)
  (declare (xargs :mode :program))
  (cond ((equal (fn-symb x) 'binary-+) (in-term-order-+ x mfc state))
    ((equal (fn-symb x) 'binary-*) (in-term-order-* x mfc state))
    (t t)))

(defun negative-addends-p-1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) nil)
    ((fquotep x) (and (rational-constant-p x) (< (unquote x) 0)))
    ((eq (ffn-symb x) 'unary--) (and (not (eq (fn-symb (arg1 x)) 'unary--))
        (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state)))
    ((eq (ffn-symb x) 'binary-*) (and (rational-constant-p (arg1 x))
        (< (unquote (arg1 x)) 0)))
    ((eq (ffn-symb x) 'binary-+) (and (negative-addends-p-1 (arg1 x) mfc state)
        (negative-addends-p-1 (arg2 x) mfc state)))
    (t nil)))

(defun negative-addends-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (negative-addends-p-1 x mfc state)))

(defun negative-addends-balance
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) -1)
    ((fquotep x) (if (and (rational-constant-p x) (< (unquote x) 0))
        1
        -1))
    ((eq (ffn-symb x) 'unary--) (if (and (not (eq (fn-symb (arg1 x)) 'unary--))
          (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state))
        1
        -1))
    ((eq (ffn-symb x) 'binary-*) (if (and (rational-constant-p (arg1 x))
          (< (unquote (arg1 x)) 0))
        1
        -1))
    ((eq (ffn-symb x) 'binary-+) (+ (negative-addends-balance (arg1 x) mfc state)
        (negative-addends-balance (arg2 x) mfc state)))
    (t -1)))

(defun mostly-negative-addends-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (< 0 (negative-addends-balance x mfc state))))

(defun weak-negative-addends-p-1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) nil)
    ((fquotep x) (rational-constant-p x))
    ((eq (ffn-symb x) 'unary--) (and (not (eq (fn-symb (arg1 x)) 'unary--))
        (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state)))
    ((eq (ffn-symb x) 'binary-*) (and (rational-constant-p (arg1 x))
        (< (unquote (arg1 x)) 0)))
    ((eq (fn-symb x) 'binary-+) (and (negative-addends-p-1 (arg1 x) mfc state)
        (negative-addends-p-1 (arg2 x) mfc state)))
    (t nil)))

(defun weak-negative-addends-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (weak-negative-addends-p-1 x mfc state)))

(defun weak-negative-addends-balance
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) -1)
    ((fquotep x) (if (rational-constant-p x)
        0
        -1))
    ((eq (ffn-symb x) 'unary--) (if (and (not (eq (fn-symb (arg1 x)) 'unary--))
          (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state))
        1
        -1))
    ((eq (ffn-symb x) 'binary-*) (if (and (rational-constant-p (arg1 x))
          (< (unquote (arg1 x)) 0))
        1
        -1))
    ((eq (ffn-symb x) 'binary-+) (+ (weak-negative-addends-balance (arg1 x) mfc state)
        (weak-negative-addends-balance (arg2 x) mfc state)))
    (t -1)))

(defun weak-mostly-negative-addends-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (< 0 (weak-negative-addends-balance x mfc state))))

(defun divisive-factors-p-1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) nil)
    ((quotep x) (and (not (integer-constant-p x))
        (rational-constant-p x)
        (equal (numerator (unquote x)) 1)))
    ((eq (ffn-symb x) 'unary-/) (and (not (eq (fn-symb (arg1 x)) 'unary-/))
        (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state)))
    ((eq (ffn-symb x) 'expt) (if (quotep (arg2 x))
        (and (integer-constant-p (arg2 x)) (< (unquote (arg2 x)) 0))
        (negative-addends-p (arg2 x) mfc state)))
    ((eq (fn-symb x) 'binary-*) (and (divisive-factors-p-1 (arg1 x) mfc state)
        (divisive-factors-p-1 (arg2 x) mfc state)))
    (t nil)))

(defun divisive-factors-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (divisive-factors-p-1 x mfc state)))

(defun divisive-factors-balance
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) -1)
    ((quotep x) (if (and (not (integer-constant-p x))
          (rational-constant-p x)
          (equal (numerator (unquote x)) 1))
        1
        -1))
    ((eq (ffn-symb x) 'unary-/) (if (and (not (eq (fn-symb (arg1 x)) 'unary-/))
          (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state))
        1
        -1))
    ((eq (ffn-symb x) 'expt) (if (if (quotep (arg2 x))
          (and (integer-constant-p (arg2 x)) (< (unquote (arg2 x)) 0))
          (mostly-negative-addends-p (arg2 x) mfc state))
        1
        -1))
    ((eq (fn-symb x) 'binary-*) (+ (divisive-factors-balance (arg1 x) mfc state)
        (divisive-factors-balance (arg2 x) mfc state)))
    (t -1)))

(defun mostly-divisive-factors-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (< 0 (divisive-factors-balance x mfc state))))

(defun weak-divisive-factors-p-1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) nil)
    ((quotep x) (rational-constant-p x))
    ((eq (ffn-symb x) 'unary-/) (and (not (eq (fn-symb (arg1 x)) 'unary-/))
        (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state)))
    ((eq (ffn-symb x) 'expt) (if (quotep (arg2 x))
        (and (integer-constant-p (arg2 x)) (< (unquote (arg2 x)) 0))
        (weak-negative-addends-p (arg2 x) mfc state)))
    ((eq (fn-symb x) 'binary-*) (and (weak-divisive-factors-p-1 (arg1 x) mfc state)
        (weak-divisive-factors-p-1 (arg2 x) mfc state)))
    (t nil)))

(defun weak-divisive-factors-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (weak-divisive-factors-p-1 x mfc state)))

(defun weak-divisive-factors-balance
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((variablep x) -1)
    ((quotep x) (if (rational-constant-p x)
        0
        -1))
    ((eq (ffn-symb x) 'unary-/) (if (and (not (eq (fn-symb (arg1 x)) 'unary-/))
          (proveably-acl2-numberp 'x `((x . ,(ARG1 X))) mfc state))
        1
        -1))
    ((eq (ffn-symb x) 'expt) (if (if (quotep (arg2 x))
          (and (integer-constant-p (arg2 x)) (< (unquote (arg2 x)) 0))
          (mostly-negative-addends-p (arg2 x) mfc state))
        1
        -1))
    ((eq (fn-symb x) 'binary-*) (+ (weak-divisive-factors-balance (arg1 x) mfc state)
        (weak-divisive-factors-balance (arg2 x) mfc state)))
    (t -1)))

(defun weak-mostly-divisive-factors-p
  (x mfc state)
  (declare (xargs :guard t))
  (if (quotep x)
    nil
    (< 0 (weak-divisive-factors-balance x mfc state))))

(defun ok-to-lift-p
  (x)
  (declare (xargs :guard t))
  (cond ((variablep x) t)
    ((fquotep x) t)
    ((and (consp (cdr x)) (equal (car x) 'not)) (ok-to-lift-p (cadr x)))
    ((and (consp (cdr x))
       (equal (car x) 'if)
       (consp (cddr x))
       (consp (cdddr x))) (and (ok-to-lift-p (cadr x))
        (ok-to-lift-p (caddr x))
        (ok-to-lift-p (cadddr x))))
    ((consp x) (member-eq (car x)
        '(acl2-numberp rationalp
          integerp
          natp
          posp
          complex-rationalp
          equal
          eql
          <)))))

(defun addends
  (sum)
  (declare (xargs :guard t))
  (if (eq (fn-symb sum) 'binary-+)
    (cons (arg1 sum) (addends (arg2 sum)))
    (list sum)))

(defun factors
  (product)
  (declare (xargs :guard t))
  (if (eq (fn-symb product) 'binary-*)
    (cons (arg1 product) (factors (arg2 product)))
    (list product)))

(defun make-product
  (factors)
  (declare (xargs :guard t))
  (cond ((atom factors) ''1)
    ((atom (cdr factors)) (car factors))
    ((atom (cddr factors)) (list 'binary-* (car factors) (cadr factors)))
    (t (list 'binary-* (car factors) (make-product (cdr factors))))))

(defun set-equal
  (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (and (subsetp-equal a b) (subsetp-equal b a)))

(defun common-factors
  (factors sum)
  (declare (xargs :measure (acl2-count sum)
      :guard (true-listp factors)))
  (cond ((atom factors) nil)
    ((eq (fn-symb sum) 'binary-+) (common-factors (intersection-equal factors (factors (arg1 sum)))
        (arg2 sum)))
    (t (intersection-equal factors (factors sum)))))

(defun remainder
  (common-factors sum)
  (declare (xargs :guard (true-listp common-factors)))
  (if (eq (fn-symb sum) 'binary-+)
    (let ((first (make-product (set-difference-equal (factors (arg1 sum)) common-factors))))
      (list 'binary-+ first (remainder common-factors (arg2 sum))))
    (make-product (set-difference-equal (factors sum) common-factors))))

(defun mfc-obj
  (x mfc state)
  (declare (xargs :guard t))
  (declare (ignore x state))
  (if (and (consp mfc) (consp (cdr mfc)))
    (cadr mfc)
    '?))

(defun ts-fix
  (x)
  (declare (xargs :guard t))
  (let ((int-x (ifix x)))
    (if (and (<= *min-type-set* int-x) (<= int-x *max-type-set*))
      int-x
      0)))

(defun simplify-ok-p-1
  (orig-term new-term alist mfc state)
  (declare (xargs :guard t
      :guard-hints (("Goal" :in-theory (disable arg1 arg2 mfc-obj ts-fix)))))
  (let ((orig-lhs (arg1 orig-term)) (orig-rhs (arg2 orig-term))
      (new-lhs (arg1 new-term))
      (new-rhs (arg2 new-term)))
    (if (and (ts-subsetp (ts-fix (mfc-ts orig-lhs mfc state))
          *ts-integer*)
        (ts-subsetp (ts-fix (mfc-ts orig-rhs mfc state))
          *ts-integer*))
      (and (let ((rewritten-new-lhs (mfc-rw+ new-lhs alist '? nil mfc state)))
          (ts-subsetp (ts-fix (mfc-ts rewritten-new-lhs mfc state))
            *ts-integer*))
        (let ((rewritten-new-rhs (mfc-rw+ new-rhs alist '? nil mfc state)))
          (ts-subsetp (ts-fix (mfc-ts rewritten-new-rhs mfc state))
            *ts-integer*)))
      t)))

(defun simplify-ok-p
  (orig-term new-term alist mfc state)
  (declare (xargs :guard t))
  (let ((relation (fn-symb orig-term)) (obj (mfc-obj orig-term mfc state))
      (ancestors (mfc-ancestors mfc))
      (goal (mfc-clause mfc)))
    (cond ((eq obj t) (cond ((eq relation '<) t)
          ((eq relation 'equal) (simplify-ok-p-1 orig-term new-term alist mfc state))
          (t nil)))
      ((eq obj nil) (cond ((eq relation '<) (simplify-ok-p-1 orig-term new-term alist mfc state))
          ((eq relation 'equal) t)
          (t nil)))
      ((null ancestors) (let ((parity (present-in-goal-1 orig-term goal)))
          (cond ((eq parity 'positive) (cond ((eq relation '<) t)
                ((eq relation 'equal) (simplify-ok-p-1 orig-term new-term alist mfc state))
                (t nil)))
            ((eq parity 'negative) (cond ((eq relation '<) (simplify-ok-p-1 orig-term new-term alist mfc state))
                ((eq relation 'equal) t)
                (t nil)))
            (t nil))))
      (t t))))