From: Andrew Reynolds Date: Fri, 25 Feb 2022 22:01:01 +0000 (-0600) Subject: Syntax fixes for LFSC signature (#8172) X-Git-Tag: cvc5-1.0.0~370 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9764781383b86608cae4bff2fe3cd0edc6e1107;p=cvc5.git Syntax fixes for LFSC signature (#8172) --- diff --git a/proofs/lfsc/signatures/arith_rules.plf b/proofs/lfsc/signatures/arith_rules.plf index 8c134181e..095d3d0bd 100644 --- a/proofs/lfsc/signatures/arith_rules.plf +++ b/proofs/lfsc/signatures/arith_rules.plf @@ -94,7 +94,7 @@ ; 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 +(program sc_check_int_tight_lb ((t term) (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)))))) diff --git a/proofs/lfsc/signatures/cnf_rules.plf b/proofs/lfsc/signatures/cnf_rules.plf index c593a0a95..90744e204 100644 --- a/proofs/lfsc/signatures/cnf_rules.plf +++ b/proofs/lfsc/signatures/cnf_rules.plf @@ -20,9 +20,9 @@ (declare cnf_xor_neg1 (! f1 term (! f2 term (holds (or (xor f1 f2) (or (not f1) (or f2 false))))))) (declare cnf_xor_neg2 (! f1 term (! f2 term (holds (or (xor f1 f2) (or f1 (or (not f2) false))))))) -(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or (not c) (or f1 false))))))) -(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or c (or f2 false))))))) -(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or f1 (or f2 false))))))) -(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not c) (or (not f1) false))))))) -(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or c (or (not f2) false))))))) -(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not f1) (or (not f2) false))))))) +(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or (not c) (or f1 false)))))))) +(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or c (or f2 false)))))))) +(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or f1 (or f2 false)))))))) +(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not c) (or (not f1) false)))))))) +(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or c (or (not f2) false)))))))) +(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not f1) (or (not f2) false)))))))) diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf index 7bdd6539c..6c30ca523 100644 --- a/proofs/lfsc/signatures/quantifiers_rules.plf +++ b/proofs/lfsc/signatures/quantifiers_rules.plf @@ -43,7 +43,7 @@ (! body term (! p (holds bodyi) (! r (^ (sc_substitute body v s) bodyi) - (holds (exists v u body))))))))) + (holds (exists v u body)))))))))) (declare skolem_intro (! u term (! t term