--- /dev/null
+; 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.
--- /dev/null
+(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))
+ ))
+ ))))))))
+ ))))
+)
; 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.
(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
(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:
;;
(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))
projects / cvc5.git / commitdiff