Sterling Example: unsat_proofs:drat

File: syntax.sos

[Reduce File] [Raw File]

Module unsat_proofs:drat

Builds on unsat_proofs:lrat


dratProof ::= addDratEmpty
            | addDratClause(clause, dratProof)
            | deleteDrat(clause, dratProof)

Projection dratProof :

File: check.sos

[Reduce File] [Raw File]

Module unsat_proofs:drat

Judgment checkDrat : [clause] dratProof*

drup Known emptyClause
---------------------------- [CD-Empty]
checkDrat Known addDratEmpty


drup Known C
checkDrat C::Known Rest
-------------------------------------- [CD-Add]
checkDrat Known addDratClause(C, Rest)


select C KRest Known
checkDrat KRest Rest
----------------------------------- [CD-Delete]
checkDrat Known deleteDrat(C, Rest)


              /*known clauses, clause*/
Fixed Judgment drup : [clause] clause
                   /*known clauses, assignment*/
Fixed Judgment drup_help : [clause] [lit]

gatherLits C L
negateLitList L NL
drup_help Known NL
================== [DRUP]
drup Known C



mem C Known
unsat_clause A C
==================== [DRUPH-End]
drup_help Known A


mem C Known
unit_clause A C L
drup_help Known L::A
==================== [DRUPH-Step]
drup_help Known A

File: toDrat.sos

[Reduce File] [Raw File]

Module unsat_proofs:drat

Judgment toDrat : [(int, clause)] proof* dratProof

-------------------------------------------- [TD-EmptyLrat]
toDrat Known emptyLrat(ID, Prf) addDratEmpty


remove_all Known ID KRest
toDrat (ID, C)::KRest Rest DRest
-------------------------------------------- [TD-AddLrup]
{toDrat Known addLrupProof(ID, C, Prf, Rest)
              addDratClause(C, DRest)}


select (ID, C) KRest Known
toDrat KRest Rest DRest
------------------------------------------- [TD-DeleteLrat]
{toDrat Known deleteLratProof(ID, Rest)
                      deleteDrat(C, DRest)}


Known |{proof}- P ~~> PT
toDrat Known PT D
------------------------ [TD-D]*
toDrat Known P D