diff options
| -rw-r--r-- | proofs/lfsc/signatures/core_defs.plf | 146 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/theory_def.plf | 421 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/util_defs.plf | 104 |
3 files changed, 671 insertions, 0 deletions
diff --git a/proofs/lfsc/signatures/core_defs.plf b/proofs/lfsc/signatures/core_defs.plf new file mode 100644 index 000000000..73532b3d1 --- /dev/null +++ b/proofs/lfsc/signatures/core_defs.plf @@ -0,0 +1,146 @@ +; This file defines how SMT-LIB sorts and terms are represented in LFSC. Notice +; that we use an embedding where "sort" and "term" are LFSC types. This file +; contains the "core" definitions of SMT-LIB, e.g. those that are specified +; in the SMT-LIB standard, covering Boolean connectives, ITE, equality, and +; quantifiers. We additionally define core definitions required for representing +; higher-order applications, which are used throughout. + +; At a high level, the LFSC signature for SMT-LIB uses the following principles: +; +; (1) Apart from indexed function symbols, all terms are simply typed, that is, +; the type of all terms is "term", as defined below. +; +; (2) The higher-order apply function "apply", as defined below, is used to +; construct all function applications. Since LFSC does not natively support +; n-ary function symbols, apply always expects two arguments. The use of this +; apply symbol is in turn curried when representing function applications with +; more than 2 arguments. +; +; (3) We use the following style when defining function symbols X: +; (a) We declare a simply typed version of the symbol: +; `(declare f_X term)` +; In other words, f_X is a term, which is the function X itself. +; (b) We define a macro that is a fully applied application of X. For example, +; when X expects two arguments, then we define: +; `(define X (# t1 term (# t2 term (apply (apply f_X t1) t2))))` +; More generally, this application consists of a right-associative chain +; of higher-order apply and f_X. +; Given this definition, we may write applications of X using SMT-LIB +; like syntax `(X a b)`. +; +; (4) Like SMT-LIB, we do not distinguish formulas and terms. Instead, formulas +; can be seen as terms of Boolean sort. +; +; (5) We use a type `holds` which takes a term as an argument. This is expected +; to take a Boolean term, e.g. a formula. The meaning of `(holds t)` is that +; `t` can be inferred in the current context. +; +; Note that since our signature does not strictly enforce that terms type +; check, the meta-level argument for the soundness of the signature relies +; on the fact that the proof rules do not introduce terms that are not well +; sorted according to SMT-LIB. Moreover, we assume that the input formula from +; the user contains only well sorted terms. + +; Sorts +(declare sort type) + +; Terms +(declare term type) + +; holds: term t holds, where t should have Boolean type +(declare holds (! t term type)) + +; function type constructor +(declare arrow (! s1 sort (! s2 sort sort))) + +; higher-order apply +(declare apply (! t1 term (! t2 term term))) + +; Boolean value terms +(declare true term) +(declare false term) + +; Negation +(declare f_not term) +(define not (# t term (apply f_not t))) + +; Conjunction +(declare f_and term) +(define and (# t1 term (# t2 term (apply (apply f_and t1) t2)))) + +; Disjunction +(declare f_or term) +(define or (# t1 term (# t2 term (apply (apply f_or t1) t2)))) + +; Implication +(declare f_=> term) +(define => (# t1 term (# t2 term (apply (apply f_=> t1) t2)))) + +; Xor +(declare f_xor term) +(define xor (# t1 term (# t2 term (apply (apply f_xor t1) t2)))) + +; ITE +(declare f_ite term) +(define ite (# c term (# t1 term (# t2 term (apply (apply (apply f_ite c) t1) t2))))) + +; Equality: +(declare f_= term) +(define = (# t1 term (# t2 term (apply (apply f_= t1) t2)))) + +; Disequality: +(declare f_distinct term) +(define distinct (# t1 term (# t2 term (apply (apply f_distinct t1) t2)))) + +;; ---- free constants +; A "free constant" is an input variable to an SMT-LIB problem. We identify +; each free constant by an integer identifier (argument v:mpz) and a sort +; (argument s:sort). Given a user input, we assign unique integer identifiers +; to each variable. +(declare var (! v mpz (! s sort term))) + +;; ---- variables +; A "bound variable" is a variable that is explicitly bound by a quantifier +; (e.g. universal, existential, lambda, witness). In this signature, +; bound variables are represented explicitly as free terms. Like free constants, +; they are identified by an integer identifier (argument v:mpz) and a sort +; (argument s:sort). +(declare bvar (! v mpz (! s sort term))) + +;; ---- quantifiers +; A quantified formula is represented as an indexed symbol whose arguments +; indicate which bound variable is being bound. Notice that quantified formulas +; bind only one variable at a time. Like SMT-LIB, we support both universal +; and existential quantification. We also support lambda and witness terms. +; In detail, the term (f_forall v s) binds the bound variable (bvar v s) +; universally. To write the SMT-LIB term (forall ((x Int)) (P x)), we write: +; `(apply (forall v Int) (apply P (bvar v Int)))` +; where v is the integer identifier associated with x. +(declare f_forall (! v mpz (! s sort term))) +(define forall (# v mpz (# s sort (# t term (apply (f_forall v s) t))))) + +; existentials +(declare f_exists (! v mpz (! s sort term))) +(define exists (# v mpz (# s sort (# t term (apply (f_exists v s) t))))) + +; witness, similar to Hilbert's choice operator. However, it is not necessarily +; the case that (witness ((x Int)) (P x)) and (witness ((y Int)) (Q y)) are +; equal when (exists ((x Int)) (P x)) and (exists ((y Int)) (Q y)) are +; equivalent. +(declare f_witness (! v mpz (! s sort term))) +(define witness (# v mpz (# s sort (# t term (apply (f_witness v s) t))))) + +; lambda +(declare f_lambda (! v mpz (! s sort term))) +(define lambda (# v mpz (# s sort (# t term (apply (f_lambda v s) t))))) + +; ---- Skolem variables +; A "Skolem variable" is an internally introduced variable. Its semantics are +; the same as free constants. In contrast to free constants, we identify Skolem +; variables by a term, which they are indexed by. Given a Skolem variable +; (skolem t), we call t the "witness term" of this Skolem. The witness term +; of a Skolem is often a term that the Skolem was used to abstract during +; solving. It is *not* necessarily the case that the witness term for a Skolem +; is an application of witness. Some Skolem variables, e.g. those used for +; purification, are associated with a quantifier-free term. +(declare skolem (! w term term)) diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf new file mode 100644 index 000000000..9d762b03b --- /dev/null +++ b/proofs/lfsc/signatures/theory_def.plf @@ -0,0 +1,421 @@ +; depends: core_defs.plf + +; This file defines the sort and function symbols for all SMT-LIB standard +; theories, as well as extensions supported by cvc5. + +;; ---- Sorts + +; Booleans +(declare Bool sort) +; Integers +(declare Int sort) +; Reals +(declare Real sort) +; Arrays, parametrized by index and element sorts +(declare Array (! i sort (! e sort sort))) +; Strings +(declare String sort) +; Sequences, parametrized by an element sort +(declare Seq (! e sort sort)) +; Regular languages +(declare RegLan sort) +; Bit-vectors, parametrized by an integer bit-width +(declare BitVec (! w mpz sort)) +; Floating points, parametrized by exponent and significand bit-widths +(declare FloatingPoint (! e mpz (! s mpz sort))) +; Rounding modes for floating points +(declare RoundingMode sort) +; Sets, parametrized by an element sort +(declare Set (! e sort sort)) +; Bags (i.e. multi-sets), parametrized by an element sort +(declare Bag (! e sort sort)) + +;; ---- Arithmetic + +; We define the signature for theories of integer and real arithmetic with +; extensions here. Apart from real and integer values, the signature does +; not distinguish between integer and real versions of the overloaded operators +; of arithmetic. Instead, a single operator is used for both versions, which +; we prefix its name with `a.` where "a" is for "arithmetic". For example, +; `f_a.+` denotes the function for arithmetic addition and is used for +; applications of addition for both real and integer terms. Other non-overloaded +; operators, e.g. for transcendentals, are not prefixed by `a.`. + +; a real-valued constant, indexed by its rational value, represented as an mpq. +(declare real (! v mpq term)) +; a integer-valued constant, indexed by its integer value, represented as an mpz. +(declare int (! v mpz term)) +(declare f_a.+ term) +(define a.+ (# x term (# y term (apply (apply f_a.+ x) y)))) +(declare f_a.- term) +(define a.- (# x term (# y term (apply (apply f_a.- x) y)))) +(declare f_a.u- term) +(define a.u- (# x term (apply f_a.u- x))) +(declare f_a.* term) +(define a.* (# x term (# y term (apply (apply f_a.* x) y)))) +(declare f_a./ term) +(define a./ (# x term (# y term (apply (apply f_a./ x) y)))) +(declare f_a./_total term) +(define a./_total (# x term (# y term (apply (apply f_a./_total x) y)))) +(declare f_a.> term) +(define a.> (# x term (# y term (apply (apply f_a.> x) y)))) +(declare f_a.>= term) +(define a.>= (# x term (# y term (apply (apply f_a.>= x) y)))) +(declare f_a.< term) +(define a.< (# x term (# y term (apply (apply f_a.< x) y)))) +(declare f_a.<= term) +(define a.<= (# x term (# y term (apply (apply f_a.<= x) y)))) +(declare f_a.^ term) +(define a.^ (# x term (# y term (apply (apply f_a.^ x) y)))) +; Transcendentals +(declare real.pi term) +(declare f_exp term) +(define exp (# x term (apply f_exp x))) +(declare f_sin term) +(define sin (# x term (apply f_sin x))) +(declare f_cos term) +(define cos (# x term (apply f_cos x))) +(declare f_tan term) +(define tan (# x term (apply f_tan x))) +(declare f_csc term) +(define csc (# x term (apply f_csc x))) +(declare f_sec term) +(define sec (# x term (apply f_sec x))) +(declare f_cot term) +(define cot (# x term (apply f_cot x))) +(declare f_arcsin term) +(define arcsin (# x term (apply f_arcsin x))) +(declare f_arccos term) +(define arccos (# x term (apply f_arccos x))) +(declare f_arctan term) +(define arctan (# x term (apply f_arctan x))) +(declare f_arccsc term) +(define arccsc (# x term (apply f_arccsc x))) +(declare f_arcsec term) +(define arcsec (# x term (apply f_arcsec x))) +(declare f_arccot term) +(define arccot (# x term (apply f_arccot x))) +(declare f_sqrt term) +(define sqrt (# x term (apply f_sqrt x))) +(declare f_a.div term) +(define a.div (# x term (# y term (apply (apply f_a.div x) y)))) +(declare f_a.mod term) +(define a.mod (# x term (# y term (apply (apply f_a.mod x) y)))) +(declare f_a.div_total term) +(define a.div_total (# x term (# y term (apply (apply f_a.div_total x) y)))) +(declare f_a.mod_total term) +(define a.mod_total (# x term (# y term (apply (apply f_a.mod_total x) y)))) +; Other extended terms +(declare f_to_real term) +(define to_real (# x term (apply f_to_real x))) +(declare f_to_int term) +(define to_int (# x term (apply f_to_int x))) +(declare f_is_int term) +(define is_int (# x term (apply f_is_int x))) +(declare f_abs term) +(define abs (# x term (apply f_abs x))) +; "integer-and", see Zohar et al VMCAI 2022. +(declare f_iand (! x mpz term)) +(define iand (# x mpz (# y term (# z term (apply (apply (f_iand x) y) z))))) + +;; ---- Arrays +(declare f_select term) +(define select (# x term (# y term (apply (apply f_select x) y)))) +(declare f_store term) +(define store (# x term (# y term (# z term (apply (apply (apply f_store x) y) z))))) +(declare f_array_const (! s sort term)) +(define array_const (# x sort (# y term (apply (f_array_const x) y))) +(declare f_eqrange term) +(define eqrange (# x term (# y term (# z term (# w term (apply (apply (apply (apply f_eqrange x) y) z) w)))))) + +;; ---- Datatypes +; tester, indexed by the constructor that it tests +(declare is (! c term term)) +; updater, indexed by the selector field that it updates +(declare update (! s term term)) +; "shared selector" for (sort, index), see Reynolds et al IJCAR 2018. +(declare sel (! s sort (! z mpz term))) + +;; ---- Strings + +; In strings, values (i.e. word constants) are represented as null-terminated +; concatenation chains of character constants, indexed by Unicode code points. +; This means that the SMT-LIB syntax "ABC" denoting a string of length 3 is +; represented in LFSC as the term: +; `(str.++ (char 65) (str.++ (char 66) (str.++ (char 67) emptystr)))` + +; The empty string +(declare emptystr term) +; A character constant, indexed by its Unicode code point +(declare char (! v mpz term)) +(declare f_str.len term) +(define str.len (# x term (apply f_str.len x))) +(declare f_str.++ term) +(define str.++ (# x term (# y term (apply (apply f_str.++ x) y)))) +(declare f_str.substr term) +(define str.substr (# x term (# y term (# z term (apply (apply (apply f_str.substr x) y) z))))) +(declare f_str.contains term) +(define str.contains (# x term (# y term (apply (apply f_str.contains x) y)))) +(declare f_str.replace term) +(define str.replace (# x term (# y term (# z term (apply (apply (apply f_str.replace x) y) z))))) +(declare f_str.indexof term) +(define str.indexof (# x term (# y term (# z term (apply (apply (apply f_str.indexof x) y) z))))) +(declare f_str.at term) +(define str.at (# x term (# y term (apply (apply f_str.at x) y)))) +(declare f_str.prefixof term) +(define str.prefixof (# x term (# y term (apply (apply f_str.prefixof x) y)))) +(declare f_str.suffixof term) +(define str.suffixof (# x term (# y term (apply (apply f_str.suffixof x) y)))) +(declare f_str.rev term) +(define str.rev (# x term (apply f_str.rev x))) +(declare f_str.update term) +(define str.update (# x term (# y term (# z term (apply (apply (apply f_str.update x) y) z))))) +(declare f_str.tolower term) +(define str.tolower (# x term (apply f_str.tolower x))) +(declare f_str.toupper term) +(define str.toupper (# x term (apply f_str.toupper x))) +(declare f_str.to_code term) +(define str.to_code (# x term (apply f_str.to_code x))) +(declare f_str.from_code term) +(define str.from_code (# x term (apply f_str.from_code x))) +(declare f_str.is_digit term) +(define str.is_digit (# x term (apply f_str.is_digit x))) +(declare f_str.to_int term) +(define str.to_int (# x term (apply f_str.to_int x))) +(declare f_str.from_int term) +(define str.from_int (# x term (apply f_str.from_int x))) +(declare f_str.< term) +(define str.< (# x term (# y term (apply (apply f_str.< x) y)))) +(declare f_str.<= term) +(define str.<= (# x term (# y term (apply (apply f_str.<= x) y)))) +(declare f_str.indexof_re term) +(define str.indexof_re (# x term (# y term (# z term (apply (apply (apply f_str.indexof_re x) y) z))))) +(declare f_str.replace_re term) +(define str.replace_re (# x term (# y term (# z term (apply (apply (apply f_str.replace_re x) y) z))))) +(declare f_str.replace_re_all term) +(define str.replace_re_all (# x term (# y term (# z term (apply (apply (apply f_str.replace_re_all x) y) z))))) +; Regular expressions +(declare re.allchar term) +(declare re.none term) +(declare re.all term) +(declare re.empty term) ; singleton RE containing empty string, used as null terminator +(declare f_str.to_re term) +(define str.to_re (# x term (apply f_str.to_re x))) +(declare f_re.* term) +(define re.* (# x term (apply f_re.* x))) +(declare f_re.+ term) +(define re.+ (# x term (apply f_re.+ x))) +(declare f_re.opt term) +(define re.opt (# x term (apply f_re.opt x))) +(declare f_re.comp term) +(define re.comp (# x term (apply f_re.comp x))) +(declare f_re.range term) +(define re.range (# x term (# y term (apply (apply f_re.range x) y)))) +(declare f_re.++ term) +(define re.++ (# x term (# y term (apply (apply f_re.++ x) y)))) +(declare f_re.inter term) +(define re.inter (# x term (# y term (apply (apply f_re.inter x) y)))) +(declare f_re.union term) +(define re.union (# x term (# y term (apply (apply f_re.union x) y)))) +(declare f_re.diff term) +(define re.diff (# x term (# y term (apply (apply f_re.diff x) y)))) +(declare f_re.loop (! n1 mpz (! n2 mpz term))) +(define re.loop (# n1 mpz (# n2 mpz (# x term (apply (f_re.loop n1 n2) x))))) +(declare f_str.in_re term) +(define str.in_re (# x term (# y term (apply (apply f_str.in_re x) y)))) +; Sequences +(declare seq.empty (! s sort term)) +(declare f_seq.unit term) +(define seq.unit (# x term (apply f_seq.unit x))) +(declare f_seq.nth term) +(define seq.nth (# x term (# y term (apply (apply f_seq.nth x) y)))) +(declare f_seq.len term) +(define seq.len (# x term (apply f_seq.len x))) +(declare f_seq.++ term) +(define seq.++ (# x term (# y term (apply (apply f_seq.++ x) y)))) +(declare f_seq.extract term) +(define seq.extract (# x term (# y term (# z term (apply (apply (apply f_seq.extract x) y) z))))) +(declare f_seq.contains term) +(define seq.contains (# x term (# y term (apply (apply f_seq.contains x) y)))) +(declare f_seq.replace term) +(define seq.replace (# x term (# y term (# z term (apply (apply (apply f_seq.replace x) y) z))))) +(declare f_seq.indexof term) +(define seq.indexof (# x term (# y term (# z term (apply (apply (apply f_seq.indexof x) y) z))))) +(declare f_seq.prefixof term) +(define seq.prefixof (# x term (# y term (apply (apply f_seq.prefixof x) y)))) +(declare f_seq.suffixof term) +(define seq.suffixof (# x term (# y term (apply (apply f_seq.suffixof x) y)))) +(declare f_seq.rev term) +(define seq.rev (# x term (apply f_seq.rev x))) +(declare f_seq.update term) +(define seq.update (# x term (# y term (# z term (apply (apply (apply f_seq.update x) y) z))))) +; skolem types +(declare skolem_re_unfold_pos (! t term (! r term (! z mpz term)))) + +;; ---- Bit-vectors + +; A bit-vector constant, indexed by a bitvec, denoting its value. +(declare bv (! b bitvec term)) +(declare f_bvnot term) +(define bvnot (# x term (apply f_bvnot x))) +(declare f_bvand term) +(define bvand (# x term (# y term (apply (apply f_bvand x) y)))) +(declare f_bvor term) +(define bvor (# x term (# y term (apply (apply f_bvor x) y)))) +(declare f_bvxor term) +(define bvxor (# x term (# y term (apply (apply f_bvxor x) y)))) +(declare f_bvnand term) +(define bvnand (# x term (# y term (apply (apply f_bvnand x) y)))) +(declare f_bvnor term) +(define bvnor (# x term (# y term (apply (apply f_bvnor x) y)))) +(declare f_bvxnor term) +(define bvxnor (# x term (# y term (apply (apply f_bvxnor x) y)))) +(declare f_bvmul term) +(define bvmul (# x term (# y term (apply (apply f_bvmul x) y)))) +(declare f_bvneg term) +(define bvneg (# x term (apply f_bvneg x))) +(declare f_bvadd term) +(define bvadd (# x term (# y term (apply (apply f_bvadd x) y)))) +(declare f_bvsub term) +(define bvsub (# x term (# y term (apply (apply f_bvsub x) y)))) +(declare f_bvudiv term) +(define bvudiv (# x term (# y term (apply (apply f_bvudiv x) y)))) +(declare f_bvurem term) +(define bvurem (# x term (# y term (apply (apply f_bvurem x) y)))) +(declare f_bvsdiv term) +(define bvsdiv (# x term (# y term (apply (apply f_bvsdiv x) y)))) +(declare f_bvsrem term) +(define bvsrem (# x term (# y term (apply (apply f_bvsrem x) y)))) +(declare f_bvsmod term) +(define bvsmod (# x term (# y term (apply (apply f_bvsmod x) y)))) +(declare f_bvshl term) +(define bvshl (# x term (# y term (apply (apply f_bvshl x) y)))) +(declare f_bvlshr term) +(define bvlshr (# x term (# y term (apply (apply f_bvlshr x) y)))) +(declare f_bvashr term) +(define bvashr (# x term (# y term (apply (apply f_bvashr x) y)))) +(declare f_bvult term) +(define bvult (# x term (# y term (apply (apply f_bvult x) y)))) +(declare f_bvule term) +(define bvule (# x term (# y term (apply (apply f_bvule x) y)))) +(declare f_bvugt term) +(define bvugt (# x term (# y term (apply (apply f_bvugt x) y)))) +(declare f_bvuge term) +(define bvuge (# x term (# y term (apply (apply f_bvuge x) y)))) +(declare f_bvslt term) +(define bvslt (# x term (# y term (apply (apply f_bvslt x) y)))) +(declare f_bvsle term) +(define bvsle (# x term (# y term (apply (apply f_bvsle x) y)))) +(declare f_bvsgt term) +(define bvsgt (# x term (# y term (apply (apply f_bvsgt x) y)))) +(declare f_bvsge term) +(define bvsge (# x term (# y term (apply (apply f_bvsge x) y)))) +(declare f_bvcomp term) +(define bvcomp (# x term (# y term (apply (apply f_bvcomp x) y)))) +(declare f_concat term) +(define concat (# x term (# y term (apply (apply f_concat x) y)))) +(declare f_rotate_left (! v mpz term)) +(define rotate_left (# x mpz (# y term (apply (f_rotate_left x) y)))) +(declare f_rotate_right (! v mpz term)) +(define rotate_right (# x mpz (# y term (apply (f_rotate_right x) y)))) +(declare f_zero_extend (! v mpz term)) +(define zero_extend (# x mpz (# y term (apply (f_zero_extend x) y)))) +(declare f_sign_extend (! v mpz term)) +(define sign_extend (# x mpz (# y term (apply (f_sign_extend x) y)))) +(declare f_repeat (! v mpz term)) +(define repeat (# x mpz (# y term (apply (f_repeat x) y)))) +(declare f_extract (! i mpz (! j mpz term))) +(define extract (# x mpz (# y mpz (# z term (apply (f_extract x y) z))))) +(declare f_bv2nat term) +(define bv2nat (# x term (apply f_bv2nat x))) +(declare f_int2bv (! i mpz term)) +(define int2bv (# x mpz (# y term (apply (f_int2bv x) y)))) +; Internal definitions for Bitblasting +(declare f_bbT term) +(define bbT (# x term (# y term (apply (apply f_bbT x) y)))) +(declare f_bitOf (! b mpz term)) +(define bitOf (# b mpz (# x term (apply (f_bitOf b) x)))) +(declare f_BITVECTOR_EAGER_ATOM term) +(define BITVECTOR_EAGER_ATOM (# x term (apply f_BITVECTOR_EAGER_ATOM x))) +; The empty bitvector, which is used as the null terminator of bvconcat chains +(declare emptybv term) + +;; ---- Sets +(declare emptyset (! s sort term)) +(declare univset (! s sort term)) +(declare f_singleton term) +(define singleton (# x term (apply f_singleton x))) +(declare f_union term) +(define union (# x term (# y term (apply (apply f_union x) y)))) +(declare f_intersection term) +(define intersection (# x term (# y term (apply (apply f_intersection x) y)))) +(declare f_setminus term) +(define setminus (# x term (# y term (apply (apply f_setminus x) y)))) +(declare f_complement term) +(define complement (# x term (apply f_complement x))) +(declare f_member term) +(define member (# x term (# y term (apply (apply f_member x) y)))) +(declare f_subset term) +(define subset (# x term (# y term (apply (apply f_subset x) y)))) +(declare f_card term) +(define card (# x term (apply f_card x))) +(declare f_choose term) +(define choose (# x term (apply f_choose x))) +(declare f_is_singleton term) +(define is_singleton (# x term (apply f_is_singleton x))) +(declare f_join term) +(define join (# x term (# y term (apply (apply f_join x) y)))) +(declare f_product term) +(define product (# x term (# y term (apply (apply f_product x) y)))) +(declare f_transpose term) +(define transpose (# x term (apply f_transpose x))) +(declare f_tclosure term) +(define tclosure (# x term (apply f_tclosure x))) +(declare f_iden term) +(define iden (# x term (apply f_iden x))) +(declare f_join_image term) +(define join_image (# x term (# y term (apply (apply f_join_image x) y)))) +(declare f_insert term) +(define insert (# x term (# y term (apply (apply f_insert x) y)))) + +;; ---- Bags +(declare emptybag (! s sort term)) +(declare f_union_max term) +(define union_max (# x term (# y term (apply (apply f_union_max x) y)))) +(declare f_union_disjoint term) +(define union_disjoint (# x term (# y term (apply (apply f_union_disjoint x) y)))) +(declare f_intersection_min term) +(define intersection_min (# x term (# y term (apply (apply f_intersection_min x) y)))) +(declare f_difference_subtract term) +(define difference_subtract (# x term (# y term (apply (apply f_difference_subtract x) y)))) +(declare f_difference_remove term) +(define difference_remove (# x term (# y term (apply (apply f_difference_remove x) y)))) +(declare f_subbag term) +(define subbag (# x term (# y term (apply (apply f_subbag x) y)))) +(declare f_bag.count term) +(define bag.count (# x term (# y term (apply (apply f_bag.count x) y)))) +(declare f_bag term) +(define bag (# x term (# y term (apply (apply f_bag x) y)))) +(declare f_duplicate_removal term) +(define duplicate_removal (# x term (apply f_duplicate_removal x))) + +;; ---- Separation Logic +(declare sep.nil (! s sort term)) +(declare f_sep term) +(define sep (# x term (# y term (apply (apply f_sep x) y)))) +(declare f_sep_label term) +(define sep_label (# x term (# y term (apply (apply f_sep_label x) y)))) +(declare f_wand term) +(define wand (# x term (# y term (apply (apply f_wand x) y)))) +(declare f_pto term) +(define pto (# x term (# y term (apply (apply f_pto x) y)))) +; the empty heap constraint +(declare sep.emp term) +; internally generated in separation logic reductions +(declare f_SEP_LABEL term) +(define SEP_LABEL (# x term (# y term (apply (apply f_SEP_LABEL x) y)))) + +;; ---- UF with cardinality +; internally generated for finite model finding +(declare f_fmf.card term) +(define fmf.card (# x term (# y term (apply (apply f_fmf.card x) y)))) diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf new file mode 100644 index 000000000..5639cc54e --- /dev/null +++ b/proofs/lfsc/signatures/util_defs.plf @@ -0,0 +1,104 @@ +; depends: core_defs.plf + +; This file contains utilities used throughout the proof signatures. + +; A "flag" is a Boolean value. +(declare flag type) +(declare tt flag) +(declare ff flag) + +; "Ok" is a unit value, used to indicate that e.g. a side condition ran successfully. +(declare Ok type) +(declare ok Ok) + +; A pair of terms. +(declare termPair type) +(declare pair (! first term (! second term termPair))) + +; Bits, used to represent bit-vectors +(declare bit type) +(declare b0 bit) +(declare b1 bit) + +; A bit-vector, which is a list of bits. Used to represent a value of bit-vector type. +(declare bitvec type) +(declare bvn bitvec) +(declare bvc (! b bit (! v bitvec bitvec))) + +;; ---- Side conditions + +; Get the argument from an f-application t, fail if t is not an f-application. +(program getarg ((f term) (t term)) term + (match t ((apply t1 t2) (ifequal t1 f t2 (fail term))))) + +; Get the argument from an f-application t, return the term t itself if it is not an f-application. +(program try_getarg ((f term) (t term)) term + (match t ((apply t1 t2) (ifequal t1 f t2 t)) (default t))) + +; Convert to original form. +; This replaces the Skolems that occur in `t` with their witness terms provided +; that the witness term of `t` is *not* an application of the witness +; quantifier. In other words, Skolem variables whose witness terms have +; witness quantification are left unchanged; all others are converted. This +; method is commonly used to recovert the "unpurified" version of a term, so +; that certain reasoning steps e.g. witness sharing (see Reynolds et al +; FMCAD 2020) can be justified. +(program sc_to_original ((t term)) term + (match t + ((apply t1 t2) (apply (sc_to_original t1) (sc_to_original t2))) + ((skolem w) + ; witness terms stay beneath skolems, other terms are converted + (match w + ((apply w1 w2) + (match w1 + ((f_witness v s) t) + (default w))) + (default w))) + (default t) + )) + +; Make a skolem, which ensures that the given term is in original form. For +; consistency, we require that the witness term for all Skolems are in +; original form. Failure to use this side condition when introducing fresh +; Skolems will result in proofs failing to check due to mismatched uses of +; Skolem variables in conclusions. +(program sc_mk_skolem ((t term)) term (skolem (sc_to_original t))) + +;; ---- Proof rules + +; "proof-let", which is used to introduce a variable corresponding to the +; conclusion of a proof. For example: +; `(plet _ _ P (\ u Q))` +; is a proof where the variable `u` has type `(holds g)`, where `g` is +; the conclusion of proof `P`. Notice that `u` can be freely used in `Q`. We +; use this rule whenever a proof is used multiple times in a scope, for the +; purposes of compressing the size of proofs. + +(declare plet (! f term + (! g term + (! p (holds g) + (! u (! v (holds g) (holds f)) + (holds f)))))) + +; "scope", which defines a proof under an assumption. This introduces an +; assumption that can be used in a child proof, and concludes a disjunction +; having that assumption. For example: +; `(scope _ g (\ u Q))` +; is a proof where the variable `u` has type `(holds g)`, which can be freely +; used in `Q`. If `Q` has type `(holds f)`, the above has type +; `(holds (or (not g) f))`, in other words, either the assumption `g` does not +; hold, or `f` holds. +; Note that this assumes f is in n-ary, null-terminated form (see +; nary_programs.plf). +; This rule corresponds to the cvc5 internal calculus rule "SCOPE". + +(declare scope (! f term + (! g term + (! u (! v (holds g) (holds f)) + (holds (or (not g) f)))))) + +; "trust", which is used when the proof of a given fact `f` was not provided +; by the solver. Any LFSC proof with trust indicates that the proof was +; incomplete. + +(declare trust (! f term (holds f))) |