Extensibella: Extensibella Example: unsat

Extensibella Example: unsat_proofs:frat

Language Specification

File: syntax.sos

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 :





/*Replace the first ID with the second one, yielding the last proof
  Has known clauses for translation*/
Judgment replaceID : [(int, clause)] int int proof* proof
/*Replace the first ID with the second one in the proof*/
Fixed Judgment replaceIDProof : int int [int] [int]


replaceIDProof From To Prf NewPrf
----------------------------------------------- [RID-EmptyLrat]
{replaceID Known From To emptyLrat(ID, Prf)
                         emptyLrat(ID, NewPrf)}


replaceIDProof From To Prf NewPrf
replaceID Known From To Rest NewRest
------------------------------------------------------- [RID-AddLrup]
{replaceID Known From To addLrupProof(ID, C, Prf, Rest)
              addLrupProof(ID, C, NewPrf, NewRest)}


ID != From
replaceID Known From To Rest NewRest
-------------------------------------------------- [RID-DeleteOther]
{replaceID Known From To deleteLratProof(ID, Rest)
              deleteLratProof(ID, NewRest)}


replaceID Known From To Rest NewRest
---------------------------------------------------- [RID-DeleteFrom]
{replaceID Known From To deleteLratProof(From, Rest)
              deleteLratProof(To, NewRest)}


Known |{proof}- P ~~> PT
replaceID Known From To PT NewP
------------------------------- [RID-Default]*
replaceID Known From To P NewP



============================ [RIDP-Nil]
replaceIDProof From To [] []


replaceIDProof From To Rest NewRest
============================================= [RIDP-ConsReplace]
replaceIDProof From To From::Rest To::NewRest


From != ID
replaceIDProof From To Rest NewRest
=========================================== [RIDP-ConsDiff]
replaceIDProof From To ID::Rest ID::NewRest

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)


/*need a second rule to show Ext_Ind*/
mem (ID, C) Known
checkProof Known Rest
--------------------------------------------- [CP-RelocateClauseSame]
checkProof Known relocateClause(ID, ID, 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 :


Fixed Judgment fullElaborate : formula proof proof

formulaToKnown 1 F Known
elaborate Known P Needed E
========================== [FullElaborate]
fullElaborate F P E

Fixed Judgment fullElaborateFrat : formula fratProof fratProof

formulaToKnown 1 F Known
elaborateFratProof Known [] P Needed E
====================================== [FullElaborateFrat]
fullElaborateFrat F P E


Judgment elaborateFratProof : {
             [(int, clause)] [(int, clause)] fratProof*
             [(int, clauseUsedness)] fratProof}


select (ID, C) CRest Clauses /*pull out this clause*/
elaborateFratProof CRest (ID, C)::Known Rest Needed E
select (ID, needed) NRest Needed
----------------------------------------------------- [EFP-AddNeeded]
{elaborateFratProof Clauses Known
                    addOriginal(ID, C, Rest) NRest
                    addOriginal(ID, C, E)}


select (ID, C) CRest Clauses /*pull out this clause*/
elaborateFratProof CRest (ID, C)::Known Rest Needed E
select (ID, unknown) NRest Needed
----------------------------------------------------- [EFP-AddUnknown]
{elaborateFratProof Clauses Known
                    addOriginal(ID, C, Rest) NRest E}


elaborate Known P Needed E
------------------------------------------------------- [EFP-End]
{elaborateFratProof Clauses Known endOriginal(P) Needed
                    endOriginal(E)}


                /*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}


/*remove_all then select inherently gives To != From*/
remove_all Known To KRest
select (From, C) KRest2 KRest
{elaborate (To, C)::KRest2 Rest
           Needed ERest}
select (To, needed) NRest Needed
------------------------------------ [Ela-RelocateNeeded-Diff]
{elaborate Known
    relocateClause(From, To, Rest)
    (From, needed)::NRest
    relocateClause(From, To, ERest)}


elaborate Known Rest Needed ERest
--------------------------------- [Ela-RelocateNeeded-Same]
{elaborate Known
    relocateClause(ID, ID, Rest)
    Needed ERest}


remove_all Known To KRest
select (From, C) KRest2 KRest
elaborate (To, C)::KRest2 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-Default]*
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-Default]*
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)

Extensibella Example: unsat_proofs:frat

Language Specification

File: syntax.sos

File: check.sos

File: elaboration.sos

Reasoning