Sterling Example: unsat_proofs:frat

File: syntax.sos

[Reduce File] [Raw File]

Module unsat_proofs:frat

Builds on unsat_proofs:lrat


/*original clauses (o lines) at the start of the proof
  Note that, unlike regular FRAT, we require all o lines to be at the
  start (in full FRAT, o lines may mix with a and d lines).*/
fratProof ::= addOriginal(int, clause, fratProof)
            | endOriginal(proof)

Projection fratProof :





proof ::= ...
        /*final clauses (f lines) at the end of the proof, with and
          without hints*/
        | endFrat(int, finalClauses)
        | endFratPrf(int, [int], finalClauses)
        /*add a middle clause without a hint*/
        | addProofless(int, clause, proof)
        /*move a known clause from one ID to another
          (relocateClause(From, To, Rest)*/
        | relocateClause(int, int, proof)
        /*delete the specific clause with its ID*/
        | deleteFrat(int, clause, proof)
        /*text comment in the proof (c lines)*/
        | commentProof(string, proof)


rupProof Known emptyClause Prf
------------------------------------------------------ [Proj-EndFrat]
Known |{proof}- endFrat(ID, FC) ~~> emptyLrat(ID, Prf)


------------------------------------------- [Proj-EndFratPrf]
Known |{proof}- endFratPrf(ID, Prf, FC) ~~>
                emptyLrat(ID, Prf)


rupProof Known C Prf
---------------------------------------------- [Proj-AddProofless]
Known |{proof}- addProofless(ID, C, Rest) ~~>
                addLrupProof(ID, C, Prf, Rest)


/*
  Adds clause again, but with the new ID, then deletes the original
*/
T != F
mem (F, C) Known
---------------------------------------------- [Proj-RelocateProof]
Known |{proof}- relocateClause(F, T, Rest) ~~>
                addLrupProof(T, C, [F],
                     deleteLratProof(F, Rest))


----------------------------------------------------- [Proj-RelocateProofSame]
Known |{proof}- relocateClause(ID, ID, Rest) ~~> Rest


--------------------------------------- [Proj-DeleteFrat]
K |{proof}- deleteFrat(ID, C, Rest) ~~>
            deleteLratProof(ID, Rest)


------------------------------------------------ [Proj-CommentProof]
K |{proof}- commentProof(Comment, Rest) ~~> Rest





finalClauses ::= addFClause(int, clause, finalClauses)
               | endFClause

Projection finalClauses :

File: check.sos

[Reduce File] [Raw File]

Module unsat_proofs:frat


Fixed Judgment fratProveFormula : formula fratProof

formulaToKnown 1 F KnownClauses
checkFratProof KnownClauses [] Prf
================================== [FratProveFormula]
fratProveFormula F Prf





    /*clauses in the formula, known clauses, o lines + regular proof*/
Judgment checkFratProof : [(int, clause)] [(int, clause)] fratProof*

select (ID, C) CRest Clauses /*pull out this clause*/
checkFratProof CRest (ID, C)::Known Rest
----------------------------------------------------- [CFP-AddOriginal]
checkFratProof Clauses Known addOriginal(ID, C, Rest)


checkProof Known Prf /*transition to checking the regular proof*/
--------------------------------------------- [CFP-EndOriginal]
checkFratProof Clauses Known endOriginal(Prf)





/*Check Proof*/

remove_all Known ID KRest
rupProof Known emptyClause Prf /*creates proof itself*/
checkFinalClauses (ID, emptyClause)::KRest Final
------------------------------------------------ [CP-EndFrat]
checkProof Known endFrat(ID, Final)


remove_all Known ID KRest
rupProof Known emptyClause Prf
checkFinalClauses (ID, emptyClause)::KRest Final
------------------------------------------------ [CP-EndFratPrf]
checkProof Known endFratPrf(ID, Prf, Final)


remove_all Known ID KRest
rupProof Known C Prf
checkProof (ID, C)::KRest Rest
------------------------------------------ [CP-AddProofless]
checkProof Known addProofless(ID, C, Rest)


To != From
remove_all Known To KRest
select (From, C) KRest2 KRest
checkProof (To, C)::KRest2 Rest
----------------------------------------------- [CP-RelocateClause]
checkProof Known relocateClause(From, To, Rest)


select (ID, C) KRest Known
checkProof KRest Rest
---------------------------------------- [CP-DeleteFrat]
checkProof Known deleteFrat(ID, C, Rest)


checkProof Known Rest
-------------------------------------------- [CP-CommentProof]
checkProof Known commentProof(Comment, Rest)





Judgment checkFinalClauses : [(int, clause)] finalClauses*

select (ID, C) KRest Known
checkFinalClauses KRest Rest
----------------------------------------------- [CFC-AddFClause]
checkFinalClauses Known addFClause(ID, C, Rest)


------------------------------- [CFC-EndOriginal]
checkFinalClauses [] endFClause

File: elaboration.sos

[Reduce File] [Raw File]

Module unsat_proofs:frat

/*
  Note on elaboration:
  The second pass in FRAT elaboration is done after we have produced
  only LRAT clauses.  This part is not extensibly interesting because
  of this, so we do not define it here.
*/

/*
  In elaboration, we work backward and don't initially know if a
  clause will be necessary, so we mark it as unknown.  Once we find a
  use of it, we mark it as needed.  If it is still marked as unknown
  once we reach where it was added, we know it is not needed and can
  drop it.
*/
clauseUsedness ::= needed | unknown
Projection clauseUsedness :

                /*clauses coming down, original proof, clauses needed,
                  output proof*/
Judgment elaborate : {[(int, clause)] proof* [(int, clauseUsedness)]
                      proof}


endKnownClauses FC Needed
select (ID, needed) NRest Needed
rupProof Known emptyClause Prf
makeUsed NRest Prf Updated
---------------------------------------- [Ela-EndFrat]
{elaborate Known endFrat(ID, FC) Updated
           emptyLrat(ID, Prf)}


endKnownClauses FC Needed
select (ID, needed) NRest Needed
makeUsed NRest Prf Updated
------------------------------------------------ [Ela-EndFratPrf]
{elaborate Known endFratPrf(ID, Prf, FC) Updated
             emptyLrat(ID, Prf)}


/*Note we do not have rules for proof endings without the set of final
  clauses.  This is because we need the final clauses for the
  elaboration step to know the remaining clauses.*/


select (ID, C) KRest Known
elaborate KRest Rest Needed ERest
----------------------------------------- [Ela-DeleteFrat]
{elaborate Known deleteFrat(ID, C, Rest)
             (ID, unknown)::Needed ERest}
/*Add as unknown because this is the first time we've seen it, going
  thourgh the proof backward, so we don't know if it is used*/


select (ID, C) KRest Known
elaborate KRest Rest Needed ERest
------------------------------------------ [Ela-DeleteLratProof]
{elaborate Known deleteLratProof(ID, Rest)
           (ID, unknown)::Needed ERest}


remove_all Known ID KRest
elaborate (ID, C)::KRest Rest Needed ERest
select (ID, needed) NRest Needed
makeUsed NRest Prf Updated
--------------------------------------------- [Ela-AddLrupProofNeeded]
{elaborate Known
     addLrupProof(ID, C, Prf, Rest)
     Updated addLrupProof(ID, C, Prf, ERest)}


remove_all Known ID KRest
elaborate (ID, C)::KRest Rest Needed ERest
select (ID, unknown) NRest Needed
------------------------------------------ [Ela-AddLrupProofUnknown]
{elaborate Known
     addLrupProof(ID, C, Prf, Rest)
     NRest ERest}


remove_all Known ID KRest
elaborate (ID, C)::KRest Rest Needed ERest
select (ID, needed) NRest Needed
rupProof Known C Prf
makeUsed NRest Prf Updated
-------------------------------------------- [Ela-AddProoflessNeeded]
{elaborate Known addProofless(ID, C, Rest)
    Updated addLrupProof(ID, C, Prf, ERest)}


remove_all Known ID KRest
elaborate (ID, C)::KRest Rest Needed ERest
select (ID, unknown) NRest Needed
------------------------------------------ [Ela-AddProoflessUnknown]
{elaborate Known addProofless(ID, C, Rest)
           NRest ERest}


select (From, C) KRest Known
elaborate (To, C)::KRest Rest Needed ERest
select (To, needed) NRest Needed
----------------------------------------------- [Ela-RelocateNeeded]
{elaborate Known relocateClause(From, To, Rest)
           (From, needed)::NRest
           relocateClause(From, To, ERest)}


select (From, C) KRest Known
elaborate (To, C)::KRest Rest Needed ERest
select (To, unknown) NRest Needed
----------------------------------------------- [Ela-RelocateUnknown]
{elaborate Known relocateClause(From, To, Rest)
           (From, unknown)::NRest ERest}


elaborate Known Rest Needed ERest
-------------------------------------------------------- [Ela-Comment]
elaborate Known commentProof(Comment, Rest) Needed ERest


Known |{proof}- P ~~> PT
elaborate Known PT Needed EP
---------------------------- [Ela-D]*
elaborate Known P Needed EP





/*produce the set of clauses known at the end of the proof*/
Judgment endKnownClauses : finalClauses* [(int, clauseUsedness)]


----------------------------- [EKC-End]
endKnownClauses endFClause []


isEmpty C
endKnownClauses Rest KRest
---------------------------------------- [EKC-AddEmpty]
{endKnownClauses addFClause(ID, C, Rest)
                 (ID, needed)::KRest}


!isEmpty C
endKnownClauses Rest KRest
----------------------------------------- [EKC-AddNonEmpty]
{endKnownClauses addFClause(ID, C, Rest)
                 (ID, unknown)::KRest}





/*
  This relation permits us to have empty-ish clause constructors from
  other extensions that still work here
*/
Judgment isEmpty : clause*

------------------- [IsEmpty-EmptyClause]
isEmpty emptyClause


|{clause}- C ~~> CT
isEmpty CT
------------------- [IsEmpty-D]*
isEmpty C





/*Mark everything in the proof as needed
  {original known clauses, proof, updated clauses}*/
Fixed Judgment makeUsed : {[(int, clauseUsedness)] [int]
                           [(int, clauseUsedness)]}

======================= [MU-Nil]
makeUsed Known [] Known


select (ID, needed) KRest Known
makeUsed KRest Rest KOut
========================================== [MU-ConsNeeded]
makeUsed Known ID::Rest (ID, needed)::KOut


select (ID, unknown) KRest Known
makeUsed KRest Rest KOut
========================================== [MU-ConsUnknown]
makeUsed Known ID::Rest (ID, needed)::KOut


/*Add the delete clauses to the given proof
 {known clauses, clause ID's to delete, original proof, output proof}*/
Fixed Judgment addDeletes : [int] proof proof

================= [AD-Nil]
addDeletes [] P P


addDeletes Rest P PRest
================================================ [AD-Cons]
addDeletes ID::Rest P deleteLratProof(ID, PRest)