equal
deleted
inserted
replaced
11 section{* General settings and functions for our representation of clauses *} |
11 section{* General settings and functions for our representation of clauses *} |
12 |
12 |
13 subsection{* Types for Literals, Clauses and ProofSteps *} |
13 subsection{* Types for Literals, Clauses and ProofSteps *} |
14 text {* We encode Literals as integers and Clauses as sorted Lists. *} |
14 text {* We encode Literals as integers and Clauses as sorted Lists. *} |
15 |
15 |
16 types ClauseId = nat |
16 type_synonym ClauseId = nat |
17 types Lit = int |
17 type_synonym Lit = int |
18 types Clause = "Lit list" |
18 type_synonym Clause = "Lit list" |
19 |
19 |
20 text {* This resembles exactly to Isat's Proof Steps *} |
20 text {* This resembles exactly to Isat's Proof Steps *} |
21 |
21 |
22 types Resolvants = "ClauseId * (Lit * ClauseId) list" |
22 type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list" |
23 datatype ProofStep = |
23 datatype ProofStep = |
24 ProofDone bool |
24 ProofDone bool |
25 | Root ClauseId Clause |
25 | Root ClauseId Clause |
26 | Conflict ClauseId Resolvants |
26 | Conflict ClauseId Resolvants |
27 | Delete ClauseId |
27 | Delete ClauseId |