-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.rkt
120 lines (116 loc) · 4.8 KB
/
main.rkt
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
112
113
114
115
116
117
118
119
120
#lang racket
(provide (all-defined-out))
(require "sls.rkt"
"parsing/parse.rkt"
"parsing/transform.rkt"
"fp2real.rkt"
"elim-eqs.rkt"
racket/cmdline)
(define main
(λ ()
(let* ([seed (make-parameter 1)]
[c2 (make-parameter 1/2)]
[wp (make-parameter 0.001)]
[step (make-parameter 200)]
[start-with-zeros? (make-parameter #t)]
[try-real-models? (make-parameter #f)]
[print-models? (make-parameter #f)]
[elim-eqs? (make-parameter #f)]
[vns (make-parameter #f)]
[enable-log (make-parameter #f)]
[file-to-analyze
(command-line
#:program "sls"
#:once-each ["--seed"
seed-arg
"RNG seed"
(define n-seed (string->number seed-arg))
(if (and n-seed
(exact-positive-integer? n-seed)
(>= n-seed 0)
(<= n-seed (sub1 (expt 2 31))))
(seed n-seed)
(error "not a valid seed"))]
["--c2"
c2-arg
"Score scaling constant"
(define n-c2 (string->number c2-arg))
(if (and n-c2 (rational? n-c2) (>= n-c2 0) (<= n-c2 1))
(c2 n-c2)
(error "not a valid score scaling constant"))]
["--wp"
wp-arg
"Diversification probability"
(define n-wp (string->number wp-arg))
(if (and n-wp (>= n-wp 0) (<= n-wp 1))
(wp n-wp)
(error "not a valid diversification probability"))]
["--step"
step-arg
"Search steps"
(define n-step (string->number step-arg))
(if (and n-step (exact-nonnegative-integer? n-step))
(step n-step)
(error "not a valid search step"))]
["--initialize-with-random"
("Initialize search space with random values"
"otherwise search space is initialized to all 0s")
(start-with-zeros? #f)]
["--try-real-models"
("Try real models as initial models")
(try-real-models? #t)]
["--vns" ("Enable variable neighborhood search") (vns #t)]
["--elim-eqs" ("Enable Z3 `solve-eqs` tactics") (elim-eqs? #t)]
["--print-models" ("Print models") (print-models? #t)]
["--debug" ("Enable logger") (enable-log #t)]
#:args (filename) ; expect one command-line argument: <filename>
; return the argument as a filename to compile
filename)]
[input-file
(if (elim-eqs?) (eliminate-eqs file-to-analyze) file-to-analyze)]
[script (file->sexp input-file)]
[formula (remove-fpconst
(simplify (unnest (formula->nnf (remove-let-bindings
(get-formula script))))))]
[var-info (get-var-info script)])
(begin
(random-seed (seed))
(if (enable-log)
(let* ([oliver-logger (make-logger 'oliver-says)]
[oliver-lr (make-log-receiver oliver-logger 'debug)])
(begin
(void (thread (λ ()
(let loop ()
(define v (sync oliver-lr))
(printf "[~a] ~a\n"
(vector-ref v 0)
(vector-ref v 1))
(loop)))))
(current-logger oliver-logger)))
42)
(define initial-models
(let ([models (if (start-with-zeros?)
(initialize/Assignment var-info)
(randomize/Assignment var-info))])
(if (try-real-models?)
(let ([real-models (get-real-model input-file)])
(if real-models