diff options
-rw-r--r-- | proofs/signatures/drat.plf | 145 | ||||
-rw-r--r-- | proofs/signatures/drat_test.plf | 152 |
2 files changed, 293 insertions, 4 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index d777a143a..d0f647452 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -229,21 +229,158 @@ (collect_pseudo_resolvents cs c))))))) ; Is this proof a valid DRAT proof of bottom? -(program is_drat_proof_of_bottom ((f cnf) (proof DRATProof)) bool +(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool (match proof (DRATProofn (cnf_has_bottom f)) ((DRATProofa c p) (match (is_rat f c) - (tt (is_drat_proof_of_bottom (cnfc c f) p)) + (tt (is_specified_drat_proof (cnfc c f) p)) (ff ff))) ((DRATProofd c p) - (is_drat_proof_of_bottom (cnf_remove_clause c f) p)))) + (is_specified_drat_proof (cnf_remove_clause c f) p)))) +; =============================== ; +; Operational DRAT implementation ; +; =============================== ; + +; Operation DRAT is defined in the paper "Two Flavors of DRAT". +; Below is an extension of the DRAT signature to handle it. + +; Notes on types. +; For operational DRAT it is useful to manifest partial assignments in values +; (although we still use the global assignment in some places). To this end, +; literals are used to represent single-variable assignments ((pos v) denotes +; {v maps to true}) and clauses are partial assignments by way of being +; literal lists. + +; Copy the partial assignment represented by a clause into the global +; assignment. Fails if that clause represents an inconsistent partial +; assignment (e.g. v is both true and false) +(program clause_into_global ((a clause)) Unit + (match a + (cln unit) + ((clc l rest) + (do (lit_mk_sat l) (clause_into_global rest))))) + +; Remove the partial assignment represented by c from the global assignment +(program clause_undo_into_global ((a clause)) Unit + (match a + (cln unit) + ((clc l rest) + (do (lit_un_mk_sat l) (clause_undo_into_global rest))))) + +; Does this clause have no floating literals w.r.t. the global assignment? +(program clause_no_floating ((c clause)) bool + (match c + (cln tt) + ((clc l rest) (match (lit_is_floating l) + (tt ff) + (ff (clause_no_floating rest)))))) + +; Does this clause have no sat literals w.r.t. the global assignment? +(program clause_no_sat ((c clause)) bool + (match c + (cln tt) + ((clc l rest) (match (lit_is_sat l) + (tt ff) + (ff (clause_no_sat rest)))))) + +; Does this clause have one sat literal w.r.t. the global assignment? +(program clause_one_sat ((c clause)) bool + (match c + (cln ff) + ((clc l rest) (match (lit_is_sat l) + (tt (clause_no_sat rest)) + (ff (clause_one_sat rest)))))) + +; Is this clause a unit clause w.r.t. the global assignment? +; This notion is defined as: +; * A clause where no literals are floating, and exactly one is sat. +(program clause_is_unit_wrt_up_model ((c clause) (up_model clause)) bool + (let c' (clause_dedup c) + (do (clause_into_global up_model) + (let result (match (clause_no_floating c') + (tt (clause_one_sat c')) + (ff ff)) + (do (clause_undo_into_global up_model) + result))))) + +; Result from constructing a UP model (defined in "Two Flavors of DRAT") +; Technically, we're constructing the shared UP model -- the intersection of all +; UP models. +; Informally, this is just the partial assignment implied by UP. +; +; This type is necessary, because constructing a UP model can reveal an +; inconsistent UP model -- one which assigns some variable to true and false. +; This would break our machinery, so we special case it. +(declare UPConstructionResult type) +; An actual model +(declare UPCRModel (! up_model clause UPConstructionResult)) +; Bottom is implied! +(declare UPCRBottom UPConstructionResult) + + +; Do unit propagation on `f`, constructing a UP model for it. +(program build_up_model ((f cnf)) clause + (match (unit_search f) + (USRBottom UPCRBottom) + (USRNoUnit (UPCRModel cln)) + ((USRUnit l f') + (let result (build_up_model f') + (do (lit_un_mk_sat l) + (match result + (UPCRBottom UPCRBottom) + ((UPCRModel model) (UPCRModel (clc l model))))))))) + +; Given some starting assignment (`up_model`), continue UP to construct a larger +; model. +(program extend_up_model ((f cnf) (up_model clause)) clause + (do (clause_into_global up_model) + (let result (build_up_model f) + (do (clause_undo_into_global up_model) + (match result + (UPCRBottom UPCRBottom) + ((UPCRModel up_model') + (UPCRModel (clause_append up_model up_model')))))))) + +; Helper for `is_operational_drat_proof` which takes a UP model for the working +; formula. The UP model is important for determining which clause deletions +; actually are executed in operational DRAT. Passing the UP model along +; prevents it from being fully recomputed everytime. +(program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool + (match pf + (DRATProofn (cnf_has_bottom f)) + ((DRATProofd c pf') + (match (clause_is_unit_wrt_up_model c up_model) + (tt (is_operational_drat_proof_h f up_model pf')) + (ff (is_operational_drat_proof_h + (cnf_remove_clause c f) up_model pf')))) + ((DRATProofa c pf') + (let f' (cnfc c f) + (match (is_rat f c) + (tt (match (extend_up_model f' up_model) + (UPCRBottom tt) + ((UPCRModel up_model') + (is_operational_drat_proof_h f' up_model' pf')))) + (ff ff)))))) + +; Is this an operational DRAT proof of bottom for this formula? +(program is_operational_drat_proof ((f cnf) (pf DRATProof)) bool + (match (build_up_model f) + (UPCRBottom tt) + ((UPCRModel model) (is_operational_drat_proof_h f model pf)))) + +; Is this a specified or operational DRAT proof of bottom for this formula? +(program is_drat_proof ((f cnf) (pf DRATProof)) bool + (match (is_specified_drat_proof f pf) + (tt tt) + (ff (is_operational_drat_proof f pf)))) + (declare drat_proof_of_bottom (! f cnf (! proof_of_formula (cnf_holds f) (! proof DRATProof - (! sc (^ (is_drat_proof_of_bottom f proof) tt) + (! sc (^ (is_drat_proof f proof) tt) bottom))))) diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf index 57de39111..2ede6df34 100644 --- a/proofs/signatures/drat_test.plf +++ b/proofs/signatures/drat_test.plf @@ -280,3 +280,155 @@ (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) (DRATProofa cln DRATProofn))))))))))))))) + +; ===================================== ; +; Test Suite from "Two Flavors of DRAT" ; +; ===================================== ; + +; The paper includes a number of proofs which explore specified and operational +; DRAT validity. + +; Our test predicate for asserting the specified and operational validity of +; DRAT proofs +(declare spec_oper_test + (! f cnf + (! proof DRATProof + (! spec_validity bool + (! oper_validity bool + (! sc (^ (bool_and + (bool_eq (is_specified_drat_proof f proof) spec_validity) + (bool_eq (is_operational_drat_proof f proof) oper_validity) + ) tt) + TestSuccess)))))) + + +(declare x var) +(declare y var) +(declare z var) +(declare w var) +(define ex_1_formula + (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln))) + (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln))) + (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln))) + (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln))) + (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln))) + (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln))) + (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln))) + (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln))) + cnfn))))))))) + +; Spec-valid, operationally-invalid +(define ex_1_pf_pi + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg x) cln)) + (DRATProofd (clc (pos w) (clc (neg x) cln)) + (DRATProofa (clc (neg w) (clc (neg x) cln)) + (DRATProofa (clc (pos w) (clc (pos x) cln)) + (DRATProofa (clc (pos y) (clc (pos w) cln)) + (DRATProofa cln + DRATProofn))))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_1_pf_pi tt ff))) + +; Spec-invalid, operationally valid +(define ex_1_pf_sigma + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofd (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg y) cln)) + (DRATProofa (clc (neg w) (clc (neg y) cln)) + (DRATProofa (clc (pos w) cln) + (DRATProofa cln + DRATProofn)))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt))) + +(declare x1 var) +(declare x2 var) +(declare x3 var) +(declare x4 var) +(declare x5 var) +(declare x6 var) +(declare x7 var) +(declare x8 var) +(declare x9 var) +(declare x10 var) + +(define ex_2_formula + (cnfc (clc (pos x1) cln) + (cnfc (clc (neg x1) (clc (pos x2) cln)) + (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln))) + (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln))) + (cnfc (clc (pos x5) (clc (pos x6) cln)) + (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln))) + (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln))) + (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln))) + (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln))) + (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln))) + (cnfc (clc (neg x8) (clc (pos x5) cln)) + (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln))) + (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln))) + (cnfc (clc (neg x10) (clc (pos x9) cln)) + (cnfc (clc (neg x9) (clc (pos x7) cln)) + (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln)))) + cnfn))))))))))))))))) + +; Spec-valid, operationally-valid +(define ex_2_pf_tau + (DRATProofa (clc (pos x5) cln) + (DRATProofa (clc (pos x4) cln) + (DRATProofa (clc (pos x9) cln) + (DRATProofa cln + DRATProofn))))) + +(check + (: TestSuccess + (spec_oper_test ex_2_formula ex_2_pf_tau tt tt))) + +; Spec-valid, operationally unspecified in the paper, but its operationally valid. +(define ex_3_pf_tau_prime + (DRATProofa (clc (pos x5) cln) + (DRATProofd (clc (neg x1) (clc (pos x2) cln)) + (DRATProofa (clc (pos x9) cln) + (DRATProofa cln + DRATProofn))))) + +(check + (: TestSuccess + (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt))) + +; Spec-invalid, operationally-invalid +(define ex_4_pf_pi_prime + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg x) cln)) + (DRATProofa (clc (neg w) (clc (neg x) cln)) + (DRATProofa (clc (pos w) (clc (pos x) cln)) + (DRATProofa (clc (pos y) (clc (pos w) cln)) + (DRATProofa cln + DRATProofn)))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff))) + + +; Spec-valid, operationally valid +(define ex_5_pf_sigma_prime + (DRATProofa (clc (pos x) (clc (pos y) cln)) + (DRATProofa (clc (pos x) cln) + (DRATProofa (clc (pos w) (clc (neg y) cln)) + (DRATProofa (clc (neg w) (clc (neg y) cln)) + (DRATProofa (clc (pos w) cln) + (DRATProofa cln + DRATProofn))))))) + +(check + (: TestSuccess + (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt))) + |