Fixes and additions for LFSC signatures (#8120)

Fixes a critical issue in the re intersection rule, where a null terminator was missed.

Also adds a sketch of the theory signature for floating points.

diff --git a/proofs/lfsc/signatures/strings_rules.plf b/proofs/lfsc/signatures/strings_rules.plf
index 301d6f77b8d7e6366956ec97af0876c569e5ae83..5d4f5ad3db5cf6e69b022381665e3f819b1751ef 100644 (file)
--- a/proofs/lfsc/signatures/strings_rules.plf
+++ b/proofs/lfsc/signatures/strings_rules.plf
@@ -107,7 +107,7 @@
   (holds (or (and (= (str.len t) (int 0)) (and (= t emptystr) true)) (or (a.> (str.len t) (int 0)) false)))))
 
 (declare re_inter (! x term (! s term (! t term (! p1 (holds (str.in_re x s)) (! p2 (holds (str.in_re x t)) 
-  (holds (str.in_re x (re.inter s t)))))))))
+  (holds (str.in_re x (re.inter s (re.inter t (re.* re.allchar)))))))))))
 
 (declare string_reduction (! r term (! t term (! s sort (! u (^ (sc_string_reduction t s) r)
   (holds r))))))))

diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index e797bcf4184076cad7b3c372b111b4f7f106f7a8..da9689ab92a3e2397abb0f122d8e1bf0729686d8 100644 (file)
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -126,7 +126,7 @@
 (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)))
+(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))))))
 
@@ -342,6 +342,85 @@
 ; The empty bitvector, which is used as the null terminator of bvconcat chains
 (declare emptybv term)
 
+
+;; ---- Floating points
+
+; a floating point constant is indexed by 3 bitvector constants
+(declare fp (! s bitvec (! e bitvec (! i bitvec term))))
+(declare f_fp.add term)
+(define fp.add (# x term (# y term (# z term (apply (apply (apply f_fp.add x) y) z)))))
+(declare f_fp.sub term)
+(define fp.sub (# x term (# y term (# z term (apply (apply (apply f_fp.sub x) y) z)))))
+(declare f_fp.mul term)
+(define fp.mul (# x term (# y term (# z term (apply (apply (apply f_fp.mul x) y) z)))))
+(declare f_fp.div term)
+(define fp.div (# x term (# y term (# z term (apply (apply (apply f_fp.div x) y) z)))))
+(declare f_fp.fma term)
+(define fp.fma (# x term (# y term (# z term (# w term (apply (apply  (apply (apply f_fp.fma x) y) z) w))))))
+(declare f_fp.sqrt term)
+(define fp.sqrt (# x term (# y term (apply (apply f_fp.sqrt x) y))))
+(declare f_fp.rem term)
+(define fp.rem (# x term (# y term (apply (apply f_fp.rem x) y))))
+(declare f_fp.roundToIntegral term)
+(define fp.roundToIntegral (# x term (# y term (apply (apply f_fp.roundToIntegral x) y))))
+(declare f_fp.min term)
+(define fp.min (# x term (# y term (apply (apply f_fp.min x) y))))
+(declare f_fp.max term)
+(define fp.max (# x term (# y term (apply (apply f_fp.max x) y))))
+(declare f_fp.leq term)
+(define fp.leq (# x term (# y term (apply (apply f_fp.leq x) y))))
+(declare f_fp.lt term)
+(define fp.lt (# x term (# y term (apply (apply f_fp.lt x) y))))
+(declare f_fp.geq term)
+(define fp.geq (# x term (# y term (apply (apply f_fp.geq x) y))))
+(declare f_fp.gt term)
+(define fp.gt (# x term (# y term (apply (apply f_fp.gt x) y))))
+(declare f_fp.eq term)
+(define fp.eq (# x term (# y term (apply (apply f_fp.eq x) y))))
+(declare f_to_fp_unsigned (! i mpz (! j mpz term)))
+(define to_fp_unsigned (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_unsigned x y) z) w))))))
+(declare f_fp.to_ubv (! i mpz term))
+(define fp.to_ubv (# x mpz (# z term (# w term (apply (apply (f_fp.to_ubv x) z) w)))))
+(declare f_fp.to_sbv (! i mpz term))
+(define fp.to_sbv (# x mpz (# z term (# w term (apply (apply (f_fp.to_sbv x) z) w)))))
+(declare f_fp.abs term)
+(define fp.abs (# x term (apply f_fp.abs x)))
+(declare f_fp.neg term)
+(define fp.neg (# x term (apply f_fp.neg x)))
+(declare f_fp.isNormal term)
+(define fp.isNormal (# x term (apply f_fp.isNormal x)))
+(declare f_fp.isSubnormal term)
+(define fp.isSubnormal (# x term (apply f_fp.isSubnormal x)))
+(declare f_fp.isZero term)
+(define fp.isZero (# x term (apply f_fp.isZero x)))
+(declare f_fp.isInfinite term)
+(define fp.isInfinite (# x term (apply f_fp.isInfinite x)))
+(declare f_fp.isNaN term)
+(define fp.isNaN (# x term (apply f_fp.isNaN x)))
+(declare f_fp.isNegative term)
+(define fp.isNegative (# x term (apply f_fp.isNegative x)))
+(declare f_fp.isPositive term)
+(define fp.isPositive (# x term (apply f_fp.isPositive x)))
+(declare f_fp.to_real term)
+(define fp.to_real (# x term (apply f_fp.to_real x)))
+; to avoid overloading, must distinguish types
+(declare f_to_fp_fp (! i mpz (! j mpz term)))
+(define to_fp_fp (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_fp x y) z) w))))))
+(declare f_to_fp_real (! i mpz (! j mpz term)))
+(define to_fp_real (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_real x y) z) w))))))
+(declare f_to_fp_sbv (! i mpz (! j mpz term)))
+(define to_fp_sbv (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_sbv x y) z) w))))))
+(declare f_to_fp_generic (! i mpz (! j mpz term)))
+(define to_fp_generic (# x mpz (# y mpz (# z term (# w term (apply (apply (f_to_fp_generic x y) z) w))))))
+(declare f_to_fp_bv (! i mpz (! j mpz term)))
+(define to_fp_bv (# x mpz (# y mpz (# z term (apply (f_to_fp_bv x y) z)))))
+; rounding modes
+(declare roundNearestTiesToEven term)
+(declare roundNearestTiesToAway term)
+(declare roundTowardPositive term)
+(declare roundTowardNegative term)
+(declare roundTowardZero term)
+
 ;; ---- Sets
 (declare set.empty (! s sort term))
 (declare set.universe (! s sort term))
@@ -410,12 +489,16 @@
 (define bag.from_set (# x term (apply f_bag.from_set x)))
 (declare f_bag.to_set term)
 (define bag.to_set (# x term (apply f_bag.to_set x)))
+(declare f_bag.member term)
+(define bag.member (# x term (# y term (apply (apply f_bag.member x) y))))
 (declare f_bag.map term)
 (define bag.map (# x term (# y term (apply (apply f_bag.map x) y))))
 (declare f_bag.filter term)
 (define bag.filter (# x term (# y term (apply (apply f_bag.filter x) y))))
 (declare f_bag.fold term)
-(define bag.fold (# x term (# y term (apply (apply f_bag.fold x) y))))
+(define bag.fold (# x term (# y term (# z term (apply (apply (apply f_bag.fold x) y) z)))))
+(declare f_table.product term)
+(define table.product (# x term (# y term (apply (apply f_table.product x) y))))
 
 ;; ---- Separation Logic
 (declare sep.nil (! s sort term))
@@ -434,6 +517,5 @@
 (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))))
+; internally generated for finite model finding. Note this is an indexed constant.
+(declare fmf.card (! s sort (! i mpz term)))