File: options.py.save

package info (click to toggle)
p9m4 0.5.dfsg-3
  • links: PTS
  • area: main
  • in suites: buster, stretch
  • size: 664 kB
  • ctags: 296
  • sloc: python: 2,909; makefile: 21; csh: 7
file content (685 lines) | stat: -rw-r--r-- 39,449 bytes parent folder | download | duplicates (5)
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
# system imports

import os, sys
import re
import wx

# local imports

import utilities
from wx_utilities import *

# Indexes into options (for 'flag' and 'parm', unless noted otherwise)

Id       = 0
Label_id = 1
Share    = 2
Type     = 3  # for all records
Name     = 4  # for all records
Value    = 5
Default  = 6
Range    = 7  # ignored for 'flag
Tip      = 8

Column   = 5  # only for 'group'


# Option records:
#
# [widget_id, label_id, 'flag',       name, value, default, tooltip, share]
# [widget_id, label_id, 'parm',       name, value, default, tooltip, share, min, max]
# [widget_id, label_id, 'stringparm', name, value, default, tooltip, share [r1,...,rn]]
# [None, None, 'group', group_name, column]

def id_to_option(id, options):
    for opt in options:
        if opt[Type] in ['flag', 'parm', 'stringparm'] and opt[Id] == id:
            return opt
    return None

def name_to_option(name, options):
    for opt in options:
        if opt[Type] in ['flag', 'parm', 'stringparm'] and opt[Name] == name:
            return opt
    return None

def nondefault_options(options, work):
    """We pass in a partially constructed string so that
    we can prevent duplicates."""
    for opt in options:
        if (opt[Type] in ['flag', 'parm', 'stringparm'] and
            opt[Value] != opt[Default]):
            triple = (opt[Type], opt[Name], opt[Value])
            if not utilities.member(triple, work):
                work.append(triple)
    return work

def separate_option_triples_by_case(triples):
    # upper = lower = []  # WRONG!!  MAKES THEM THE SAME LIST!!
    upper = []
    lower = []
    for (type,name,value) in triples:
        if name[0].isupper():
            upper.append((type,name,value))
        else:
            lower.append((type,name,value))
    return (lower, upper)

def option_triples_contains_name(triples, name):
    for (_,n,_) in triples:
        if name == n:
            return True
    return False

def option_triples_to_string(triples):
    s = ''
    for (type,name,value) in triples:
        if type == 'flag':
            if value:
                s += '  set(%s).\n' % name
            else:
                s += '  clear(%s).\n' % name
        elif type == 'parm':
            s += '  assign(%s, %d).\n' % (name,value)
        elif type == 'stringparm':
            s += '  assign(%s, %s).\n' % (name,value)
    return s

def print_sharing(opt):
    print '  option: %d %s %s' % (opt[Id], opt[Name], str(opt[Value]))
    for o in opt[Share]:
        print '        %d %s' % (o[Id], o[Name])

def update_label(opt):
    label = wx.FindWindowById(opt[Label_id])
    if opt[Value] == opt[Default]:
        label.SetForegroundColour('BLACK')
        label.Refresh()
    else:
        label.SetForegroundColour('RED')
        label.Refresh()

def update_option(opt, value):
    opt[Value] = value
    update_label(opt)
    x = wx.FindWindowById(opt[Id])
    if opt[Type] in ['flag', 'parm']:
        x.SetValue(value)
    elif opt[Type] == 'stringparm':
        x.SetStringSelection(value)

def update_shared(opt):
    for shared_opt in opt[Share]:
        if shared_opt != opt:
            update_option(shared_opt, opt[Value])

def link_options(opt1, opt2):
    if opt1 in opt2[Share] or opt2 in opt1[Share]:
        error_dialog('link_options, already linked?')
    else:
        shared = opt1[Share] + opt2[Share]
        for opt in shared:
            opt[Share] = shared

def link_options_by_names(options1, options2, names):
    for name in names:
        opt1 = options1.name_to_opt(name)
        opt2 = options2.name_to_opt(name)
        if opt1 and opt2:
            link_options(opt1, opt2)
            # print 'Link:'; print_sharing(opt1)
            # print '     '; print_sharing(opt2)
        else:
            error_dialog('link_options_by_names: not found')

class Options_panel(wx.Panel):
    def __init__(self, parent, title, logo_bitmap, options):

        self.options = options
        wx.Panel.__init__(self, parent)

        if logo_bitmap:
            heading = wx.StaticBitmap(self, -1, logo_bitmap)
        else:
            heading = wx.StaticText(self, -1, title) # title.replace(' ', '_'))
            font = wx.SystemSettings_GetFont(wx.SYS_DEFAULT_GUI_FONT)
            font.SetPointSize(font.GetPointSize()+2)
            font.SetWeight(wx.FONTWEIGHT_BOLD)
            heading.SetFont(font)

        reset_btn = wx.Button(self, -1, 'Reset These to Defaults')
        self.Bind(wx.EVT_BUTTON, self.on_reset, reset_btn)

        groups = []

        for opt in self.options:
            if opt[Type] in ['flag', 'parm', 'stringparm']:

                if groups == []:
                    # in case the options are not divided into groups
                    box = wx.StaticBox(self, -1, '')
                    g_sizer = wx.GridBagSizer(5, 5)
                    groups.append((box, g_sizer, 'left'))
                    row = 0

                id = wx.NewId()
                label_id = wx.NewId()
                opt[Id] = id
                opt[Label_id] = label_id
                opt[Value] = opt[Default]
                opt[Share] = [opt]  # note: this creates a cyclic structure

                label = wx.StaticText(self, label_id, opt[Name] + ':')

                if opt[Type] == 'flag':
                    x = wx.CheckBox(self, id, '')
                    self.Bind(wx.EVT_CHECKBOX, self.on_change, x)
                    x.SetValue(opt[Default])
                    tip = opt[Tip]
                elif opt[Type] == 'parm':
                    (min, max) = opt[Range]
                    x = wx.SpinCtrl(self,id,min=min,max=max,size=(75,-1))
                    self.Bind(wx.EVT_SPINCTRL, self.on_change, x)
                    x.SetValue(opt[Default])
                    tip = ('%s Range is [%d ... %d].' % (opt[Tip], min, max))
                else: # stringparmparm
                    x = wx.Choice(self, id, choices=opt[Range])
                    self.Bind(wx.EVT_CHOICE, self.on_change, x)
                    x.SetStringSelection(opt[Default])
                    tip = opt[Tip]
                    
                label.SetToolTipString(tip)
                x.SetToolTipString(tip)

                g_sizer.Add(label, (row,0), (1,1), wx.ALIGN_RIGHT|wx.ALIGN_CENTER_VERTICAL)
                g_sizer.Add(x,     (row,1), (1,1), wx.ALIGN_LEFT|wx.ALIGN_CENTER_VERTICAL)
                row += 1

            elif opt[Type] == 'group':
                box = wx.StaticBox(self, -1, opt[Name])
                g_sizer = wx.GridBagSizer(5, 5)
                groups.append((box, g_sizer, opt[Column]))
                row = 0
            else:
                # dividers? space?
                pass

        sizer       = wx.BoxSizer(wx.VERTICAL)
        opt_sizer   = wx.BoxSizer(wx.HORIZONTAL)
        left_sizer  = wx.BoxSizer(wx.VERTICAL)
        right_sizer = wx.BoxSizer(wx.VERTICAL)
        right_column_populated = False

        for (box, g_sizer, column) in groups:
            box_sizer = wx.StaticBoxSizer(box, wx.VERTICAL)
            box_sizer.Add(g_sizer, 0, wx.ALL|wx.ALIGN_CENTER, 5)
            if column == 'left':
                left_sizer.Add(box_sizer, 0, wx.ALL|wx.GROW, 5)
            else:
                right_sizer.Add(box_sizer, 0, wx.ALL|wx.GROW, 5)
                right_column_populated = True

        opt_sizer.Add(left_sizer, 0, wx.ALL, 0)
        if right_column_populated:
            opt_sizer.Add(right_sizer, 0, wx.ALL, 0)
        sizer.Add(heading, 0, wx.ALIGN_CENTER, 5)
        sizer.Add(opt_sizer, 0, wx.ALIGN_CENTER, 5)
        sizer.Add(reset_btn, 0, wx.ALIGN_CENTER, 5)

        self.SetSizer(sizer)

    def on_change(self, evt):
        opt = id_to_option(evt.GetId(), self.options)
        x = evt.GetEventObject()
        if opt[Type] in ['flag', 'parm']:
            opt[Value] = x.GetValue()
        elif opt[Type] == 'stringparm':
            opt[Value] = x.GetStringSelection()
        update_label(opt)
        update_shared(opt)

    def on_reset(self, evt):
        for opt in self.options:
            if (opt[Type] in ['flag', 'parm', 'stringparm'] and
                opt[Value] != opt[Default]):

                update_option(opt, opt[Default])
                update_shared(opt)
        
# END class Options_panel(Panel)

class M4_options:

    options = [

        [None, None, None, 'group', 'Basic Options', 'left'],
        [None, None, None, 'parm', 'domain_size', None, 2, [2,sys.maxint], 'Initial domain size.'],
        [None, None, None, 'parm', 'iterate_up_to', None, 10, [-1,sys.maxint], 'Final domain size.'],
        [None, None, None, 'parm', 'increment', None, 1, [1,sys.maxint], 'Increment for next domain size (when final > initial).'],
        [None, None, None, 'parm', 'max_models', None, 1, [-1,sys.maxint], 'Stop search at this number of models (-1 means no limit).'],
        [None, None, None, 'parm', 'max_seconds', None, 60, [-1,sys.maxint], 'Overall time limit.'],
        [None, None, None, 'parm', 'max_seconds_per', None, -1, [-1,sys.maxint], 'Time limit for each domain size.'],
        [None, None, None, 'flag', 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],

#        [None, None, None, 'group', 'Output Options', 'left'],
#        [None, None, None, 'flag', 'print_models', None, 1, None, 'Print models in standard form (for input to other LADR programs).'],
#        [None, None, None, 'flag', 'print_models_tabular', None, 0, None, 'Print models in a tabular form.'],
#        [None, None, None, 'flag', 'verbose', None, 0, None, 'Show more in the output file.'],
#        [None, None, None, 'flag', 'trace', None, 0, None, 'USE THIS ONLY ON VERY SMALL SEARCHES!!'],

        [None, None, None, 'group', 'Other Options', 'left'],
        [None, None, None, 'flag', 'integer_ring', None, 0, None, 'Impose a ring structure (see sample input Ring-19.in).'],
        [None, None, None, 'flag', 'iterate_primes', None, 0, None, 'Search structures of prime size only.'],
        [None, None, None, 'flag', 'skolems_last', None, 0, None, 'Decide Skolem symbols last.'],
        [None, None, None, 'parm', 'max_megs', None, 200, [-1,sys.maxint], 'Memory limit for Mace4 process (approximate).'],
        [None, None, None, 'flag', 'print_models', None, 1, None, 'Output models that are found.'],
        [None, None, None, 'stringparm', 'Model_Format', None, 'standard2', ['standard', 'standard2', 'portable', 'tabular', 'xml', 'raw', 'cooked', 'tex'], 'Format for models/counterexamples.  This option is different from the others in that it is used by the postprocessor "interpformat" rather than by Mace4.  This option is not given to Mace4 and is therefore not saved by "File->Save".'],

        [None, None, None, 'group', 'Experimental Options', 'right'],
        [None, None, None, 'flag', 'lnh', None, 1, None, 'Least Number Optimization.'],
        [None, None, None, 'flag', 'negprop', None, 1, None, 'Apply negative propagation.'],
        [None, None, None, 'flag', 'neg_assign', None, 1, None, 'Negative propagation is triggered by assignments.'],
        [None, None, None, 'flag', 'neg_assign_near', None, 1, None, 'Negative propagation is triggered by near-assignments.'],
        [None, None, None, 'flag', 'neg_elim', None, 1, None, 'Negative propagation is triggered by eliminations.'],
        [None, None, None, 'flag', 'neg_elim_near', None, 1, None, 'Negative propagation is triggered by near-eliminations.'],
        [None, None, None, 'parm', 'selection_order', None, 2, [0,2], '0: all, 1: concentric, 2: concentric-band.'],
        [None, None, None, 'parm', 'selection_measure', None, 4, [0,4], '0: first, 1: most occurrences, 2: most propagations, 3: most contradictions, 4: fewest values.'],
        ]

    def __init__(self, parent, logo_bitmap):
        self.panel = wx.Panel(parent)
        self.options_panel = Options_panel(self.panel, 'Mace4 Options',
                                 logo_bitmap, self.options)
        sizer = wx.BoxSizer(wx.VERTICAL)
        sizer.Add((0,0), 1)
        sizer.Add(self.options_panel, 0, wx.ALIGN_CENTER, 0)
        sizer.Add((0,0), 3)
        self.panel.SetSizer(sizer)

    def nondefaults(self):
        triples = nondefault_options(self.options, [])
        # always include max_seconds, because GUI default != program default.
        for name in ['max_seconds']:
            if not option_triples_contains_name(triples, name):
                opt = self.name_to_opt(name)
                if opt:
                    triples.append((opt[Type],opt[Name],opt[Value]))
        return triples

    def name_to_opt(self, name):
        return name_to_option(name, self.options)

    def share_external_option(self, external_opt):
        local_opt = self.name_to_opt(external_opt[Name])
        if not local_opt:
            error_dialog('share_external_option(M4), not found')
        else:
            link_options(local_opt, external_opt)
            # print 'External(M4):'; print_sharing(local_opt)
            # print '             '; print_sharing(external_opt)

    def reset(self):
        self.options_panel.on_reset(None)

    def output_transformed(self):
        sys.stdout.write('    options = ')
        output_trans(self.options)
        sys.stdout.write('\n\n')

def output_trans(options):
    print '        ['
    for opt in options:
        if opt[Type] == "group":
            print "\n        [None, None, None, '%s', '%s', '%s']," % (opt[Type], opt[Name], opt[Column])
        elif opt[Type] == "flag":
            print "        [None, None, None, '%s', '%s', None, %d, None, '%s']," % (opt[Type], opt[Name], opt[Default], opt[Tip])
        elif opt[Type] == "parm":
            print "        [None, None, None, '%s', '%s', None, %d, [%d,%d], '%s']," % (opt[Type], opt[Name], opt[Default], opt[Min], opt[Max], opt[Tip])
        elif opt[Type] == "stringparm":
            print "        [None, None, None, '%s', '%s', None, '%s', %s, '%s']," % (opt[Type], opt[Name], opt[Default], opt[Range], opt[Tip])
    sys.stdout.write("        ]")

# end class M4_options

class P9_options:

    option_sets = [

        ('Basic Options', 
        [
        [None, None, None, 'parm', 'max_weight', None, 100, [-sys.maxint,sys.maxint], 'Discard inferred clauses with weight greater than this.'],
        [None, None, None, 'parm', 'pick_given_ratio', None, 0, [0,sys.maxint], 'Selection by (Weight : Age) ratio  (except for hints).'],
        [None, None, None, 'stringparm', 'order', None, 'lpo', ['lpo', 'rpo', 'kbo'], 'Overall term ordering: Lexicographic Path Ordering (LPO), Recursive Path Ordering (RPO), Knuth-Bendix Ordering (KBO).  If the search fails with LPO, try KBO.'],
        [None, None, None, 'stringparm', 'eq_defs', None, 'unfold', ['unfold', 'fold', 'pass'], 'Adjustment of term ordering, based on equational definitions in the input.\nUnfold: eliminate defined operations at the start of the search;\nFold: introduce the defined operation whenever possible;\nPass: let equational definitions be oriented by the term ordering.'],
        [None, None, None, 'flag', 'expand_relational_defs', None, 0, None, 'Use relational definitions in the input to immediately expand occurrences of the defined relations in the input.'],
        [None, None, None, 'flag', 'restrict_denials', None, 0, None, 'This flag applies only to Horn sets.  It restricts the application of inference rules when negative clauses are involved, with the goal of producing more direct (forward) proofs.'],
        [None, None, None, 'parm', 'max_seconds', None, 60, [-1,sys.maxint], 'Stop the search at this number of seconds (CPU, not wall clock).'],
        [None, None, None, 'flag', 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],
        [None, None, None, 'stringparm', 'Proof_Format', None, 'standard', ['standard', 'parents_only', 'xml', 'hints', 'ivy'], 'Format for proofs.  This option is different from the others in that it is used by the postprocessor "prooftrans" rather than by Prover9.  This option is not given to Prover9 and is therefore not saved by "File->Save".'],
        ]),

        ('Meta Options', 
        [
        [None, None, None, 'flag', 'auto', None, 1, None, 'Automatic Mode.  This flag simply sets or clears the following 4 flags.'],
        [None, None, None, 'flag', 'auto_limits', None, 1, None, 'Search limits.'],
        [None, None, None, 'flag', 'auto_denials', None, 1, None, 'Automatic handling of denials (negative clauses in Horn sets).'],
        [None, None, None, 'flag', 'auto_inference', None, 1, None, 'Automatic selection of inference rules, based on the input.'],
        [None, None, None, 'flag', 'auto_process', None, 1, None, 'Processing of inferred clauses.'],
        [None, None, None, 'flag', 'auto2', None, 0, None, 'Experimental automatic mode.'],
        ]),

        ('Term Ordering', 
        [
        [None, None, None, 'stringparm', 'order', None, 'lpo', ['lpo', 'rpo', 'kbo'], 'Overall term ordering: Lexicographic Path Ordering (LPO), Recursive Path Ordering (RPO), Knuth-Bendix Ordering (KBO).  If the search fails with LPO, try KBO.'],
        [None, None, None, 'stringparm', 'eq_defs', None, 'unfold', ['unfold', 'fold', 'pass'], 'Adjustment of term ordering, based on equational definitions in the input.\nUnfold: eliminate defined operations at the start of the search;\nFold: introduce the defined operation whenever possible;\nPass: let equational definitions be oriented by the term ordering.'],
        [None, None, None, 'flag', 'inverse_order', None, 1, None, 'Adjustment of term ordering, based on occurrences of inverse axioms in the input.'],
        ]),

        ('Limits', 
        [

        [None, None, None, 'group', 'Search Limits', 'left'],
        [None, None, None, 'parm', 'max_given', None, -1, [-1,sys.maxint], 'Stop the search at this number of given clauses.'],
        [None, None, None, 'parm', 'max_kept', None, -1, [-1,sys.maxint], 'Stop the search at this number of kept clauses.'],
        [None, None, None, 'parm', 'max_proofs', None, 1, [-1,sys.maxint], 'Stop the search at this number of proofs.'],
        [None, None, None, 'parm', 'max_megs', None, 200, [-1,sys.maxint], 'Stop the search when the process has used about this amount of memory.'],
        [None, None, None, 'parm', 'max_seconds', None, 60, [-1,sys.maxint], 'Stop the search at this number of seconds (CPU, not wall clock).'],
        [None, None, None, 'parm', 'max_minutes', None, -1, [-1,sys.maxint], ''],
        [None, None, None, 'parm', 'max_hours', None, -1, [-1,sys.maxint], ''],
        [None, None, None, 'parm', 'max_days', None, -1, [-1,sys.maxint], ''],

        [None, None, None, 'group', 'Limits on Kept Clauses', 'right'],
        [None, None, None, 'parm', 'max_weight', None, 100, [-sys.maxint,sys.maxint], 'Discard inferred clauses with weight greater than this.'],
        [None, None, None, 'parm', 'max_depth', None, -1, [-1,sys.maxint], 'Discard inferred clauses with depth greater than this.'],
        [None, None, None, 'parm', 'max_literals', None, -1, [-1,sys.maxint], 'Discard inferred clauses with more literals than this.'],
        [None, None, None, 'parm', 'max_vars', None, -1, [-1,sys.maxint], 'Discard inferred clauses with more variables than this.'],

        [None, None, None, 'group', 'Sos Control', 'right'],
        [None, None, None, 'parm', 'sos_limit', None, 20000, [-1,sys.maxint], 'Limit on the size of the SOS list (the list of clauses that have been kept, but not yet selected as given clauses).  As the SOS fills up, a heuristic is used to discards new clauses that are unlikely to be used due to this limit.'],
#       [None, None, None, 'parm', 'min_sos_limit', None, 0, [0,sys.maxint], 'Unused'],
#       [None, None, None, 'parm', 'lrs_interval', None, 50, [1,sys.maxint], 'Limited resource heuristic: '],
#       [None, None, None, 'parm', 'lrs_ticks', None, -1, [-1,sys.maxint], 'Limited resource heuristic: '],
        ]),

        ('Search Prep', 
        [
        [None, None, None, 'flag', 'expand_relational_defs', None, 0, None, 'Use relational definitions in the input to immediately expand occurrences of the defined relations in the input.'],
        [None, None, None, 'flag', 'dont_flip_input', None, 0, None, 'Do not flip input equalities, even if they violate the term ordering.  Using this flag can cause nontermination of rewriting.  It is usually better to adjust the term ordering instead.'],
        [None, None, None, 'flag', 'process_initial_sos', None, 1, None, 'Treat input clauses as if they were inferred; exceptions are the application of max_weight, max_level, max_vars, and max_literals.'],
        [None, None, None, 'flag', 'sort_initial_sos', None, 0, None, 'Sort the initial assumptions.  The order is largely  arbitrary.'],
        [None, None, None, 'flag', 'predicate_elim', None, 1, None, 'Try to eliminate predicate (relation) symbols before the search starts.'],
#       [None, None, None, 'parm', 'fold_denial_max', None, 0, [-1,sys.maxint], ''],
        ]),

        ('Goals/Denials', 
        [
        [None, None, None, 'flag', 'restrict_denials', None, 0, None, 'This flag applies only to Horn sets.  It restricts the application of inference rules when negative clauses are involved, with the goal of producing more direct (forward) proofs.'],
        [None, None, None, 'flag', 'reuse_denials', None, 0, None, 'This flag allows multiple proofs of goals.  (Applies to Horn sets only.'],
        ]),

        ('Select Given', 
        [

        [None, None, None, 'group', 'Selection Ratio', 'left'],
        [None, None, None, 'parm', 'hints_part', None, sys.maxint, [0,sys.maxint], 'Component for clauses that match hint.'],
        [None, None, None, 'parm', 'age_part', None, 1, [0,sys.maxint], 'Component for the oldest clauses.'],
        [None, None, None, 'parm', 'weight_part', None, 0, [0,sys.maxint], 'Component for the lightest clauses.'],
        [None, None, None, 'parm', 'false_part', None, 4, [0,sys.maxint], 'Component for the lightest false (w.r.t. an interpretation) clauses.'],
        [None, None, None, 'parm', 'true_part', None, 4, [0,sys.maxint], 'Component for the lightest true (w.r.t. an interpretation) clauses.'],
        [None, None, None, 'parm', 'random_part', None, 0, [0,sys.maxint], 'Component for random clauses.'],

        [None, None, None, 'group', 'Meta Options', 'right'],
        [None, None, None, 'parm', 'pick_given_ratio', None, 0, [0,sys.maxint], 'Selection by (Weight : Age) ratio  (except for hints).'],
        [None, None, None, 'flag', 'breadth_first', None, 0, None, 'Selection by age only (except for hints).'],
        [None, None, None, 'flag', 'lightest_first', None, 0, None, 'Selection by weight only (except for hints).'],
        [None, None, None, 'flag', 'random_given', None, 0, None, 'Random selection (except for hints).'],
#       [None, None, None, 'flag', 'default_parts', None, 1, None, ''],

        [None, None, None, 'group', 'Others', 'right'],
        [None, None, None, 'flag', 'input_sos_first', None, 1, None, 'Before starting with selection ratio, select input clauses.'],
        [None, None, None, 'flag', 'breadth_first_hints', None, 0, None, 'For hints component, select by age rather than by weight.'],
        [None, None, None, 'parm', 'eval_limit', None, 1024, [-1,sys.maxint], 'Limit on the number of ground instances for evaluation in an explicit interpretation (for semantic guidance).'],
        ]),

        ('Inference Rules', 
        [

        [None, None, None, 'group', 'Ordinary Rules', 'left'],
        [None, None, None, 'flag', 'binary_resolution', None, 0, None, 'Binary resolution (not necessarily positive).'],
        [None, None, None, 'flag', 'neg_binary_resolution', None, 0, None, 'Negative binary resolution.'],
        [None, None, None, 'flag', 'hyper_resolution', None, 0, None, 'Synonym for pos_hyperresolution.'],
        [None, None, None, 'flag', 'pos_hyper_resolution', None, 0, None, 'Positive hyperresolution.'],
        [None, None, None, 'flag', 'neg_hyper_resolution', None, 0, None, 'Negative hyperresolution.'],
        [None, None, None, 'flag', 'ur_resolution', None, 0, None, 'Unit resulting resolution.'],
        [None, None, None, 'flag', 'pos_ur_resolution', None, 0, None, 'Positive-unit resulting resolution.'],
        [None, None, None, 'flag', 'neg_ur_resolution', None, 0, None, 'Negative-unit resulting resolution.'],
        [None, None, None, 'flag', 'paramodulation', None, 0, None, 'The inference rule for equality.'],

        [None, None, None, 'group', 'Other Rules', 'left'],
        [None, None, None, 'parm', 'new_constants', None, 0, [-1,sys.maxint], 'If > 0, introduce new constants when equations such as x*x\'=y*y\' are derived.  The value of this parameter is a limit on the number of times the rule will be applied.'],
        [None, None, None, 'flag', 'factor', None, 0, None, ''],

        [None, None, None, 'group', 'General Restrictions', 'right'],
        [None, None, None, 'stringparm', 'literal_selection', None, 'max_negative', ['max_negative', 'all_negative', 'none'], 'Method for determining which literals in a multi-literal clause are eligible for resolution or paramodulation.'],
        [None, None, None, 'flag', 'positive_inference', None, 0, None, 'Resolution and Paramodulation are restricted so that one of the parents is a positive clause.'],

        [None, None, None, 'group', 'Resolution Restrictions', 'right'],
        [None, None, None, 'flag', 'ordered_res', None, 1, None, 'Resolved literals in one or more parents must be maximal in the clause.  (Does not apply to UR resolution.)'],
        [None, None, None, 'flag', 'check_res_instances', None, 0, None, 'The maximality checks are done after the application of the unifier for the inference.'],
        [None, None, None, 'flag', 'initial_nuclei', None, 0, None, 'For hyperresolution and UR resolution the nucleus for the inference must be an initial clause (this restriction can block all proofs).'],
        [None, None, None, 'parm', 'ur_nucleus_limit', None, -1, [-1,sys.maxint], 'The nucleus for each UR-resolution inference can have at most this many  literals.'],

        [None, None, None, 'group', 'Paramodulation Restrictions', 'right'],
        [None, None, None, 'flag', 'ordered_para', None, 1, None, 'For paramodulation inferences, one or both parents must be maximal in the clause.'],
        [None, None, None, 'flag', 'check_para_instances', None, 0, None, 'The maximality checks are done after the application of the unifier for the inference.'],
        [None, None, None, 'flag', 'para_from_vars', None, 1, None, 'Paramodulation is allowed from variables (not allowing can block all proofs)..'],
        [None, None, None, 'flag', 'para_units_only', None, 0, None, 'Paramodulation is applied to unit clauses only (this restriction can block all proofs).'],
#       [None, None, None, 'flag', 'basic_paramodulation', None, 0, None, ''],
        [None, None, None, 'parm', 'para_lit_limit', None, -1, [-1,sys.maxint], 'Paramodulation is not applied to clauses with more than this number of literals (using this restriction can block all proofs).'],
        ]),

        ('Rewriting', 
        [

        [None, None, None, 'group', 'Term Rewriting Limits', 'left'],
        [None, None, None, 'parm', 'demod_step_limit', None, 1000, [-1,sys.maxint], 'When rewriting derived clauses, apply at most this many rewrite steps.  Under most settings, rewriting is guaranteed to terminate, but it can be intractable.'],
        [None, None, None, 'parm', 'demod_size_limit', None, 1000, [-1,sys.maxint], 'When rewriting derived clauses, stop if the term being rewritten has more than this many symbols.'],

        [None, None, None, 'group', 'Lex-Dependent Rewriting', 'right'],
        [None, None, None, 'flag', 'lex_dep_demod', None, 1, None, 'Apply non-orientable equations as rewrite rules if the instance used for the rewrite is orientable.'],
        [None, None, None, 'flag', 'lex_dep_demod_sane', None, 1, None, 'This is a restriction on lex_dep_demod.  A non-orientable equation can be used for rewriting only if the two sides have the same number of symbols.'],
        [None, None, None, 'parm', 'lex_dep_demod_lim', None, 11, [-1,sys.maxint], 'This is a restriction on lex_dep_demod.  A non-orientable equation can be used for rewriting only if it has fewer than this number of symbols.'],
        [None, None, None, 'flag', 'lex_order_vars', None, 0, None, 'Incorporate (uninstantiated) variables into the term ordering, treating them as constants.  For example, x*y < y*x.  This cuts down the search, but it can block all proofs.'],

        [None, None, None, 'group', 'Others', 'left'],
        [None, None, None, 'flag', 'back_demod', None, 0, None, 'Use newly derived equations to rewrite old clauses.'],
        [None, None, None, 'flag', 'unit_deletion', None, 0, None, 'Remove literals from newly derived clauses with old unit clauses.'],
        [None, None, None, 'flag', 'back_unit_deletion', None, 0, None, 'Use newly derived unit clauses to remove literals from old clauses.'],
        [None, None, None, 'flag', 'cac_redundancy', None, 1, None, 'Eliminate some redundancy when there are commutative or associative-commutative operations.'],
        ]),

        ('Weighting', 
        [

        [None, None, None, 'group', 'Symbol Weights', 'left'],
        [None, None, None, 'parm', 'variable_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of variables .'],
        [None, None, None, 'parm', 'constant_weight', None, 1, [-sys.maxint,sys.maxint], 'Default weight of constants.'],
        [None, None, None, 'parm', 'not_weight', None, 0, [-sys.maxint,sys.maxint], 'Weight of the negation symbol.'],
        [None, None, None, 'parm', 'or_weight', None, 0, [-sys.maxint,sys.maxint], 'Weight of the disjunction symbol.'],
        [None, None, None, 'parm', 'sk_constant_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of Skolem constants.  This option can be useful, because Skolem constants cannot appear in weighting rules.'],
        [None, None, None, 'parm', 'prop_atom_weight', None, 1, [-sys.maxint,sys.maxint], 'Weight of propositional atoms.'],

        [None, None, None, 'group', 'Penalties', 'right'],
        [None, None, None, 'parm', 'skolem_penalty', None, 1, [0,sys.maxint], 'If a term contains a (non-constant) Skolem function, its weight is multiplied by this value.'],
        [None, None, None, 'parm', 'nest_penalty', None, 0, [0,sys.maxint], 'For each nest of two identical function symbols, e.g., f(f(x,y),z), this value is added tot he weight of the term.'],
        [None, None, None, 'parm', 'depth_penalty', None, 0, [-sys.maxint,sys.maxint], 'After the weight of clause C is calculated, its weight is increased by depth(C) * this_value.'],
        [None, None, None, 'parm', 'var_penalty', None, 0, [-sys.maxint,sys.maxint], 'After the weight of clause C is calculated, its weight is increased by number_of_vars(C) * this_value.'],

        [None, None, None, 'group', 'Others', 'right'],
        [None, None, None, 'parm', 'default_weight', None, sys.maxint, [-sys.maxint,sys.maxint], ''],
        ]),

        ('Process Inferred', 
        [
        [None, None, None, 'flag', 'safe_unit_conflict', None, 0, None, 'In some cases, a proof may be missed because a newly-derived clause is deleted by a limit such as max_weight.  This flag eliminates some of those cases.'],
        [None, None, None, 'flag', 'back_subsume', None, 1, None, 'When a newly-derived clause C is kept, discard all old clauses that are subsumed by C.'],
        ]),

        ('Input/Output', 
        [
#       [None, None, None, 'flag', 'echo_input', None, 1, None, ''],
#       [None, None, None, 'flag', 'bell', None, 1, None, ''],
#       [None, None, None, 'flag', 'quiet', None, 0, None, ''],
        [None, None, None, 'flag', 'print_initial_clauses', None, 1, None, 'Show clauses after preprocessing, before the start of the search.'],
        [None, None, None, 'flag', 'print_given', None, 1, None, 'Print clauses when they are selected as given clauses.  These clauses say a lot about the progress of the search.'],
        [None, None, None, 'flag', 'print_gen', None, 0, None, 'Print all newly-derived clauses.  This flag can cause an enormous amount of output for nontrivial searches.'],
        [None, None, None, 'flag', 'print_kept', None, 0, None, 'Print newly-derived clauses if they pass the retention tests.'],
        [None, None, None, 'flag', 'print_labeled', None, 0, None, 'Print newly-kept clauses that have labels.'],
        [None, None, None, 'flag', 'print_proofs', None, 1, None, 'Print all proofs that are found.'],
#       [None, None, None, 'flag', 'default_output', None, 1, None, ''],
        [None, None, None, 'flag', 'print_clause_properties', None, 0, None, 'When a clause is printed, show some if its syntactic properties (mostly for debugging).'],
        [None, None, None, 'stringparm', 'stats', None, 'lots', ['none', 'some', 'lots', 'all'], 'How many statistics should be printed at the end of the perch and in "reports".'],
        [None, None, None, 'parm', 'report', None, -1, [-1,sys.maxint], 'Output a statistics report every n seconds.'],
#       [None, None, None, 'parm', 'report_stderr', None, -1, [-1,sys.maxint], ''],
        [None, None, None, 'flag', 'prolog_style_variables', None, 0, None, 'Variables start with upper case instead of starting with u,v,w,x,y,z.'],
        [None, None, None, 'stringparm', 'Proof_Format', None, 'standard', ['standard', 'parents_only', 'xml', 'hints', 'ivy'], 'Format for proofs.  This option is different from the others in that it is used by the postprocessor "prooftrans" rather than by Prover9.  This option is not given to Prover9 and is therefore not saved by "File->Save".'],
        ]),

        ('Hints', 
        [
        [None, None, None, 'flag', 'limit_hint_matchers', None, 0, None, 'Apply the parameters max_weight, max_vars, max_depth, and max_literals to clauses that match hints (as well as to those that do not match hints).'],
        [None, None, None, 'flag', 'collect_hint_labels', None, 0, None, 'When equivalent hints are input, only the first is kept.  This flag causes any labels on the discarded hints to be appended to the retained hint.'],
        [None, None, None, 'flag', 'degrade_hints', None, 1, None, 'The more times a hint is matched, the less its effect becomes.'],
        [None, None, None, 'flag', 'back_demod_hints', None, 1, None, 'This flag causes hints, as well as ordinary clauses, to be rewritten by newly-derived equations.'],
        ]),

        ('Other Options', 
        [
        [None, None, None, 'parm', 'random_seed', None, 0, [-1,sys.maxint], 'Seed for random number generation.'],
        ]),
        ]

    def output_transformed(self):
        print '    options_sets = ['
        for (name,options) in self.option_sets:
            print "\n        ('%s', " % name
            output_trans(options)
            print "),"
        print "        ]"
        
    def __init__(self, parent):
        """ Use the option_set table to build adictionary, indexed by
        set name, of (hidden) options panels.
        """
        panels = {}
        for (name,options) in self.option_sets:
            panels[name] = Options_panel(parent, name, None, options)
            panels[name].Show(False)  # start out hidden
        # find and mark the shared options
        for (_,options1) in self.option_sets:
            for opt1 in options1:
                if opt1[Type] in ['flag', 'parm', 'stringparm']:
                    for (_,options2) in self.option_sets:
                        for opt2 in options2:
                            if (opt1[Type] == opt2[Type] and
                                opt1[Name] == opt2[Name] and
                                not opt1 in opt2[Share]):

                                link_options(opt1, opt2)
                                # print 'Share:'; print_sharing(opt1)
                                # print '      '; print_sharing(opt2)
        self.panels = panels

    def optionset_names(self):
        result = []
        for (name,_) in self.option_sets:
            result.append(name)
        return result

    def nondefaults(self):
        triples = []
        # order:  1,2,3,...,0  (because "basic" should be last)
        for (_,options) in self.option_sets[1:]:
            triples = nondefault_options(options, triples)
        triples = nondefault_options(self.option_sets[0][1], triples)
        # always include max_seconds, because GUI default is not program default
        if not option_triples_contains_name(triples, 'max_seconds'):
            opt = self.name_to_opt('max_seconds')
            if opt:
                triples.append((opt[Type],opt[Name],opt[Value]))
        return triples

    def name_to_opt(self, name):
        for (_,options) in self.option_sets:
            opt = name_to_option(name, options)
            if opt:
                return opt
        return None

    def share_external_option(self, external_opt):
        local_opt = self.name_to_opt(external_opt[Name])
        if not local_opt:
            error_dialog('share_external_option(P4), not found')
        else:
            link_options(local_opt, external_opt)
            # print 'External(P9):'; print_sharing(local_opt)
            # print '             '; print_sharing(external_opt)

    def reset(self):
        for key in self.panels.keys():
            self.panels[key].on_reset(None)

# end class P9_options

def set_options(opt_str, opt_class):

    not_handled = ''

    pat_flag = '(set|clear)\s*\(\s*([a-z0-9_]+)\s*\)'  # without period
    r_flag = re.compile(pat_flag)

    pat_parm = 'assign\s*\(\s*([a-z0-9_]+)\s*,\s*([a-z0-9_-]+)\s*\)'  # without period
    r_parm = re.compile(pat_parm)

    opts = opt_str.split('.')[:-1]  # no option after last period
    for command in opts:
        m = r_flag.match(command)
        if m:
            (op,name) = m.groups()
            opt = opt_class.name_to_opt(name)
            if opt and opt[Type] == 'flag':
                update_option(opt, op == 'set')
                update_shared(opt)
            else:
                not_handled += command + '.\n'
        else:
            m = r_parm.match(command)
            if m:
                (name,string_val) = m.groups()
                try:
                    value = int(string_val)
                    opt_type = 'parm'
                except:
                    value = string_val
                    opt_type = 'stringparm'
                opt = opt_class.name_to_opt(name)
                if opt and opt[Type] == opt_type:
                    update_option(opt, value)
                    update_shared(opt)
                else:
                    not_handled += command + '.\n'
            else:
                not_handled += command + '.\n'
    return not_handled
    
def opt_intersect(s1, s2):
    t1 = s1.split('.\n')
    t2 = s2.split('.\n')
    y = utilities.intersect(t1, t2)
    return '.\n'.join(y)
    
def set_options_either(opt_str, class1, class2):
    x1 = set_options(opt_str, class1)
    x2 = set_options(opt_str, class2)
    # (x1 intersect x2) was handled by neither
    return opt_intersect(x1,x2)