Updates to LFSC signatures (#7840)

Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions.

6 files changed, 112 insertions, 54 deletions

diff --git a/proofs/lfsc/signatures/arith_programs.plf b/proofs/lfsc/signatures/arith_programs.plf
index 219bbe326..69999fbd0 100644
--- a/proofs/lfsc/signatures/arith_programs.plf
+++ b/proofs/lfsc/signatures/arith_programs.plf
@@ -1,5 +1,14 @@
 ; depends: theory_def.plf
 
+
+; get the mpq from the real constant term c
+(program sc_arith_get_mpq ((c term)) mpq
+  (match c ((real q) q)))
+
+; get the mpz from the integer constant term c
+(program sc_arith_get_mpz ((c term)) mpz
+  (match c ((int z) z)))
+
 ; get the relation symbol from f, for example for (a.>= t1 t2), return a.>=
 (program sc_arith_get_rel ((f term)) term
   (match f ((apply f1 f2) (match f1 ((apply f11 f12) f11)))))
diff --git a/proofs/lfsc/signatures/arith_rules.plf b/proofs/lfsc/signatures/arith_rules.plf
index 850c2b5e6..8c134181e 100644
--- a/proofs/lfsc/signatures/arith_rules.plf
+++ b/proofs/lfsc/signatures/arith_rules.plf
@@ -70,7 +70,39 @@
   (! res term
   (! f1 term
   (! f2 term
-  (! p (holds f1)
-  (! p (holds f2)
+  (! p1 (holds f1)
+  (! p2 (holds f2)
   (! r (^ (sc_arith_trichotomy f1 f2) res)
     (holds res))))))))
+
+; Returns ok if c is the greatest integer less than (integer or real) constant
+; t. We compute this via conditions 0 <= c-t ^ (c-t)-1 <= 0.
+(program sc_check_int_tight_ub ((t term) (c term)) Ok
+  (mpq_between_zero_one (mp_add (match t ((int ct) (mpz_to_mpq ct)) ((real ct) ct))
+                                (mp_neg (mpz_to_mpq (sc_arith_get_mpz c))))))
+
+; Integer tight upper bound rule, which uses the above side condition to
+; compute whether c is the greatest integer less than t. The constant c must
+; be provided to applications of this rule.
+(declare int_tight_ub
+  (! s term
+  (! t term
+  (! c term
+  (! p (holds (a.< s t))
+  (! r (^ (sc_check_int_tight_ub t c) ok)
+    (holds (a.<= s c))))))))
+
+; Returns ok if c2 is the least integer greater than c1. We compute this
+; via conditions 0 <= c1-c2 ^ (c1-c2)-1 <= 0.
+(program sc_check_int_tight_lb ((t mpq) (c term)) Ok
+  (mpq_between_zero_one (mp_add (mpz_to_mpq (sc_arith_get_mpz c))
+                                (mp_neg (match t ((int ct) (mpz_to_mpq ct)) ((real ct) ct))))))
+
+; Similar to int_tight_ub, but for lower bound.
+(declare int_tight_lb
+  (! s term
+  (! t term
+  (! c term
+  (! p (holds (a.> s t))
+  (! r (^ (sc_check_int_tight_lb t c) ok)
+    (holds (a.>= s c))))))))
diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf
index 6a152772f..4e36fc91f 100644
--- a/proofs/lfsc/signatures/strings_programs.plf
+++ b/proofs/lfsc/signatures/strings_programs.plf
@@ -231,7 +231,6 @@
         ((char n) t12))))
     (emptystr t)))
 
-
 ; Flatten constants in str.++ application s. Notice that the rewritten form
 ; of strings in cvc5 are such that constants are grouped into constants of
 ; length >=1 which we call "word" constants. For example, the cvc5 rewritten
diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf
index 9d762b03b..691fd4ea9 100644
--- a/proofs/lfsc/signatures/theory_def.plf
+++ b/proofs/lfsc/signatures/theory_def.plf
@@ -341,63 +341,63 @@
 (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))))
+(declare set.empty (! s sort term))
+(declare set.universe (! s sort term))
+(declare f_set.singleton term)
+(define set.singleton (# x term (apply f_set.singleton x)))
+(declare f_set.union term)
+(define set.union (# x term (# y term (apply (apply f_set.union x) y))))
+(declare f_set.inter term)
+(define set.inter (# x term (# y term (apply (apply f_set.inter x) y))))
+(declare f_set.minus term)
+(define set.minus (# x term (# y term (apply (apply f_set.minus x) y))))
+(declare f_set.complement term)
+(define set.complement (# x term (apply f_set.complement x)))
+(declare f_set.member term)
+(define set.member (# x term (# y term (apply (apply f_set.member x) y))))
+(declare f_set.subset term)
+(define set.subset (# x term (# y term (apply (apply f_set.subset x) y))))
+(declare f_set.card term)
+(define set.card (# x term (apply f_set.card x)))
+(declare f_set.choose term)
+(define set.choose (# x term (apply f_set.choose x)))
+(declare f_set.is_singleton term)
+(define set.is_singleton (# x term (apply f_set.is_singleton x)))
+(declare f_rel.join term)
+(define rel.join (# x term (# y term (apply (apply f_rel.join x) y))))
+(declare f_rel.product term)
+(define rel.product (# x term (# y term (apply (apply f_rel.product x) y))))
+(declare f_rel.transpose term)
+(define rel.transpose (# x term (apply f_rel.transpose x)))
+(declare f_rel.tclosure term)
+(define rel.tclosure (# x term (apply f_rel.tclosure x)))
+(declare f_rel.iden term)
+(define rel.iden (# x term (apply f_rel.iden x)))
+(declare f_rel.join_image term)
+(define rel.join_image (# x term (# y term (apply (apply f_rel.join_image x) y))))
+(declare f_set.insert term)
+(define set.insert (# x term (# y term (apply (apply f_set.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 bag.empty (! s sort term))
+(declare f_bag.union_max term)
+(define bag.union_max (# x term (# y term (apply (apply f_bag.union_max x) y))))
+(declare f_bag.union_disjoint term)
+(define bag.union_disjoint (# x term (# y term (apply (apply f_bag.union_disjoint x) y))))
+(declare f_bag.inter_min term)
+(define bag.inter_min (# x term (# y term (apply (apply f_bag.inter_min x) y))))
+(declare f_bag.difference_subtract term)
+(define bag.difference_subtract (# x term (# y term (apply (apply f_bag.difference_subtract x) y))))
+(declare f_bag.difference_remove term)
+(define bag.difference_remove (# x term (# y term (apply (apply f_bag.difference_remove x) y))))
+(declare f_bag.subbag term)
+(define bag.subbag (# x term (# y term (apply (apply f_bag.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)))
+(declare f_bag.duplicate_removal term)
+(define bag.duplicate_removal (# x term (apply f_bag.duplicate_removal x)))
 
 ;; ---- Separation Logic
 (declare sep.nil (! s sort term))
diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf
index 8d1793666..5880ab8fc 100644
--- a/proofs/lfsc/signatures/util_defs.plf
+++ b/proofs/lfsc/signatures/util_defs.plf
@@ -30,6 +30,13 @@
   (mp_ifzero (mp_add (mp_neg v1) v2) t s)
 )
 
+; Returns true if 0 <= c <= 1
+(program mpq_between_zero_one ((c mpq)) Ok
+  (mp_ifneg c
+    (fail Ok)
+    (let c2 (mp_add c (mp_neg 1/1))
+      (mp_ifneg c2 ok (mp_ifzero c2 ok (fail Ok))))))
+
 ;; ---- Side conditions
 
 ; Get the argument from an f-application t, fail if t is not an f-application.
diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index 3772e2386..8c659dc0c 100644
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -568,6 +568,15 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
       pf << h << h << h << cs[0] << cs[1];
     }
     break;
+    case PfRule::INT_TIGHT_UB:
+    case PfRule::INT_TIGHT_LB:
+    {
+      Node res = pn->getResult();
+      Assert(res.getNumChildren() == 2);
+      Assert(res[1].getKind() == CONST_RATIONAL);
+      pf << h << h << d_tproc.convert(res[1]) << cs[0];
+    }
+    break;
     // strings
     case PfRule::STRING_LENGTH_POS: pf << as[0]; break;
     case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break;
@@ -581,6 +590,8 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
     case PfRule::CONCAT_CSPLIT:
       pf << h << h << h << h << args[0].getConst<bool>() << cs[0] << cs[1];
       break;
+    case PfRule::CONCAT_CONFLICT:
+      pf << h << h << args[0].getConst<bool>() << cs[0];
       break;
     case PfRule::RE_UNFOLD_POS:
       if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT)