From: Alex Ozdemir Date: Tue, 11 Dec 2018 19:46:38 +0000 (-0800) Subject: LRAT signature (#2731) X-Git-Tag: cvc5-1.0.0~4329 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c114dc487d94d72ebf3453611c42b28777d6482;p=cvc5.git LRAT signature (#2731) * LRAT signature Added an LRAT signature. It is almost entirely side-conditions, but it works. There is also a collection of tests for it. You can run them by invoking ``` lfscc smt.plf sat.plf lrat.plf lrat_test.plf ``` * Update proofs/signatures/lrat.plf per Yoni's suggestion. Co-Authored-By: alex-ozdemir * Responding to Yoni's comments. * Removed unused varaibles Some tests declared `var`s which were unused. Now they don't. --- diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf new file mode 100644 index 000000000..f5af891bc --- /dev/null +++ b/proofs/signatures/lrat.plf @@ -0,0 +1,566 @@ +; LRAT Proof signature +; LRAT format detailed in "Efficient Certified RAT Verification" +; Author: aozdemir +; Depends On: sat.plf, smt.plf + + +; A general note about the design of the side conditions: +; Some side-conditions make use of a _global assignment_ encoded in +; 0 (true) / 1 (false) marks on variables. + +; A list of clauses, CNF if interpretted as a formula, +; but also sometimes just a list +(declare cnf type) +(declare cnfn cnf) +(declare cnfc (! h clause (! t cnf cnf))) + +; Unit (https://en.wikipedia.org/wiki/Unit_type) +; For functions that don't return anything +(declare Unit type) ; The type with only one value (like `void` in C) +(declare unit Unit) ; That value + +; Boolean operator (not short-circuiting) +(program bool_or ((l bool) (r bool)) bool (match l (ff r) (tt tt))) +(program bool_and ((l bool) (r bool)) bool (match l (tt r) (ff ff))) +(program bool_not ((b bool)) bool (match b (tt ff) (ff tt))) + +; =================== ; +; Working CNF formula ; +; =================== ; + +; Represents a CNF formula as a map from clause indices to clauses +; Should be sorted ascending, always! +; Here, and for all collections, the suffix "n" denotes the empty collection and +; the suffix "c" denotes the constructor for the collection in the style of lisp's +; "cons cells" +(declare CMap type) +(declare CMapn CMap) +(declare CMapc (! i mpz (! c clause (! r CMap CMap)))) + +; ================= ; +; LRAT Proof Format ; +; ================= ; + +; CI lists are lists of clause indices. +; They represent clauses to delete. +; They must be sorted. +(declare CIList type) +(declare CIListn CIList) +(declare CIListc (! z mpz (! zs CIList CIList))) + +; Traces are a list of clause indices into the working CNF formula +; They represent the clauses that will be unit in a unit propegation to bottom +; Thus their elements are *not* in value order. +(declare Trace type) +(declare Tracen Trace) +(declare Tracec (! z mpz (! zs Trace Trace))) + +; RAT Hint list +; Each hint is +; * An index indicating a clause in the working CNF formula to resolve with +; * A trace indicating how UP should be done after that resolution +(declare RATHints type) +(declare RATHintsn RATHints) +(declare RATHintsc + (! target mpz + (! trace Trace + (! rest RATHints + RATHints)))) + +; LRAT proof +(declare LRATProof type) +(declare LRATProofn LRATProof) +; Deletion (includes a list of clause indices to delete) +(declare LRATProofd (! cis CIList (! rest LRATProof LRATProof))) +; Addition: a clause index, a clause, RUP trace for that clause, and hints for +; what resolutions should happen then, and how those resolutions imply bottom +; via UP. +; If the list of hints is empty, then bottom is already implied. +(declare LRATProofa + (! ci mpz + (! c clause + (! t Trace + (! h RATHints + (! rest LRATProof + LRATProof)))))) + +; ========================================== ; +; Functional programs for manipulating types ; +; ========================================== ; + +; Flip the polarity of the literal +(program lit_flip ((l lit)) lit + (match l + ((pos v) (neg v)) + ((neg v) (pos v)))) + +; Are two literal equal? +(program lit_eq ((l1 lit) (l2 lit)) bool + (match l1 + ((pos v1) (match l2 + ((pos v2) (ifequal v1 v2 tt ff)) + ((neg v2) ff))) + ((neg v1) (match l2 + ((pos v2) ff) + ((neg v2) (ifequal v1 v2 tt ff)))))) + +; Remove **all** occurences of a literal from clause +(program clause_remove_all ((l lit) (c clause)) clause + (match c + (cln cln) + ((clc l' c') + (let rest_res (clause_remove_all l c') + (match (lit_eq l l') + (tt rest_res) + (ff (clc l' rest_res))))))) + +; Return the clause's first literal +; fails on an empty clause +(program clause_head ((c clause)) lit + (match c + (cln (fail lit)) + ((clc l c') l))) + +; Does a clause contain some literal? +(program clause_contains_lit ((c clause) (l lit)) bool + (match c + ((clc l' c') (match (lit_eq l l') + (tt tt) + (ff (clause_contains_lit c' l)))) + (cln ff))) + +; Append two traces +(program Trace_concat ((t1 Trace) (t2 Trace)) Trace + (match t1 + (Tracen t2) + ((Tracec h1 r1) (Tracec h1 (Trace_concat r1 t2))))) + +; Return whether a list of RAT hits is empty +(program RATHints_is_empty ((h RATHints)) bool + (match h + (RATHintsn tt) + ((RATHintsc a b c) ff))) + +; Insert into a CMap, preserving order +(program CMap_insert ((i mpz) (c clause) (cs CMap)) CMap + (match cs + (CMapn (CMapc i c CMapn)) + ((CMapc i' c' r) + (mp_ifneg (mpz_sub i i') + (CMapc i c cs) + (CMapc i' c' (CMap_insert i c r)))))) + +; Get from a CMap +(program CMap_get ((i mpz) (cs CMap)) clause + (match cs + (CMapn (fail clause)) + ((CMapc i' c r) + (mp_ifzero (mpz_sub i i') + c + (CMap_get i r))))) + +; Remove from CMap. Only removes one element. +(program CMap_remove ((i mpz) (cs CMap)) CMap + (match cs + (CMapn CMapn) + ((CMapc i' c r) + (mp_ifzero (mpz_sub i i') + r + (CMapc i' c (CMap_remove i r)))))) + +; Remove many indices from a CMap. Asuumes the input list is sorted. +(program CMap_remove_many ((is CIList) (cs CMap)) CMap + (match + is + (CIListn cs) + ((CIListc i is') + (match + cs + (CMapn (fail CMap)) ; All deletion indices must be valid! + ((CMapc ci c cs') + (mp_ifzero (mpz_sub i ci) + (CMap_remove_many is' cs') + (CMapc ci c (CMap_remove_many is cs')))))))) + +; Given a map of clauses and a literal, return all indices in the map +; corresponsing to clauses that could resolve against that literal. i.e. for x, +; return the indices of all clauses containing x. +(program collect_resolution_targets_w_lit ((cs CMap) (l lit)) CIList + (match cs + (CMapn CIListn) + ((CMapc i c cs') + (let rest_solution (collect_resolution_targets_w_lit cs' l) + (match (clause_contains_lit c l) + (tt (CIListc i rest_solution)) + (ff rest_solution)))))) + +; Given a clause and a maps of clauses, return all indices in the map +; corresponding to clauses which could resolve with this one on its first +; literal +(program collect_resolution_targets ((cs CMap) (c clause)) CIList + (collect_resolution_targets_w_lit cs (lit_flip (clause_head c)))) + +; Is this clause a tautology? +; Internally uses mark 5 to flag variables that occur (+) +; and mark 6 to flag variables that occur (-) +(program is_t ((c clause)) bool + (match + c + (cln ff) + ((clc l c') (match + l + ((pos v) + (ifmarked5 + v + (is_t c') + (ifmarked6 + v + tt + (do + (markvar5 v) + (let r (is_t c') (do (markvar5 v) r)))))) + ((neg v) + (ifmarked6 + v + (is_t c') + (ifmarked5 + v + tt + (do + (markvar6 v) + (let r (is_t c') (do (markvar6 v) r)))))))))) + +; ===================================================================== ; +; Programs for manipulating and querying the global variable assignment ; +; ===================================================================== ; + +; This assignment marks values of type `var`. +; It marks a variable with 1 if that variable is true +; It marks a variable with 2 if that variable is false +; A variable should not be marked with both! +; A variable may be marked with neither, indicating that variable is presently +; unassigned, which we call "floating". + +; Mark the variable within to satisfy this literal. +; fails if the literal is already UNSAT +(program lit_mk_sat ((l lit)) Unit + (match l + ((pos v) (ifmarked2 v + (fail Unit) + (ifmarked1 v unit (do (markvar1 v) unit)))) + ((neg v) (ifmarked1 v + (fail Unit) + (ifmarked2 v unit (do (markvar2 v) unit)))))) + +; Mark the variable within to falsify this literal. +; fails is the literal is already SAT +(program lit_mk_unsat ((l lit)) Unit + (match l + ((neg v) (ifmarked2 v + (fail Unit) + (ifmarked1 v unit (do (markvar1 v) unit)))) + ((pos v) (ifmarked1 v + (fail Unit) + (ifmarked2 v unit (do (markvar2 v) unit)))))) + +; Unmarks the variable within a satified literal to render it neither satified nor falsified +; fails if the literal is not already satisfied +(program lit_un_mk_sat ((l lit)) Unit + (match l + ((pos v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit))) + ((neg v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit))))) + +; Unmarks the variable within a falsified literal to render it neither satified nor falsified +; fails if the literal is not already falsified +(program lit_un_mk_unsat ((l lit)) Unit + (match l + ((pos v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit))) + ((neg v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit))))) + +; Is a literal presently satisfied? +(program lit_is_sat ((l lit)) bool + (match l + ((pos v) (ifmarked1 v tt ff)) + ((neg v) (ifmarked2 v tt ff)))) + +; Is a literal presently falsified? +(program lit_is_unsat ((l lit)) bool + (match l + ((pos v) (ifmarked2 v tt ff)) + ((neg v) (ifmarked1 v tt ff)))) + +; Is a literal presently neither satisfied nor falsified? +(program lit_is_floating ((l lit)) bool + (bool_not (bool_or (lit_is_sat l) (lit_is_unsat l)))) + +; Does this clause contain a floating literal? +(program clause_has_floating ((c clause)) bool + (match c + (cln ff) + ((clc l c') (match (lit_is_floating l) + (tt tt) + (ff (clause_has_floating c')))))) + +; Is this clause falsified? i.e. are all its clauses falsified? +(program clause_is_unsat ((c clause)) bool + (match c + (cln tt) + ((clc l c') (match (lit_is_unsat l) + (tt (clause_is_unsat c')) + (ff ff))))) + +; Is this clause presently satisfied? +(program clause_is_sat ((c clause)) bool + (match c + (cln ff) + ((clc l c') (match (lit_is_sat l) + (tt tt) + (ff (clause_is_sat c')))))) + +; Falsify **all** contained literals. +; Fails on a tautological clause +(program clause_mk_all_unsat ((c clause)) Unit + (match c + (cln unit) + ((clc l c') (do + (lit_mk_unsat l) + (clause_mk_all_unsat c'))))) + +; Unfalsifies **all** contained literals +; Fails on a clause with duplicate literals +(program clause_un_mk_all_unsat ((c clause)) Unit + (match c + (cln unit) + ((clc l c') (do + (lit_un_mk_unsat l) + (clause_un_mk_all_unsat c'))))) + +; Get the first floating literal out of this clause. +; fails if there are no floating literals +(program clause_first_floating ((c clause)) lit + (match c + (cln (fail lit)) + ((clc l c') (match (lit_is_floating l) + (tt l) + (ff (clause_first_floating c')))))) + +; ===================================== ; +; High-Level Programs for LRAT Checking ; +; ===================================== ; + +; The return type for verifying that a clause is unit and modifying the global +; assignment to satisfy it +(declare MarkResult type) +; The clause is unit, and this is the (previoiusly floating) literal that is now satified. +(declare MRUnit (! l lit MarkResult)) +; The clause was unsat! +(declare MRUnsat MarkResult) +; The clauss was already satisfied. +(declare MRSat MarkResult) +; The clause had multiple floating literals. +(declare MRNotUnit MarkResult) + +; Determine wether this clause is sat, unsat, unit, or not unit, and if it is +; unit, it modifies the global assignment to satisfy the clause, and returns +; the literal that was made SAT by the new mark. +; +; Fails if `c` is a TAUT +(program clause_check_unit_and_maybe_mark ((c clause)) MarkResult + (match (clause_is_sat c) + (tt MRSat) + (ff (match (clause_is_unsat c) + (tt MRUnsat) + (ff (match (is_t c) + (tt (fail MarkResult)) + (ff ; Dedent + (match (clause_has_floating c) + (tt (let first (clause_first_floating c) + (do (lit_mk_sat first) + (match (clause_has_floating c) + (tt (do (lit_un_mk_sat first) MRNotUnit)) + (ff (MRUnit first)))))) + ; Unreachable. If clause is not floating it must have been SAT or UNSAT. + (ff (fail MarkResult)) + )))))))) + +; The return type for the process of Trace-guided unit propegation +(declare UPResult type) +; The trace guided unit propegation correctly, but that unit propegation did not end in an empty clause +(declare UPR_Ok UPResult) +; The trace guided unit propegation correctly to an empty clause +(declare UPR_Bottom UPResult) +; The trace was malformed, +;; i.e. at some point indicates that a non-unit, non-empty clause should be examined +(declare UPR_Broken UPResult) + +; Execute the unit propegation indicated by the trace. Report whether that +; unit propegation succeeds and produces bottom, fails, or succeeds but does +; not produce bottom. +; +; If the trace tries to propegate through a TAUT clause, fails. +(program do_up ((cs CMap) (t Trace)) UPResult + (match + t + (Tracen UPR_Ok) + ((Tracec i r) (match (clause_check_unit_and_maybe_mark (CMap_get i cs)) + ((MRUnit l) + (let res (do_up cs r) + (do (lit_un_mk_sat l) res))) + (MRUnsat UPR_Bottom) + (MRSat UPR_Broken) + (MRNotUnit UPR_Broken))))) + + +; Determine whether a list of indices agrees with the list of indices latent in +; a list of hints. Both lists should be sorted. +(program resolution_targets_match ( + (computed CIList) + (given RATHints)) bool + (match given + (RATHintsn + (match computed + (CIListn tt) + ((CIListc a b) ff))) + ((RATHintsc hint_idx t given') + (match computed + ((CIListc comp_idx computed') + (mp_ifzero (mpz_sub hint_idx comp_idx) + (resolution_targets_match computed' given') + (ff))) + (CIListn ff))))) + + +; Determines whether `t` is a witness that `c` is an Assymetric Tautology in `cs`. +; +; Does unit propegation in the formula `cs`, beginning by falsifying +; all literals in `c`, and then looking at the clauses indicated by `t`. +; Assumes no marks, and cleans up marks afterwards. +; +; Fails if `c` has duplicates +(program is_at_trace ((cs CMap) (c clause) (t Trace)) UPResult + (match (is_t c) + (ff + (do + (clause_mk_all_unsat c) + (let result (do_up cs t) + (do (clause_un_mk_all_unsat c) result)))) + (tt + UPR_Bottom))) + + + +; List of (clause, trace) pairs +(declare CTPairs type) +(declare CTPn CTPairs) +(declare CTPc (! c clause (! t Trace (! rest CTPairs CTPairs)))) + +; For each RAT hint, construct the pseudo-resolvant for that hint, and the net +; trace for that hint. Return a list of these. +; +; Pseudo resolvant: if l v C is the clause, and D is another clause containing +; ~l, then l v C v (D \ ~l) is the pseudo-resolvant, which is the actual +; resolant, plut l, which would be implied by UP. +; +; The net trace is the global trace (`t`), plut the trace for that specific +; resolvant. +(program construct_ct_pairs ( + (cs CMap) + (c clause) + (t Trace) + (hints RATHints) + ) CTPairs + (match hints + (RATHintsn CTPn) + ((RATHintsc i ht hints') + (CTPc + (clause_append c + (clause_remove_all (lit_flip (clause_head c)) + (CMap_get i cs))) + (Trace_concat t ht) + (construct_ct_pairs cs c t hints'))))) + +; Goes through a list of clause, trace pairs and verifies that each clause is +; an AT via that trace. +; Fails if any putative AT is a TAUT or contains duplicates +(program are_all_at ( + (cs CMap) + (l CTPairs) + ) UPResult + (match l + (CTPn UPR_Bottom) + ((CTPc c t l') + (match (is_at_trace cs c t) + (UPR_Ok UPR_Ok) + (UPR_Broken UPR_Broken) + (UPR_Bottom (are_all_at cs l')))))) + +; Is this trace, and list of hints, proof that `c` is an Resolution Assymeytic +; Tautology? +; Fails is the hints are empty (i.e. `c` should be AT, and c is TAUT or contains duplicates) +; Also fails if any of the pseudo-resolvants are TAUT or contain duplicates. +(program is_rat_trace ((cs CMap) (c clause) (t Trace) (hints RATHints)) UPResult + (match + (RATHints_is_empty hints) + (tt ; Empty RAT hints -- the clause must be AT + (is_at_trace cs c t)) + (ff ; Ew -- we must verify this is a RAT + (match (resolution_targets_match + (collect_resolution_targets cs c) + hints) + (ff ; Res targets are bad + UPR_Broken) + (tt + (are_all_at cs (construct_ct_pairs cs c t hints))))))) + +; Is this proof an LRAT proof of bottom? +; Fails if any added AT is a TAUT or contains duplicates OR if any added RAT +; produces pseudo-resolvants which are TAUT or contain duplicates +(program is_lrat_proof_of_bottom ((f CMap) (proof LRATProof)) bool + (match proof + ((LRATProofd indices rest) + (is_lrat_proof_of_bottom + (CMap_remove_many indices f) + rest)) + ((LRATProofa idx c trace hints rest) + (match (is_rat_trace f c trace hints) + (UPR_Bottom + (match + c + (cln tt) + ((clc a b) + (is_lrat_proof_of_bottom (CMap_insert idx c f) rest)))) + (UPR_Ok ff) + (UPR_Broken ff))) + (LRATProofn ff)) + ) + +; Proof of a CMap from clause proofs. +; The idx is unelidable b/c it is unspecified. +(declare CMap_holds (! c CMap type)) +(declare CMapn_proof (CMap_holds CMapn)) +(declare CMapc_proof + (! idx mpz ; Not elidable! + (! c clause + (! rest CMap + (! proof_c (holds c) + ( ! proof_rest (CMap_holds rest) + (CMap_holds (CMapc idx c rest)))))))) + +(define bottom (holds cln)) +(declare lrat_proof_of_bottom + (! cm CMap + (! proof_cm (CMap_holds cm) + (! proof LRATProof + (! sc (^ (is_lrat_proof_of_bottom cm proof) tt) + bottom))))) + + +; TODO(aozdemir) Reducing the amount of checking that resides in side-conditions. +; Steps +; 1. Unroll the traversal of is_lrat_proof_of_bottom into a serialized +; sequence of axiom applications. +; The axioms would likely correspond to DELETE, IS T, IS AT, IS RAT. +; They would manipulate a CMap by way of side-conditions. +; 2. Unroll AT checks by manifesting the assignment in data rather than marks, +; and having axioms like IS_UNSAT, IS_UNIT_ON_LITERAL. +; 3. Unroll RAT checks in a similar fashion, although more painfully. diff --git a/proofs/signatures/lrat_test.plf b/proofs/signatures/lrat_test.plf new file mode 100644 index 000000000..3ba785507 --- /dev/null +++ b/proofs/signatures/lrat_test.plf @@ -0,0 +1,786 @@ +(declare test_clause_append + (! c1 clause + (! c2 clause + (! cr clause + (! sc (^ (clause_append c1 c2) cr) type))))) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (test_clause_append + (clc (pos v1) (clc (neg v2) cln)) + (clc (pos v3) (clc (neg v2) cln)) + (clc (pos v1) (clc (neg v2) (clc (pos v3) (clc (neg v2) cln)))) + ) + ))) +) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v2 var + (% v3 var + (test_clause_append + cln + (clc (pos v3) (clc (neg v2) cln)) + (clc (pos v3) (clc (neg v2) cln)) + ) + )) +) + +; Test passes if the (test_clause_append ...) application is well-typed. +(check + (% v2 var + (% v3 var + (test_clause_append + (clc (pos v3) (clc (neg v2) cln)) + cln + (clc (pos v3) (clc (neg v2) cln)) + ) + )) +) + +(declare test_CMap_remove_many + (! is CIList + (! cs CMap + (! csr CMap + (! sc (^ (CMap_remove_many is cs) csr) type))))) + +; Test passes if the (test_CMap_remove_many ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ cs_out (CMapc 3 c2 (CMapc 5 c3 CMapn)) + (@ is_in (CIListc 0 (CIListc 4 (CIListc 6 CIListn))) + (test_CMap_remove_many + is_in + cs_in + cs_out + ) + ))) + )))) + )))) +) + +; Test passes if the (test_CMap_remove_many ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ cs_out (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ is_in (CIListc 4 CIListn) + (test_CMap_remove_many + is_in + cs_in + cs_out + ) + ))) + )))) + )))) +) + +(declare test_clause_remove_all + (! l lit + (! c clause + (! c' clause + (! sc (^ (clause_remove_all l c) c') type))))) + +; Test passes if the (test_clause_remove_all ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v4) (clc (neg v2) (clc (neg v2) (clc (pos v2) (clc (pos v1) cln))))) + (@ c2 (clc (pos v4) (clc (pos v2) (clc (pos v1) cln))) + (test_clause_remove_all + (neg v2) + c1 + c2 + ) + )) + )))) +) + +(declare test_collect_resolution_targets + (! cs CMap + (! c clause + (! is CIList + (! sc (^ (collect_resolution_targets cs c) is) type))))) + +; Test passes if the (test_collect_resolution_targets ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v3) cln)) + (@ c4 (clc (neg v3) (clc (pos v3) cln)) + (@ ct (clc (neg v3) (clc (neg v4) cln)) + (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) + (@ is_out (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) + (test_collect_resolution_targets + cs_in + ct + is_out + ) + ))) + )))) + )))) +) + +(declare test_resolution_targets_match + (! c CIList + (! g RATHints + (! ans bool + (! sc (^ (resolution_targets_match c g) ans) type))))) + +; Test passes if the (test_resolution_targets_match ...) application is well-typed. +(check + (@ idxs_in (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) + (@ hints_in + (RATHintsc 0 Tracen + (RATHintsc 4 Tracen + (RATHintsc 5 Tracen + (RATHintsc 6 Tracen + RATHintsn)))) + (test_resolution_targets_match + idxs_in + hints_in + tt + ) + )) +) + +; Test passes if the (test_resolution_targets_match ...) application is well-typed. +(check + (@ idxs_in (CIListc 0 (CIListc 2 (CIListc 5 (CIListc 6 CIListn)))) + (@ hints_in + (RATHintsc 0 Tracen + (RATHintsc 4 Tracen + (RATHintsc 5 Tracen + (RATHintsc 6 Tracen + RATHintsn)))) + (test_resolution_targets_match + idxs_in + hints_in + ff + ) + )) +) + +(declare test_is_at_trace + (! cs CMap + (! c clause + (! t Trace + (! r UPResult + (! sc (^ (is_at_trace cs c t) r) type)))))) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 3 (Tracec 5 (Tracec 6 Tracen))) + (test_is_at_trace + cs + c + t + UPR_Bottom + ) + ))) + )))) + )))) +) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 3 (Tracec 5 Tracen)) + (test_is_at_trace + cs + c + t + UPR_Ok + ) + ))) + )))) + )))) +) + +; Test passes if the (test_is_at_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v3) (clc (neg v2) cln)) + (@ c2 (clc (neg v3) (clc (neg v1) cln)) + (@ c3 (clc (neg v2) (clc (pos v1) cln)) + (@ c4 (clc (neg v3) (clc (pos v2) cln)) + (@ cs (CMapc 1 c1 (CMapc 2 c2 (CMapc 3 c3 (CMapc 4 c4 CMapn)))) + (@ c (clc (neg v3) cln) + (@ t (Tracec 2 (Tracec 1 Tracen)) + (test_is_at_trace + cs + c + t + UPR_Broken + ) + ))) + )))) + )))) +) + +(declare test_is_rat_trace (! cs CMap + (! c clause + (! t Trace + (! h RATHints + (! r UPResult + (! sc (^ (is_rat_trace cs c t h) r) type))))))) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + RATHintsn)) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 3 (Tracec 1 Tracen)) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 CMapn)))))))) + (@ c (clc (pos v1) cln) + (@ t Tracen + (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 3 Tracen) + RATHintsn))) + (test_is_rat_trace + cs + c + t + h + UPR_Broken + ) + )))) + )))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ c9 (clc (pos v1) cln) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + (CMapc 9 c9 + CMapn))))))))) + (@ c (clc (pos v2) cln) + (@ t (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + (@ h RATHintsn + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + ))))))))) + )))) +) + +; Test passes if the (test_is_rat_trace ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ c9 (clc (pos v1) cln) + (@ c10 (clc (pos v2) cln) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + (CMapc 9 c9 + (CMapc 10 c10 + CMapn)))))))))) + (@ c cln + (@ t (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + (@ h RATHintsn + (test_is_rat_trace + cs + c + t + h + UPR_Bottom + ) + )))) + )))))))))) + )))) +) + +(declare test_is_lrat_proof_of_bottom + (! f CMap + (! p LRATProof + (! r bool + (! sc (^ (is_lrat_proof_of_bottom f p) r) type))))) + +; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + CMapn)))))))) + (@ p + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (test_is_lrat_proof_of_bottom + cs + p + tt + ) + )) + )))))))) + )))) +) + +; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (@ cs (CMapc 1 c1 + (CMapc 2 c2 + (CMapc 3 c3 + (CMapc 4 c4 + (CMapc 5 c5 + (CMapc 6 c6 + (CMapc 7 c7 + (CMapc 8 c8 + CMapn)))))))) + (@ p + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 Tracen)))) + RATHintsn + LRATProofn))))) + (test_is_lrat_proof_of_bottom + cs + p + ff + ) + )) + )))))))) + )))) +) + +; Proof from Figure 2 of "Efficient Certified RAT Verification" +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ pf_c1 + (CMapc_proof 2 _ _ pf_c2 + (CMapc_proof 3 _ _ pf_c3 + (CMapc_proof 4 _ _ pf_c4 + (CMapc_proof 5 _ _ pf_c5 + (CMapc_proof 6 _ _ pf_c6 + (CMapc_proof 7 _ _ pf_c7 + (CMapc_proof 8 _ _ pf_c8 + CMapn_proof)))))))) + (@ lrat_proof_witness + (LRATProofa 9 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) + (LRATProofa 10 + (clc (pos v2) cln) + (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 11 + cln + (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + )))))))) + )))) +) + +; Clauses 1 and 9 are identical. +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ pf_c1 + (CMapc_proof 2 _ _ pf_c2 + (CMapc_proof 3 _ _ pf_c3 + (CMapc_proof 4 _ _ pf_c4 + (CMapc_proof 5 _ _ pf_c5 + (CMapc_proof 6 _ _ pf_c6 + (CMapc_proof 7 _ _ pf_c7 + (CMapc_proof 8 _ _ pf_c8 + (CMapc_proof 9 _ _ pf_c9 + CMapn_proof))))))))) + (@ lrat_proof_witness + (LRATProofa 10 + (clc (pos v1) cln) + Tracen + (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) + (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) + (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) + RATHintsn))) + (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) + (LRATProofa 11 + (clc (pos v2) cln) + (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 12 + cln + (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + ))))))))) + )))) +) + +; Proof from Figure 1 of "Efficient Certified RAT Verification" +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (@ pf_cmap + (CMapc_proof 1 _ _ pf_c1 + (CMapc_proof 2 _ _ pf_c2 + (CMapc_proof 3 _ _ pf_c3 + (CMapc_proof 4 _ _ pf_c4 + (CMapc_proof 5 _ _ pf_c5 + (CMapc_proof 6 _ _ pf_c6 + (CMapc_proof 7 _ _ pf_c7 + (CMapc_proof 8 _ _ pf_c8 + CMapn_proof)))))))) + (@ lrat_proof_witness + (LRATProofa 9 + (clc (pos v1) (clc (pos v2) cln)) + (Tracec 1 (Tracec 6 (Tracec 3 Tracen))) + RATHintsn + (LRATProofd (CIListc 1 CIListn) + (LRATProofa 10 + (clc (pos v1) (clc (pos v3) cln)) + (Tracec 9 (Tracec 8 (Tracec 6 Tracen))) + RATHintsn + (LRATProofd (CIListc 6 CIListn) + (LRATProofa 11 + (clc (pos v1) cln) + (Tracec 10 (Tracec 9 (Tracec 4 (Tracec 8 Tracen)))) + RATHintsn + (LRATProofd (CIListc 8 (CIListc 9 (CIListc 10 CIListn))) + (LRATProofa 12 + (clc (pos v2) cln) + (Tracec 11 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) + RATHintsn + (LRATProofd (CIListc 3 (CIListc 7 CIListn)) + (LRATProofa 13 + cln + (Tracec 11 (Tracec 12 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) + RATHintsn + LRATProofn + ))))))))) + (: + (holds cln) + (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) + )) + )))))))) + )))) +) diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index b95caa8fd..8f40aa8bf 100644 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -19,8 +19,8 @@ ; code to check resolutions -(program append ((c1 clause) (c2 clause)) clause - (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2))))) +(program clause_append ((c1 clause) (c2 clause)) clause + (match c1 (cln c2) ((clc l c1') (clc l (clause_append c1' c2))))) ; we use marks as follows: ; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. @@ -49,7 +49,7 @@ (match m (tt (do (ifmarked4 v v (markvar4 v)) c')) (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) - ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2))) ((clr l c1) (match l ; set mark 1 to indicate we should remove v, and fail if diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 06dc16153..57dc5bd1e 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -439,6 +439,22 @@ (holds C)) (holds (clc (neg v) C)))))))))) +;; Numeric primitives + +(program mpz_sub ((x mpz) (y mpz)) mpz + (mp_add x (mp_mul (~1) y))) + +(program mp_ispos ((x mpz)) formula + (mp_ifneg x false true)) + +(program mpz_eq ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + +(program mpz_lt ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true false)) + +(program mpz_lte ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) ;; Example: ;; diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 6012e052a..934951a86 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -3,20 +3,6 @@ (declare trust-bad (th_holds false)) ; helper stuff -(program mpz_sub ((x mpz) (y mpz)) mpz - (mp_add x (mp_mul (~1) y))) - -(program mp_ispos ((x mpz)) formula - (mp_ifneg x false true)) - -(program mpz_eq ((x mpz) (y mpz)) formula - (mp_ifzero (mpz_sub x y) true false)) - -(program mpz_lt ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true false)) - -(program mpz_lte ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) (program mpz_ ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false))