Sterling Example: unsat_proofs:clauses

File: syntax.sos

[Reduce File] [Raw File] 
Module unsat_proofs:clauses

Builds on unsat_proofs:lrat

clause ::= ...
         | rangeClause(int, int)
         | noteClause(string, clause)


Low <= High
1 + Low = PlusOne
---------------------------------------------- [Proj-RangeClauseStep]
|{clause}- rangeClause(Low, High) ~~>
      or(pos(Low), rangeClause(PlusOne, High))


Low > High
------------------------------------------------- [Proj-RangeClauseEnd]
|{clause}- rangeClause(Low, High) ~~> emptyClause


---------------------------------------------- [Proj-NoteClause]
|{clause}- noteClause(Note, Clause) ~~> Clause

File: sat.sos

[Reduce File] [Raw File] 
Module unsat_proofs:clauses


Low <= X
X <= High
mem pos(X) A
----------------------------------- [SC-RangeClause]
sat_clause A rangeClause(Low, High)


sat_clause A Clause
------------------------------------- [SC-NoteClause]
sat_clause A noteClause(Note, Clause)





range Low High R
negs R N
subset N A
------------------------------------- [USC-RangeClause]
unsat_clause A rangeClause(Low, High)


unsat_clause A Clause
--------------------------------------- [USC-NoteClause]
unsat_clause A noteClause(Note, Clause)



Fixed Judgment negs : [int] [lit]

========== [Negs-Nil]
negs [] []


negs Rest LRest
=========================== [Negs-Cons]
negs I::Rest neg(I)::LRest



Fixed Judgment posLits : [int] [lit]

============= [PL-Nil]
posLits [] []


posLits Rest LRest
============================= [PL-Cons]
posLits I::Rest pos(I)::LRest

File: check.sos

[Reduce File] [Raw File] 
Module unsat_proofs:clauses


range Low High R
posLits R L
----------------------------------- [GL-RangeClause]
gatherLits rangeClause(Low, High) L


gatherLits Clause L
------------------------------------- [GL-NoteClause]
gatherLits noteClause(Note, Clause) L




range Low High Range
select I RangeRest Range
!mem pos(I) A
!mem neg(I) A
negs RangeRest N
subset N A
------------------------------------------- [UC-RangeClause]
unit_clause A rangeClause(Low, High) pos(I)


unit_clause A Clause L
---------------------------------------- [UC-NoteClause]
unit_clause A noteClause(Note, Clause) L
Back to example home