1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
(in-package "SAT")
(include-book "assignment-equiv")
(include-book "create-farray")
(include-book "reader")
(defun create-rat-checker (nVars st)
(declare (xargs :guard (posp nVars)
:stobjs (st)))
(create-farray
(list 1
1
(1+ nVars)
(+ 2 (* 2 nVars)))
0 st))
;; create a new farray for rat-checker
(create-rat-checker 4641 st)
;; write number of variables to rat-checker
(fwrite *num-vars* 0 4641 *s* st)
(defttag t)
(remove-untouchable acl2::create-state t)
(defun read-and-parse-local-state (filename)
;; This function requires the STATE, so we use the next form
(with-local-state
;; "Powerful" macro that provides access to the state, but
;; requires the two events above.
(mv-let (err num-vars num-clauses formula state)
(ACL2::read-and-parse filename)
(mv err num-vars num-clauses formula))))
;; Example Read -- filename can be changed.
;; (defconst *cnf*
;; (mv-let (err num-vars num-clauses formula)
;; (read-and-parse-local-state "small-unsat.cnf")
;; (list err num-vars num-clauses formula)))
(defconst *cnf*
(mv-let (err num-vars num-clauses formula)
(read-and-parse-local-state "R_4_4_18.cnf")
(list err num-vars num-clauses formula)))
(defun read-and-parse-proof-local-state (filename)
;; This function requires the STATE, so we use the next form
(with-local-state
;; "Powerful" macro that provides access to the state, but
;; requires the two events above.
(mv-let (err num-clauses proof state)
(ACL2::read-and-parse-proof filename)
(mv err num-clauses proof))))
;; (defconst *proof*
;; (mv-let (err num-clauses proof)
;; (read-and-parse-proof-local-state "small-unsat.rat")
;; (list err num-clauses proof)))
(defconst *proof*
(mv-let (err num-clauses proof)
(read-and-parse-proof-local-state "R_4_4_18.rat")
(list err num-clauses proof)))
;; (assignment-stp st)
;; (clause-listp (caddr *proof*))
;; (formulap (cadddr *cnf*))
(defun verify-proof-st-count (clause-list formula count max st)
(declare (xargs :guard (and (assignment-stp st)
(clause-listp clause-list)
(clause-list-in-rangep clause-list st)
(formulap formula)
(formula-in-rangep formula st)
(natp count)
(posp max))
:stobjs (st)))
(if (atom clause-list)
(mv t st)
(mv-let (vc st)
(verify-clause-st (car clause-list) formula st)
(if (not vc)
(mv nil st)
(if (equal (mod count 1000) 0)
(b* ((percent (floor (* 100 count) max))
(- (cw "~x0% (~x1 / ~x2) ~%" percent count max)))
(verify-proof-st-count (cdr clause-list)
(cons (car clause-list) formula)
(1+ count)
max
st))
(verify-proof-st-count (cdr clause-list)
(cons (car clause-list) formula)
(1+ count)
max
st))))))
(time$
(verify-proof-st-count (caddr *proof*)
(cadddr *cnf*)
0
(cadr *proof*)
st))
|
