From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:27:33 +0000 (-0500) Subject: Add LFSC signature for n-ary programs (#7360) X-Git-Tag: cvc5-1.0.0~1041 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59aa30fe471f80b5e507561a4bd34fd3c9e52a09;p=cvc5.git Add LFSC signature for n-ary programs (#7360) This is the last utility signature. Theory signatures will be added afterwards. --- diff --git a/proofs/lfsc/signatures/nary_programs.plf b/proofs/lfsc/signatures/nary_programs.plf new file mode 100644 index 000000000..f04e6ba40 --- /dev/null +++ b/proofs/lfsc/signatures/nary_programs.plf @@ -0,0 +1,179 @@ +; depends: core_defs.plf util_defs.plf + +; This file defines a library of methods for reasoning about n-ary functions. +; Notice that since LFSC does not have support for n-ary function symbols, we +; represent n-ary function applications in a null-terminated, Curried form. +; In particular, the term `(or A B C)` is represented in LFSC as: +; `(apply (apply f_or A) (apply (apply f_or B) (apply (apply f_or C) false)))` +; i.e. using the macro definitions in core_defs: +; `(or A (or B (or C false)))` +; where notice that `false` is the null-terminator for `or`. Many operators +; are treated in this way, including Boolean connectives `and` and `or`, +; arithmetic plus and multiplication, string concatenation, and so on. +; We call the term like the one above "an f_or-application in n-ary form". +; When applicable, we simply write "f-application" to refer to a term that is +; in n-ary form. We call A, B, C the "elements" of the f-application above. +; We say that an f-application is a "singleton" if it consists of a single +; element, e.g. `(or A false)`. +; +; This file defines a set of side conditions that are useful in defining +; theory-specific proof rules involving n-ary functions and are agnostic to the +; function in question. When applicable, the side conditions take the n-ary +; function `f` as an argument, or its null terminator `null`. + +; Head and tail for n-ary operators with null terminators. These methods +; fail if t is not an f-application. +(program nary_head ((f term) (t term)) term + (match t ((apply t1 t2) (getarg f t1)))) +(program nary_tail ((f term) (t term)) term + (match t ((apply t1 t2) (let t12 (getarg f t1) t2)))) + +; Remove the first occurrence of term l from t. This side condition fails if t +; is not an f-application, or if t does not contain l. +(program nary_rm_first ((f term) (t term) (l term)) term + (match t + ((apply t1 t2) ; otherwise at end, l not found + (let t12 (getarg f t1) + (ifequal t12 l t2 (apply t1 (nary_rm_first f t2 l)))))) + ; otherwise not an f-app in n-ary form +) + +; Same as `nary_rm_first`, but also checks whether t is l itself and returns null if so, +; where null is a null terminator. +(program nary_rm_first_or_self ((f term) (t term) (l term) (null term)) term + (ifequal t l null (nary_rm_first f t l)) +) + +; Does t contain l? This side condition may fail if t is not an f-application. +(program nary_ctn ((f term) (t term) (l term)) flag + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (ifequal t12 l tt (nary_ctn f t2 l)))) + ; otherwise not an f-app in n-ary form + (default ff)) +) + +; Same as `nary_ctn`, but also checks if t is l, returning true if so. +(program nary_ctn_or_self ((f term) (t term) (l term)) flag + (ifequal t l tt (nary_ctn f t l)) +) + +; Returns true if t is a subset of s, when these terms were interpreted as sets. +; This side condition may fail if t or s is not an f-application. +(program nary_is_subset ((f term) (t term) (s term)) flag + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (ifequal (nary_ctn_or_self f s t12) tt (nary_is_subset f t2 s) ff))) + ; otherwise not in n-ary form + (default tt)) +) + +; Concatenates terms t1 and t2 that are f-applications in n-ary form. +(program nary_concat ((f term) (t1 term) (t2 term) (null term)) term + (match t1 + ((apply t11 t12) + (let t112 (getarg f t11) + (apply t11 (nary_concat f t12 t2 null)))) + (default t2)) ; any non-application term is interpreted as null +) + +; Insert element elem at the beginning of the f-application t. +(program nary_insert ((f term) (elem term) (t term) (null term)) term + (ifequal elem null t (apply (apply f elem) t))) + +; Dual to `nary_insert`. Returns a term pair ( elem, t' ) where elem is the +; head of t, and t' is the tail of t. +(program nary_decompose ((f term) (t term) (null term)) termPair + (match t + ((apply t1 t2) + (match t1 + ((apply t11 t12) (ifequal t11 f (pair t12 t2) (pair null t))) + (default (pair null t)))) + (default (pair null t))) +) + +; N-ary elimination. This replaces a singleton f-application with its element. +; For example, this replaces e.g. (or t false) with t. +(program nary_elim ((f term) (t term) (null term)) term + (match t + ((apply t1 t2) + ; if null terminated, then we return the head, otherwise not in n-ary form + (ifequal t2 null (getarg f t1) t)) + (default (ifequal t null t (fail term)))) +) + +; N-ary introduction, which is the inverse of nary_elim. This turns a term t into +; a (singleton) f-application if it is not already in n-ary form. For example, +; this replaces t with (or t false) if t is not already in n-ary form. +(program nary_intro ((f term) (t term) (null term)) term + (match t + ((apply t1 t2) + (match t1 + ((apply t11 t12) (ifequal t11 f t (apply (apply f t) null))) + (default (apply (apply f t) null)))) + (default (ifequal t null t (apply (apply f t) null)))) +) + +; Extract the n^th element of f-application t. This side condition fails if +; t is not an f-application, or contains fewer than n elements. +(program nary_extract ((f term) (t term) (n mpz)) term + (match t + ((apply t1 t2) + (mp_ifzero n + (getarg f t1) + (nary_extract f t2 (mp_add n (mp_neg 1)))))) +) + +; Helper for dropping duplicates from an f-application t. Elements occur in +; the returned f-application in the order they first appear in t. +; This side condition takes an accumulator tacc which tracks which terms it is +; adding to the return value. We require an explicit accumulator to ensure +; propering ordering for cases like (or A B B A), where (or A B) should be +; returned instead of (or B A). +; This method fails if t is not an f-application. +(program nary_drop_dups_rec ((f term) (t term) (tacc term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (let c (nary_ctn f tacc t12) + (let t2d (nary_drop_dups_rec f t2 (ifequal c tt tacc (apply t1 tacc))) + (ifequal c tt t2d (apply t1 t2d)))))) + (default t)) +) + +; Drop all duplicates in an f-application t using the helper method +; `nary_drop_dups_rec`. +(program nary_drop_dups ((f term) (t term) (null term)) term + (nary_elim f (nary_drop_dups_rec f t null) null) +) + +; Truncate, which returns the f-application in which the subterm c has been +; replaced by the null terminator, where c is an f-application that is a +; suffix of t. For example, (or t1 ... tn c) ---> (or t1 ... tn false). +; This side condition fails if c is not a suffix of f-application t. +(program nary_truncate ((f term) (t term) (c term) (null term)) term + (ifequal t c null + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (apply t1 (nary_truncate f t2 c null)))))) +) + +; Helper for reverse, which takes an accumulator of terms we have added in +; reverse order to the value we will return. This side condition fails if +; t is not an f-application. +(program nary_reverse_rec ((f term) (t term) (acc term) (null term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f t1) + (nary_reverse_rec f t2 (apply t1 acc) null))) + (default (ifequal t null acc (fail term)))) +) + +; Reverse the elements in f-application t using the helper method +; `nary_reverse_rec`. +(program nary_reverse ((f term) (t term) (null term)) term + (nary_reverse_rec f t null null) +)