21 lines
832 B
Diff
21 lines
832 B
Diff
--- proofs/signatures/drat.plf.orig 2019-04-09 10:14:31.000000000 -0600
|
|
+++ proofs/signatures/drat.plf 2019-09-09 17:42:41.118932870 -0600
|
|
@@ -322,7 +322,7 @@
|
|
|
|
|
|
; Do unit propagation on `f`, constructing a UP model for it.
|
|
-(program build_up_model ((f cnf)) clause
|
|
+(program build_up_model ((f cnf)) UPConstructionResult
|
|
(match (unit_search f)
|
|
(USRBottom UPCRBottom)
|
|
(USRNoUnit (UPCRModel cln))
|
|
@@ -335,7 +335,7 @@
|
|
|
|
; Given some starting assignment (`up_model`), continue UP to construct a larger
|
|
; model.
|
|
-(program extend_up_model ((f cnf) (up_model clause)) clause
|
|
+(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult
|
|
(do (clause_into_global up_model)
|
|
(let result (build_up_model f)
|
|
(do (clause_undo_into_global up_model)
|