« back to all changes in this revision
Viewing changes to mace4.src/msearch.c~
- browse files at revision 11
- compare with another revision
- download diff
- download tarball
- view history from revision 11
- Committer: Package Import Robot
- Author(s): Frank Lichtenheld
- Date: 2013-05-25 11:43:32 UTC
- mfrom: (5.1.5 sid)
- Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.
* Upload to unstable.
* Change maintainer to QA group.
- files added:
- .pc
- .pc/01-libtoolise.patch
- .pc/01-libtoolise.patch/apps.src
- .pc/01-libtoolise.patch/ladr
- .pc/01-libtoolise.patch/mace4.src
- .pc/01-libtoolise.patch/provers.src
- .pc/01-libtoolise.patch/test.src
- .pc/03-no-2.5isms.patch
- .pc/03-no-2.5isms.patch/utilities
- debian/source
- files removed:
- Changelog.save
- files modified:
- Changelog
added
removed
mace4.src/msearch.c~
1
/* Copyright (C) 2006, 2007 William McCune
2
3
This file is part of the LADR Deduction Library.
4
5
The LADR Deduction Library is free software; you can redistribute it
6
and/or modify it under the terms of the GNU General Public License,
7
version 2.
8
9
The LADR Deduction Library is distributed in the hope that it will be
10
useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12
GNU General Public License for more details.
13
14
You should have received a copy of the GNU General Public License
15
along with the LADR Deduction Library; if not, write to the Free Software
16
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
17
*/
18
19
#include "msearch.h"
20
#include "../ladr/banner.h"
21
22
// #define DEBUG
23
24
/*****************************************************************************/
25
/* Variables -- most are used (extern) by other source files */
26
27
/* Options and Statistics */
28
29
Mace_options Opt;
30
struct mace_stats Mstats;
31
32
/* List of symbols and associated data */
33
34
Symbol_data Symbols;
35
36
/* This maps OPS symbol IDs to MACE symbol IDs, which start with 0. */
37
38
static int Sn_map_size;
39
Symbol_data *Sn_to_mace_sn;
40
41
/* Cell table is indexed by eterm IDs. */
42
43
int Number_of_cells;
44
struct cell *Cells; /* the table of cells (dynamically allocated) */
45
struct cell **Ordered_cells; /* (pointers to) permutation of Cells */
46
int First_skolem_cell;
47
48
/* Misc Variables*/
49
50
int Domain_size;
51
Term *Domain; /* array of terms representing (shared) domain elements */
52
BOOL Skolems_last;
53
54
Plist Ground_clauses; /* Mclauses (see ground.h) */
55
56
int Relation_flag; /* term flag */
57
int Negation_flag; /* term flag */
58
59
int Eq_sn;
60
int Or_sn;
61
int Not_sn;
62
63
static int Max_domain_element_in_input; /* For Least Number Heuristic */
64
65
static Plist Models; /* in case we collect models as terms */
66
67
Clock Mace4_clock;
68
69
/* stats for entire run */
70
71
unsigned Total_models;
72
73
static double Start_seconds;
74
static double Start_domain_seconds;
75
static int Start_megs;
76
77
/* end of variables */
78
/*****************************************************************************/
79
80
/* search return codes */
81
82
enum {
83
SEARCH_GO_MODELS, /* continue: model(s) found on current path */
84
SEARCH_GO_NO_MODELS, /* continue: no models found on current path */
85
SEARCH_MAX_MODELS, /* stop */
86
SEARCH_MAX_MEGS, /* stop */
87
SEARCH_MAX_TOTAL_SECONDS, /* stop */
88
SEARCH_MAX_DOMAIN_SECONDS, /* stop */
89
SEARCH_DOMAIN_OUT_OF_RANGE /* stop */
90
};
91
92
/* Ground terms. MACE4 operates on ground clauses, which are
93
represented by the structure mclause. Ground terms (and
94
atoms) are represented with ordinary LADR terms. There are
95
a few tricks:
96
97
(1) We use upward pointers from terms to superterms
98
and from atoms to clauses.
99
100
(2) We need to mark atoms with a termflag, so that we know
101
when to stop when following the upward pointers. Also,
102
a termflag is used to indicate that an atom is negated.
103
104
(3) Domain elements are represented by variables (sorry,
105
but it is very convenient to do so). Also, there is only
106
one actual copy of each domain element (structure sharing
107
of domain elements). Global array *Domain contains them.
108
109
IDs. If all of the arguments of a term (including atoms) are
110
domain elements, that term is called an eterm. For example,
111
f(3,4), a, P(0), and Q.
112
113
Each eterm has a unique ID which is used as an index into
114
the cell table, for example, when a new eterm is obtained by
115
evaluating a subterm to a domain element, we have to quickly
116
check if this new eterm can be evaluated. We do this by
117
calculating its ID and looking up in Cells[ID].value.
118
And when we have a new assignment, say f(3,4)=2, we find the
119
list of occurrences of f(3,4) by looking in Cells[ID].occurrences.
120
*/
121
122
/*************
123
*
124
* init_mace_options()
125
*
126
*************/
127
128
/* DOCUMENTATION
129
*/
130
131
/* PUBLIC */
132
void init_mace_options(Mace_options opt)
133
{
134
opt->domain_size = init_parm("domain_size", 0, 0, INT_MAX);
135
opt->start_size = init_parm("start_size", 2, 2, INT_MAX);
136
opt->end_size = init_parm("end_size", -1, -1, INT_MAX);
137
opt->iterate_up_to = init_parm("iterate_up_to", -1, -1, INT_MAX);
138
opt->max_models = init_parm("max_models", 1, -1, INT_MAX);
139
opt->max_seconds = init_parm("max_seconds", -1, -1, INT_MAX);
140
opt->max_seconds_per = init_parm("max_seconds_per", -1, -1, INT_MAX);
141
opt->selection_order = init_parm("selection_order", 2, 0, 2);
142
opt->selection_measure = init_parm("selection_measure",4, 0, 4);
143
opt->increment = init_parm("increment", 1, 1, INT_MAX);
144
opt->max_megs = init_parm("max_megs", 200, -1, INT_MAX);
145
opt->report_stderr = init_parm("report_stderr", -1, -1, INT_MAX);
146
147
opt->print_models = init_flag("print_models", TRUE);
148
opt->print_models_tabular = init_flag("print_models_tabular", FALSE);
149
opt->lnh = init_flag("lnh", TRUE);
150
opt->trace = init_flag("trace", FALSE);
151
opt->negprop = init_flag("negprop", TRUE);
152
opt->neg_assign = init_flag("neg_assign", TRUE);
153
opt->neg_assign_near = init_flag("neg_assign_near", TRUE);
154
opt->neg_elim = init_flag("neg_elim", TRUE);
155
opt->neg_elim_near = init_flag("neg_elim_near", TRUE);
156
opt->verbose = init_flag("verbose", FALSE);
157
opt->integer_ring = init_flag("integer_ring", FALSE);
158
opt->order_domain = init_flag("order_domain", FALSE);
159
opt->arithmetic = init_flag("arithmetic", FALSE);
160
opt->iterate_primes = init_flag("iterate_primes", FALSE);
161
opt->iterate_nonprimes = init_flag("iterate_nonprimes", FALSE);
162
opt->skolems_last = init_flag("skolems_last", FALSE);
163
opt->return_models = init_flag("return_models", FALSE);
164
165
opt->iterate = init_stringparm("iterate", 5,
166
"all",
167
"evens",
168
"odds",
169
"primes",
170
"nonprimes");
171
172
/* dependencies */
173
174
flag_flag_dependency(opt->print_models_tabular,TRUE,opt->print_models,FALSE);
175
flag_flag_dependency(opt->print_models,TRUE,opt->print_models_tabular,FALSE);
176
177
flag_flag_dependency(opt->iterate_primes, TRUE,opt->iterate_nonprimes,FALSE);
178
flag_flag_dependency(opt->iterate_nonprimes, TRUE,opt->iterate_primes,FALSE);
179
180
parm_parm_dependency(opt->domain_size, opt->start_size, 1, TRUE);
181
parm_parm_dependency(opt->domain_size, opt->end_size, 1, TRUE);
182
183
parm_parm_dependency(opt->iterate_up_to, opt->end_size, 1, TRUE);
184
185
flag_stringparm_dependency(opt->iterate_primes,TRUE,opt->iterate,"primes");
186
flag_stringparm_dependency(opt->iterate_nonprimes,TRUE,opt->iterate,"nonprimes");
187
188
flag_flag_dependency(opt->integer_ring, TRUE, opt->lnh, FALSE);
189
flag_flag_dependency(opt->order_domain, TRUE, opt->lnh, FALSE);
190
flag_flag_dependency(opt->arithmetic, TRUE, opt->lnh, FALSE);
191
192
flag_parm_dependency(opt->arithmetic,TRUE,opt->selection_order,0);
193
194
} /* init_mace_options */
195
196
/*************
197
*
198
* exit_string()
199
*
200
*************/
201
202
static
203
char *exit_string(int code)
204
{
205
char *message;
206
switch (code) {
207
case MAX_MODELS_EXIT: message = "max_models"; break;
208
case ALL_MODELS_EXIT: message = "all_models"; break;
209
case EXHAUSTED_EXIT: message = "exhausted"; break;
210
case MAX_MEGS_YES_EXIT: message = "max_megs_yes"; break;
211
case MAX_MEGS_NO_EXIT: message = "max_megs_no" ; break;
212
case MAX_SEC_YES_EXIT: message = "max_sec_yes"; break;
213
case MAX_SEC_NO_EXIT: message = "max_sec_no"; break;
214
case MACE_SIGINT_EXIT: message = "mace_sigint"; break;
215
case MACE_SIGSEGV_EXIT: message = "mace_sigsegv"; break;
216
default: message = "???";
217
}
218
return message;
219
} /* exit_string */
220
221
/*************
222
*
223
* mace4_exit()
224
*
225
*************/
226
227
void mace4_exit(int exit_code)
228
{
229
if (Opt && flag(Opt->verbose))
230
p_mem();
231
232
if (Opt && parm(Opt->report_stderr) > 0)
233
fprintf(stderr, "Domain_size=%d. Models=%d. User_CPU=%.2f.\n",
234
Domain_size, Total_models, user_seconds());
235
236
printf("\nUser_CPU=%.2f, System_CPU=%.2f, Wall_clock=%d.\n",
237
user_seconds(), system_seconds(), wallclock());
238
239
if (Total_models == 0)
240
printf("\nExiting with failure.\n");
241
else
242
printf("\nExiting with %d model%s.\n",
243
Total_models, Total_models == 1 ? "" : "s");
244
245
fprintf(stderr, "\n------ process %d exit (%s) ------\n",
246
my_process_id(), exit_string(exit_code));
247
printf("\nProcess %d exit (%s) %s",
248
my_process_id(), exit_string(exit_code), get_date());
249
250
printf("The process finished %s", get_date());
251
exit(exit_code);
252
} /* mace4_exit */
253
254
/*************
255
*
256
* initialize_for_search()
257
*
258
* This is the initialization that has to be done only once
259
* for a given set of clauses. It is independent of the
260
* domain size.
261
*
262
*************/
263
264
static
265
void initialize_for_search(Plist clauses)
266
{
267
int max, i;
268
Symbol_data s;
269
270
Mace4_clock = clock_init("Mace4");
271
272
/* In ground clauses, VARIABLEs represent domain elements,
273
so from here on, print variables as integers. */
274
275
// set_variable_style(INTEGER_STYLE);
276
277
/* These flags are for ground clause (mclause) literals. */
278
279
Relation_flag = claim_term_flag();
280
Negation_flag = claim_term_flag();
281
282
/* Cache some symbol numbers. */
283
284
Eq_sn = str_to_sn(eq_sym(), 2);
285
Or_sn = str_to_sn(or_sym(), 2);
286
Not_sn = str_to_sn(not_sym(), 1);
287
288
/* Set up Symbols list. */
289
290
init_built_in_symbols(); /* =/2 (and maybe others) */
291
292
/* Maybe initialize for arithmetic. */
293
294
if (flag(Opt->arithmetic))
295
init_arithmetic();
296
297
Skolems_last = flag(Opt->skolems_last);
298
299
/* Collect data for each symbol. */
300
301
Max_domain_element_in_input = -1;
302
i = collect_mace4_syms(clauses, flag(Opt->arithmetic));
303
Max_domain_element_in_input = MAX(Max_domain_element_in_input, i);
304
305
if (Max_domain_element_in_input == -1)
306
printf("\n%% There are no natural numbers in the input.\n");
307
else
308
printf("\n%% The largest natural number in the input is %d.\n",
309
Max_domain_element_in_input);
310
311
/* Set up map from ordinary symnums to mace symnums. */
312
313
max = 0;
314
i = 0;
315
316
for (s = Symbols; s != NULL; s = s->next) {
317
s->mace_sn = i++;
318
/* printf("mace symbol: %s/%d\n", sn_to_str(s->sn), sn_to_arity(s->sn)); */
319
max = (s->sn > max ? s->sn : max);
320
}
321
322
Sn_map_size = max+1;
323
324
Sn_to_mace_sn = malloc(Sn_map_size * sizeof(void *));
325
326
for (i = 0; i < Sn_map_size; i++)
327
Sn_to_mace_sn[i] = NULL;
328
329
for (s = Symbols; s != NULL; s = s->next) {
330
Sn_to_mace_sn[s->sn] = s;
331
}
332
} /* initialize_for_search */
333
334
/*************
335
*
336
* init_for_domain_size()
337
*
338
* Given the list of (general) clauses, set up the various data
339
* structures that will be needed for a given domain size.
340
*
341
*************/
342
343
static
344
void init_for_domain_size(void)
345
{
346
int i, j, nextbase, id;
347
Symbol_data s;
348
349
/* Give each symbol its "base" value, which is used to index cells. */
350
351
nextbase = 0;
352
for (s = Symbols; s != NULL; s = s->next) {
353
s->base = nextbase;
354
nextbase += int_power(Domain_size, s->arity);
355
}
356
357
/* Set up the array of domain terms. All ground terms refer to these. */
358
359
Domain = malloc(Domain_size * sizeof(void *));
360
for (i = 0; i < Domain_size; i++)
361
Domain[i] = get_variable_term(i);
362
363
/* Set up the table of cells. */
364
365
Number_of_cells = nextbase;
366
Cells = malloc(Number_of_cells * sizeof(struct cell));
367
Ordered_cells = malloc(Number_of_cells * sizeof(void *));
368
369
for (id = 0; id < Number_of_cells; id++) {
370
struct cell *c = Cells + id;
371
int n;
372
c->id = id;
373
c->occurrences = NULL;
374
c->value = NULL;
375
c->symbol = find_symbol_node(id);
376
c->eterm = decode_eterm_id(id);
377
c->max_index = max_index(id, c->symbol);
378
n = id_to_domain_size(id);
379
c->possible = malloc(n * sizeof(void *));
380
for (j = 0; j < n; j++)
381
c->possible[j] = Domain[j]; /* really just a flag */
382
}
383
384
order_cells(flag(Opt->verbose));
385
386
if (flag(Opt->negprop))
387
init_negprop_index();
388
} /* init_for_domain_size */
389
390
/*************
391
*
392
* built_in_assignments()
393
*
394
*************/
395
396
static
397
void built_in_assignments(void)
398
{
399
Symbol_data s;
400
for (s = Symbols; s != NULL; s = s->next) {
401
if (s->attribute == EQUALITY_SYMBOL) {
402
int i, j;
403
for (i = 0; i < Domain_size; i++)
404
for (j = 0; j < Domain_size; j++)
405
Cells[X2(s->base,i,j)].value = (Domain[i==j ? 1 : 0]);
406
}
407
}
408
} /* built_in_assignments */
409
410
/*************
411
*
412
* special_assignments()
413
*
414
*************/
415
416
static
417
void special_assignments(void)
418
{
419
if (flag(Opt->integer_ring)) {
420
/* Fix [+,-,*] as the ring of integers mod domain_size. */
421
/* If any of those operations doesn't exist, then ignore it.*/
422
Symbol_data s;
423
for (s = Symbols; s != NULL; s = s->next) {
424
int i, j;
425
if (is_symbol(s->sn, "+", 2)) {
426
for (i = 0; i < Domain_size; i++)
427
for (j = 0; j < Domain_size; j++)
428
Cells[X2(s->base,i,j)].value = Domain[(i + j) % Domain_size];
429
}
430
else if (is_symbol(s->sn, "*", 2)) {
431
for (i = 0; i < Domain_size; i++)
432
for (j = 0; j < Domain_size; j++)
433
Cells[X2(s->base,i,j)].value = Domain[(i * j) % Domain_size];
434
}
435
else if (is_symbol(s->sn, "-", 1)) {
436
for (i = 0; i < Domain_size; i++)
437
Cells[X1(s->base,i)].value = Domain[(Domain_size - i) % Domain_size];
438
}
439
else if (is_symbol(s->sn, "--", 2)) {
440
for (i = 0; i < Domain_size; i++)
441
for (j = 0; j < Domain_size; j++)
442
Cells[X2(s->base,i,j)].value = Domain[((i + Domain_size) - j) %
443
Domain_size];
444
}
445
}
446
}
447
if (flag(Opt->order_domain)) {
448
Symbol_data s;
449
for (s = Symbols; s != NULL; s = s->next) {
450
int i, j;
451
if (is_symbol(s->sn, "<", 2)) {
452
for (i = 0; i < Domain_size; i++)
453
for (j = 0; j < Domain_size; j++)
454
Cells[X2(s->base,i,j)].value = (Domain[i<j ? 1 : 0]);
455
}
456
if (is_symbol(s->sn, "<=", 2)) {
457
for (i = 0; i < Domain_size; i++)
458
for (j = 0; j < Domain_size; j++)
459
Cells[X2(s->base,i,j)].value = (Domain[i<=j ? 1 : 0]);
460
}
461
}
462
}
463
} /* special_assignments */
464
465
/*************
466
*
467
* check_that_ground_clauses_are_true()
468
*
469
*************/
470
471
static
472
BOOL check_that_ground_clauses_are_true(void)
473
{
474
Plist g;
475
BOOL ok = TRUE;
476
for (g = Ground_clauses; g != NULL; g = g->next) {
477
Mclause c = g->v;
478
if (!c->subsumed) {
479
fprintf(stderr, "ERROR, model reported, but clause not true!\n");
480
fprintf(stdout, "ERROR, model reported, but clause not true! ");
481
p_mclause(c);
482
ok = FALSE;
483
}
484
}
485
return ok;
486
} /* check_that_ground_clauses_are_true */
487
488
/*************
489
*
490
* possible_model()
491
*
492
*************/
493
494
static
495
int possible_model(void)
496
{
497
if (flag(Opt->arithmetic)) {
498
if (!check_with_arithmetic(Ground_clauses))
499
return SEARCH_GO_NO_MODELS;
500
}
501
else if (!check_that_ground_clauses_are_true())
502
fatal_error("possible_model, bad model found");
503
504
{
505
static int next_message = 1;
506
Total_models++;
507
Mstats.current_models++;
508
509
if (flag(Opt->return_models)) {
510
Term modelterm = interp_term();
511
Interp model = compile_interp(modelterm, FALSE);
512
zap_term(modelterm);
513
Models = plist_append(Models, model);
514
}
515
516
if (flag(Opt->print_models))
517
print_model_standard(stdout, TRUE);
518
else if (flag(Opt->print_models_tabular))
519
p_model(FALSE);
520
else if (next_message == Total_models) {
521
printf("\nModel %d has been found.\n", Total_models);
522
next_message *= 10;
523
}
524
fflush(stdout);
525
if (parm(Opt->max_models) != -1 && Total_models >= parm(Opt->max_models))
526
return SEARCH_MAX_MODELS;
527
else
528
return SEARCH_GO_MODELS;
529
}
530
} /* possible_model */
531
532
/*************
533
*
534
* mace_megs()
535
*
536
*************/
537
538
static
539
int mace_megs(void)
540
{
541
return (megs_malloced() - Start_megs) + (estack_bytes() / (1024*1024));
542
} /* mace_megs */
543
544
/*************
545
*
546
* check_time_memory()
547
*
548
*************/
549
550
static
551
int check_time_memory(void)
552
{
553
static int Next_report;
554
555
double seconds = user_seconds();
556
int max_seconds = parm(Opt->max_seconds);
557
int max_seconds_per = parm(Opt->max_seconds_per);
558
int max_megs = parm(Opt->max_megs);
559
int report = parm(Opt->report_stderr);
560
561
if (max_seconds != -1 && seconds - Start_seconds > max_seconds)
562
return SEARCH_MAX_TOTAL_SECONDS;
563
else if (max_seconds_per != -1 &&
564
seconds - Start_domain_seconds > parm(Opt->max_seconds_per))
565
return SEARCH_MAX_DOMAIN_SECONDS;
566
else if (max_megs != -1 && mace_megs() > parm(Opt->max_megs))
567
return SEARCH_MAX_MEGS;
568
else {
569
if (report > 0) {
570
if (Next_report == 0)
571
Next_report = parm(Opt->report_stderr);
572
if (seconds >= Next_report) {
573
fprintf(stderr, "Domain_size=%d. Models=%d. User_CPU=%.2f.\n", Domain_size, Total_models, seconds);
574
fflush(stderr);
575
while (seconds >= Next_report)
576
Next_report += report;
577
}
578
}
579
return SEARCH_GO_NO_MODELS;
580
}
581
} /* check_time_memory */
582
583
/*************
584
*
585
* mace4_skolem_check()
586
*
587
*************/
588
589
static
590
BOOL mace4_skolem_check(int id)
591
{
592
/* Should we keep going w.r.t. the Skolem restriction? */
593
if (!flag(Opt->skolems_last))
594
return TRUE;
595
else if (Cells[id].symbol->attribute == SKOLEM_SYMBOL) {
596
printf("pruning\n");
597
return FALSE;
598
}
599
else
600
return TRUE;
601
} /* mace4_skolem_check */
602
603
/*************
604
*
605
* p_possible_values()
606
*
607
*************/
608
609
#if 0
610
static
611
void p_possible_values(void)
612
{
613
int i;
614
for (i = 0; i < Number_of_cells; i++) {
615
if (Cells[i].symbol->attribute == ORDINARY_SYMBOL) {
616
int j;
617
printf("Cell %d: ", i);
618
for (j = 0; j < id_to_domain_size(i); j++) {
619
if (Cells[i].possible[j] != NULL)
620
printf(" %d", j);
621
}
622
printf("\n");
623
}
624
}
625
} /* p_possible_values */
626
#endif
627
628
/*************
629
*
630
* search()
631
*
632
* Max_constrained is the maximum constrained domain element
633
* (or -1 is none is constrained). Greater domain elements
634
* can all be considered symmetric. An element can become
635
* constrained in two ways: (1) it is an index of some selected
636
* cell, or (2) it is the value assigned to some selected cell.
637
* (Propagation does not constrain elements. This might need
638
* careful justification.)
639
*
640
* To apply the least number heuristic, we consider values
641
* 0 ... MIN(max_constrained+1, Domain_size-1).
642
*
643
* To make this effective, we should keep max_constrained as low as
644
* possible by selecting cells with maximum index <= max_constrained.
645
*
646
* return:
647
* SEARCH_GO_MODELS
648
* SEARCH_GO_NO_MODELS
649
* SEARCH_MAX_MODELS
650
* SEARCH_MAX_MEGS
651
* SEARCH_MAX_TOTAL_SECONDS
652
* SEARCH_MAX_DOMAIN_SECONDS
653
*
654
*************/
655
656
static
657
int search(int max_constrained, int depth)
658
{
659
int id;
660
BOOL go;
661
int rc = check_time_memory();
662
if (rc != SEARCH_GO_NO_MODELS)
663
return rc;
664
else {
665
id = select_cell(max_constrained);
666
if (id == -1) {
667
rc = possible_model();
668
return rc;
669
}
670
else {
671
int i, last; /* we'll do 0 .. last */
672
int x = Cells[id].max_index;
673
max_constrained = MAX(max_constrained, x);
674
Mstats.selections++;
675
676
if (flag(Opt->trace)) {
677
printf("select: ");
678
p_model(FALSE);
679
/* p_possible_values(); */
680
}
681
682
if (Cells[id].symbol->type == RELATION)
683
last = 1;
684
else if (flag(Opt->lnh))
685
last = MIN(max_constrained+1, Domain_size-1);
686
else
687
last = Domain_size-1;
688
689
for (i = 0, go = TRUE; i <= last && go; i++) {
690
Estack stk;
691
Mstats.assignments++;
692
693
if (flag(Opt->trace)) {
694
printf("assign: ");
695
fwrite_term(stdout, Cells[id].eterm);
696
printf("=%d (%d) depth=%d\n", i, last, depth);
697
}
698
699
stk = assign_and_propagate(id, Domain[i]);
700
701
if (stk != NULL) {
702
/* no contradiction found during propagation, so we recurse */
703
rc = search(MAX(max_constrained, i), depth+1);
704
/* undo assign_and_propagate changes */
705
restore_from_stack(stk);
706
if (rc == SEARCH_GO_MODELS)
707
go = mace4_skolem_check(id);
708
else
709
go = (rc == SEARCH_GO_NO_MODELS);
710
}
711
}
712
return rc;
713
}
714
}
715
} /* search */
716
717
/*************
718
*
719
* mace4n() -- look for a model of a specific size
720
*
721
*************/
722
723
static
724
int mace4n(Plist clauses, int order)
725
{
726
Plist p, g;
727
int i, rc;
728
Mstate initial_state = get_mstate();
729
730
Variable_style save_style = variable_style();
731
set_variable_style(INTEGER_STYLE);
732
733
if (Max_domain_element_in_input >= order) {
734
if (flag(Opt->arithmetic)) {
735
if (!ok_for_arithmetic(clauses, order))
736
return SEARCH_DOMAIN_OUT_OF_RANGE;
737
}
738
else
739
return SEARCH_DOMAIN_OUT_OF_RANGE;
740
}
741
742
Domain_size = order;
743
744
init_for_domain_size();
745
746
built_in_assignments(); /* Fill out equality table (and maybe others). */
747
748
special_assignments(); /* assignments determined by options */
749
750
/* Instantiate clauses over the domain. This also
751
(1) makes any domain element constants into real domain elements,
752
(2) applies OR, NOT, and EQ simplification, and
753
(3) does unit propagation (which pushes events onto initial_state->stack).
754
Do the units first, then the 2-clauses, then the rest. */
755
756
for (p = clauses; initial_state->ok && p != NULL; p = p->next)
757
if (number_of_literals(p->v) < 2)
758
generate_ground_clauses(p->v, initial_state);
759
760
for (p = clauses; initial_state->ok && p != NULL; p = p->next)
761
if (number_of_literals(p->v) == 2)
762
generate_ground_clauses(p->v, initial_state);
763
764
for (p = clauses; initial_state->ok && p != NULL; p = p->next)
765
if (number_of_literals(p->v) > 2)
766
generate_ground_clauses(p->v, initial_state);
767
768
/* The preceding calls push propagation events onto initial_state->stack.
769
We won't have to undo those initial events during the search,
770
but we can undo them after the search.
771
*/
772
773
if (flag(Opt->verbose)) {
774
printf("\nInitial partial model:\n");
775
p_model(FALSE);
776
fflush(stdout);
777
}
778
779
/* Here we go! */
780
781
if (initial_state->ok)
782
rc = search(Max_domain_element_in_input, 0);
783
else
784
rc = SEARCH_GO_NO_MODELS; /* contradiction in initial state */
785
786
/* Free all of the memory associated with the current domain size. */
787
788
restore_from_stack(initial_state->stack);
789
free_mstate(initial_state);
790
791
if (flag(Opt->negprop))
792
free_negprop_index();
793
794
free(Ordered_cells);
795
Ordered_cells = NULL;
796
797
for (i = 0; i < Number_of_cells; i++) {
798
zap_mterm(Cells[i].eterm);
799
free(Cells[i].possible);
800
}
801
free(Cells);
802
Cells = NULL;
803
804
for (i = 0; i < Domain_size; i++)
805
zap_term(Domain[i]);
806
free(Domain);
807
Domain = NULL;
808
809
for (g = Ground_clauses; g != NULL; g = g->next)
810
zap_mclause(g->v);
811
zap_plist(Ground_clauses);
812
Ground_clauses = NULL;
813
814
set_variable_style(save_style);
815
return rc;
816
} /* mace4n */
817
818
/*************
819
*
820
* iterate_ok()
821
*
822
*************/
823
824
static
825
BOOL iterate_ok(int n, char *class)
826
{
827
if (str_ident(class, "all"))
828
return TRUE;
829
else if (str_ident(class, "evens"))
830
return n % 2 == 0;
831
else if (str_ident(class, "odds"))
832
return n % 2 == 1;
833
else if (str_ident(class, "primes"))
834
return prime(n);
835
else if (str_ident(class, "nonprimes"))
836
return !prime(n);
837
else {
838
fatal_error("iterate_ok, unknown class");
839
return FALSE; /* to please compiler */
840
}
841
} /* iterate_ok */
842
843
/*************
844
*
845
* next_domain_size()
846
*
847
*************/
848
849
static
850
int next_domain_size(n)
851
{
852
int top = (parm(Opt->end_size) == -1 ? INT_MAX : parm(Opt->end_size));
853
854
if (n == 0)
855
n = parm(Opt->start_size); /* first call */
856
else
857
n += parm(Opt->increment);
858
859
while (!iterate_ok(n, stringparm1(Opt->iterate)))
860
n += parm(Opt->increment);
861
862
return (n > top ? -1 : n);
863
} /* next_domain_size */
864
865
/*************
866
*
867
* mace4()
868
*
869
*************/
870
871
/* DOCUMENTATION
872
*/
873
874
/* PUBLIC */
875
Mace_results mace4(Plist clauses, Mace_options opt)
876
{
877
int n, rc;
878
Mace_results results = malloc(sizeof(struct mace_results));
879
880
disable_max_megs(); /* mace4 does its own max_megs check */
881
Start_seconds = user_seconds();
882
Start_megs = megs_malloced();
883
884
Opt = opt; /* put options into a global variable */
885
initialize_for_search(clauses);
886
887
n = next_domain_size(0); /* returns -1 if we're done */
888
rc = SEARCH_GO_NO_MODELS;
889
890
while (n >= 2 && (rc == SEARCH_GO_NO_MODELS || rc == SEARCH_GO_MODELS)) {
891
char str[20];
892
sprintf(str, "DOMAIN SIZE %d", n);
893
print_separator(stdout, str, TRUE);
894
fflush(stdout);
895
fprintf(stderr,"\n=== Mace4 starting on domain size %d. ===\n",n);
896
897
Start_domain_seconds = user_seconds();
898
clock_start(Mace4_clock);
899
rc = mace4n(clauses, n);
900
if (rc == SEARCH_MAX_DOMAIN_SECONDS) {
901
printf("\n====== Domain size %d terminated by max_seconds_per. ======\n",n);
902
rc = SEARCH_GO_NO_MODELS;
903
}
904
else if (rc == SEARCH_DOMAIN_OUT_OF_RANGE) {
905
printf("\n====== Domain size %d skipped because domain elememt too big. ======\n",n);
906
rc = SEARCH_GO_NO_MODELS;
907
}
908
clock_stop(Mace4_clock);
909
p_stats();
910
reset_current_stats();
911
clock_reset(Mace4_clock);
912
n = next_domain_size(n); /* returns -1 if we're done */
913
}
914
915
/* free memory used for all domain sizes */
916
free_estack_memory();
917
free(Sn_to_mace_sn);
918
Sn_to_mace_sn = NULL;
919
920
results->success = Total_models != 0;
921
results->models = Models; /* NULL if no models or not collecting models */
922
results->user_seconds = user_seconds() - Start_seconds;
923
924
if (rc == SEARCH_MAX_MODELS)
925
results->return_code = MAX_MODELS_EXIT;
926
else if (rc == SEARCH_GO_MODELS || rc == SEARCH_GO_NO_MODELS)
927
results->return_code = Total_models==0 ? EXHAUSTED_EXIT : ALL_MODELS_EXIT;
928
else if (rc == SEARCH_MAX_TOTAL_SECONDS)
929
results->return_code = Total_models==0 ? MAX_SEC_NO_EXIT : MAX_SEC_YES_EXIT;
930
else if (rc == SEARCH_MAX_MEGS)
931
results->return_code = Total_models==0 ? MAX_MEGS_NO_EXIT : MAX_MEGS_YES_EXIT;
932
else
933
fatal_error("mace4: unknown return code");
934
935
enable_max_megs();
936
return results;
937
} /* mace4 */
Loggerhead is a web-based interface for Breezy
Version: 2.0.1