building-blocks

(defun numeric-constant-p
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (and (nvariablep x) (fquotep x) (acl2-numberp (unquote x))))

(defun rational-constant-p
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (and (nvariablep x) (fquotep x) (rationalp (unquote x))))

(defun negative-addends-p
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((variablep x) nil)
    ((fquotep x) (and (rational-constant-p x) (< (unquote x) 0)))
    ((eq (ffn-symb x) 'unary--) (or (variablep (arg1 x))
        (not (eq (ffn-symb (arg1 x)) 'unary--))))
    ((eq (ffn-symb x) 'binary-*) (and (rational-constant-p (arg1 x))
        (< (unquote (arg1 x)) 0)))
    ((eq (fn-symb x) 'binary-+) (and (negative-addends-p (arg1 x))
        (negative-addends-p (arg2 x))))
    (t nil)))

(defun weak-negative-addends-p
  (x)
  (declare (xargs :guard (pseudo-termp x)))
  (cond ((variablep x) nil)
    ((fquotep x) (rational-constant-p x))
    ((eq (ffn-symb x) 'unary--) (or (variablep (arg1 x))
        (not (eq (ffn-symb (arg1 x)) 'unary--))))
    ((eq (ffn-symb x) 'binary-*) (and (rational-constant-p (arg1 x))
        (< (unquote (arg1 x)) 0)))
    ((eq (fn-symb x) 'binary-+) (and (weak-negative-addends-p (arg1 x))
        (weak-negative-addends-p (arg2 x))))
    (t nil)))

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

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

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

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

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

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

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