		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::pot-lst

(macro) display the linear arithmetic database based on the current context

This is a relatively advanced command. For discussion of a related but more elementary command, including remarks about the utility of such a command, see ACL2-pc::type-alist. See linear-arithmetic for a description of the ACL2 linear arithmetic decision procedure

Examples:
(pot-lst nil t)   ; display linear pot-lst based on governors only (default)
pot-lst           ; same as (pot-lst nil t) -- governors only (default)
(pot-lst nil)     ; same as (pot-lst nil t) -- governors only (default)
(pot-lst nil t nil nil) ; same as above
(pot-lst nil t nil t)   ; same as above, except: raw format
(pot-lst t t)     ; display pot-lst based on conclusion and governors
(pot-lst t)       ; same as (pot-lst t nil) -- conclusion only
(pot-lst nil nil) ; based on neither conclusion nor governors

General Form:
(pot-lst &optional concl-flg govs-flg rawp)

where if govs-flg is omitted then it defaults to (not concl-flg), and each of the other optional arguments defaults to nil.

This command displays the linear database, also known as the linear pot-lst, that is computed from a suitable set of assumptions. That set of assumptions always includes all top-level hypotheses. By default, and when govs-flg is supplied a non-nil value, the set of assumptions includes all governors (which are based on surrounding if-expressions that must be true or false). The negation of the current goal's top-level conclusion is also included in the assumptions when concl-flg is supplied a non-nil value.

The computed pot-lst is based on the result of forward chaining from the set of assumptions as described above. By default, that pot-lst is displayed in a self-explanatory way. Here is an (admittedly contrived) example.

ACL2 !>(verify (implies (and (>= (- (nth 3 x) a) 7)
                             (< (nth 3 x) b)
                             (< c b))
                        (< (nth 3 x) d)))
->: promote
->: th
*** Top-level hypotheses:
1. (<= 7 (+ (NTH 3 X) (- A)))
2. (< (NTH 3 X) B)
3. (< C B)

The current subterm is:
(< (NTH 3 X) D)
->: pot-lst
Current pot-lst:
-----
For maximal term B
the list of polynomials is:
((A + 7 < B))
-----
For maximal term C
the list of polynomials is:
((C < B))
-----
For maximal term (NTH '3 X)
the list of polynomials is:
(((NTH '3 X) < B) (A + 7 <= (NTH '3 X)))

NIL
->: (pot-lst t t)
Current pot-lst:
-----
For maximal term B
the list of polynomials is:
((A + 7 < B))
-----
For maximal term C
the list of polynomials is:
((C < B))
-----
For maximal term D
the list of polynomials is:
((D < B))
-----
For maximal term (NTH '3 X)
the list of polynomials is:
(((NTH '3 X) < B) (A + 7 <= (NTH '3 X)) (D <= (NTH '3 X)))

NIL
->:

You can get the internal form of the pot-lst by supplying all optional arguments including a non-nil value for rawp.