diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-02 08:16:29 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-02 13:16:29 +0000 |
commit | 7ea2ea8f708fc7b5e8ea370898fbcb8cbf487aec (patch) | |
tree | 4b8f96bfea654df4877d290ec6e3c0585e83afd9 | |
parent | b5849b2061c841926f7548858613223d1e805b21 (diff) |
Add LFSC signature for quantifiers (#7540)
Also includes a fix for the Boolean signature. After the strings PR and this one, the initial LFSC signature is complete.
-rw-r--r-- | proofs/lfsc/signatures/boolean_programs.plf | 4 | ||||
-rw-r--r-- | proofs/lfsc/signatures/boolean_rules.plf | 2 | ||||
-rw-r--r-- | proofs/lfsc/signatures/quantifiers_rules.plf | 51 | ||||
-rw-r--r-- | proofs/lfsc/signatures/util_defs.plf | 5 |
4 files changed, 59 insertions, 3 deletions
diff --git a/proofs/lfsc/signatures/boolean_programs.plf b/proofs/lfsc/signatures/boolean_programs.plf index 9bf87f69f..eecc71a98 100644 --- a/proofs/lfsc/signatures/boolean_programs.plf +++ b/proofs/lfsc/signatures/boolean_programs.plf @@ -55,9 +55,9 @@ ; Pulls not from a list of children of an or-application. In terms of SMT-LIB ; syntax, this side condition converts: -; (or (not F1) ... (not Fn)) to (not (and F1 ... Fn)) +; (or (not F1) ... (not Fn)) to (and F1 ... Fn) (program sc_not_and_rev ((t term)) term - (not (nary_elim f_and (sc_not_and_rev_rec t) true)) + (nary_elim f_and (sc_not_and_rev_rec t) true) ) ; Process scope side condition. This side condition is used for constructing the diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf index b6df71177..af16af1f9 100644 --- a/proofs/lfsc/signatures/boolean_rules.plf +++ b/proofs/lfsc/signatures/boolean_rules.plf @@ -45,7 +45,7 @@ (declare not_and (! c1 term (! c2 term (! p1 (holds (not c1)) (! r (^ (sc_not_and c1) c2) (holds c2)))))) -(declare not_and_rev (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (sc_not_and_rev c1) c2) (holds c2)))))) +(declare not_and_rev (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (sc_not_and_rev c1) c2) (holds (not c2))))))) ; Process scope, which is used to translate PfRule::SCOPE. It runs the side ; condition sc_process_scope on f to generate an equivalent formula g. diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf new file mode 100644 index 000000000..7bdd6539c --- /dev/null +++ b/proofs/lfsc/signatures/quantifiers_rules.plf @@ -0,0 +1,51 @@ +; depends: theory_def.plf util_defs.plf + +; Substitute, which returns the result of replacing all occurrences of the +; bound variable whose identifier is v with the term s. It is the responsibility +; of the caller to ensure that all occurrences of (bvar v u) in t are such that +; u is the sort of s. Otherwise, this will return a term that is not well +; sorted. +(program sc_substitute ((t term) (v mpz) (s term)) term + (match t + ((bvar v1 u1) (mpz_ifequal v v1 s t)) + ((apply t1 t2) (apply (sc_substitute t1 v s) (sc_substitute t2 v s))) + (default t) + )) + +; Concludes the instantiation for the term of the outermost quantifier in the +; rule PfRule::INSTANTIATE. We do not enforce type checking of term s +; currently, which should be of sort u. +(declare instantiate (! body term + (! v mpz + (! u sort + (! s term + (! bodyi term + (! p (holds (forall v u body)) + (! r (^ (sc_substitute body v s) bodyi) + (holds bodyi))))))))) + +; Concludes the skolemization for the term of the outermost quantifier in the +; rule PfRule::SKOLEMIZE. +(declare skolemize (! body term + (! v mpz + (! s sort + (! bodyi term + (! p (holds (exists v s body)) + (! r (^ (sc_substitute body v (skolem (witness v s body))) bodyi) + (holds bodyi)))))))) + +; We do not enforce type checking of s currently, which should be of +; sort u. +(declare exists_intro (! bodyi term + (! v mpz + (! u sort + (! s term + (! body term + (! p (holds bodyi) + (! r (^ (sc_substitute body v s) bodyi) + (holds (exists v u body))))))))) + +(declare skolem_intro (! u term + (! t term + (! r (^ (sc_mk_skolem t) u) + (holds (= u t)))))) diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf index 5639cc54e..8d1793666 100644 --- a/proofs/lfsc/signatures/util_defs.plf +++ b/proofs/lfsc/signatures/util_defs.plf @@ -25,6 +25,11 @@ (declare bvn bitvec) (declare bvc (! b bit (! v bitvec bitvec))) +; Returns term t if v1 = v2, and term s otherwise. +(program mpz_ifequal ((v1 mpz) (v2 mpz) (t term) (s term)) term + (mp_ifzero (mp_add (mp_neg v1) v2) t s) +) + ;; ---- Side conditions ; Get the argument from an f-application t, fail if t is not an f-application. |