;
; This signature checks **Specified DRAT**.
-(declare cnf_holds (! c cnf type))
-(declare cnfn_proof (cnf_holds cnfn))
-(declare cnfc_proof
- (! c clause
- (! deduped_c clause
- (! rest cnf
- (! proof_c (holds c)
- (! proof_rest (cnf_holds rest)
- (! sc (^ (clause_dedup c) deduped_c)
- (cnf_holds (cnfc c rest)))))))))
-
; A DRAT proof itself: a list of addition or deletion instructions.
(declare DRATProof type)
(declare DRATProofn DRATProof)
--- /dev/null
+; Depends on sat.plf
+
+; This file exists to support the **definition introduction** (or **extension**)
+; rule in the paper:
+; "Extended Resolution Simulates DRAT"
+; which can be found at http://www.cs.utexas.edu/~marijn/publications/ijcar18.pdf
+;
+; The core idea of extended resolution is that given **any** formula f
+; involving the variables from some SAT problem, one can introduce the
+; constraint
+;
+; new <=> f
+;
+; without changing satisfiability, where "new" is a fresh variable.
+;
+; This signature does not provide axioms for facilitating full use of this
+; idea. Instead, this signature facilitates use of one specific kind of
+; extension, that of the form:
+;
+; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
+;
+; which translates into the clauses:
+;
+; new v l_1 v l_2 v ... v l_n
+; new v ~old
+; for each i <= n: l_i v ~new v old
+;
+; This kind of extension is (a) sufficient to simulate DRAT proofs and (b) easy
+; to convert to clauses, which is why we use it.
+
+; A definition witness value for:
+; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
+; It witnesses the fact that new was fresh when it was defined by the above.
+;
+; Thus it witnesses that the above, when added to the formula consisting of the
+; conjunction all the already-proven clauses, produces an equisatisfiable
+; formula.
+(declare definition (! new var (! old lit (! others clause type))))
+
+; Given `old` and `others`, this takes a continuation which expects
+; 1. a fresh variable `new`
+; 2. a definition witness value for:
+; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
+;
+; Aside:
+; In programming a **continuation** of some computation is a function that
+; takes the results of that computation as arguments to produce a final
+; result.
+;
+; In proof-construction a **continuation** of some reasoning is a function
+; that takes the results of that reasoning as arguments to proof a final
+; result.
+;
+; That definition witness value can be clausified using the rule below.
+;
+; There need to be two different rules because the side-condition for
+; clausification needs access to the new variable, which doesn't exist except
+; inside the continuation, which is out-of-scope for any side-condition
+; associated with this rule.
+(declare decl_definition
+ (! old lit
+ (! others clause ; List of vars
+ (! pf_continuation (! new var (! def (definition new old others)
+ (holds cln)))
+ (holds cln)))))
+
+; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each
+; literal and returns a list of clauses as a `cnf`.
+(program clause_add_suffix_all ((list clause) (suffix clause)) cnf
+ (match list
+ (cln cnfn)
+ ((clc l rest) (cnfc (clc l suffix)
+ (clause_add_suffix_all rest suffix)))))
+
+; This translates a definition witness value for the def:
+;
+; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
+;
+; into the clauses:
+;
+; new v l_1 v l_2 v ... v l_n
+; new v ~old
+; for each i <= n: l_i v ~new v old (encoded as (cnf_holds ...))
+(declare clausify_definition
+ (! new var
+ (! old lit
+ (! others clause
+ ; Given a definition { new <-> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) }
+ (! def (definition new old others)
+ (! negOld lit
+ (! mkNegOld (^ (lit_flip old) negOld)
+ (! provenCnf cnf
+ (! mkProvenCnf (^ (clause_add_suffix_all
+ others
+ (clc (neg new) (clc old cln))) provenCnf)
+ ; If you can prove bottom from its clausal representation
+ (! pf_continuation
+ ; new v l_1 v l_2 v ... v l_n
+ (! pf_c1 (holds (clc (pos new) others))
+ ; new v ~old
+ (! pf_c2 (holds (clc (pos new) (clc negOld cln)))
+ ; for each i <= n: l_i v ~new v old
+ (! pf_cs (cnf_holds provenCnf)
+ (holds cln))))
+ ; Then you've proven bottom
+ (holds cln)))))))))))
+
+; This axiom is useful for converting a proof of some CNF formula (a value of
+; type (cnf_holds ...)) into proofs of the constituent clauses (many values of
+; type (holds ...)).
+; Given
+; 1. a proof of some cnf, first ^ rest, and
+; 2. a proof continuation that
+; a. takes in proofs of
+; i. first and
+; ii. rest and
+; b. proceeds to prove bottom,
+; proves bottom.
+(declare cnfc_unroll_towards_bottom
+ (! first clause
+ (! rest cnf
+ (! pf (cnf_holds (cnfc first rest))
+ (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln)))
+ (holds cln))))))
+
--- /dev/null
+; Depends on er.plf
+
+; Type for representing success when testing a side-condition
+(declare TestSuccess type)
+
+; Test for clause_add_suffix_all
+(declare test_clause_add_suffix_all
+ (! list clause
+ (! suffix clause
+ (! result cnf
+ (! (^ (clause_add_suffix_all list suffix) result)
+ TestSuccess)))))
+
+(check
+ (% a lit
+ (% b lit
+ (% c lit
+ (test_clause_add_suffix_all
+ (clc a (clc b cln))
+ (clc c cln)
+ (cnfc (clc a (clc c cln))
+ (cnfc (clc b (clc c cln))
+ cnfn))
+ )
+ )))
+)
+
+; This is a circuitous proof that uses the definition introduction and
+; unrolling rules
+(check
+ (% v1 var
+ (% v2 var
+ (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
+ (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
+ (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
+ (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
+ (: (holds cln)
+ (decl_definition
+ (neg v1)
+ (clc (neg v2) cln)
+ (\ v3
+ (\ def3
+ (clausify_definition _ _ _ def3 _ _
+ (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
+ (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
+ (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
+ (cnfc_unroll_towards_bottom _ _ pf_cnf3
+ (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
+ (\ pf_cnfn
+ ; Clauses
+ (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2
+ (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3
+ (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1
+ (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1
+ (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2
+ (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty
+ pf_c13
+ ))
+ ))
+ ))
+ ))
+ ))
+ ))
+ )))
+ )))
+ )
+ ))
+ )
+ )
+ ))))
+ ))
+)
+
+; This is a test of ER proof produced by drat2er on Example 1 from:
+; https://www.cs.utexas.edu/~marijn/drat-trim/
+(check
+ (% v1 var
+ (% v2 var
+ (% v3 var
+ (% v4 var
+ (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+ (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+ (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+ (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+ (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+ (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+ (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+ (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+ (: (holds cln)
+ (decl_definition
+ (neg v1)
+ cln
+ (\ v5
+ (\ def1
+ (clausify_definition _ _ _ def1 _ _
+ (\ pf_c9 ; type: (holds (clc (pos def1v) cln))
+ (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
+ (\ idc0 ; type: (cnf_holds cnfn)
+ (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
+ (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
+ (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
+ (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
+ (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
+ (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
+ (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
+ (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
+ pf_c18
+ ))))))))))))))))
+ )))
+ )
+ ))
+ )
+ )
+ ))))))))
+ ))))
+)
; Some side-conditions make use of a _global assignment_ encoded in
; 0 (true) / 1 (false) marks on variables.
-; A list of clauses, CNF if interpretted as a formula,
-; but also sometimes just a list
-(declare cnf type)
-(declare cnfn cnf)
-(declare cnfc (! h clause (! t cnf cnf)))
-
; Unit (https://en.wikipedia.org/wiki/Unit_type)
; For functions that don't return anything
(declare Unit type) ; The type with only one value (like `void` in C)
; Functional programs for manipulating types ;
; ========================================== ;
-; Flip the polarity of the literal
-(program lit_flip ((l lit)) lit
- (match l
- ((pos v) (neg v))
- ((neg v) (pos v))))
-
; Are two literal equal?
(program lit_eq ((l1 lit) (l2 lit)) bool
(match l1
(ff (clause_contains_lit c' l))))
(cln ff)))
-; Returns a copy of `c` with any duplicate literals removed.
-; Never fails.
-; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
-; afterwards.
-(program clause_dedup ((c clause)) clause
- (match c
- (cln cln)
- ((clc l rest)
- (match l
- ((pos v) (ifmarked3
- v
- (clause_dedup rest)
- (do (markvar3 v)
- (let result (clc (pos v) (clause_dedup rest))
- (do (markvar3 v) result)))))
- ((neg v) (ifmarked4
- v
- (clause_dedup rest)
- (do (markvar4 v)
- (let result (clc (neg v) (clause_dedup rest))
- (do (markvar4 v) result)))))))))
-
; Append two traces
(program Trace_concat ((t1 Trace) (t2 Trace)) Trace
(match t1
(declare pos (! x var lit))
(declare neg (! x var lit))
+; Flip the polarity of the literal
+(program lit_flip ((l lit)) lit
+ (match l
+ ((pos v) (neg v))
+ ((neg v) (pos v))))
+
(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))
+; A list of clauses, CNF if interpretted as a formula,
+; but also sometimes just a list
+(declare cnf type)
+(declare cnfn cnf)
+(declare cnfc (! h clause (! t cnf cnf)))
+
; constructs for general clauses for R, Q, satlem
(declare concat_cl (! c1 clause (! c2 clause clause)))
(! u2 (! v (holds c) (holds c2))
(holds c2))))))
+
+; Returns a copy of `c` with any duplicate literals removed.
+; Never fails.
+; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
+; afterwards.
+(program clause_dedup ((c clause)) clause
+ (match c
+ (cln cln)
+ ((clc l rest)
+ (match l
+ ((pos v) (ifmarked3
+ v
+ (clause_dedup rest)
+ (do (markvar3 v)
+ (let result (clc (pos v) (clause_dedup rest))
+ (do (markvar3 v) result)))))
+ ((neg v) (ifmarked4
+ v
+ (clause_dedup rest)
+ (do (markvar4 v)
+ (let result (clc (neg v) (clause_dedup rest))
+ (do (markvar4 v) result)))))))))
+
+(declare cnf_holds (! c cnf type))
+(declare cnfn_proof (cnf_holds cnfn))
+(declare cnfc_proof
+ (! c clause
+ (! deduped_c clause
+ (! rest cnf
+ (! proof_c (holds c)
+ (! proof_rest (cnf_holds rest)
+ (! sc (^ (clause_dedup c) deduped_c)
+ (cnf_holds (cnfc c rest)))))))))
+
; A little example to demonstrate simplify_clause.
; It can handle nested clr's of both polarities,
; and correctly cleans up marks when it leaves a
projects / cvc5.git / commitdiff