From da087b4f6cc677261961f5ea8a7c5b08b02060c7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Dec 2021 09:49:58 -0600 Subject: [PATCH] Updates to LFSC signatures (#7840) Includes the addition of print 2 rules from Amazon benchmarks, and updates to the names of functions. --- proofs/lfsc/signatures/arith_programs.plf | 9 ++ proofs/lfsc/signatures/arith_rules.plf | 36 ++++++- proofs/lfsc/signatures/strings_programs.plf | 1 - proofs/lfsc/signatures/theory_def.plf | 102 ++++++++++---------- proofs/lfsc/signatures/util_defs.plf | 7 ++ src/proof/lfsc/lfsc_printer.cpp | 11 +++ 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() << cs[0] << cs[1]; break; + case PfRule::CONCAT_CONFLICT: + pf << h << h << args[0].getConst() << cs[0]; break; case PfRule::RE_UNFOLD_POS: if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT) -- 2.30.2