From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Oct 2021 13:33:04 +0000 (-0500)
Subject: Add core LFSC signatures (#7289)
X-Git-Tag: cvc5-1.0.0~1070
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b17ee60bc45e030113bcfdf5cdf575b0f6f961f1;p=cvc5.git

Add core LFSC signatures (#7289)

These files define how terms and sorts are represented. It also adds basic utilities used throughout.
---

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)))