1 /*-----------------------------------------------------------------------
2
3 File : che_litselection.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Functions for selection certain literals (and hence superposition
10 strategies).
11
12
13 Copyright 1998, 1999 by the author.
14 This code is released under the GNU General Public Licence and
15 the GNU Lesser General Public License.
16 See the file COPYING in the main E directory for details..
17 Run "eprover -h" for contact information.
18
19 Changes
20
21 <1> Fri May 21 22:16:27 GMT 1999
22 New
23
24 -----------------------------------------------------------------------*/
25
26 #include "che_litselection.h"
27
28
29
30 /*---------------------------------------------------------------------*/
31 /* Global Variables */
32 /*---------------------------------------------------------------------*/
33
34
35 static LitSelNameFunAssocCell name_fun_assoc[] =
36 {
37 {"NoSelection", SelectNoLiterals},
38 {"NoGeneration", SelectNoGeneration},
39 {"SelectNegativeLiterals", SelectNegativeLiterals},
40 {"PSelectNegativeLiterals", PSelectNegativeLiterals},
41 {"SelectPureVarNegLiterals", SelectFirstVariableLiteral},
42 {"PSelectPureVarNegLiterals", PSelectFirstVariableLiteral},
43 {"SelectLargestNegLit", SelectLargestNegativeLiteral},
44 {"PSelectLargestNegLit", PSelectLargestNegativeLiteral},
45 {"SelectSmallestNegLit", SelectSmallestNegativeLiteral},
46 {"PSelectSmallestNegLit", PSelectSmallestNegativeLiteral},
47 {"SelectLargestOrientable", SelectLargestOrientableLiteral},
48 {"PSelectLargestOrientable", PSelectLargestOrientableLiteral},
49 {"MSelectLargestOrientable", MSelectLargestOrientableLiteral},
50 {"SelectSmallestOrientable", SelectSmallestOrientableLiteral},
51 {"PSelectSmallestOrientable", PSelectSmallestOrientableLiteral},
52 {"MSelectSmallestOrientable", MSelectSmallestOrientableLiteral},
53 {"SelectDiffNegLit", SelectDiffNegativeLiteral},
54 {"PSelectDiffNegLit", PSelectDiffNegativeLiteral},
55 {"SelectGroundNegLit", SelectGroundNegativeLiteral},
56 {"PSelectGroundNegLit", PSelectGroundNegativeLiteral},
57 {"SelectOptimalLit", SelectOptimalLiteral},
58 {"PSelectOptimalLit", PSelectOptimalLiteral},
59 {"SelectMinOptimalLit", SelectMinOptimalLiteral},
60 {"PSelectMinOptimalLit", PSelectMinOptimalLiteral},
61 {"SelectMinOptimalNoTypePred", SelectMinOptimalNoTypePred},
62 {"PSelectMinOptimalNoTypePred", PSelectMinOptimalNoTypePred},
63 {"SelectMinOptimalNoXTypePred", SelectMinOptimalNoXTypePred},
64 {"PSelectMinOptimalNoXTypePred", PSelectMinOptimalNoXTypePred},
65 {"SelectMinOptimalNoRXTypePred", SelectMinOptimalNoRXTypePred},
66 {"PSelectMinOptimalNoRXTypePred", PSelectMinOptimalNoRXTypePred},
67 {"SelectCondOptimalLit", SelectCondOptimalLiteral},
68 {"PSelectCondOptimalLit", PSelectCondOptimalLiteral},
69 {"SelectAllCondOptimalLit", SelectAllCondOptimalLiteral},
70 {"PSelectAllCondOptimalLit", PSelectAllCondOptimalLiteral},
71 {"SelectOptimalRestrDepth2", SelectDepth2OptimalLiteral},
72 {"PSelectOptimalRestrDepth2", PSelectDepth2OptimalLiteral},
73 {"SelectOptimalRestrPDepth2", SelectPDepth2OptimalLiteral},
74 {"PSelectOptimalRestrPDepth2", PSelectPDepth2OptimalLiteral},
75 {"SelectOptimalRestrNDepth2", SelectNDepth2OptimalLiteral},
76 {"PSelectOptimalRestrNDepth2", PSelectNDepth2OptimalLiteral},
77 {"SelectNonRROptimalLit", SelectNonRROptimalLiteral},
78 {"PSelectNonRROptimalLit", PSelectNonRROptimalLiteral},
79 {"SelectNonStrongRROptimalLit", SelectNonStrongRROptimalLiteral},
80 {"PSelectNonStrongRROptimalLit", PSelectNonStrongRROptimalLiteral},
81 {"SelectAntiRROptimalLit", SelectAntiRROptimalLiteral},
82 {"PSelectAntiRROptimalLit", PSelectAntiRROptimalLiteral},
83 {"SelectNonAntiRROptimalLit", SelectNonAntiRROptimalLiteral},
84 {"PSelectNonAntiRROptimalLit", PSelectNonAntiRROptimalLiteral},
85 {"SelectStrongRRNonRROptimalLit", SelectStrongRRNonRROptimalLiteral},
86 {"PSelectStrongRRNonRROptimalLit", PSelectStrongRRNonRROptimalLiteral},
87 {"SelectUnlessUniqMax", SelectUnlessUniqMaxOptimalLiteral},
88 {"PSelectUnlessUniqMax", PSelectUnlessUniqMaxOptimalLiteral},
89 {"SelectUnlessPosMax", SelectUnlessPosMaxOptimalLiteral},
90 {"PSelectUnlessPosMax", PSelectUnlessPosMaxOptimalLiteral},
91 {"SelectUnlessUniqPosMax", SelectUnlessUniqPosMaxOptimalLiteral},
92 {"PSelectUnlessUniqPosMax", PSelectUnlessUniqPosMaxOptimalLiteral},
93 {"SelectUnlessUniqMaxPos", SelectUnlessUniqMaxPosOptimalLiteral},
94 {"PSelectUnlessUniqMaxPos", PSelectUnlessUniqMaxPosOptimalLiteral},
95 {"SelectComplex", SelectComplex},
96 {"PSelectComplex", PSelectComplex},
97 {"SelectComplexExceptRRHorn", SelectComplexExceptRRHorn},
98 {"PSelectComplexExceptRRHorn", PSelectComplexExceptRRHorn},
99 {"SelectLComplex", SelectLComplex},
100 {"PSelectLComplex", PSelectLComplex},
101 {"SelectMaxLComplex", SelectMaxLComplex},
102 {"PSelectMaxLComplex", PSelectMaxLComplex},
103 {"SelectMaxLComplexNoTypePred", SelectMaxLComplexNoTypePred},
104 {"PSelectMaxLComplexNoTypePred", PSelectMaxLComplexNoTypePred},
105 {"SelectMaxLComplexNoXTypePred", SelectMaxLComplexNoXTypePred},
106 {"PSelectMaxLComplexNoXTypePred", PSelectMaxLComplexNoXTypePred},
107 {"SelectComplexPreferNEQ", SelectComplexPreferNEQ},
108 {"PSelectComplexPreferNEQ", PSelectComplexPreferNEQ},
109 {"SelectComplexPreferEQ", SelectComplexPreferEQ},
110 {"PSelectComplexPreferEQ", PSelectComplexPreferEQ},
111 {"SelectComplexExceptUniqMaxHorn", SelectComplexExceptUniqMaxHorn},
112 {"PSelectComplexExceptUniqMaxHorn", PSelectComplexExceptUniqMaxHorn},
113 {"MSelectComplexExceptUniqMaxHorn", MSelectComplexExceptUniqMaxHorn},
114 {"SelectNewComplex", SelectNewComplex},
115 {"PSelectNewComplex", PSelectNewComplex},
116 {"SelectNewComplexExceptUniqMaxHorn", SelectNewComplexExceptUniqMaxHorn},
117 {"PSelectNewComplexExceptUniqMaxHorn", PSelectNewComplexExceptUniqMaxHorn},
118 {"SelectMinInfpos", SelectMinInfpos},
119 {"PSelectMinInfpos", PSelectMinInfpos},
120 {"HSelectMinInfpos", HSelectMinInfpos},
121 {"GSelectMinInfpos", GSelectMinInfpos},
122 {"SelectMinInfposNoTypePred", SelectMinInfposNoTypePred},
123 {"PSelectMinInfposNoTypePred", PSelectMinInfposNoTypePred},
124 {"SelectMin2Infpos", SelectMin2Infpos},
125 {"PSelectMin2Infpos", PSelectMin2Infpos},
126 {"SelectComplexExceptUniqMaxPosHorn", SelectComplexExceptUniqMaxPosHorn},
127 {"PSelectComplexExceptUniqMaxPosHorn", PSelectComplexExceptUniqMaxPosHorn},
128 {"SelectUnlessUniqMaxSmallestOrientable", SelectUnlessUniqMaxSmallestOrientable},
129 {"PSelectUnlessUniqMaxSmallestOrientable",PSelectUnlessUniqMaxSmallestOrientable},
130 {"SelectDivLits", SelectDiversificationLiterals},
131 {"SelectDivPreferIntoLits", SelectDiversificationPreferIntoLiterals},
132 {"SelectMaxLComplexG", SelectMaxLComplexG},
133 {"SelectMaxLComplexAvoidPosPred", SelectMaxLComplexAvoidPosPred},
134 {"SelectMaxLComplexAPPNTNp", SelectMaxLComplexAPPNTNp},
135 {"SelectMaxLComplexAPPNoType", SelectMaxLComplexAPPNoType},
136 {"SelectMaxLComplexAvoidPosUPred", SelectMaxLComplexAvoidPosUPred},
137 {"SelectComplexG", SelectComplexG},
138 {"SelectComplexAHP", SelectComplexAHP},
139 {"PSelectComplexAHP", PSelectComplexAHP},
140 {"SelectNewComplexAHP", SelectNewComplexAHP},
141 {"PSelectNewComplexAHP", PSelectNewComplexAHP},
142 {"SelectComplexAHPExceptRRHorn", SelectComplexAHPExceptRRHorn},
143 {"PSelectComplexAHPExceptRRHorn", PSelectComplexAHPExceptRRHorn},
144
145 {"SelectNewComplexAHPExceptRRHorn", SelectNewComplexAHPExceptRRHorn},
146 {"PSelectNewComplexAHPExceptRRHorn", PSelectNewComplexAHPExceptRRHorn},
147
148 {"SelectNewComplexAHPExceptUniqMaxHorn", SelectNewComplexAHPExceptUniqMaxHorn},
149 {"PSelectNewComplexAHPExceptUniqMaxHorn", PSelectNewComplexAHPExceptUniqMaxHorn},
150 {"SelectNewComplexAHPNS", SelectNewComplexAHPNS},
151 {"SelectVGNonCR", SelectVGNonCR},
152
153 {"SelectCQArEqLast", SelectCQArEqLast},
154 {"SelectCQArEqFirst", SelectCQArEqFirst},
155 {"SelectCQIArEqLast", SelectCQIArEqLast},
156 {"SelectCQIArEqFirst", SelectCQIArEqFirst},
157 {"SelectCQAr", SelectCQAr},
158 {"SelectCQIAr", SelectCQIAr},
159 {"SelectCQArNpEqFirst", SelectCQArNpEqFirst},
160 {"SelectCQIArNpEqFirst", SelectCQIArNpEqFirst},
161
162 {"SelectGrCQArEqFirst", SelectGrCQArEqFirst},
163 {"SelectCQGrArEqFirst", SelectCQGrArEqFirst},
164 {"SelectCQArNTEqFirst", SelectCQArNTEqFirst},
165 {"SelectCQIArNTEqFirst", SelectCQIArNTEqFirst},
166 {"SelectCQArNTNpEqFirst", SelectCQArNTNpEqFirst},
167 {"SelectCQIArNTNpEqFirst", SelectCQIArNTNpEqFirst},
168 {"SelectCQArNXTEqFirst" , SelectCQArNXTEqFirst},
169 {"SelectCQIArNXTEqFirst" , SelectCQIArNXTEqFirst},
170
171 {"SelectCQArNTNp", SelectCQArNTNp},
172 {"SelectCQIArNTNp", SelectCQIArNTNp},
173 {"SelectCQArNT", SelectCQArNT},
174 {"SelectCQIArNT", SelectCQIArNT},
175 {"SelectCQArNp", SelectCQArNp},
176 {"SelectCQIArNp", SelectCQIArNp},
177
178 {"SelectCQArNpEqFirstUnlessPDom", SelectCQArNpEqFirstUnlessPDom},
179 {"SelectCQArNTEqFirstUnlessPDom", SelectCQArNTEqFirstUnlessPDom},
180
181 {"SelectCQPrecW", SelectCQPrecW},
182 {"SelectCQIPrecW", SelectCQIPrecW},
183 {"SelectCQPrecWNTNp", SelectCQPrecWNTNp},
184 {"SelectCQIPrecWNTNp", SelectCQIPrecWNTNp},
185
186 {NULL, (LiteralSelectionFun)NULL}
187 };
188
189
190 static long literal_weight_counter=0;
191
192 /*---------------------------------------------------------------------*/
193 /* Forward Declarations */
194 /*---------------------------------------------------------------------*/
195
196
197 /*---------------------------------------------------------------------*/
198 /* Internal Functions */
199 /*---------------------------------------------------------------------*/
200
201 #define lit_sel_diff_weight(handle) \
202 ((100*EqnStandardDiff(handle))+EqnStandardWeight(handle))
203
204 /*-----------------------------------------------------------------------
205 //
206 // Function: find_maxlcomplex_literal()
207 //
208 // Find a maximal negative literal to select (see
209 // SelectMaxLComplex() below.
210 //
211 // Global Variables: -
212 //
213 // Side Effects : -
214 //
215 /----------------------------------------------------------------------*/
216
find_maxlcomplex_literal(Clause_p clause)217 static Eqn_p find_maxlcomplex_literal(Clause_p clause)
218 {
219 Eqn_p handle = clause->literals, selected = NULL;
220 long select_weight, weight;
221
222 while(handle)
223 {
224 if(EqnIsNegative(handle)&&
225 EqnIsMaximal(handle) &&
226 TermIsVar(handle->lterm) &&
227 TermIsVar(handle->rterm))
228 {
229 selected = handle;
230 break;
231 }
232 handle = handle->next;
233 }
234 if(selected)
235 {
236 return selected;
237 }
238 select_weight = -1;
239 handle = clause->literals;
240
241 while(handle)
242 {
243 if(EqnIsNegative(handle) && EqnIsMaximal(handle)&&
244 EqnIsGround(handle))
245 {
246 weight = lit_sel_diff_weight(handle);
247 if(weight > select_weight)
248 {
249 select_weight = weight;
250 selected = handle;
251 }
252 }
253 handle = handle->next;
254 }
255 if(selected)
256 {
257 return selected;
258 }
259 select_weight = -1;
260 handle = clause->literals;
261
262 while(handle)
263 {
264 if(EqnIsNegative(handle) && EqnIsMaximal(handle))
265 {
266 weight = lit_sel_diff_weight(handle);
267 if(weight > select_weight)
268 {
269 select_weight = weight;
270 selected = handle;
271 }
272 }
273 handle = handle->next;
274 }
275 return selected;
276 }
277
278
279 /*-----------------------------------------------------------------------
280 //
281 // Function: find_lcomplex_literal()
282 //
283 // Find a non-maximal negative literal to select (see
284 // SelectComplex() below.
285 //
286 // Global Variables: -
287 //
288 // Side Effects : -
289 //
290 /----------------------------------------------------------------------*/
291
find_lcomplex_literal(Clause_p clause)292 static Eqn_p find_lcomplex_literal(Clause_p clause)
293 {
294 Eqn_p handle = clause->literals, selected = NULL;
295 long select_weight, weight;
296
297 while(handle)
298 {
299 if(EqnIsNegative(handle)&&
300 !EqnIsMaximal(handle) &&
301 TermIsVar(handle->lterm) &&
302 TermIsVar(handle->rterm))
303 {
304 selected = handle;
305 break;
306 }
307 handle = handle->next;
308 }
309 if(selected)
310 {
311 return selected;
312 }
313
314 select_weight = -1;
315 handle = clause->literals;
316
317 while(handle)
318 {
319 if(EqnIsNegative(handle)&&!EqnIsMaximal(handle)&&EqnIsGround(handle))
320 {
321 weight = lit_sel_diff_weight(handle);
322 if(weight > select_weight)
323 {
324 select_weight = weight;
325 selected = handle;
326 }
327 }
328 handle = handle->next;
329 }
330 if(selected)
331 {
332 return selected;
333 }
334
335 select_weight = -1;
336 handle = clause->literals;
337
338 while(handle)
339 {
340 if(EqnIsNegative(handle)&&!EqnIsMaximal(handle))
341 {
342 weight = lit_sel_diff_weight(handle);
343 if(weight > select_weight)
344 {
345 select_weight = weight;
346 selected = handle;
347 }
348 }
349 handle = handle->next;
350 }
351 return selected;
352 }
353
354
355
356 /*-----------------------------------------------------------------------
357 //
358 // Function: find_smallest_neg_ground_lit()
359 //
360 // Return smallest negative ground literal, or NULL if no negative
361 // ground literal exists.
362 //
363 // Global Variables: -
364 //
365 // Side Effects : -
366 //
367 /----------------------------------------------------------------------*/
368
find_smallest_neg_ground_lit(Clause_p clause)369 static Eqn_p find_smallest_neg_ground_lit(Clause_p clause)
370 {
371 Eqn_p handle = clause->literals, selected = NULL;
372 long select_weight = LONG_MAX;
373
374 while(handle)
375 {
376 if(EqnIsNegative(handle)&&
377 EqnIsGround(handle))
378 {
379 assert(EqnIsOriented(handle));
380
381 if(EqnStandardWeight(handle) < select_weight)
382 {
383 selected = handle;
384 select_weight = EqnStandardWeight(handle);
385 }
386 }
387 handle = handle->next;
388 }
389 return selected;
390 }
391
392
393 /*-----------------------------------------------------------------------
394 //
395 // Function: find_smallest_max_neg_ground_lit()
396 //
397 // Return the ground literal with the smallest maximal side. Assumes
398 // that all literals have been oriented (if possible).
399 //
400 // Global Variables: -
401 //
402 // Side Effects : -
403 //
404 /----------------------------------------------------------------------*/
405
find_smallest_max_neg_ground_lit(Clause_p clause)406 static Eqn_p find_smallest_max_neg_ground_lit(Clause_p clause)
407 {
408 Eqn_p handle = clause->literals, selected = NULL;
409 long select_weight = LONG_MAX;
410
411 while(handle)
412 {
413 if(EqnIsNegative(handle)&&
414 EqnIsGround(handle))
415 {
416 /* assert(EqnIsOriented(handle)); Only true if we don't run
417 * into LPORecursionDepthLimit */
418
419 if(handle->lterm->weight < select_weight)
420 {
421 selected = handle;
422 select_weight = handle->lterm->weight;
423 }
424 }
425 handle = handle->next;
426 }
427 return selected;
428 }
429
430
431 /*-----------------------------------------------------------------------
432 //
433 // Function: find_ng_min11_infpos_no_xtype_lit()
434 //
435 // Return the non-ground, non-xpos literal with the smallest number
436 // of inference positions.
437 //
438 // Global Variables: -
439 //
440 // Side Effects : -
441 //
442 /----------------------------------------------------------------------*/
443
find_ng_min11_infpos_no_xtype_lit(Clause_p clause)444 static Eqn_p find_ng_min11_infpos_no_xtype_lit(Clause_p clause)
445 {
446 Eqn_p handle = clause->literals, selected = NULL;
447 long select_weight = LONG_MAX, weight;
448
449 while(handle)
450 {
451 if(EqnIsNegative(handle)&&
452 !EqnIsGround(handle)&&
453 !EqnIsXTypePred(handle))
454 {
455 weight = TermWeight(handle->lterm,1,1);
456 if(!EqnIsOriented(handle))
457 {
458 weight += TermWeight(handle->rterm,1,1);
459 }
460 if(weight < select_weight)
461 {
462 select_weight = weight;
463 selected = handle;
464 }
465 }
466 handle = handle->next;
467 }
468 return selected;
469 }
470
471
472
473 /*-----------------------------------------------------------------------
474 //
475 // Function: find_max_xtype_no_type_lit()
476 //
477 // Return the biggest xtype literal (but never a type literal).
478 //
479 // Global Variables: -
480 //
481 // Side Effects : -
482 //
483 /----------------------------------------------------------------------*/
484
find_max_xtype_no_type_lit(Clause_p clause)485 static Eqn_p find_max_xtype_no_type_lit(Clause_p clause)
486 {
487 Eqn_p handle = clause->literals, selected = NULL;
488 long select_weight = -1, weight;
489
490 while(handle)
491 {
492 if(EqnIsNegative(handle)&&
493 EqnIsXTypePred(handle) &&
494 !EqnIsTypePred(handle))
495 {
496 assert(EqnIsOriented(handle));
497
498 weight = handle->lterm->weight;
499 if(weight > select_weight)
500 {
501 select_weight = weight;
502 selected = handle;
503 }
504 }
505 handle = handle->next;
506 }
507 return selected;
508 }
509
510
511
512
513 /*-----------------------------------------------------------------------
514 //
515 // Function: clause_select_pos()
516 //
517 // Select all positive literals in clause.
518 //
519 // Global Variables: -
520 //
521 // Side Effects : -
522 //
523 /----------------------------------------------------------------------*/
524
clause_select_pos(Clause_p clause)525 static void clause_select_pos(Clause_p clause)
526 {
527 Eqn_p handle=clause->literals;
528
529 assert(clause->neg_lit_no);
530
531 while(handle)
532 {
533 if(EqnIsPositive(handle))
534 {
535 EqnSetProp(handle, EPIsSelected);
536 }
537 handle = handle->next;
538 }
539 }
540
541
542 /*-----------------------------------------------------------------------
543 //
544 // Function: lit_eval_compare()
545 //
546 // Return integer smaller than 0, 0, or int > than zero if le1 is
547 // smaller, equal to, or larger than le2 (by weight). Highest
548 // priority is implicit sign!
549 //
550 // Global Variables: -
551 //
552 // Side Effects : -
553 //
554 /----------------------------------------------------------------------*/
555
lit_eval_compare(const void * le1,const void * le2)556 int lit_eval_compare(const void* le1, const void* le2)
557 {
558 const LitEval_p eval1 = (const LitEval_p) le1;
559 const LitEval_p eval2 = (const LitEval_p) le2;
560 int res;
561
562 res = EqnIsPositive(eval1->literal)-EqnIsPositive(eval2->literal);
563 if(res)
564 {
565 return res;
566 }
567 res = eval1->w1 - eval2->w1;
568 if(res)
569 {
570 return res;
571 }
572 res = eval1->w2 - eval2->w2;
573 if(res)
574 {
575 return res;
576 }
577 res = eval1->w3 - eval2->w3;
578 return res;
579 }
580
581 /*-----------------------------------------------------------------------
582 //
583 // Function: generic_uniq_selection()
584 //
585 // Function implementing generic weight-based selection for cases
586 // where at most one negative literal is selected (the one which is
587 // assigned minimal weight by weight_fun).
588 //
589 // Global Variables: -
590 //
591 // Side Effects : -
592 //
593 /----------------------------------------------------------------------*/
594
generic_uniq_selection(OCB_p ocb,Clause_p clause,bool positive,bool needs_ordering,LitWeightFun weight_fun,void * data)595 void generic_uniq_selection(OCB_p ocb, Clause_p clause, bool positive,
596 bool needs_ordering,
597 LitWeightFun weight_fun, void* data)
598 {
599 int len = ClauseLiteralNumber(clause);
600 LitEval_p lits, tmp;
601 int i, cand;
602 Eqn_p handle;
603 bool selected = false;
604
605 assert(ocb);
606 assert(clause);
607 assert(clause->neg_lit_no);
608 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
609
610 lits = SizeMalloc(len*sizeof(LitEvalCell));
611 if(needs_ordering)
612 {
613 ClauseCondMarkMaximalTerms(ocb, clause);
614 }
615 for(handle=clause->literals, i=0; handle; handle=handle->next,i++)
616 {
617 lits[i].literal = handle;
618 tmp = &(lits[i]);
619 LitEvalInit(tmp);
620 assert(clause);
621 weight_fun(tmp, clause, data);
622 }
623 cand = 0;
624 for(handle=clause->literals->next, i=1; handle; handle=handle->next,i++)
625 {
626 if(lit_eval_compare(&(lits[i]),&(lits[cand]))<0)
627 {
628 cand = i;
629 }
630 }
631 /*printf("cand: %d :",cand);
632 ClausePrint(stdout, clause, true);
633 printf("\n");*/
634
635 assert(EqnIsNegative(lits[cand].literal));
636 if(!lits[cand].forbidden)
637 {
638 EqnSetProp(lits[cand].literal, EPIsSelected);
639 selected = true;
640 ClauseDelProp(clause, CPIsOriented);
641 }
642 SizeFree(lits,len*sizeof(LitEvalCell));
643 if(positive && selected)
644 {
645 clause_select_pos(clause);
646 }
647 }
648
649 /*-----------------------------------------------------------------------
650 //
651 // Function: pos_pred_dist_array_compute()
652 //
653 // Compute a distribution array of predicate symbols (or
654 // uninterpreted predicate symbols in positive literals of clause.
655 //
656 // Global Variables: -
657 //
658 // Side Effects : Memory operations
659 //
660 /----------------------------------------------------------------------*/
661
662
pos_pred_dist_array_compute(Clause_p clause)663 static PDArray_p pos_pred_dist_array_compute(Clause_p clause)
664 {
665 PDArray_p pred_dist;
666 Eqn_p handle;
667
668 pred_dist = PDIntArrayAlloc(10,30);
669
670 for(handle = clause->literals;
671 handle && EqnIsPositive(handle);
672 handle = handle->next)
673 {
674 PDArrayElementIncInt(pred_dist, EqnGetPredCode(handle), 1);
675 }
676 return pred_dist;
677 }
678
679 #define pred_dist_array_free(array) PDArrayFree(array)
680
681
682 /*---------------------------------------------------------------------*/
683 /* Exported Functions */
684 /*---------------------------------------------------------------------*/
685
686
687 /*-----------------------------------------------------------------------
688 //
689 // Function: GetLitSelFun()
690 //
691 // Given an external name, return a literal selection function or
692 // NULL if the name does not match any known function.
693 //
694 // Global Variables: LiteralSelectionFunNames, litsel_fun_array
695 //
696 // Side Effects : -
697 //
698 /----------------------------------------------------------------------*/
699
GetLitSelFun(char * name)700 LiteralSelectionFun GetLitSelFun(char* name)
701 {
702 int i;
703
704 assert(name);
705
706 for(i=0; name_fun_assoc[i].name; i++)
707 {
708 if(strcmp(name, name_fun_assoc[i].name)==0)
709 {
710 return name_fun_assoc[i].fun;
711 }
712 }
713 return (LiteralSelectionFun)0;
714 }
715
716
717 /*-----------------------------------------------------------------------
718 //
719 // Function: GetLitSelName()
720 //
721 // Given a LiteralSelectionFun, return the corresponding
722 // name. Fails/Undefined, if function is not found.
723 //
724 // Global Variables: -
725 //
726 // Side Effects : -
727 //
728 /----------------------------------------------------------------------*/
729
GetLitSelName(LiteralSelectionFun fun)730 char* GetLitSelName(LiteralSelectionFun fun)
731 {
732 int i;
733 char *res = NULL;
734
735 assert(fun);
736 for(i=0; name_fun_assoc[i].name; i++)
737 {
738 if(name_fun_assoc[i].fun == fun)
739 {
740 res = name_fun_assoc[i].name;
741 assert(res);
742 break;
743 }
744 }
745 assert(res);
746 return res;
747 }
748
749 /*-----------------------------------------------------------------------
750 //
751 // Function: LitSelAppendNames()
752 //
753 // Append all valid literal selection function names
754 // (comma-seperated) to str.
755 //
756 // Global Variables: -
757 //
758 // Side Effects : Memory operations
759 //
760 /----------------------------------------------------------------------*/
761
LitSelAppendNames(DStr_p str)762 void LitSelAppendNames(DStr_p str)
763 {
764 int i;
765 char* sel = "";
766
767 for(i=0; name_fun_assoc[i].name; i++)
768 {
769 DStrAppendStr(str, sel);
770 DStrAppendStr(str, name_fun_assoc[i].name);
771 sel = ", ";
772 }
773 }
774
775
776
777 /*-----------------------------------------------------------------------
778 //
779 // Function: SelectNoLiterals()
780 //
781 // Unselect all literals (now a dummy, this is done further up).
782 //
783 // Global Variables: -
784 //
785 // Side Effects : -
786 //
787 /----------------------------------------------------------------------*/
788
SelectNoLiterals(OCB_p ocb,Clause_p clause)789 void SelectNoLiterals(OCB_p ocb, Clause_p clause)
790 {
791 assert(clause);
792 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
793 }
794
795 /*-----------------------------------------------------------------------
796 //
797 // Function: SelectNoGeneration()
798 //
799 // Do nothing with a clause.
800 //
801 // Global Variables: -
802 //
803 // Side Effects : -
804 //
805 /----------------------------------------------------------------------*/
806
SelectNoGeneration(OCB_p ocb,Clause_p clause)807 void SelectNoGeneration(OCB_p ocb, Clause_p clause)
808 {
809 assert(clause);
810 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
811 }
812
813
814 /*-----------------------------------------------------------------------
815 //
816 // Function: SelectNegativeLiterals()
817 //
818 // If the clause has negative literals, mark them as selected.
819 //
820 // Global Variables: -
821 //
822 // Side Effects : Changes property in literals
823 //
824 /----------------------------------------------------------------------*/
825
SelectNegativeLiterals(OCB_p ocb,Clause_p clause)826 void SelectNegativeLiterals(OCB_p ocb, Clause_p clause)
827 {
828 Eqn_p handle = clause->literals;
829
830 while(handle)
831 {
832 if(!EqnIsPositive(handle))
833 {
834 EqnSetProp(handle, EPIsSelected);
835 }
836 handle = handle->next;
837 }
838 }
839
840
841 /*-----------------------------------------------------------------------
842 //
843 // Function: PSelectNegativeLiterals()
844 //
845 // If the clause has negative literals, mark all literals as
846 // selected.
847 //
848 // Global Variables: -
849 //
850 // Side Effects : Changes property in literals
851 //
852 /----------------------------------------------------------------------*/
853
PSelectNegativeLiterals(OCB_p ocb,Clause_p clause)854 void PSelectNegativeLiterals(OCB_p ocb, Clause_p clause)
855 {
856 Eqn_p handle = clause->literals;
857
858 while(handle)
859 {
860 EqnSetProp(handle, EPIsSelected);
861 handle = handle->next;
862 }
863 }
864
865
866 /*-----------------------------------------------------------------------
867 //
868 // Function: SelectFirstVariableLiteral()
869 //
870 // Select first literal of the form X!=Y.
871 //
872 // Global Variables: -
873 //
874 // Side Effects : Changes property in literals
875 //
876 /----------------------------------------------------------------------*/
877
SelectFirstVariableLiteral(OCB_p ocb,Clause_p clause)878 void SelectFirstVariableLiteral(OCB_p ocb, Clause_p clause)
879 {
880 Eqn_p handle = ClauseFindNegPureVarLit(clause);
881
882 if(handle)
883 {
884 EqnSetProp(handle, EPIsSelected);
885 }
886 }
887
888
889 /*-----------------------------------------------------------------------
890 //
891 // Function: PSelectFirstVariableLiteral()
892 //
893 // If a literal of the form X!=Y exist, select it and all positive
894 // literals. Otherwise unselect all literals.
895 //
896 // Global Variables: -
897 //
898 // Side Effects : Changes property in literals
899 //
900 /----------------------------------------------------------------------*/
901
PSelectFirstVariableLiteral(OCB_p ocb,Clause_p clause)902 void PSelectFirstVariableLiteral(OCB_p ocb, Clause_p clause)
903 {
904 Eqn_p handle = ClauseFindNegPureVarLit(clause);
905
906 if(handle)
907 {
908 clause_select_pos(clause);
909 }
910 }
911
912
913 /*-----------------------------------------------------------------------
914 //
915 // Function: SelectLargestNegativeLiteral()
916 //
917 // Select the largest of the clauses negative literals.
918 //
919 // Global Variables: -
920 //
921 // Side Effects : Changes property in literals
922 //
923 /----------------------------------------------------------------------*/
924
SelectLargestNegativeLiteral(OCB_p ocb,Clause_p clause)925 void SelectLargestNegativeLiteral(OCB_p ocb, Clause_p clause)
926 {
927 Eqn_p handle = clause->literals, selected = NULL;
928 long select_weight = 0;
929
930 while(handle)
931 {
932 if(EqnIsNegative(handle))
933 {
934 if(EqnStandardWeight(handle) > select_weight)
935 {
936 select_weight = EqnStandardWeight(handle);
937 selected = handle;
938 }
939 }
940 handle = handle->next;
941 }
942 assert(selected);
943 EqnSetProp(selected, EPIsSelected);
944 }
945
946
947 /*-----------------------------------------------------------------------
948 //
949 // Function: PSelectLargestNegativeLiteral()
950 //
951 // If clause has negative literals, select the largest of the
952 // clauses negative literals and positive literals.
953 //
954 // Global Variables: -
955 //
956 // Side Effects : Changes property in literals
957 //
958 /----------------------------------------------------------------------*/
959
PSelectLargestNegativeLiteral(OCB_p ocb,Clause_p clause)960 void PSelectLargestNegativeLiteral(OCB_p ocb, Clause_p clause)
961 {
962 Eqn_p handle = clause->literals, selected = NULL;
963 long select_weight = 0;
964
965 while(handle)
966 {
967 if(EqnIsPositive(handle))
968 {
969 EqnSetProp(handle, EPIsSelected);
970 }
971 else
972 {
973 if(EqnStandardWeight(handle) > select_weight)
974 {
975 select_weight = EqnStandardWeight(handle);
976 selected = handle;
977 }
978 }
979 handle = handle->next;
980 }
981 assert(selected);
982 EqnSetProp(selected, EPIsSelected);
983 }
984
985
986
987 /*-----------------------------------------------------------------------
988 //
989 // Function: SelectSmallestNegativeLiteral()
990 //
991 // Select the smallest of the clauses negative literals.
992 //
993 // Global Variables: -
994 //
995 // Side Effects : Changes property in literals
996 //
997 /----------------------------------------------------------------------*/
998
SelectSmallestNegativeLiteral(OCB_p ocb,Clause_p clause)999 void SelectSmallestNegativeLiteral(OCB_p ocb, Clause_p clause)
1000 {
1001 Eqn_p handle = clause->literals, selected = NULL;
1002 long select_weight = LONG_MAX;
1003
1004 while(handle)
1005 {
1006 if(EqnIsNegative(handle))
1007 {
1008 if(EqnStandardWeight(handle) < select_weight)
1009 {
1010 select_weight = EqnStandardWeight(handle);
1011 selected = handle;
1012 }
1013 }
1014 handle = handle->next;
1015 }
1016 assert(selected);
1017 EqnSetProp(selected, EPIsSelected);
1018 }
1019
1020 /*-----------------------------------------------------------------------
1021 //
1022 // Function: PSelectSmallestNegativeLiteral()
1023 //
1024 // If clause has negative literals, select the smallest of the
1025 // clauses negative literals and positive literals.
1026 //
1027 // Global Variables: -
1028 //
1029 // Side Effects : Changes property in literals
1030 //
1031 /----------------------------------------------------------------------*/
1032
PSelectSmallestNegativeLiteral(OCB_p ocb,Clause_p clause)1033 void PSelectSmallestNegativeLiteral(OCB_p ocb, Clause_p clause)
1034 {
1035 Eqn_p handle = clause->literals, selected = NULL;
1036 long select_weight = LONG_MAX;
1037
1038 while(handle)
1039 {
1040 if(EqnIsPositive(handle))
1041 {
1042 EqnSetProp(handle, EPIsSelected);
1043 }
1044 else
1045 {
1046 if(EqnStandardWeight(handle) < select_weight)
1047 {
1048 select_weight = EqnStandardWeight(handle);
1049 selected = handle;
1050 }
1051 }
1052 handle = handle->next;
1053 }
1054 assert(selected);
1055 EqnSetProp(selected, EPIsSelected);
1056 }
1057
1058
1059 /*-----------------------------------------------------------------------
1060 //
1061 // Function: SelectLargestOrientableLiteral()
1062 //
1063 // If there is at least one negative orientable literal, select the
1064 // largest one, otherwise select the largest one.
1065 //
1066 // Global Variables: -
1067 //
1068 // Side Effects : Changes property in literals
1069 //
1070 /----------------------------------------------------------------------*/
1071
SelectLargestOrientableLiteral(OCB_p ocb,Clause_p clause)1072 void SelectLargestOrientableLiteral(OCB_p ocb, Clause_p clause)
1073 {
1074 Eqn_p handle = clause->literals, selected = NULL;
1075 long select_weight = 0;
1076 bool oriented = false;
1077
1078 ClauseCondMarkMaximalTerms(ocb, clause);
1079
1080 while(handle)
1081 {
1082 if(EqnIsNegative(handle))
1083 {
1084 if((!oriented && EqnIsOriented(handle))
1085 ||
1086 (
1087 ((oriented&&EqnIsOriented(handle))||(!oriented&&!EqnIsOriented(handle)))
1088 &&
1089 (EqnStandardWeight(handle) > select_weight)
1090 ))
1091 {
1092 select_weight = EqnStandardWeight(handle);
1093 oriented = EqnIsOriented(handle);
1094 selected = handle;
1095 }
1096 }
1097 handle = handle->next;
1098 }
1099 assert(selected);
1100 EqnSetProp(selected, EPIsSelected);
1101 ClauseDelProp(clause, CPIsOriented);
1102 }
1103
1104
1105 /*-----------------------------------------------------------------------
1106 //
1107 // Function: PSelectLargestOrientableLiteral()
1108 //
1109 // If there is at least one negative orientable literal, select the
1110 // largest one, otherwise select the largest one. Also select
1111 // positive literals.
1112 //
1113 // Global Variables: -
1114 //
1115 // Side Effects : Changes property in literals
1116 //
1117 /----------------------------------------------------------------------*/
1118
PSelectLargestOrientableLiteral(OCB_p ocb,Clause_p clause)1119 void PSelectLargestOrientableLiteral(OCB_p ocb, Clause_p clause)
1120 {
1121 Eqn_p handle = clause->literals, selected = NULL;
1122 long select_weight = 0;
1123 bool oriented = false;
1124
1125 ClauseCondMarkMaximalTerms(ocb, clause);
1126
1127 while(handle)
1128 {
1129 if(EqnIsPositive(handle))
1130 {
1131 EqnSetProp(handle, EPIsSelected);
1132 }
1133 else
1134 {
1135 if((!oriented && EqnIsOriented(handle))
1136 ||
1137 (
1138 ((oriented&&EqnIsOriented(handle))||(!oriented&&!EqnIsOriented(handle)))
1139 &&
1140 (EqnStandardWeight(handle) > select_weight)
1141 ))
1142 {
1143 select_weight = EqnStandardWeight(handle);
1144 oriented = EqnIsOriented(handle);
1145 selected = handle;
1146 }
1147 }
1148 handle = handle->next;
1149 }
1150 assert(selected);
1151 EqnSetProp(selected, EPIsSelected);
1152 ClauseDelProp(clause, CPIsOriented);
1153 }
1154
1155
1156 /*-----------------------------------------------------------------------
1157 //
1158 // Function: MSelectLargestOrientableLiteral()
1159 //
1160 // For horn clauses, call PSelectLargestOrientableLiteral,
1161 // otherwise call SelectLargestOrientableLiteral.
1162 //
1163 // Global Variables: -
1164 //
1165 // Side Effects : Changes property in literals
1166 //
1167 /----------------------------------------------------------------------*/
1168
MSelectLargestOrientableLiteral(OCB_p ocb,Clause_p clause)1169 void MSelectLargestOrientableLiteral(OCB_p ocb, Clause_p clause)
1170 {
1171 if(ClauseIsHorn(clause))
1172 {
1173 PSelectLargestOrientableLiteral(ocb,clause);
1174 }
1175 else
1176 {
1177 SelectLargestOrientableLiteral(ocb,clause);
1178 }
1179 }
1180
1181
1182 /*-----------------------------------------------------------------------
1183 //
1184 // Function: SelectSmallestOrientableLiteral()
1185 //
1186 // If there is at least one negative orientable literal, select the
1187 // smallest one, otherwise select the largest one.
1188 //
1189 // Global Variables: -
1190 //
1191 // Side Effects : Changes property in literals
1192 //
1193 /----------------------------------------------------------------------*/
1194
SelectSmallestOrientableLiteral(OCB_p ocb,Clause_p clause)1195 void SelectSmallestOrientableLiteral(OCB_p ocb, Clause_p clause)
1196 {
1197 Eqn_p handle = clause->literals, selected = NULL;
1198 long select_weight = LONG_MAX;
1199 bool oriented = false;
1200
1201 ClauseCondMarkMaximalTerms(ocb, clause);
1202
1203 while(handle)
1204 {
1205 if(EqnIsNegative(handle))
1206 {
1207 if((!oriented && EqnIsOriented(handle))
1208 ||
1209 (
1210 ((oriented&&EqnIsOriented(handle))||(!oriented&&!EqnIsOriented(handle)))
1211 &&
1212 (EqnStandardWeight(handle) < select_weight)
1213 ))
1214 {
1215 select_weight = EqnStandardWeight(handle);
1216 oriented = EqnIsOriented(handle);
1217 selected = handle;
1218 }
1219 }
1220 handle = handle->next;
1221 }
1222 assert(selected);
1223 EqnSetProp(selected, EPIsSelected);
1224 ClauseDelProp(clause, CPIsOriented);
1225 }
1226
1227
1228 /*-----------------------------------------------------------------------
1229 //
1230 // Function: PSelectSmallestOrientableLiteral()
1231 //
1232 // If there is at least one negative orientable literal, select the
1233 // smallest one, otherwise select the largest one. Also select
1234 // positive literals.
1235 //
1236 // Global Variables: -
1237 //
1238 // Side Effects : Changes property in literals
1239 //
1240 /----------------------------------------------------------------------*/
1241
PSelectSmallestOrientableLiteral(OCB_p ocb,Clause_p clause)1242 void PSelectSmallestOrientableLiteral(OCB_p ocb, Clause_p clause)
1243 {
1244 Eqn_p handle = clause->literals, selected = NULL;
1245 long select_weight = LONG_MAX;
1246 bool oriented = false;
1247
1248 ClauseCondMarkMaximalTerms(ocb, clause);
1249
1250 while(handle)
1251 {
1252 if(EqnIsPositive(handle))
1253 {
1254 EqnSetProp(handle, EPIsSelected);
1255 }
1256 else
1257 {
1258 if((!oriented && EqnIsOriented(handle))
1259 ||
1260 (
1261 ((oriented&&EqnIsOriented(handle))||(!oriented&&!EqnIsOriented(handle)))
1262 &&
1263 (EqnStandardWeight(handle) < select_weight)
1264 ))
1265 {
1266 select_weight = EqnStandardWeight(handle);
1267 oriented = EqnIsOriented(handle);
1268 selected = handle;
1269 }
1270 }
1271 handle = handle->next;
1272 }
1273 assert(selected);
1274 EqnSetProp(selected, EPIsSelected);
1275 ClauseDelProp(clause, CPIsOriented);
1276 }
1277
1278
1279 /*-----------------------------------------------------------------------
1280 //
1281 // Function: MSelectSmallestOrientableLiteral()
1282 //
1283 // For horn clauses, call PSelectSmallestOrientableLiteral,
1284 // otherwise call SelectSmallestOrientableLiteral.
1285 //
1286 // Global Variables: -
1287 //
1288 // Side Effects : Changes property in literals
1289 //
1290 /----------------------------------------------------------------------*/
1291
MSelectSmallestOrientableLiteral(OCB_p ocb,Clause_p clause)1292 void MSelectSmallestOrientableLiteral(OCB_p ocb, Clause_p clause)
1293 {
1294 if(ClauseIsHorn(clause))
1295 {
1296 PSelectSmallestOrientableLiteral(ocb,clause);
1297 }
1298 else
1299 {
1300 SelectSmallestOrientableLiteral(ocb,clause);
1301 }
1302 }
1303
1304
1305 /*-----------------------------------------------------------------------
1306 //
1307 // Function: SelectDiffNegativeLiteral()
1308 //
1309 // Select the most unbalanced of the clauses negative literals.
1310 //
1311 // Global Variables: -
1312 //
1313 // Side Effects : Changes property in literals
1314 //
1315 /----------------------------------------------------------------------*/
1316
SelectDiffNegativeLiteral(OCB_p ocb,Clause_p clause)1317 void SelectDiffNegativeLiteral(OCB_p ocb, Clause_p clause)
1318 {
1319 Eqn_p handle = clause->literals, selected = NULL;
1320 long select_weight = -1;
1321
1322 while(handle)
1323 {
1324 if(EqnIsNegative(handle))
1325 {
1326 if(lit_sel_diff_weight(handle) > select_weight)
1327 {
1328 select_weight = lit_sel_diff_weight(handle);
1329 selected = handle;
1330 }
1331 }
1332 handle = handle->next;
1333 }
1334 assert(selected);
1335 EqnSetProp(selected, EPIsSelected);
1336 }
1337
1338
1339 /*-----------------------------------------------------------------------
1340 //
1341 // Function: PSelectDiffNegativeLiteral()
1342 //
1343 // If clause has negative literals, select the most unbalanced one
1344 // of the clauses negative literals and all positive literals.
1345 //
1346 // Global Variables: -
1347 //
1348 // Side Effects : Changes property in literals
1349 //
1350 /----------------------------------------------------------------------*/
1351
PSelectDiffNegativeLiteral(OCB_p ocb,Clause_p clause)1352 void PSelectDiffNegativeLiteral(OCB_p ocb, Clause_p clause)
1353 {
1354 Eqn_p handle = clause->literals, selected = NULL;
1355 long select_weight = -1;
1356
1357 while(handle)
1358 {
1359 if(EqnIsPositive(handle))
1360 {
1361 EqnSetProp(handle, EPIsSelected);
1362 }
1363 else
1364 {
1365 if(lit_sel_diff_weight(handle) > select_weight)
1366 {
1367 select_weight = lit_sel_diff_weight(handle);
1368 selected = handle;
1369 }
1370 }
1371 handle = handle->next;
1372 }
1373 assert(selected);
1374 EqnSetProp(selected, EPIsSelected);
1375 }
1376
1377
1378 /*-----------------------------------------------------------------------
1379 //
1380 // Function: SelectGroundNegativeLiteral()
1381 //
1382 // If there are negative ground literals, select the one with maximal
1383 // lit_sel_diff_weight.
1384 //
1385 // Global Variables: -
1386 //
1387 // Side Effects : Changes property in literals
1388 //
1389 /----------------------------------------------------------------------*/
1390
SelectGroundNegativeLiteral(OCB_p ocb,Clause_p clause)1391 void SelectGroundNegativeLiteral(OCB_p ocb, Clause_p clause)
1392 {
1393 Eqn_p handle = clause->literals, selected = NULL;
1394 long select_weight = -1;
1395
1396 while(handle)
1397 {
1398 if(EqnIsNegative(handle) && EqnIsGround(handle))
1399 {
1400 if(lit_sel_diff_weight(handle) > select_weight)
1401 {
1402 select_weight = lit_sel_diff_weight(handle);
1403 selected = handle;
1404 }
1405 }
1406 handle = handle->next;
1407 }
1408 if(selected)
1409 {
1410 EqnSetProp(selected, EPIsSelected);
1411 }
1412 }
1413
1414
1415 /*-----------------------------------------------------------------------
1416 //
1417 // Function: PSelectGroundNegativeLiteral()
1418 //
1419 // If there are negative ground literals, select the one with maximal
1420 // lit_sel_diff_weight and select all positive literals.
1421 //
1422 // Global Variables: -
1423 //
1424 // Side Effects : Changes property in literals
1425 //
1426 /----------------------------------------------------------------------*/
1427
PSelectGroundNegativeLiteral(OCB_p ocb,Clause_p clause)1428 void PSelectGroundNegativeLiteral(OCB_p ocb, Clause_p clause)
1429 {
1430 Eqn_p handle = clause->literals, selected = NULL;
1431 long select_weight = -1;
1432
1433 while(handle)
1434 {
1435 if(EqnIsNegative(handle))
1436 {
1437 if(EqnIsGround(handle))
1438 {
1439 if(lit_sel_diff_weight(handle) > select_weight)
1440 {
1441 select_weight = lit_sel_diff_weight(handle);
1442 selected = handle;
1443 }
1444 }
1445 }
1446 else
1447 {
1448 assert(EqnIsPositive(handle));
1449 EqnSetProp(handle, EPIsSelected);
1450 }
1451 handle = handle->next;
1452 }
1453 if(selected)
1454 {
1455 EqnSetProp(selected, EPIsSelected);
1456 }
1457 else
1458 {
1459 EqnListDelProp(clause->literals, EPIsSelected);
1460 }
1461 }
1462
1463
1464 /*-----------------------------------------------------------------------
1465 //
1466 // Function: SelectOptimalLiteral()
1467 //
1468 // (Hah! Believe it at your peril ;-). If there is a ground negative
1469 // literal, select it, otherwise select the negative literal with the
1470 // largest size difference.
1471 //
1472 // Global Variables: -
1473 //
1474 // Side Effects : Changes property in literals
1475 //
1476 /----------------------------------------------------------------------*/
1477
SelectOptimalLiteral(OCB_p ocb,Clause_p clause)1478 void SelectOptimalLiteral(OCB_p ocb, Clause_p clause)
1479 {
1480 Eqn_p handle = clause->literals, selected = NULL;
1481 long select_weight = -1;
1482
1483 while(handle)
1484 {
1485 if(EqnIsNegative(handle) && EqnIsGround(handle))
1486 {
1487 if(lit_sel_diff_weight(handle) > select_weight)
1488 {
1489 select_weight = lit_sel_diff_weight(handle);
1490 selected = handle;
1491 }
1492 }
1493 handle = handle->next;
1494 }
1495 if(selected)
1496 {
1497 EqnSetProp(selected, EPIsSelected);
1498 }
1499 else
1500 {
1501 SelectDiffNegativeLiteral(ocb,clause);
1502 }
1503 }
1504
1505
1506
1507 /*-----------------------------------------------------------------------
1508 //
1509 // Function: PSelectOptimalLiteral()
1510 //
1511 // (Hah! Believe it at your peril ;-). If there is a ground negative
1512 // literal, select it, otherwise select the negative literal with the
1513 // largest size difference and all positive literals.
1514 //
1515 // Global Variables: -
1516 //
1517 // Side Effects : Changes property in literals
1518 //
1519 /----------------------------------------------------------------------*/
1520
PSelectOptimalLiteral(OCB_p ocb,Clause_p clause)1521 void PSelectOptimalLiteral(OCB_p ocb, Clause_p clause)
1522 {
1523 Eqn_p handle = clause->literals, selected = NULL;
1524 long select_weight = -1;
1525
1526 while(handle)
1527 {
1528 if(EqnIsNegative(handle) && EqnIsGround(handle))
1529 {
1530 if(lit_sel_diff_weight(handle) > select_weight)
1531 {
1532 select_weight = lit_sel_diff_weight(handle);
1533 selected = handle;
1534 }
1535 }
1536 handle = handle->next;
1537 }
1538 if(selected)
1539 {
1540 EqnSetProp(selected, EPIsSelected);
1541 }
1542 else
1543 {
1544 PSelectDiffNegativeLiteral(ocb,clause);
1545 }
1546 }
1547
1548
1549 /*-----------------------------------------------------------------------
1550 //
1551 // Function: SelectMinOptimalLiteral()
1552 //
1553 // If there is a ground negative
1554 // literal, select it, otherwise select the smallest negative
1555 // literal.
1556 //
1557 // Global Variables: -
1558 //
1559 // Side Effects : Changes property in literals
1560 //
1561 /----------------------------------------------------------------------*/
1562
SelectMinOptimalLiteral(OCB_p ocb,Clause_p clause)1563 void SelectMinOptimalLiteral(OCB_p ocb, Clause_p clause)
1564 {
1565 Eqn_p handle = clause->literals, selected = NULL;
1566 long select_weight = LONG_MAX, weight;
1567
1568 while(handle)
1569 {
1570 if(EqnIsNegative(handle) && EqnIsGround(handle))
1571 {
1572 weight = EqnStandardWeight(handle);
1573 if(weight < select_weight)
1574 {
1575 select_weight = weight;
1576 selected = handle;
1577 }
1578 }
1579 handle = handle->next;
1580 }
1581 if(selected)
1582 {
1583 EqnSetProp(selected, EPIsSelected);
1584 }
1585 else
1586 {
1587 SelectSmallestNegativeLiteral(ocb,clause);
1588 }
1589 }
1590
1591
1592 /*-----------------------------------------------------------------------
1593 //
1594 // Function: PSelectMinOptimalLiteral()
1595 //
1596 // If there is a ground negative
1597 // literal, select it, otherwise select the smallest negative
1598 // literal and positive literals.
1599 //
1600 // Global Variables: -
1601 //
1602 // Side Effects :
1603 //
1604 /----------------------------------------------------------------------*/
1605
PSelectMinOptimalLiteral(OCB_p ocb,Clause_p clause)1606 void PSelectMinOptimalLiteral(OCB_p ocb, Clause_p clause)
1607 {
1608 Eqn_p handle = clause->literals, selected = NULL;
1609 long select_weight = LONG_MAX, weight;
1610
1611 while(handle)
1612 {
1613 if(EqnIsNegative(handle) && EqnIsGround(handle))
1614 {
1615 weight = EqnStandardWeight(handle);
1616 if(weight < select_weight)
1617 {
1618 select_weight = weight;
1619 selected = handle;
1620 }
1621 }
1622 handle = handle->next;
1623 }
1624 if(selected)
1625 {
1626 EqnSetProp(selected, EPIsSelected);
1627 }
1628 else
1629 {
1630 PSelectSmallestNegativeLiteral(ocb,clause);
1631 }
1632 }
1633
1634
1635 /*-----------------------------------------------------------------------
1636 //
1637 // Function: SelectMinOptimalNoTypePred()
1638 //
1639 // If there is a ground negative
1640 // literal, select it, otherwise select the smallest negative
1641 // literal, but never select type literals.
1642 //
1643 // Global Variables: -
1644 //
1645 // Side Effects : Changes property in literals
1646 //
1647 /----------------------------------------------------------------------*/
1648
SelectMinOptimalNoTypePred(OCB_p ocb,Clause_p clause)1649 void SelectMinOptimalNoTypePred(OCB_p ocb, Clause_p clause)
1650 {
1651 Eqn_p selected = NULL;
1652
1653 selected = find_smallest_neg_ground_lit(clause);
1654
1655 if(!selected)
1656 {
1657 Eqn_p handle = clause->literals;
1658 long select_weight = LONG_MAX, weight;
1659 while(handle)
1660 {
1661 if(EqnIsNegative(handle) && !EqnIsTypePred(handle))
1662 {
1663 weight = EqnStandardWeight(handle);
1664 if(weight < select_weight)
1665 {
1666 select_weight = weight;
1667 selected = handle;
1668 }
1669 }
1670 handle = handle->next;
1671 }
1672 }
1673 if(selected)
1674 {
1675 EqnSetProp(selected, EPIsSelected);
1676 ClauseDelProp(clause, CPIsOriented);
1677 }
1678 }
1679
1680
1681 /*-----------------------------------------------------------------------
1682 //
1683 // Function: PSelectMinOptimalNoTypePred()
1684 //
1685 // If there is a ground negative
1686 // literal, select it, otherwise select the smallest negative
1687 // literal, but never select type literals. If a negative literal is
1688 // selected, also select positive ones.
1689 //
1690 // Global Variables: -
1691 //
1692 // Side Effects : Changes property in literals
1693 //
1694 /----------------------------------------------------------------------*/
1695
PSelectMinOptimalNoTypePred(OCB_p ocb,Clause_p clause)1696 void PSelectMinOptimalNoTypePred(OCB_p ocb, Clause_p clause)
1697 {
1698 Eqn_p selected = NULL;
1699
1700 selected = find_smallest_neg_ground_lit(clause);
1701
1702 if(!selected)
1703 {
1704 Eqn_p handle = clause->literals;
1705 long select_weight = LONG_MAX, weight;
1706 while(handle)
1707 {
1708 if(EqnIsNegative(handle) && !EqnIsTypePred(handle))
1709 {
1710 weight = EqnStandardWeight(handle);
1711 if(weight < select_weight)
1712 {
1713 select_weight = weight;
1714 selected = handle;
1715 }
1716 }
1717 handle = handle->next;
1718 }
1719 }
1720 if(selected)
1721 {
1722 EqnSetProp(selected, EPIsSelected);
1723 clause_select_pos(clause);
1724 ClauseDelProp(clause, CPIsOriented);
1725 }
1726 }
1727
1728
1729 /*-----------------------------------------------------------------------
1730 //
1731 // Function: SelectMinOptimalNoXTypePred()
1732 //
1733 // If there is a ground negative
1734 // literal, select it, otherwise select the smallest negative
1735 // literal, but never select extendet type literals.
1736 //
1737 // Global Variables: -
1738 //
1739 // Side Effects : Changes property in literals
1740 //
1741 /----------------------------------------------------------------------*/
1742
SelectMinOptimalNoXTypePred(OCB_p ocb,Clause_p clause)1743 void SelectMinOptimalNoXTypePred(OCB_p ocb, Clause_p clause)
1744 {
1745 Eqn_p selected = NULL;
1746
1747 selected = find_smallest_neg_ground_lit(clause);
1748
1749 if(!selected)
1750 {
1751 Eqn_p handle = clause->literals;
1752 long select_weight = LONG_MAX, weight;
1753 while(handle)
1754 {
1755 if(EqnIsNegative(handle) && !EqnIsXTypePred(handle))
1756 {
1757 weight = EqnStandardWeight(handle);
1758 if(weight < select_weight)
1759 {
1760 select_weight = weight;
1761 selected = handle;
1762 }
1763 }
1764 handle = handle->next;
1765 }
1766 }
1767 if(selected)
1768 {
1769 EqnSetProp(selected, EPIsSelected);
1770 ClauseDelProp(clause, CPIsOriented);
1771 }
1772 }
1773
1774
1775 /*-----------------------------------------------------------------------
1776 //
1777 // Function: PSelectMinOptimalNoXTypePred()
1778 //
1779 // If there is a ground negative
1780 // literal, select it, otherwise select the smallest negative
1781 // literal, but never select extendet type literals. If a negative
1782 // literal is selected, also select positive ones.
1783 //
1784 // Global Variables: -
1785 //
1786 // Side Effects : Changes property in literals
1787 //
1788 /----------------------------------------------------------------------*/
1789
PSelectMinOptimalNoXTypePred(OCB_p ocb,Clause_p clause)1790 void PSelectMinOptimalNoXTypePred(OCB_p ocb, Clause_p clause)
1791 {
1792 Eqn_p selected = NULL;
1793
1794 selected = find_smallest_neg_ground_lit(clause);
1795
1796 if(!selected)
1797 {
1798 Eqn_p handle = clause->literals;
1799 long select_weight = LONG_MAX, weight;
1800 while(handle)
1801 {
1802 if(EqnIsNegative(handle) && !EqnIsXTypePred(handle))
1803 {
1804 weight = EqnStandardWeight(handle);
1805 if(weight < select_weight)
1806 {
1807 select_weight = weight;
1808 selected = handle;
1809 }
1810 }
1811 handle = handle->next;
1812 }
1813 }
1814 if(selected)
1815 {
1816 EqnSetProp(selected, EPIsSelected);
1817 clause_select_pos(clause);
1818 ClauseDelProp(clause, CPIsOriented);
1819 }
1820 }
1821
1822
1823 /*-----------------------------------------------------------------------
1824 //
1825 // Function: SelectMinOptimalNoRXTypePred()
1826 //
1827 // If there is a ground negative
1828 // literal, select it, otherwise select the smallest negative
1829 // literal, but never select real extended type literals.
1830 //
1831 // Global Variables: -
1832 //
1833 // Side Effects : Changes property in literals
1834 //
1835 /----------------------------------------------------------------------*/
1836
SelectMinOptimalNoRXTypePred(OCB_p ocb,Clause_p clause)1837 void SelectMinOptimalNoRXTypePred(OCB_p ocb, Clause_p clause)
1838 {
1839 Eqn_p selected = NULL;
1840
1841 selected = find_smallest_neg_ground_lit(clause);
1842
1843 if(!selected)
1844 {
1845 Eqn_p handle = clause->literals;
1846 long select_weight = LONG_MAX, weight;
1847 while(handle)
1848 {
1849 if(EqnIsNegative(handle) && !EqnIsRealXTypePred(handle))
1850 {
1851 weight = EqnStandardWeight(handle);
1852 if(weight < select_weight)
1853 {
1854 select_weight = weight;
1855 selected = handle;
1856 }
1857 }
1858 handle = handle->next;
1859 }
1860 }
1861 if(selected)
1862 {
1863 EqnSetProp(selected, EPIsSelected);
1864 ClauseDelProp(clause, CPIsOriented);
1865 }
1866 }
1867
1868
1869 /*-----------------------------------------------------------------------
1870 //
1871 // Function: PSelectMinOptimalNoRXTypePred()
1872 //
1873 // If there is a ground negative
1874 // literal, select it, otherwise select the smallest negative
1875 // literal, but never select real extendet type literals. If a
1876 // negative literal is selected, also select positive ones.
1877 //
1878 // Global Variables: -
1879 //
1880 // Side Effects : Changes property in literals
1881 //
1882 /----------------------------------------------------------------------*/
1883
PSelectMinOptimalNoRXTypePred(OCB_p ocb,Clause_p clause)1884 void PSelectMinOptimalNoRXTypePred(OCB_p ocb, Clause_p clause)
1885 {
1886 Eqn_p selected = NULL;
1887
1888 selected = find_smallest_neg_ground_lit(clause);
1889
1890 if(!selected)
1891 {
1892 Eqn_p handle = clause->literals;
1893 long select_weight = LONG_MAX, weight;
1894 while(handle)
1895 {
1896 if(EqnIsNegative(handle) && !EqnIsRealXTypePred(handle))
1897 {
1898 weight = EqnStandardWeight(handle);
1899 if(weight < select_weight)
1900 {
1901 select_weight = weight;
1902 selected = handle;
1903 }
1904 }
1905 handle = handle->next;
1906 }
1907 }
1908 if(selected)
1909 {
1910 EqnSetProp(selected, EPIsSelected);
1911 clause_select_pos(clause);
1912 ClauseDelProp(clause, CPIsOriented);
1913 }
1914 }
1915
1916
1917 /*-----------------------------------------------------------------------
1918 //
1919 // Function: SelectCondOptimalLiteral()
1920 //
1921 // As above, but if the clause has a positive literal that is very
1922 // uninstantiated, select no literal at all.
1923 //
1924 // Global Variables: -
1925 //
1926 // Side Effects : Changes property in literals
1927 //
1928 /----------------------------------------------------------------------*/
1929
1930 #define VAR_FACTOR 3
1931
SelectCondOptimalLiteral(OCB_p ocb,Clause_p clause)1932 void SelectCondOptimalLiteral(OCB_p ocb, Clause_p clause)
1933 {
1934 Eqn_p handle = clause->literals;
1935 bool found = false;
1936 long weight, sweight;
1937
1938 while(handle)
1939 {
1940 if(EqnIsPositive(handle))
1941 {
1942 weight = TermWeight(handle->lterm, 0,VAR_FACTOR);
1943 sweight = TermStandardWeight(handle->lterm);
1944
1945 if(EqnIsEquLit(handle))
1946 {
1947 weight += TermWeight(handle->rterm, 0,VAR_FACTOR);
1948 sweight += TermStandardWeight(handle->rterm);
1949 }
1950 if(sweight <= weight)
1951 {
1952 found = true;
1953 break;
1954 }
1955 }
1956 handle = handle->next;
1957 }
1958 if(!found)
1959 {
1960 SelectOptimalLiteral(ocb,clause);
1961 }
1962 else
1963 {
1964 EqnListDelProp(clause->literals, EPIsSelected);
1965 }
1966 }
1967
1968
1969 /*-----------------------------------------------------------------------
1970 //
1971 // Function: PSelectCondOptimalLiteral()
1972 //
1973 // As above, but select positive literals as well.
1974 //
1975 // Global Variables: -
1976 //
1977 // Side Effects : Changes property in literals
1978 //
1979 /----------------------------------------------------------------------*/
1980
PSelectCondOptimalLiteral(OCB_p ocb,Clause_p clause)1981 void PSelectCondOptimalLiteral(OCB_p ocb, Clause_p clause)
1982 {
1983 Eqn_p handle = clause->literals;
1984 bool found = false;
1985 long weight, sweight;
1986
1987 while(handle)
1988 {
1989 if(EqnIsPositive(handle))
1990 {
1991 weight = TermWeight(handle->lterm, 0,VAR_FACTOR);
1992 sweight = TermStandardWeight(handle->lterm);
1993
1994 if(EqnIsEquLit(handle))
1995 {
1996 weight += TermWeight(handle->rterm, 0,VAR_FACTOR);
1997 sweight += TermStandardWeight(handle->rterm);
1998 }
1999 if(sweight <= weight)
2000 {
2001 found = true;
2002 break;
2003 }
2004 }
2005 handle = handle->next;
2006 }
2007 if(!found)
2008 {
2009 PSelectOptimalLiteral(ocb,clause);
2010 }
2011 else
2012 {
2013 EqnListDelProp(clause->literals, EPIsSelected);
2014 }
2015 }
2016
2017
2018 /*-----------------------------------------------------------------------
2019 //
2020 // Function: SelectAllCondOptimalLiteral()
2021 //
2022 // As above, but if the clause has only positive literals that are very
2023 // uninstantiated, select no literal at all.
2024 //
2025 // Global Variables: -
2026 //
2027 // Side Effects : Changes property in literals
2028 //
2029 /----------------------------------------------------------------------*/
2030
SelectAllCondOptimalLiteral(OCB_p ocb,Clause_p clause)2031 void SelectAllCondOptimalLiteral(OCB_p ocb, Clause_p clause)
2032 {
2033 Eqn_p handle = clause->literals;
2034 bool found = true;
2035 long weight, sweight;
2036
2037 while(handle)
2038 {
2039 if(EqnIsPositive(handle))
2040 {
2041 weight = TermWeight(handle->lterm, 0,VAR_FACTOR);
2042 sweight = TermStandardWeight(handle->lterm);
2043
2044 if(EqnIsEquLit(handle))
2045 {
2046 weight += TermWeight(handle->rterm, 0,VAR_FACTOR);
2047 sweight += TermStandardWeight(handle->rterm);
2048 }
2049 if(sweight > weight)
2050 {
2051 found = false;
2052 break;
2053 }
2054 }
2055 handle = handle->next;
2056 }
2057 if(!found)
2058 {
2059 SelectOptimalLiteral(ocb,clause);
2060 }
2061 else
2062 {
2063 EqnListDelProp(clause->literals, EPIsSelected);
2064 }
2065 }
2066
2067
2068 /*-----------------------------------------------------------------------
2069 //
2070 // Function: PSelectAllCondOptimalLiteral()
2071 //
2072 // As above, but select positive literals as well.
2073 //
2074 // Global Variables: -
2075 //
2076 // Side Effects : Changes property in literals
2077 //
2078 /----------------------------------------------------------------------*/
2079
PSelectAllCondOptimalLiteral(OCB_p ocb,Clause_p clause)2080 void PSelectAllCondOptimalLiteral(OCB_p ocb, Clause_p clause)
2081 {
2082 Eqn_p handle = clause->literals;
2083 bool found = true;
2084 long weight, sweight;
2085
2086 while(handle)
2087 {
2088 if(EqnIsPositive(handle))
2089 {
2090 weight = TermWeight(handle->lterm, 0,VAR_FACTOR);
2091 sweight = TermStandardWeight(handle->lterm);
2092
2093 if(EqnIsEquLit(handle))
2094 {
2095 weight += TermWeight(handle->rterm, 0,VAR_FACTOR);
2096 sweight += TermStandardWeight(handle->rterm);
2097 }
2098 if(sweight > weight)
2099 {
2100 found = false;
2101 break;
2102 }
2103 }
2104 handle = handle->next;
2105 }
2106 if(!found)
2107 {
2108 PSelectOptimalLiteral(ocb,clause);
2109 }
2110 else
2111 {
2112 EqnListDelProp(clause->literals, EPIsSelected);
2113 }
2114 }
2115
2116
2117 /*-----------------------------------------------------------------------
2118 //
2119 // Function: SelectDepth2OptimalLiteral()
2120 //
2121 // Select optimal literal unless there is a literal with depth <= 2,
2122 // then select no literal.
2123 //
2124 // Global Variables: -
2125 //
2126 // Side Effects : -
2127 //
2128 /----------------------------------------------------------------------*/
2129
SelectDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2130 void SelectDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2131 {
2132 Eqn_p handle = clause->literals;
2133 bool found = false;
2134
2135 while(handle)
2136 {
2137 if(EqnDepth(handle)<=2)
2138 {
2139 found = true;
2140 break;
2141 }
2142 handle = handle->next;
2143 }
2144 if(!found)
2145 {
2146 SelectOptimalLiteral(ocb,clause);
2147 }
2148 else
2149 {
2150 EqnListDelProp(clause->literals, EPIsSelected);
2151 }
2152 }
2153
2154
2155 /*-----------------------------------------------------------------------
2156 //
2157 // Function: PSelectDepth2OptimalLiteral()
2158 //
2159 // As above, but select positive literals as well.
2160 //
2161 // Global Variables: -
2162 //
2163 // Side Effects : Changes property in literals
2164 //
2165 /----------------------------------------------------------------------*/
2166
PSelectDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2167 void PSelectDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2168 {
2169 Eqn_p handle = clause->literals;
2170 bool found = false;
2171
2172 while(handle)
2173 {
2174 if(EqnDepth(handle)<=2)
2175 {
2176 found = true;
2177 break;
2178 }
2179 handle = handle->next;
2180 }
2181 if(!found)
2182 {
2183 PSelectOptimalLiteral(ocb,clause);
2184 }
2185 else
2186 {
2187 EqnListDelProp(clause->literals, EPIsSelected);
2188 }
2189 }
2190
2191
2192 /*-----------------------------------------------------------------------
2193 //
2194 // Function: SelectPDepth2OptimalLiteral()
2195 //
2196 // Select optimal literal unless there is a positive literal with
2197 // depth <= 2, then select no literal.
2198 //
2199 // Global Variables: -
2200 //
2201 // Side Effects : Changes property in literals
2202 //
2203 /----------------------------------------------------------------------*/
2204
SelectPDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2205 void SelectPDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2206 {
2207 Eqn_p handle = clause->literals;
2208 bool found = false;
2209
2210 while(handle)
2211 {
2212 if(EqnIsPositive(handle) && (EqnDepth(handle)<=2))
2213 {
2214 found = true;
2215 break;
2216 }
2217 handle = handle->next;
2218 }
2219 if(!found)
2220 {
2221 SelectOptimalLiteral(ocb,clause);
2222 }
2223 else
2224 {
2225 EqnListDelProp(clause->literals, EPIsSelected);
2226 }
2227 }
2228
2229
2230 /*-----------------------------------------------------------------------
2231 //
2232 // Function: PSelectPDepth2OptimalLiteral()
2233 //
2234 // As above, with positive literals.
2235 //
2236 // Global Variables: -
2237 //
2238 // Side Effects : Changes property in literals
2239 //
2240 /----------------------------------------------------------------------*/
2241
PSelectPDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2242 void PSelectPDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2243 {
2244 Eqn_p handle = clause->literals;
2245 bool found = false;
2246
2247 while(handle)
2248 {
2249 if(EqnIsPositive(handle) && (EqnDepth(handle)<=2))
2250 {
2251 found = true;
2252 break;
2253 }
2254 handle = handle->next;
2255 }
2256 if(!found)
2257 {
2258 PSelectOptimalLiteral(ocb,clause);
2259 }
2260 else
2261 {
2262 EqnListDelProp(clause->literals, EPIsSelected);
2263 }
2264 }
2265
2266
2267 /*-----------------------------------------------------------------------
2268 //
2269 // Function: SelectNDepth2OptimalLiteral()
2270 //
2271 // Select optimal literal unless there is a negative literal with
2272 // depth <= 2, then select no literal.
2273 //
2274 // Global Variables: -
2275 //
2276 // Side Effects : Changes property in literals
2277 //
2278 /----------------------------------------------------------------------*/
2279
SelectNDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2280 void SelectNDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2281 {
2282 Eqn_p handle = clause->literals;
2283 bool found = false;
2284
2285 while(handle)
2286 {
2287 if(EqnIsNegative(handle) && (EqnDepth(handle)<=2))
2288 {
2289 found = true;
2290 break;
2291 }
2292 handle = handle->next;
2293 }
2294 if(!found)
2295 {
2296 SelectOptimalLiteral(ocb,clause);
2297 }
2298 else
2299 {
2300 EqnListDelProp(clause->literals, EPIsSelected);
2301 }
2302 }
2303
2304
2305 /*-----------------------------------------------------------------------
2306 //
2307 // Function: PSelectNDepth2OptimalLiteral()
2308 //
2309 // As above, with positive literals.
2310 //
2311 // Global Variables: -
2312 //
2313 // Side Effects : Changes property in literals
2314 //
2315 /----------------------------------------------------------------------*/
2316
PSelectNDepth2OptimalLiteral(OCB_p ocb,Clause_p clause)2317 void PSelectNDepth2OptimalLiteral(OCB_p ocb, Clause_p clause)
2318 {
2319 Eqn_p handle = clause->literals;
2320 bool found = false;
2321
2322 while(handle)
2323 {
2324 if(EqnIsNegative(handle) && (EqnDepth(handle)<=2))
2325 {
2326 found = true;
2327 break;
2328 }
2329 handle = handle->next;
2330 }
2331 if(!found)
2332 {
2333 PSelectOptimalLiteral(ocb,clause);
2334 }
2335 else
2336 {
2337 EqnListDelProp(clause->literals, EPIsSelected);
2338 }
2339 }
2340
2341
2342 /*-----------------------------------------------------------------------
2343 //
2344 // Function: SelectNonRROptimalLiteral()
2345 //
2346 // If a clause is not range-restricted, select the optimal literal,
2347 // otherwise select no literal.
2348 //
2349 // Global Variables: -
2350 //
2351 // Side Effects : Minimal ;-) (only by called functions)
2352 //
2353 /----------------------------------------------------------------------*/
2354
SelectNonRROptimalLiteral(OCB_p ocb,Clause_p clause)2355 void SelectNonRROptimalLiteral(OCB_p ocb, Clause_p clause)
2356 {
2357 if(!ClauseIsRangeRestricted(clause))
2358 {
2359 SelectOptimalLiteral(ocb,clause);
2360 }
2361 }
2362
2363
2364 /*-----------------------------------------------------------------------
2365 //
2366 // Function: PSelectNonRROptimalLiteral()
2367 //
2368 // If a clause is not range-restricted, select the optimal literal
2369 // and positive literals, otherwise select no literal.
2370 //
2371 // Global Variables: -
2372 //
2373 // Side Effects : Minimal ;-) (only by called functions)
2374 //
2375 /----------------------------------------------------------------------*/
2376
PSelectNonRROptimalLiteral(OCB_p ocb,Clause_p clause)2377 void PSelectNonRROptimalLiteral(OCB_p ocb, Clause_p clause)
2378 {
2379 if(!ClauseIsRangeRestricted(clause))
2380 {
2381 PSelectOptimalLiteral(ocb,clause);
2382 }
2383 }
2384
2385
2386 /*-----------------------------------------------------------------------
2387 //
2388 // Function: SelectNonStrongRROptimalLiteral()
2389 //
2390 // If a clause is not strongly range-restricted, select the optimal
2391 // literal, otherwise select no literal.
2392 //
2393 // Global Variables: -
2394 //
2395 // Side Effects : Minimal ;-) (only by called functions)
2396 //
2397 /----------------------------------------------------------------------*/
2398
SelectNonStrongRROptimalLiteral(OCB_p ocb,Clause_p clause)2399 void SelectNonStrongRROptimalLiteral(OCB_p ocb, Clause_p clause)
2400 {
2401 if(!ClauseIsStronglyRangeRestricted(clause))
2402 {
2403 SelectOptimalLiteral(ocb,clause);
2404 }
2405 }
2406
2407
2408 /*-----------------------------------------------------------------------
2409 //
2410 // Function: PSelectNonStrongRROptimalLiteral()
2411 //
2412 // If a clause is not Strong range-restricted, select the optimal
2413 // literal and positive literals, otherwise select no literal.
2414 //
2415 // Global Variables: -
2416 //
2417 // Side Effects : Minimal ;-) (only by called functions)
2418 //
2419 /----------------------------------------------------------------------*/
2420
PSelectNonStrongRROptimalLiteral(OCB_p ocb,Clause_p clause)2421 void PSelectNonStrongRROptimalLiteral(OCB_p ocb, Clause_p clause)
2422 {
2423 if(!ClauseIsStronglyRangeRestricted(clause))
2424 {
2425 PSelectOptimalLiteral(ocb,clause);
2426 }
2427 }
2428
2429
2430
2431 /*-----------------------------------------------------------------------
2432 //
2433 // Function: SelectAntiRROptimalLiteral()
2434 //
2435 // If a clause is anti-range-restricted, select the optimal literal,
2436 // otherwise select no literal.
2437 //
2438 // Global Variables: -
2439 //
2440 // Side Effects : Minimal ;-) (only by called functions)
2441 //
2442 /----------------------------------------------------------------------*/
2443
SelectAntiRROptimalLiteral(OCB_p ocb,Clause_p clause)2444 void SelectAntiRROptimalLiteral(OCB_p ocb, Clause_p clause)
2445 {
2446 assert(clause);
2447 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
2448
2449 if(clause->neg_lit_no==0)
2450 {
2451 return;
2452 }
2453 if(ClauseIsAntiRangeRestricted(clause))
2454 {
2455 SelectOptimalLiteral(ocb,clause);
2456 }
2457 }
2458
2459
2460 /*-----------------------------------------------------------------------
2461 //
2462 // Function: PSelectAntiRROptimalLiteral()
2463 //
2464 // If a clause is anti-range-restricted, select the optimal literal
2465 // and positive literals, otherwise select no literal.
2466 //
2467 // Global Variables: -
2468 //
2469 // Side Effects : Minimal ;-) (only by called functions)
2470 //
2471 /----------------------------------------------------------------------*/
2472
PSelectAntiRROptimalLiteral(OCB_p ocb,Clause_p clause)2473 void PSelectAntiRROptimalLiteral(OCB_p ocb, Clause_p clause)
2474 {
2475 if(ClauseIsAntiRangeRestricted(clause))
2476 {
2477 PSelectOptimalLiteral(ocb,clause);
2478 }
2479 }
2480
2481
2482 /*-----------------------------------------------------------------------
2483 //
2484 // Function: SelectNonAntiRROptimalLiteral()
2485 //
2486 // If a clause is not anti-range-restricted, select the optimal
2487 // literal, otherwise select no literal.
2488 //
2489 // Global Variables: -
2490 //
2491 // Side Effects : Minimal ;-) (only by called functions)
2492 //
2493 /----------------------------------------------------------------------*/
2494
SelectNonAntiRROptimalLiteral(OCB_p ocb,Clause_p clause)2495 void SelectNonAntiRROptimalLiteral(OCB_p ocb, Clause_p clause)
2496 {
2497 if(!ClauseIsAntiRangeRestricted(clause))
2498 {
2499 SelectOptimalLiteral(ocb,clause);
2500 }
2501 }
2502
2503
2504 /*-----------------------------------------------------------------------
2505 //
2506 // Function: PSelectNonAntiRROptimalLiteral()
2507 //
2508 // If a clause is not anti-range-restricted, select the optimal literal
2509 // and positive literals, otherwise select no literal.
2510 //
2511 // Global Variables: -
2512 //
2513 // Side Effects : Minimal ;-) (only by called functions)
2514 //
2515 /----------------------------------------------------------------------*/
2516
PSelectNonAntiRROptimalLiteral(OCB_p ocb,Clause_p clause)2517 void PSelectNonAntiRROptimalLiteral(OCB_p ocb, Clause_p clause)
2518 {
2519 if(!ClauseIsAntiRangeRestricted(clause))
2520 {
2521 PSelectOptimalLiteral(ocb,clause);
2522 }
2523 }
2524
2525
2526 /*-----------------------------------------------------------------------
2527 //
2528 // Function: SelectStrongRRNonRROptimalLiteral()
2529 //
2530 // If a clause is not range-restricted or strongly range-restricted
2531 // select the optimal literal, otherwise select no literal.
2532 //
2533 // Global Variables: -
2534 //
2535 // Side Effects : Minimal ;-) (only by called functions)
2536 //
2537 /----------------------------------------------------------------------*/
2538
SelectStrongRRNonRROptimalLiteral(OCB_p ocb,Clause_p clause)2539 void SelectStrongRRNonRROptimalLiteral(OCB_p ocb, Clause_p clause)
2540 {
2541 if(!ClauseIsRangeRestricted(clause)||
2542 ClauseIsStronglyRangeRestricted(clause))
2543 {
2544 SelectOptimalLiteral(ocb,clause);
2545 }
2546 }
2547
2548 /*-----------------------------------------------------------------------
2549 //
2550 // Function: PSelectStrongRRNonRROptimalLiteral()
2551 //
2552 // If a clause is not range-restricted or strongly range-restricted
2553 // select the optimal literal and positive literals, otherwise
2554 // select no literal.
2555 //
2556 // Global Variables: -
2557 //
2558 // Side Effects : Minimal ;-) (only by called functions)
2559 //
2560 /----------------------------------------------------------------------*/
2561
PSelectStrongRRNonRROptimalLiteral(OCB_p ocb,Clause_p clause)2562 void PSelectStrongRRNonRROptimalLiteral(OCB_p ocb, Clause_p clause)
2563 {
2564 if(!ClauseIsRangeRestricted(clause)||
2565 ClauseIsStronglyRangeRestricted(clause))
2566 {
2567 PSelectOptimalLiteral(ocb,clause);
2568 }
2569 else
2570 {
2571 EqnListDelProp(clause->literals, EPIsSelected);
2572 }
2573 }
2574
2575
2576 /*-----------------------------------------------------------------------
2577 //
2578 // Function: SelectUnlessUniqMaxOptimalLiteral()
2579 //
2580 // If a clause has a single maximal literal, do not select,
2581 // otherwise select the optimal literal.
2582 //
2583 // Global Variables: -
2584 //
2585 // Side Effects : Changes property in literals
2586 //
2587 /----------------------------------------------------------------------*/
2588
SelectUnlessUniqMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2589 void SelectUnlessUniqMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2590 {
2591 ClauseCondMarkMaximalTerms(ocb, clause);
2592
2593 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)>1)
2594 {
2595 SelectOptimalLiteral(ocb,clause);
2596 ClauseDelProp(clause, CPIsOriented);
2597 }
2598 }
2599
2600 /*-----------------------------------------------------------------------
2601 //
2602 // Function: PSelectUnlessUniqMaxOptimalLiteral()
2603 //
2604 // If a clause has a single maximal literal, do not select,
2605 // otherwise select the optimal literal.
2606 //
2607 // Global Variables: -
2608 //
2609 // Side Effects : Changes property in literals
2610 //
2611 /----------------------------------------------------------------------*/
2612
PSelectUnlessUniqMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2613 void PSelectUnlessUniqMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2614 {
2615 ClauseCondMarkMaximalTerms(ocb, clause);
2616
2617 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)>1)
2618 {
2619 PSelectOptimalLiteral(ocb,clause);
2620 ClauseDelProp(clause, CPIsOriented);
2621 }
2622 }
2623
2624
2625 /*-----------------------------------------------------------------------
2626 //
2627 // Function: SelectUnlessUniqMaxSmallestOrientable()
2628 //
2629 // If a clause has a single maximal literal, do not select,
2630 // otherwise select the smallest orientable literal.
2631 //
2632 // Global Variables: -
2633 //
2634 // Side Effects : Changes property in literals
2635 //
2636 /----------------------------------------------------------------------*/
2637
SelectUnlessUniqMaxSmallestOrientable(OCB_p ocb,Clause_p clause)2638 void SelectUnlessUniqMaxSmallestOrientable(OCB_p ocb, Clause_p clause)
2639 {
2640 ClauseCondMarkMaximalTerms(ocb, clause);
2641
2642 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)>1)
2643 {
2644 SelectSmallestOrientableLiteral(ocb,clause);
2645 ClauseDelProp(clause, CPIsOriented);
2646 }
2647 }
2648
2649
2650 /*-----------------------------------------------------------------------
2651 //
2652 // Function: PSelectUnlessUniqMaxSmallestOrientable()
2653 //
2654 // If a clause has a single maximal literal, do not select,
2655 // otherwise select the smallest orientable literal and all positive
2656 // ones.
2657 //
2658 // Global Variables: -
2659 //
2660 // Side Effects : Changes property in literals
2661 //
2662 /----------------------------------------------------------------------*/
2663
PSelectUnlessUniqMaxSmallestOrientable(OCB_p ocb,Clause_p clause)2664 void PSelectUnlessUniqMaxSmallestOrientable(OCB_p ocb, Clause_p clause)
2665 {
2666 ClauseCondMarkMaximalTerms(ocb, clause);
2667
2668 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)>1)
2669 {
2670 PSelectSmallestOrientableLiteral(ocb,clause);
2671 ClauseDelProp(clause, CPIsOriented);
2672 }
2673 }
2674
2675
2676
2677 /*-----------------------------------------------------------------------
2678 //
2679 // Function: SelectUnlessPosMaxOptimalLiteral()
2680 //
2681 // If a clause has a positive maximal literal (i.e. is potentially
2682 // reductive), do not select, otherwise select optimal literal.
2683 //
2684 // Global Variables: -
2685 //
2686 // Side Effects : Changes property in literals
2687 //
2688 /----------------------------------------------------------------------*/
2689
SelectUnlessPosMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2690 void SelectUnlessPosMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2691 {
2692 ClauseCondMarkMaximalTerms(ocb, clause);
2693
2694 if(EqnListQueryPropNumber(clause->literals,
2695 EPIsMaximal|EPIsPositive)==0)
2696 {
2697 SelectOptimalLiteral(ocb,clause);
2698 ClauseDelProp(clause, CPIsOriented);
2699 }
2700 }
2701
2702 /*-----------------------------------------------------------------------
2703 //
2704 // Function: PSelectUnlessPosMaxOptimalLiteral()
2705 //
2706 // If a clause has a positive maximal literal (i.e. is potentially
2707 // reductive), do not select, otherwise select optimal literal and
2708 // positive literals.
2709 //
2710 // Global Variables: -
2711 //
2712 // Side Effects : Changes property in literals
2713 //
2714 /----------------------------------------------------------------------*/
2715
PSelectUnlessPosMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2716 void PSelectUnlessPosMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2717 {
2718 ClauseCondMarkMaximalTerms(ocb, clause);
2719
2720 if(EqnListQueryPropNumber(clause->literals,
2721 EPIsMaximal|EPIsPositive)==0)
2722 {
2723 PSelectOptimalLiteral(ocb,clause);
2724 ClauseDelProp(clause, CPIsOriented);
2725 }
2726 }
2727
2728
2729 /*-----------------------------------------------------------------------
2730 //
2731 // Function: SelectUnlessUniqPosMaxOptimalLiteral()
2732 //
2733 // If a clause has a uniqe positive maximal literal do not select,
2734 // otherwise select optimal literal.
2735 //
2736 // Global Variables: -
2737 //
2738 // Side Effects : -
2739 //
2740 /----------------------------------------------------------------------*/
2741
SelectUnlessUniqPosMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2742 void SelectUnlessUniqPosMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2743 {
2744 ClauseCondMarkMaximalTerms(ocb, clause);
2745
2746 if(EqnListQueryPropNumber(clause->literals,
2747 EPIsMaximal|EPIsPositive)!=1)
2748 {
2749 SelectOptimalLiteral(ocb,clause);
2750 ClauseDelProp(clause, CPIsOriented);
2751 }
2752 }
2753
2754
2755 /*-----------------------------------------------------------------------
2756 //
2757 // Function: PSelectUnlessUniqPosMaxOptimalLiteral()
2758 //
2759 // If a clause has a uniqe positive maximal literal do not select,
2760 // otherwise select optimal literal and positive literals.
2761 //
2762 // Global Variables: -
2763 //
2764 // Side Effects : Changes property in literals
2765 //
2766 /----------------------------------------------------------------------*/
2767
PSelectUnlessUniqPosMaxOptimalLiteral(OCB_p ocb,Clause_p clause)2768 void PSelectUnlessUniqPosMaxOptimalLiteral(OCB_p ocb, Clause_p clause)
2769 {
2770 ClauseCondMarkMaximalTerms(ocb, clause);
2771
2772 if(EqnListQueryPropNumber(clause->literals,
2773 EPIsMaximal|EPIsPositive)!=1)
2774 {
2775 PSelectOptimalLiteral(ocb,clause);
2776 ClauseDelProp(clause, CPIsOriented);
2777 }
2778 }
2779
2780
2781 /*-----------------------------------------------------------------------
2782 //
2783 // Function: SelectUnlessUniqMaxPosOptimalLiteral()
2784 //
2785 // If a clause has a maximal literal that is positive, do not
2786 // select, otherwise select optimal literal.
2787 //
2788 // Global Variables: -
2789 //
2790 // Side Effects : -
2791 //
2792 /----------------------------------------------------------------------*/
2793
SelectUnlessUniqMaxPosOptimalLiteral(OCB_p ocb,Clause_p clause)2794 void SelectUnlessUniqMaxPosOptimalLiteral(OCB_p ocb, Clause_p clause)
2795 {
2796 Eqn_p handle;
2797 bool found = false;
2798
2799 ClauseCondMarkMaximalTerms(ocb, clause);
2800
2801 for(handle=clause->literals; handle; handle=handle->next)
2802 {
2803 if(EqnIsMaximal(handle))
2804 {
2805 if(!EqnIsPositive(handle))
2806 {
2807 break;
2808 }
2809 if(found)
2810 {
2811 break;
2812 }
2813 found = true;
2814 }
2815 }
2816 if(handle)
2817 {
2818 SelectOptimalLiteral(ocb,clause);
2819 ClauseDelProp(clause, CPIsOriented);
2820 }
2821 }
2822
2823
2824 /*-----------------------------------------------------------------------
2825 //
2826 // Function: PSelectUnlessUniqMaxPosOptimalLiteral()
2827 //
2828 // If a clause has a maximal literal that is positive, do not
2829 // select, otherwise select optimal literal.
2830 //
2831 // Global Variables: -
2832 //
2833 // Side Effects : Changes property in literals
2834 //
2835 /----------------------------------------------------------------------*/
2836
PSelectUnlessUniqMaxPosOptimalLiteral(OCB_p ocb,Clause_p clause)2837 void PSelectUnlessUniqMaxPosOptimalLiteral(OCB_p ocb, Clause_p clause)
2838 {
2839 Eqn_p handle;
2840 bool found = false;
2841
2842 ClauseCondMarkMaximalTerms(ocb, clause);
2843
2844 for(handle=clause->literals; handle; handle=handle->next)
2845 {
2846 if(EqnIsMaximal(handle))
2847 {
2848 if(!EqnIsPositive(handle))
2849 {
2850 break;
2851 }
2852 if(found)
2853 {
2854 break;
2855 }
2856 found = true;
2857 }
2858 }
2859 if(handle)
2860 {
2861 PSelectOptimalLiteral(ocb,clause);
2862 ClauseDelProp(clause, CPIsOriented);
2863 }
2864 }
2865
2866
2867 /*-----------------------------------------------------------------------
2868 //
2869 // Function: SelectComplex()
2870 //
2871 // If there is a pure variable literal, select it. Otherwise, if
2872 // there is at least one ground literal, select the smallest
2873 // one. Otherwise, select the literal with the largest size
2874 // difference.
2875 //
2876 // Global Variables: -
2877 //
2878 // Side Effects : Changes property in literals
2879 //
2880 /----------------------------------------------------------------------*/
2881
SelectComplex(OCB_p ocb,Clause_p clause)2882 void SelectComplex(OCB_p ocb, Clause_p clause)
2883 {
2884 Eqn_p handle, selected;
2885 long select_weight, weight;
2886
2887 selected = ClauseFindNegPureVarLit(clause);
2888
2889 if(!selected)
2890 {
2891 select_weight = LONG_MAX;
2892 handle = clause->literals;
2893
2894 while(handle)
2895 {
2896 if(EqnIsNegative(handle) && EqnIsGround(handle))
2897 {
2898 weight = EqnStandardWeight(handle);
2899 if(weight < select_weight)
2900 {
2901 select_weight = weight;
2902 selected = handle;
2903 }
2904 }
2905 handle = handle->next;
2906 }
2907 }
2908 if(selected)
2909 {
2910 EqnSetProp(selected, EPIsSelected);
2911 }
2912 else
2913 {
2914 SelectDiffNegativeLiteral(ocb, clause);
2915 }
2916 }
2917
2918
2919 /*-----------------------------------------------------------------------
2920 //
2921 // Function: PSelectComplex()
2922 //
2923 // If there is a pure variable literal, select it. Otherwise, if
2924 // there is at least one ground literal, select the smallest
2925 // one. Otherwise, select the literal with the largest size
2926 // difference and the positive literals.
2927 //
2928 // Global Variables: -
2929 //
2930 // Side Effects : Changes property in literals
2931 //
2932 /----------------------------------------------------------------------*/
2933
PSelectComplex(OCB_p ocb,Clause_p clause)2934 void PSelectComplex(OCB_p ocb, Clause_p clause)
2935 {
2936 Eqn_p handle, selected;
2937 long select_weight, weight;
2938
2939 selected = ClauseFindNegPureVarLit(clause);
2940
2941 if(!selected)
2942 {
2943 select_weight = LONG_MAX;
2944 handle = clause->literals;
2945
2946 while(handle)
2947 {
2948 if(EqnIsNegative(handle) && EqnIsGround(handle))
2949 {
2950 weight = EqnStandardWeight(handle);
2951 if(weight < select_weight)
2952 {
2953 select_weight = weight;
2954 selected = handle;
2955 }
2956 }
2957 handle = handle->next;
2958 }
2959 }
2960 if(selected)
2961 {
2962 EqnSetProp(selected, EPIsSelected);
2963 }
2964 else
2965 {
2966 PSelectDiffNegativeLiteral(ocb, clause);
2967 }
2968 }
2969
2970 /*-----------------------------------------------------------------------
2971 //
2972 // Function: SelectComplexExceptRRHorn()
2973 //
2974 // If a clause is Horn and range-restricted, do no select. Otherwise
2975 // use SelectComplex() (above).
2976 //
2977 // Global Variables: -
2978 //
2979 // Side Effects : Changes property in literals
2980 //
2981 /----------------------------------------------------------------------*/
2982
SelectComplexExceptRRHorn(OCB_p ocb,Clause_p clause)2983 void SelectComplexExceptRRHorn(OCB_p ocb, Clause_p clause)
2984 {
2985 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
2986 {
2987 SelectComplex(ocb, clause);
2988 }
2989 }
2990
2991
2992 /*-----------------------------------------------------------------------
2993 //
2994 // Function: PSelectComplexExceptRRHorn()
2995 //
2996 // If a clause is Horn and range-restricted, do no select. Otherwise
2997 // use PSelectComplex() (above).
2998 //
2999 // Global Variables: -
3000 //
3001 // Side Effects : Changes property in literals
3002 //
3003 /----------------------------------------------------------------------*/
3004
PSelectComplexExceptRRHorn(OCB_p ocb,Clause_p clause)3005 void PSelectComplexExceptRRHorn(OCB_p ocb, Clause_p clause)
3006 {
3007 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
3008 {
3009 PSelectComplex(ocb, clause);
3010 }
3011 }
3012
3013
3014 /*-----------------------------------------------------------------------
3015 //
3016 // Function: SelectLComplex()
3017 //
3018 // Similar to SelectComplex, but always select largest diff
3019 // literals first.
3020 //
3021 // Global Variables: -
3022 //
3023 // Side Effects : Changes property in literals
3024 //
3025 /----------------------------------------------------------------------*/
3026
SelectLComplex(OCB_p ocb,Clause_p clause)3027 void SelectLComplex(OCB_p ocb, Clause_p clause)
3028 {
3029 Eqn_p handle, selected;
3030 long select_weight, weight;
3031
3032 selected = ClauseFindNegPureVarLit(clause);
3033
3034 if(!selected)
3035 {
3036 select_weight = -1;
3037 handle = clause->literals;
3038
3039 while(handle)
3040 {
3041 if(EqnIsNegative(handle) && EqnIsGround(handle))
3042 {
3043 weight = lit_sel_diff_weight(handle);
3044 if(weight > select_weight)
3045 {
3046 select_weight = weight;
3047 selected = handle;
3048 }
3049 }
3050 handle = handle->next;
3051 }
3052 }
3053 if(selected)
3054 {
3055 EqnSetProp(selected, EPIsSelected);
3056 }
3057 else
3058 {
3059 SelectDiffNegativeLiteral(ocb, clause);
3060 }
3061 }
3062
3063 /*-----------------------------------------------------------------------
3064 //
3065 // Function: PSelectLComplex()
3066 //
3067 // Similar to PSelectComplex, but always select largest diff
3068 // literals first.
3069 //
3070 // Global Variables: -
3071 //
3072 // Side Effects : Changes property in literals
3073 //
3074 /----------------------------------------------------------------------*/
3075
PSelectLComplex(OCB_p ocb,Clause_p clause)3076 void PSelectLComplex(OCB_p ocb, Clause_p clause)
3077 {
3078 Eqn_p handle, selected;
3079 long select_weight, weight;
3080
3081 selected = ClauseFindNegPureVarLit(clause);
3082
3083 if(!selected)
3084 {
3085 select_weight = -1;
3086 handle = clause->literals;
3087
3088 while(handle)
3089 {
3090 if(EqnIsNegative(handle) && EqnIsGround(handle))
3091 {
3092 weight = lit_sel_diff_weight(handle);
3093 if(weight > select_weight)
3094 {
3095 select_weight = weight;
3096 selected = handle;
3097 }
3098 }
3099 handle = handle->next;
3100 }
3101 }
3102 if(selected)
3103 {
3104 EqnSetProp(selected, EPIsSelected);
3105 }
3106 else
3107 {
3108 PSelectDiffNegativeLiteral(ocb, clause);
3109 }
3110 }
3111
3112
3113 /*-----------------------------------------------------------------------
3114 //
3115 // Function: SelectMaxLComplex()
3116 //
3117 // If there is more than one maximal literal, select a negative
3118 // literal, with the following priority:
3119 //
3120 // Maximal, pure variable
3121 // Maximal, largest difference ground
3122 // Maximal, largest difference non-ground
3123 // pure variable
3124 // largest difference ground
3125 // largest difference non-ground
3126 //
3127 // Global Variables: -
3128 //
3129 // Side Effects : Changes property in literals
3130 //
3131 /----------------------------------------------------------------------*/
3132
SelectMaxLComplex(OCB_p ocb,Clause_p clause)3133 void SelectMaxLComplex(OCB_p ocb, Clause_p clause)
3134 {
3135 long lit_no;
3136 Eqn_p selected;
3137
3138 ClauseCondMarkMaximalTerms(ocb, clause);
3139
3140 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3141 if(lit_no>1)
3142 {
3143 ClauseDelProp(clause, CPIsOriented);
3144 if(EqnListQueryPropNumber(clause->literals,
3145 EPIsMaximal|EPIsPositive)!=lit_no)
3146 { /* There is at least one maximal negative literal */
3147
3148 selected = find_maxlcomplex_literal(clause);
3149 assert(selected);
3150 EqnSetProp(selected, EPIsSelected);
3151 }
3152 else
3153 { /* Normal selection */
3154 SelectLComplex(ocb, clause);
3155 }
3156 }
3157 }
3158
3159
3160 /*-----------------------------------------------------------------------
3161 //
3162 // Function: PSelectMaxLComplex()
3163 //
3164 // As above, but in the default case select positive literals as
3165 // well.
3166 //
3167 // Global Variables: -
3168 //
3169 // Side Effects : Changes property in literals
3170 //
3171 /----------------------------------------------------------------------*/
3172
PSelectMaxLComplex(OCB_p ocb,Clause_p clause)3173 void PSelectMaxLComplex(OCB_p ocb, Clause_p clause)
3174 {
3175 long lit_no;
3176 Eqn_p selected;
3177
3178 ClauseCondMarkMaximalTerms(ocb, clause);
3179
3180 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3181 if(lit_no>1)
3182 {
3183 ClauseDelProp(clause, CPIsOriented);
3184 if(EqnListQueryPropNumber(clause->literals,
3185 EPIsMaximal|EPIsPositive)!=lit_no)
3186 { /* There is at least one maximal negative literal */
3187
3188 selected = find_maxlcomplex_literal(clause);
3189 assert(selected);
3190 EqnSetProp(selected, EPIsSelected);
3191 }
3192 else
3193 { /* Normal selection */
3194 PSelectLComplex(ocb, clause);
3195 }
3196 }
3197 }
3198
3199
3200 /*-----------------------------------------------------------------------
3201 //
3202 // Function: SelectMaxLComplexNoTypePred()
3203 //
3204 // If there is more than one maximal literal, select a negative
3205 // literal, with the following priority:
3206 //
3207 // Maximal, pure variable
3208 // Maximal, largest difference ground
3209 // Maximal, largest difference non-ground
3210 // pure variable
3211 // largest difference ground
3212 // largest difference non-ground
3213 //
3214 // Never select a type literal. If all negative literals are type
3215 // literals, select nothing.
3216 //
3217 // Global Variables: -
3218 //
3219 // Side Effects : Changes property in literals
3220 //
3221 /----------------------------------------------------------------------*/
3222
SelectMaxLComplexNoTypePred(OCB_p ocb,Clause_p clause)3223 void SelectMaxLComplexNoTypePred(OCB_p ocb, Clause_p clause)
3224 {
3225 long lit_no;
3226 Eqn_p selected = NULL;
3227
3228 ClauseCondMarkMaximalTerms(ocb, clause);
3229
3230 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3231 if(lit_no>1)
3232 {
3233 ClauseDelProp(clause, CPIsOriented);
3234 if(EqnListQueryPropNumber(clause->literals,
3235 EPIsMaximal|EPIsPositive)!=lit_no)
3236 { /* There is at least one maximal negative literal */
3237
3238 selected = find_maxlcomplex_literal(clause);
3239 assert(selected);
3240 if(!EqnIsTypePred(selected))
3241 {
3242 EqnSetProp(selected, EPIsSelected);
3243 }
3244 else
3245 {
3246 selected = NULL;
3247 }
3248 }
3249 if(!selected)
3250 { /* Normal selection */
3251 selected = find_lcomplex_literal(clause);
3252 if(selected&&!EqnIsTypePred(selected))
3253 {
3254 EqnSetProp(selected, EPIsSelected);
3255 }
3256 }
3257 }
3258 }
3259
3260 /*-----------------------------------------------------------------------
3261 //
3262 // Function: PSelectMaxLComplexNoTypePred()
3263 //
3264 // If there is more than one maximal literal, select a negative
3265 // literal, with the following priority:
3266 //
3267 // Maximal, pure variable
3268 // Maximal, largest difference ground
3269 // Maximal, largest difference non-ground
3270 // pure variable
3271 // largest difference ground
3272 // largest difference non-ground
3273 //
3274 // Never select a type literal. If all negative literals are type
3275 // literals, select nothing. If selected, also select positive
3276 // literals.
3277 //
3278 // Global Variables: -
3279 //
3280 // Side Effects : Changes property in literals
3281 //
3282 /----------------------------------------------------------------------*/
3283
PSelectMaxLComplexNoTypePred(OCB_p ocb,Clause_p clause)3284 void PSelectMaxLComplexNoTypePred(OCB_p ocb, Clause_p clause)
3285 {
3286 long lit_no;
3287 Eqn_p selected = NULL;
3288
3289 ClauseCondMarkMaximalTerms(ocb, clause);
3290
3291 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3292 if(lit_no>1)
3293 {
3294 ClauseDelProp(clause, CPIsOriented);
3295 if(EqnListQueryPropNumber(clause->literals,
3296 EPIsMaximal|EPIsPositive)!=lit_no)
3297 { /* There is at least one maximal negative literal */
3298
3299 selected = find_maxlcomplex_literal(clause);
3300 assert(selected);
3301 if(!EqnIsTypePred(selected))
3302 {
3303 EqnSetProp(selected, EPIsSelected);
3304 clause_select_pos(clause);
3305 }
3306 else
3307 {
3308 selected = NULL;
3309 }
3310 }
3311 if(!selected)
3312 { /* Normal selection */
3313 selected = find_lcomplex_literal(clause);
3314 if(selected&&!EqnIsTypePred(selected))
3315 {
3316 EqnSetProp(selected, EPIsSelected);
3317 clause_select_pos(clause);
3318 }
3319 }
3320 }
3321 }
3322
3323
3324 /*-----------------------------------------------------------------------
3325 //
3326 // Function: SelectMaxLComplexNoXTypePred()
3327 //
3328 // If there is more than one maximal literal, select a negative
3329 // literal, with the following priority:
3330 //
3331 // Maximal, pure variable
3332 // Maximal, largest difference ground
3333 // Maximal, largest difference non-ground
3334 // pure variable
3335 // largest difference ground
3336 // largest difference non-ground
3337 //
3338 // Never select an extended type literal P(X1,...,Xn). If all
3339 // negative literals are extended type literals, select nothing.
3340 //
3341 // Global Variables: -
3342 //
3343 // Side Effects : Changes property in literals
3344 //
3345 /----------------------------------------------------------------------*/
3346
SelectMaxLComplexNoXTypePred(OCB_p ocb,Clause_p clause)3347 void SelectMaxLComplexNoXTypePred(OCB_p ocb, Clause_p clause)
3348 {
3349 long lit_no;
3350 Eqn_p selected = NULL;
3351
3352 ClauseCondMarkMaximalTerms(ocb, clause);
3353
3354 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3355 if(lit_no>1)
3356 {
3357 ClauseDelProp(clause, CPIsOriented);
3358 if(EqnListQueryPropNumber(clause->literals,
3359 EPIsMaximal|EPIsPositive)!=lit_no)
3360 { /* There is at least one maximal negative literal */
3361
3362 selected = find_maxlcomplex_literal(clause);
3363 assert(selected);
3364 if(!EqnIsXTypePred(selected))
3365 {
3366 EqnSetProp(selected, EPIsSelected);
3367 }
3368 else
3369 {
3370 selected = NULL;
3371 }
3372 }
3373 if(!selected)
3374 { /* Normal selection */
3375 selected = find_lcomplex_literal(clause);
3376 if(selected && !EqnIsXTypePred(selected))
3377 {
3378 EqnSetProp(selected, EPIsSelected);
3379 }
3380 }
3381 }
3382 }
3383
3384 /*-----------------------------------------------------------------------
3385 //
3386 // Function: PSelectMaxLComplexNoXTypePred()
3387 //
3388 // If there is more than one maximal literal, select a negative
3389 // literal, with the following priority:
3390 //
3391 // Maximal, pure variable
3392 // Maximal, largest difference ground
3393 // Maximal, largest difference non-ground
3394 // pure variable
3395 // largest difference ground
3396 // largest difference non-ground
3397 //
3398 // Never select an extended type literal. If all negative literals
3399 // are extended type literals, select nothing. If selected, also
3400 // select positive literals.
3401 //
3402 // Global Variables: -
3403 //
3404 // Side Effects : Changes property in literals
3405 //
3406 /----------------------------------------------------------------------*/
3407
PSelectMaxLComplexNoXTypePred(OCB_p ocb,Clause_p clause)3408 void PSelectMaxLComplexNoXTypePred(OCB_p ocb, Clause_p clause)
3409 {
3410 long lit_no;
3411 Eqn_p selected = NULL;
3412
3413 ClauseCondMarkMaximalTerms(ocb, clause);
3414
3415 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
3416 if(lit_no>1)
3417 {
3418 ClauseDelProp(clause, CPIsOriented);
3419 if(EqnListQueryPropNumber(clause->literals,
3420 EPIsMaximal|EPIsPositive)!=lit_no)
3421 { /* There is at least one maximal negative literal */
3422
3423 selected = find_maxlcomplex_literal(clause);
3424 assert(selected);
3425 if(!EqnIsXTypePred(selected))
3426 {
3427 EqnSetProp(selected, EPIsSelected);
3428 clause_select_pos(clause);
3429 }
3430 else
3431 {
3432 selected = NULL;
3433 }
3434 }
3435 if(!selected)
3436 { /* Normal selection */
3437 selected = find_lcomplex_literal(clause);
3438 if(selected&&!EqnIsXTypePred(selected))
3439 {
3440 EqnSetProp(selected, EPIsSelected);
3441 clause_select_pos(clause);
3442 }
3443 }
3444 }
3445 }
3446
3447
3448 /*-----------------------------------------------------------------------
3449 //
3450 // Function: SelectComplexPreferNEQ()
3451 //
3452 // Select a negative literal as in SelectComplex, but prefer
3453 // non-equational literals.
3454 //
3455 // Global Variables: -
3456 //
3457 // Side Effects : Changes property in literals
3458 //
3459 /----------------------------------------------------------------------*/
3460
SelectComplexPreferNEQ(OCB_p ocb,Clause_p clause)3461 void SelectComplexPreferNEQ(OCB_p ocb, Clause_p clause)
3462 {
3463 bool sel_neq = false, cur_neq;
3464 bool sel_var = false, cur_var;
3465 bool sel_ground = false, cur_ground;
3466 long sel_weight = -1, cur_weight;
3467 Eqn_p handle, selected = NULL;
3468
3469 for(handle=clause->literals; handle; handle=handle->next)
3470 {
3471 if(EqnIsNegative(handle))
3472 {
3473 cur_neq = !EqnIsEquLit(handle);
3474 cur_var = EqnIsPureVar(handle);
3475 cur_ground = EqnIsGround(handle);
3476 cur_weight = -1;
3477
3478 if(sel_neq && !cur_neq)
3479 {
3480 break;
3481 }
3482 else if(EQUIV(cur_neq, sel_neq))
3483 {
3484 if(sel_var && !cur_var)
3485 {
3486 break;
3487 }
3488 else if(EQUIV(cur_var, sel_var))
3489 {
3490 if(sel_ground && !cur_ground)
3491 {
3492 break;
3493 }
3494 else if(EQUIV(cur_ground, sel_ground))
3495 {
3496 cur_weight = lit_sel_diff_weight(handle);
3497 if(cur_weight <=sel_weight)
3498 {
3499 break;
3500 }
3501 }
3502 }
3503 }
3504 if(cur_weight == -1)
3505 {
3506 cur_weight = lit_sel_diff_weight(handle);
3507 }
3508 selected = handle;
3509 sel_weight = cur_weight;
3510 sel_ground = cur_ground;
3511 sel_var = cur_var;
3512 sel_neq = cur_neq;
3513 }
3514 }
3515 if(selected)
3516 {
3517 EqnSetProp(selected, EPIsSelected);
3518 }
3519 }
3520
3521
3522 /*-----------------------------------------------------------------------
3523 //
3524 // Function: PSelectComplexPreferNEQ()
3525 //
3526 // Select a negative literal as in PSelectComplex, but prefer
3527 // non-equational literals.
3528 //
3529 // Global Variables: -
3530 //
3531 // Side Effects : Changes property in literals
3532 //
3533 /----------------------------------------------------------------------*/
3534
PSelectComplexPreferNEQ(OCB_p ocb,Clause_p clause)3535 void PSelectComplexPreferNEQ(OCB_p ocb, Clause_p clause)
3536 {
3537 bool sel_neq = false, cur_neq;
3538 bool sel_var = false, cur_var;
3539 bool sel_ground = false, cur_ground;
3540 long sel_weight = -1, cur_weight;
3541 Eqn_p handle, selected = NULL;
3542
3543 for(handle=clause->literals; handle; handle=handle->next)
3544 {
3545 if(EqnIsNegative(handle))
3546 {
3547 cur_neq = !EqnIsEquLit(handle);
3548 cur_var = EqnIsPureVar(handle);
3549 cur_ground = EqnIsGround(handle);
3550 cur_weight = -1;
3551
3552 if(sel_neq && !cur_neq)
3553 {
3554 break;
3555 }
3556 else if(EQUIV(cur_neq, sel_neq))
3557 {
3558 if(sel_var && !cur_var)
3559 {
3560 break;
3561 }
3562 else if(EQUIV(cur_var, sel_var))
3563 {
3564 if(sel_ground && !cur_ground)
3565 {
3566 break;
3567 }
3568 else if(EQUIV(cur_ground, sel_ground))
3569 {
3570 cur_weight = lit_sel_diff_weight(handle);
3571 if(cur_weight <=sel_weight)
3572 {
3573 break;
3574 }
3575 }
3576 }
3577 }
3578 if(cur_weight == -1)
3579 {
3580 cur_weight = lit_sel_diff_weight(handle);
3581 }
3582 selected = handle;
3583 sel_weight = cur_weight;
3584 sel_ground = cur_ground;
3585 sel_var = cur_var;
3586 sel_neq = cur_neq;
3587 }
3588 }
3589 if(selected)
3590 {
3591 clause_select_pos(clause);
3592 EqnSetProp(selected, EPIsSelected);
3593 }
3594 }
3595
3596
3597 /*-----------------------------------------------------------------------
3598 //
3599 // Function: SelectComplexPreferEQ()
3600 //
3601 // Select a negative literal as in SelectComplex, but prefer
3602 // equational literals.
3603 //
3604 // Global Variables: -
3605 //
3606 // Side Effects : Changes property in literals
3607 //
3608 /----------------------------------------------------------------------*/
3609
SelectComplexPreferEQ(OCB_p ocb,Clause_p clause)3610 void SelectComplexPreferEQ(OCB_p ocb, Clause_p clause)
3611 {
3612 bool sel_eq = false, cur_eq;
3613 bool sel_var = false, cur_var;
3614 bool sel_ground = false, cur_ground;
3615 long sel_weight = -1, cur_weight;
3616 Eqn_p handle, selected = NULL;
3617
3618 for(handle=clause->literals; handle; handle=handle->next)
3619 {
3620 if(EqnIsNegative(handle))
3621 {
3622 cur_eq = EqnIsEquLit(handle);
3623 cur_var = EqnIsPureVar(handle);
3624 cur_ground = EqnIsGround(handle);
3625 cur_weight = -1;
3626
3627 if(sel_eq && !cur_eq)
3628 {
3629 break;
3630 }
3631 else if(EQUIV(cur_eq, sel_eq))
3632 {
3633 if(sel_var && !cur_var)
3634 {
3635 break;
3636 }
3637 else if(EQUIV(cur_var, sel_var))
3638 {
3639 if(sel_ground && !cur_ground)
3640 {
3641 break;
3642 }
3643 else if(EQUIV(cur_ground, sel_ground))
3644 {
3645 cur_weight = lit_sel_diff_weight(handle);
3646 if(cur_weight <=sel_weight)
3647 {
3648 break;
3649 }
3650 }
3651 }
3652 }
3653 if(cur_weight == -1)
3654 {
3655 cur_weight = lit_sel_diff_weight(handle);
3656 }
3657 selected = handle;
3658 sel_weight = cur_weight;
3659 sel_ground = cur_ground;
3660 sel_var = cur_var;
3661 sel_eq = cur_eq;
3662 }
3663 }
3664 if(selected)
3665 {
3666 EqnSetProp(selected, EPIsSelected);
3667 }
3668 }
3669
3670
3671 /*-----------------------------------------------------------------------
3672 //
3673 // Function: PSelectComplexPreferEQ()
3674 //
3675 // Select a negative literal as in PSelectComplex, but prefer
3676 // equational literals.
3677 //
3678 // Global Variables: -
3679 //
3680 // Side Effects : Changes property in literals
3681 //
3682 /----------------------------------------------------------------------*/
3683
PSelectComplexPreferEQ(OCB_p ocb,Clause_p clause)3684 void PSelectComplexPreferEQ(OCB_p ocb, Clause_p clause)
3685 {
3686 bool sel_eq = false, cur_eq;
3687 bool sel_var = false, cur_var;
3688 bool sel_ground = false, cur_ground;
3689 long sel_weight = -1, cur_weight;
3690 Eqn_p handle, selected = NULL;
3691
3692 for(handle=clause->literals; handle; handle=handle->next)
3693 {
3694 if(EqnIsNegative(handle))
3695 {
3696 cur_eq = EqnIsEquLit(handle);
3697 cur_var = EqnIsPureVar(handle);
3698 cur_ground = EqnIsGround(handle);
3699 cur_weight = -1;
3700
3701 if(sel_eq && !cur_eq)
3702 {
3703 break;
3704 }
3705 else if(EQUIV(cur_eq, sel_eq))
3706 {
3707 if(sel_var && !cur_var)
3708 {
3709 break;
3710 }
3711 else if(EQUIV(cur_var, sel_var))
3712 {
3713 if(sel_ground && !cur_ground)
3714 {
3715 break;
3716 }
3717 else if(EQUIV(cur_ground, sel_ground))
3718 {
3719 cur_weight = lit_sel_diff_weight(handle);
3720 if(cur_weight <=sel_weight)
3721 {
3722 break;
3723 }
3724 }
3725 }
3726 }
3727 if(cur_weight == -1)
3728 {
3729 cur_weight = lit_sel_diff_weight(handle);
3730 }
3731 selected = handle;
3732 sel_weight = cur_weight;
3733 sel_ground = cur_ground;
3734 sel_var = cur_var;
3735 sel_eq = cur_eq;
3736 }
3737 }
3738 if(selected)
3739 {
3740 clause_select_pos(clause);
3741 EqnSetProp(selected, EPIsSelected);
3742 }
3743 }
3744
3745
3746 /*-----------------------------------------------------------------------
3747 //
3748 // Function: SelectComplexExceptUniqMaxHorn()
3749 //
3750 // Select literal as in SelectComplex unless the clause is a Horn
3751 // clause with a unique maximal literal.
3752 //
3753 // Global Variables: -
3754 //
3755 // Side Effects : Changes property in literals
3756 //
3757 /----------------------------------------------------------------------*/
3758
SelectComplexExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)3759 void SelectComplexExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
3760 {
3761 if(ClauseIsHorn(clause))
3762 {
3763 ClauseCondMarkMaximalTerms(ocb, clause);
3764 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
3765 {
3766 return;
3767 }
3768 }
3769 SelectComplex(ocb,clause);
3770 ClauseDelProp(clause, CPIsOriented);
3771 }
3772
3773
3774 /*-----------------------------------------------------------------------
3775 //
3776 // Function: PSelectComplexExceptUniqMaxHorn()
3777 //
3778 // Select literal as in PSelectComplex unless the clause is a Horn
3779 // clause with a unique maximal literal.
3780 //
3781 // Global Variables: -
3782 //
3783 // Side Effects : Changes property in literals
3784 //
3785 /----------------------------------------------------------------------*/
3786
PSelectComplexExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)3787 void PSelectComplexExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
3788 {
3789 if(ClauseIsHorn(clause))
3790 {
3791 ClauseCondMarkMaximalTerms(ocb, clause);
3792 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
3793 {
3794 return;
3795 }
3796 }
3797 PSelectComplex(ocb,clause);
3798 ClauseDelProp(clause, CPIsOriented);
3799 }
3800
3801
3802 /*-----------------------------------------------------------------------
3803 //
3804 // Function: MSelectComplexExceptUniqMaxHorn()
3805 //
3806 // For horn clauses, call PSelectComplexExceptUniqMaxHorn,
3807 // otherwise call SelectComplexExceptUniqMaxHorn.
3808 //
3809 // Global Variables: -
3810 //
3811 // Side Effects : Changes property in literals
3812 //
3813 /----------------------------------------------------------------------*/
3814
MSelectComplexExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)3815 void MSelectComplexExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
3816 {
3817 if(ClauseIsHorn(clause))
3818 {
3819 PSelectComplexExceptUniqMaxHorn(ocb,clause);
3820 }
3821 else
3822 {
3823 SelectComplexExceptUniqMaxHorn(ocb,clause);
3824 }
3825 }
3826
3827
3828 /*-----------------------------------------------------------------------
3829 //
3830 // Function: SelectNewComplex()
3831 //
3832 // If there is a negative ground literal, select the one with the
3833 // smallest maximal side.
3834 // Else: Select the minimal inference position non-XType orientable
3835 // negative literal.
3836 // Else: Select the lagest XType literal.
3837 // Never select a Type literal - if all negative literals are type
3838 // literals, do not select at all.
3839 //
3840 // Global Variables: -
3841 //
3842 // Side Effects : -
3843 //
3844 /----------------------------------------------------------------------*/
3845
SelectNewComplex(OCB_p ocb,Clause_p clause)3846 void SelectNewComplex(OCB_p ocb, Clause_p clause)
3847 {
3848 Eqn_p selected;
3849
3850 ClauseCondMarkMaximalTerms(ocb, clause);
3851
3852 selected = find_smallest_max_neg_ground_lit(clause);
3853 if(!selected)
3854 {
3855 selected = find_ng_min11_infpos_no_xtype_lit(clause);
3856 }
3857 if(!selected)
3858 {
3859 selected = find_max_xtype_no_type_lit(clause);
3860 }
3861 if(selected)
3862 {
3863 EqnSetProp(selected, EPIsSelected);
3864 ClauseDelProp(clause, CPIsOriented);
3865 }
3866 }
3867
3868
3869 /*-----------------------------------------------------------------------
3870 //
3871 // Function: PSelectNewComplex()
3872 //
3873 // If there is a negative ground literal, select the one with the
3874 // smallest maximal side.
3875 // Else: Select the minimal inference position non-XType orientable
3876 // negative literal.
3877 // Else: Select the lagest XType literal.
3878 // Never select a Type literal - if all negative literals are type
3879 // literals, do not select at all.
3880 // If anything is selected, select positive literals as well.
3881 //
3882 // Global Variables: -
3883 //
3884 // Side Effects : -
3885 //
3886 /----------------------------------------------------------------------*/
3887
PSelectNewComplex(OCB_p ocb,Clause_p clause)3888 void PSelectNewComplex(OCB_p ocb, Clause_p clause)
3889 {
3890 Eqn_p selected;
3891
3892 ClauseCondMarkMaximalTerms(ocb, clause);
3893
3894 selected = find_smallest_max_neg_ground_lit(clause);
3895 if(!selected)
3896 {
3897 selected = find_ng_min11_infpos_no_xtype_lit(clause);
3898 }
3899 if(!selected)
3900 {
3901 selected = find_max_xtype_no_type_lit(clause);
3902 }
3903 if(selected)
3904 {
3905 EqnSetProp(selected, EPIsSelected);
3906 ClauseDelProp(clause, CPIsOriented);
3907 clause_select_pos(clause);
3908 }
3909 }
3910
3911
3912 /*-----------------------------------------------------------------------
3913 //
3914 // Function: SelectNewComplexExceptUniqMaxHorn()
3915 //
3916 // Select literal as in SelectNewsComplex unless the clause is a
3917 // Horn clause with a unique maximal literal.
3918 //
3919 // Global Variables: -
3920 //
3921 // Side Effects : Changes property in literals
3922 //
3923 /----------------------------------------------------------------------*/
3924
SelectNewComplexExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)3925 void SelectNewComplexExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
3926 {
3927 if(ClauseIsHorn(clause))
3928 {
3929 ClauseCondMarkMaximalTerms(ocb, clause);
3930 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
3931 {
3932 return;
3933 }
3934 }
3935 SelectNewComplex(ocb,clause);
3936 }
3937
3938
3939 /*-----------------------------------------------------------------------
3940 //
3941 // Function: PSelectNewComplexExceptUniqMaxHorn()
3942 //
3943 // Select literal as in PSelectNewsComplex unless the clause is a
3944 // Horn clause with a unique maximal literal.
3945 //
3946 // Global Variables: -
3947 //
3948 // Side Effects : Changes property in literals
3949 //
3950 /----------------------------------------------------------------------*/
3951
PSelectNewComplexExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)3952 void PSelectNewComplexExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
3953 {
3954 if(ClauseIsHorn(clause))
3955 {
3956 ClauseCondMarkMaximalTerms(ocb, clause);
3957 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
3958 {
3959 return;
3960 }
3961 }
3962 PSelectNewComplex(ocb,clause);
3963 }
3964
3965
3966 /*-----------------------------------------------------------------------
3967 //
3968 // Function: SelectMinInfpos()
3969 //
3970 // Select the literal with the smallest number of potential
3971 // inference positions, i.e. smallest sum of maximal size weights.
3972 //
3973 // Global Variables: -
3974 //
3975 // Side Effects : -
3976 //
3977 /----------------------------------------------------------------------*/
3978
SelectMinInfpos(OCB_p ocb,Clause_p clause)3979 void SelectMinInfpos(OCB_p ocb, Clause_p clause)
3980 {
3981 Eqn_p handle = clause->literals, selected = NULL;
3982 long select_weight = LONG_MAX, currw;
3983
3984 ClauseCondMarkMaximalTerms(ocb, clause);
3985 while(handle)
3986 {
3987 if(EqnIsNegative(handle))
3988 {
3989 currw = TermStandardWeight(handle->lterm);
3990 if(!EqnIsOriented(handle))
3991 {
3992 currw += TermStandardWeight(handle->rterm);
3993 }
3994 if(currw < select_weight)
3995 {
3996 select_weight = currw;
3997 selected = handle;
3998 }
3999 }
4000 handle = handle->next;
4001 }
4002 assert(selected);
4003 EqnSetProp(selected, EPIsSelected);
4004 ClauseDelProp(clause, CPIsOriented);
4005 }
4006
4007
4008 /*-----------------------------------------------------------------------
4009 //
4010 // Function: PSelectMinInfpos()
4011 //
4012 // Select the literal with the smallest number of potential
4013 // inference positions, i.e. smallest sum of maximal size weights,
4014 // and select positive literals as well.
4015 //
4016 // Global Variables: -
4017 //
4018 // Side Effects : -
4019 //
4020 /----------------------------------------------------------------------*/
4021
PSelectMinInfpos(OCB_p ocb,Clause_p clause)4022 void PSelectMinInfpos(OCB_p ocb, Clause_p clause)
4023 {
4024 Eqn_p handle = clause->literals, selected = NULL;
4025 long select_weight = LONG_MAX, currw;
4026
4027 ClauseCondMarkMaximalTerms(ocb, clause);
4028 while(handle)
4029 {
4030 if(EqnIsPositive(handle))
4031 {
4032 EqnSetProp(handle, EPIsSelected);
4033 }
4034 else
4035 {
4036 currw = TermStandardWeight(handle->lterm);
4037 if(!EqnIsOriented(handle))
4038 {
4039 currw += TermStandardWeight(handle->rterm);
4040 }
4041 if(currw < select_weight)
4042 {
4043 select_weight = currw;
4044 selected = handle;
4045 }
4046 }
4047 handle = handle->next;
4048 }
4049 assert(selected);
4050 EqnSetProp(selected, EPIsSelected);
4051 ClauseDelProp(clause, CPIsOriented);
4052 }
4053
4054
4055 /*-----------------------------------------------------------------------
4056 //
4057 // Function: HSelectMinInfpos()
4058 //
4059 // Select the literal with the smallest number of potential
4060 // inference positions, i.e. smallest sum of maximal size weights.
4061 // If this is not ground, select positive ones as well.
4062 //
4063 // Global Variables: -
4064 //
4065 // Side Effects : -
4066 //
4067 /----------------------------------------------------------------------*/
4068
HSelectMinInfpos(OCB_p ocb,Clause_p clause)4069 void HSelectMinInfpos(OCB_p ocb, Clause_p clause)
4070 {
4071 Eqn_p handle = clause->literals, selected = NULL;
4072 long select_weight = LONG_MAX, currw;
4073
4074 ClauseCondMarkMaximalTerms(ocb, clause);
4075 while(handle)
4076 {
4077 if(EqnIsNegative(handle))
4078 {
4079 currw = TermStandardWeight(handle->lterm);
4080 if(!EqnIsOriented(handle))
4081 {
4082 currw += TermStandardWeight(handle->rterm);
4083 }
4084 if(currw < select_weight)
4085 {
4086 select_weight = currw;
4087 selected = handle;
4088 }
4089 }
4090 handle = handle->next;
4091 }
4092 assert(selected);
4093 EqnSetProp(selected, EPIsSelected);
4094 ClauseDelProp(clause, CPIsOriented);
4095 if(!EqnIsGround(selected))
4096 {
4097 for(handle = clause->literals; handle; handle = handle->next)
4098 {
4099 if(EqnIsPositive(handle))
4100 {
4101 EqnSetProp(handle, EPIsSelected);
4102 }
4103 }
4104 }
4105 }
4106
4107
4108 /*-----------------------------------------------------------------------
4109 //
4110 // Function: GSelectMinInfpos()
4111 //
4112 // Select the literal with the smallest number of potential
4113 // inference positions, i.e. smallest sum of maximal size weights.
4114 // If this is ground, select positive ones as well.
4115 //
4116 // Global Variables: -
4117 //
4118 // Side Effects : -
4119 //
4120 /----------------------------------------------------------------------*/
4121
GSelectMinInfpos(OCB_p ocb,Clause_p clause)4122 void GSelectMinInfpos(OCB_p ocb, Clause_p clause)
4123 {
4124 Eqn_p handle = clause->literals, selected = NULL;
4125 long select_weight = LONG_MAX, currw;
4126
4127 ClauseCondMarkMaximalTerms(ocb, clause);
4128 while(handle)
4129 {
4130 if(EqnIsNegative(handle))
4131 {
4132 currw = TermStandardWeight(handle->lterm);
4133 if(!EqnIsOriented(handle))
4134 {
4135 currw += TermStandardWeight(handle->rterm);
4136 }
4137 if(currw < select_weight)
4138 {
4139 select_weight = currw;
4140 selected = handle;
4141 }
4142 }
4143 handle = handle->next;
4144 }
4145 assert(selected);
4146 EqnSetProp(selected, EPIsSelected);
4147 ClauseDelProp(clause, CPIsOriented);
4148 if(EqnIsGround(selected))
4149 {
4150 for(handle = clause->literals; handle; handle = handle->next)
4151 {
4152 if(EqnIsPositive(handle))
4153 {
4154 EqnSetProp(handle, EPIsSelected);
4155 }
4156 }
4157 }
4158 }
4159
4160
4161 /*-----------------------------------------------------------------------
4162 //
4163 // Function: SelectMinInfposNoTypePred()
4164 //
4165 // Select the literal with the smallest number of potential
4166 // inference positions, i.e. smallest sum of maximal size weights,
4167 // but never select type predicates.
4168 //
4169 // Global Variables: -
4170 //
4171 // Side Effects : -
4172 //
4173 /----------------------------------------------------------------------*/
4174
SelectMinInfposNoTypePred(OCB_p ocb,Clause_p clause)4175 void SelectMinInfposNoTypePred(OCB_p ocb, Clause_p clause)
4176 {
4177 Eqn_p handle = clause->literals, selected = NULL;
4178 long select_weight = LONG_MAX, currw;
4179
4180 ClauseCondMarkMaximalTerms(ocb, clause);
4181 while(handle)
4182 {
4183 if(EqnIsNegative(handle)&&!EqnIsTypePred(handle))
4184 {
4185 currw = TermStandardWeight(handle->lterm);
4186 if(!EqnIsOriented(handle))
4187 {
4188 currw += TermStandardWeight(handle->rterm);
4189 }
4190 if(currw < select_weight)
4191 {
4192 select_weight = currw;
4193 selected = handle;
4194 }
4195 }
4196 handle = handle->next;
4197 }
4198 if(selected)
4199 {
4200 EqnSetProp(selected, EPIsSelected);
4201 ClauseDelProp(clause, CPIsOriented);
4202 }
4203 }
4204
4205 /*-----------------------------------------------------------------------
4206 //
4207 // Function: PSelectMinInfposNoTypePred()
4208 //
4209 // Select the literal with the smallest number of potential
4210 // inference positions, i.e. smallest sum of maximal size weights,
4211 // but never select type predicates. If literal is selected, also
4212 // select positive ones.
4213 //
4214 // Global Variables: -
4215 //
4216 // Side Effects : -
4217 //
4218 /----------------------------------------------------------------------*/
4219
PSelectMinInfposNoTypePred(OCB_p ocb,Clause_p clause)4220 void PSelectMinInfposNoTypePred(OCB_p ocb, Clause_p clause)
4221 {
4222 Eqn_p handle = clause->literals, selected = NULL;
4223 long select_weight = LONG_MAX, currw;
4224
4225 ClauseCondMarkMaximalTerms(ocb, clause);
4226 while(handle)
4227 {
4228 if(EqnIsNegative(handle)&&!EqnIsTypePred(handle))
4229 {
4230 currw = TermStandardWeight(handle->lterm);
4231 if(!EqnIsOriented(handle))
4232 {
4233 currw += TermStandardWeight(handle->rterm);
4234 }
4235 if(currw < select_weight)
4236 {
4237 select_weight = currw;
4238 selected = handle;
4239 }
4240 }
4241 handle = handle->next;
4242 }
4243 if(selected)
4244 {
4245 EqnSetProp(selected, EPIsSelected);
4246 clause_select_pos(clause);
4247 ClauseDelProp(clause, CPIsOriented);
4248 }
4249 }
4250
4251
4252 /*-----------------------------------------------------------------------
4253 //
4254 // Function: SelectMin2Infpos()
4255 //
4256 // Select the literal with the smallest number of potential
4257 // inference positions, i.e. smallest sum of maximal size weights
4258 // for f_weight = 1, v_weight = 2
4259 //
4260 // Global Variables: -
4261 //
4262 // Side Effects : -
4263 //
4264 /----------------------------------------------------------------------*/
4265
SelectMin2Infpos(OCB_p ocb,Clause_p clause)4266 void SelectMin2Infpos(OCB_p ocb, Clause_p clause)
4267 {
4268 Eqn_p handle = clause->literals, selected = NULL;
4269 long select_weight = LONG_MAX, currw;
4270
4271 ClauseCondMarkMaximalTerms(ocb, clause);
4272 while(handle)
4273 {
4274 if(EqnIsNegative(handle))
4275 {
4276 currw = TermWeight(handle->lterm,2,1);
4277 if(!EqnIsOriented(handle))
4278 {
4279 currw += TermWeight(handle->rterm,2,1);
4280 }
4281 if(currw < select_weight)
4282 {
4283 select_weight = currw;
4284 selected = handle;
4285 }
4286 }
4287 handle = handle->next;
4288 }
4289 assert(selected);
4290 EqnSetProp(selected, EPIsSelected);
4291 ClauseDelProp(clause, CPIsOriented);
4292 }
4293
4294
4295 /*-----------------------------------------------------------------------
4296 //
4297 // Function: PSelectMin2Infpos()
4298 //
4299 // Select the literal with the smallest number of potential
4300 // inference positions, i.e. smallest sum of maximal size weights
4301 // (as above), and select positive literals as well.
4302 //
4303 // Global Variables: -
4304 //
4305 // Side Effects : -
4306 //
4307 /----------------------------------------------------------------------*/
4308
PSelectMin2Infpos(OCB_p ocb,Clause_p clause)4309 void PSelectMin2Infpos(OCB_p ocb, Clause_p clause)
4310 {
4311 Eqn_p handle = clause->literals, selected = NULL;
4312 long select_weight = LONG_MAX, currw;
4313
4314 ClauseCondMarkMaximalTerms(ocb, clause);
4315 while(handle)
4316 {
4317 if(EqnIsPositive(handle))
4318 {
4319 EqnSetProp(handle, EPIsSelected);
4320 }
4321 else
4322 {
4323 currw = TermWeight(handle->lterm,2,1);
4324 if(!EqnIsOriented(handle))
4325 {
4326 currw += TermWeight(handle->rterm,2,1);
4327 }
4328 if(currw < select_weight)
4329 {
4330 select_weight = currw;
4331 selected = handle;
4332 }
4333 }
4334 handle = handle->next;
4335 }
4336 assert(selected);
4337 EqnSetProp(selected, EPIsSelected);
4338 ClauseDelProp(clause, CPIsOriented);
4339 }
4340
4341
4342 /*-----------------------------------------------------------------------
4343 //
4344 // Function: SelectComplexExceptUniqMaxPosHorn()
4345 //
4346 // Select literal as in SelectComplex unless the clause is a Horn
4347 // clause with a unique maximal positive literal.
4348 //
4349 // Global Variables: -
4350 //
4351 // Side Effects : Changes property in literals
4352 //
4353 /----------------------------------------------------------------------*/
4354
SelectComplexExceptUniqMaxPosHorn(OCB_p ocb,Clause_p clause)4355 void SelectComplexExceptUniqMaxPosHorn(OCB_p ocb, Clause_p clause)
4356 {
4357 if(ClauseIsHorn(clause))
4358 {
4359 ClauseCondMarkMaximalTerms(ocb, clause);
4360 if((EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)&&
4361 (EqnListQueryPropNumber(clause->literals, EPIsMaximal|EPIsPositive)==1))
4362 {
4363 return;
4364 }
4365 }
4366 SelectComplex(ocb,clause);
4367 ClauseDelProp(clause, CPIsOriented);
4368 }
4369
4370
4371 /*-----------------------------------------------------------------------
4372 //
4373 // Function: PSelectComplexExceptUniqMaxPosHorn()
4374 //
4375 // Select literal as in PSelectComplex unless the clause is a Horn
4376 // clause with a unique maximal positive literal.
4377 //
4378 // Global Variables: -
4379 //
4380 // Side Effects : Changes property in literals
4381 //
4382 /----------------------------------------------------------------------*/
4383
PSelectComplexExceptUniqMaxPosHorn(OCB_p ocb,Clause_p clause)4384 void PSelectComplexExceptUniqMaxPosHorn(OCB_p ocb, Clause_p clause)
4385 {
4386 if(ClauseIsHorn(clause))
4387 {
4388 ClauseCondMarkMaximalTerms(ocb, clause);
4389 if((EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)&&
4390 (EqnListQueryPropNumber(clause->literals, EPIsMaximal|EPIsPositive)==1))
4391 {
4392 return;
4393 }
4394 }
4395 PSelectComplex(ocb,clause);
4396 ClauseDelProp(clause, CPIsOriented);
4397 }
4398
4399
4400 /*-----------------------------------------------------------------------
4401 //
4402 // Function: diversification_weight()
4403 //
4404 // Assign pseudo-random weight to negative literals, 0 to positive
4405 // ones.
4406 //
4407 // Global Variables:
4408 //
4409 // Side Effects :
4410 //
4411 /----------------------------------------------------------------------*/
4412
diversification_weight(LitEval_p lit,Clause_p clause,void * dummy)4413 static void diversification_weight(LitEval_p lit, Clause_p clause, void* dummy)
4414 {
4415 if(EqnIsNegative(lit->literal))
4416 {
4417 lit->w1 = literal_weight_counter % clause->neg_lit_no;
4418 }
4419 literal_weight_counter++;
4420 }
4421
4422
4423 /*-----------------------------------------------------------------------
4424 //
4425 // Function: SelectDiversificationLiterals()
4426 //
4427 // Systematically select a pseudo-random literal in clause (where
4428 // pseudo is large and random in small).
4429 //
4430 // Global Variables: -
4431 //
4432 // Side Effects : -
4433 //
4434 /----------------------------------------------------------------------*/
4435
SelectDiversificationLiterals(OCB_p ocb,Clause_p clause)4436 void SelectDiversificationLiterals(OCB_p ocb, Clause_p clause)
4437 {
4438 generic_uniq_selection(ocb,clause,false, false, diversification_weight, NULL);
4439 }
4440
4441
4442 /*-----------------------------------------------------------------------
4443 //
4444 // Function: diversification_prefer_into_weight()
4445 //
4446 // Assing pseudo-random weight to negative literals, 0 to positive
4447 // ones. However, always prefer literals comming from the into
4448 // clause of a paramodulation to those of a from clause.
4449 //
4450 // Global Variables: -
4451 //
4452 // Side Effects : -
4453 //
4454 /----------------------------------------------------------------------*/
4455
diversification_prefer_into_weight(LitEval_p lit,Clause_p clause,void * dummy)4456 static void diversification_prefer_into_weight(LitEval_p lit,
4457 Clause_p clause,
4458 void* dummy)
4459 {
4460 lit->w1 = -ClauseQueryProp(lit->literal, EPIsPMIntoLit);
4461 if(EqnIsNegative(lit->literal))
4462 {
4463 lit->w2 = literal_weight_counter % clause->neg_lit_no;
4464 }
4465 literal_weight_counter++;
4466 }
4467
4468
4469 /*-----------------------------------------------------------------------
4470 //
4471 // Function: SelectDiversificationPreferIntoLiterals()
4472 //
4473 // Systematically select a pseudo-random literal in clause (where
4474 // pseudo is large and random in small), but prefer into-literals.
4475 //
4476 // Global Variables: -
4477 //
4478 // Side Effects : -
4479 //
4480 /----------------------------------------------------------------------*/
4481
SelectDiversificationPreferIntoLiterals(OCB_p ocb,Clause_p clause)4482 void SelectDiversificationPreferIntoLiterals(OCB_p ocb, Clause_p clause)
4483 {
4484 generic_uniq_selection(ocb,clause,false, false,
4485 diversification_prefer_into_weight,
4486 NULL);
4487 }
4488
4489 /*-----------------------------------------------------------------------
4490 //
4491 // Function: maxlcomplex_weight()
4492 //
4493 // Initialize weights to mimic SelectMaxLComplexWeight()
4494 //
4495 // Global Variables: -
4496 //
4497 // Side Effects : -
4498 //
4499 /----------------------------------------------------------------------*/
4500
maxlcomplex_weight(LitEval_p lit,Clause_p clause,void * dummy)4501 static void maxlcomplex_weight(LitEval_p lit, Clause_p clause, void *dummy)
4502 {
4503 if(EqnIsNegative(lit->literal))
4504 {
4505 if(EqnIsMaximal(lit->literal))
4506 {
4507 lit->w1=0;
4508 }
4509 else
4510 {
4511 lit->w1=100;
4512 }
4513 if(!EqnIsPureVar(lit->literal))
4514 {
4515 lit->w1+=10;
4516 }
4517 if(!EqnIsGround(lit->literal))
4518 {
4519 lit->w1+=1;
4520 }
4521 lit->w2 = -lit_sel_diff_weight(lit->literal);
4522 lit->w3 = literal_weight_counter % clause->neg_lit_no;
4523 }
4524 literal_weight_counter++;
4525 }
4526
4527 /*-----------------------------------------------------------------------
4528 //
4529 // Function: SelectMaxLComplexG()
4530 //
4531 // Reimplementation of SelectMaxLComplex() using the generic literal
4532 // selection framework.
4533 //
4534 // Global Variables: -
4535 //
4536 // Side Effects : -
4537 //
4538 /----------------------------------------------------------------------*/
4539
SelectMaxLComplexG(OCB_p ocb,Clause_p clause)4540 void SelectMaxLComplexG(OCB_p ocb, Clause_p clause)
4541 {
4542 long lit_no;
4543
4544 assert(ocb);
4545 assert(clause);
4546 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4547
4548 if(clause->neg_lit_no==0)
4549 {
4550 return;
4551 }
4552 ClauseCondMarkMaximalTerms(ocb, clause);
4553
4554 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
4555
4556 if(lit_no <=1)
4557 {
4558 return;
4559 }
4560 generic_uniq_selection(ocb,clause,false, true,
4561 maxlcomplex_weight, NULL);
4562 }
4563
4564 /*-----------------------------------------------------------------------
4565 //
4566 // Function: maxlcomplexavoidpred_weight()
4567 //
4568 // Initialize weights to mimic SelectMaxLComplexWeight(), but defer
4569 // literals with which occur often in pred_dist.
4570 //
4571 // Global Variables: -
4572 //
4573 // Side Effects : -
4574 //
4575 /----------------------------------------------------------------------*/
4576
maxlcomplexavoidpred_weight(LitEval_p lit,Clause_p clause,void * pred_dist)4577 static void maxlcomplexavoidpred_weight(LitEval_p lit, Clause_p clause,
4578 void *pred_dist)
4579 {
4580 PDArray_p pd = pred_dist;
4581
4582 if(EqnIsNegative(lit->literal))
4583 {
4584 if(EqnIsMaximal(lit->literal))
4585 {
4586 lit->w1=0;
4587 }
4588 else
4589 {
4590 lit->w1=100;
4591 }
4592 if(!EqnIsPureVar(lit->literal))
4593 {
4594 lit->w1+=10;
4595 }
4596 if(!EqnIsGround(lit->literal))
4597 {
4598 lit->w1+=1;
4599 }
4600 lit->w2 = -lit_sel_diff_weight(lit->literal);
4601 if(EqnIsEquLit(lit->literal))
4602 {
4603 lit->w3 = PDArrayElementInt(pd, 0);
4604 }
4605 else
4606 {
4607 lit->w3 = PDArrayElementInt(pd, lit->literal->lterm->f_code);
4608 }
4609 }
4610 }
4611
4612 /*-----------------------------------------------------------------------
4613 //
4614 // Function: SelectMaxLComplexAvoidPosPred()
4615 //
4616 // As SelectMaxLComplex, but preferably select literals that do not
4617 // share the predicate symbol with a positive literal.
4618 //
4619 // Global Variables: -
4620 //
4621 // Side Effects : -
4622 //
4623 /----------------------------------------------------------------------*/
4624
4625
SelectMaxLComplexAvoidPosPred(OCB_p ocb,Clause_p clause)4626 void SelectMaxLComplexAvoidPosPred(OCB_p ocb, Clause_p clause)
4627 {
4628 long lit_no;
4629 PDArray_p pred_dist;
4630
4631 assert(ocb);
4632 assert(clause);
4633 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4634
4635 if(clause->neg_lit_no==0)
4636 {
4637 return;
4638 }
4639 ClauseCondMarkMaximalTerms(ocb, clause);
4640
4641 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
4642
4643 if(lit_no <=1)
4644 {
4645 return;
4646 }
4647 pred_dist = pos_pred_dist_array_compute(clause);
4648 generic_uniq_selection(ocb,clause,false, true,
4649 maxlcomplexavoidpred_weight, pred_dist);
4650 pred_dist_array_free(pred_dist);
4651 }
4652
4653
4654
4655 /*-----------------------------------------------------------------------
4656 //
4657 // Function: maxlcomplexappNTNpweight()
4658 //
4659 // Initialize weights to mimic SelectMaxLComplexWeight(), but defer
4660 // literals with which occur often in pred_dist. Never select type-
4661 // and propositional literals.
4662 //
4663 // Global Variables: -
4664 //
4665 // Side Effects : -
4666 //
4667 /----------------------------------------------------------------------*/
4668
maxlcomplexappNTNp_weight(LitEval_p lit,Clause_p clause,void * pred_dist)4669 static void maxlcomplexappNTNp_weight(LitEval_p lit, Clause_p clause,
4670 void *pred_dist)
4671 {
4672 PDArray_p pd = pred_dist;
4673
4674 if(EqnIsNegative(lit->literal))
4675 {
4676 if(EqnIsTypePred(lit->literal)||EqnIsPropositional(lit->literal))
4677 {
4678 lit->w1 = 100000;
4679 lit->forbidden = true;
4680 }
4681 else
4682 {
4683 if(EqnIsMaximal(lit->literal))
4684 {
4685 lit->w1=0;
4686 }
4687 else
4688 {
4689 lit->w1=100;
4690 }
4691 }
4692 if(!EqnIsPureVar(lit->literal))
4693 {
4694 lit->w1+=10;
4695 }
4696 if(!EqnIsGround(lit->literal))
4697 {
4698 lit->w1+=1;
4699 }
4700 lit->w2 = -lit_sel_diff_weight(lit->literal);
4701 if(EqnIsEquLit(lit->literal))
4702 {
4703 lit->w3 = PDArrayElementInt(pd, 0);
4704 }
4705 else
4706 {
4707 lit->w3 = PDArrayElementInt(pd, lit->literal->lterm->f_code);
4708 }
4709 }
4710 }
4711
4712 /*-----------------------------------------------------------------------
4713 //
4714 // Function: SelectMaxLComplexAPPNTNp()
4715 //
4716 // As SelectMaxLComplexAvoidPosPred, but also avoid propositional
4717 // and type literals.
4718 //
4719 // Global Variables: -
4720 //
4721 // Side Effects : -
4722 //
4723 /----------------------------------------------------------------------*/
4724
4725
SelectMaxLComplexAPPNTNp(OCB_p ocb,Clause_p clause)4726 void SelectMaxLComplexAPPNTNp(OCB_p ocb, Clause_p clause)
4727 {
4728 long lit_no;
4729 PDArray_p pred_dist;
4730
4731 assert(ocb);
4732 assert(clause);
4733 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4734
4735 if(clause->neg_lit_no==0)
4736 {
4737 return;
4738 }
4739 ClauseCondMarkMaximalTerms(ocb, clause);
4740
4741 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
4742
4743 if(lit_no <=1)
4744 {
4745 return;
4746 }
4747 pred_dist = pos_pred_dist_array_compute(clause);
4748 generic_uniq_selection(ocb,clause,false, true,
4749 maxlcomplexappNTNp_weight, pred_dist);
4750 pred_dist_array_free(pred_dist);
4751 }
4752
4753
4754
4755
4756 /*-----------------------------------------------------------------------
4757 //
4758 // Function: maxlcomplexavoidprednotype_weight()
4759 //
4760 // As maxlcomplexavoidpred_weigth, but never select type literals.
4761 //
4762 // Global Variables: -
4763 //
4764 // Side Effects : -
4765 //
4766 /----------------------------------------------------------------------*/
4767
maxlcomplexavoidprednotype_weight(LitEval_p lit,Clause_p clause,void * pred_dist)4768 static void maxlcomplexavoidprednotype_weight(LitEval_p lit, Clause_p clause,
4769 void *pred_dist)
4770 {
4771 maxlcomplexavoidpred_weight(lit, clause, pred_dist);
4772 if(EqnIsTypePred(lit->literal))
4773 {
4774 lit->forbidden = true;
4775 }
4776 }
4777
4778
4779 /*-----------------------------------------------------------------------
4780 //
4781 // Function: SelectMaxLComplexAPPNoType()
4782 //
4783 // As SelectMaxLComplexAvoidPosPred, but never select type
4784 // literals.
4785 //
4786 // Global Variables: -
4787 //
4788 // Side Effects : -
4789 //
4790 /----------------------------------------------------------------------*/
4791
4792
SelectMaxLComplexAPPNoType(OCB_p ocb,Clause_p clause)4793 void SelectMaxLComplexAPPNoType(OCB_p ocb, Clause_p clause)
4794 {
4795 long lit_no;
4796 PDArray_p pred_dist;
4797
4798 assert(ocb);
4799 assert(clause);
4800 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4801
4802 if(clause->neg_lit_no==0)
4803 {
4804 return;
4805 }
4806 ClauseCondMarkMaximalTerms(ocb, clause);
4807
4808 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
4809
4810 if(lit_no <=1)
4811 {
4812 return;
4813 }
4814 pred_dist = pos_pred_dist_array_compute(clause);
4815 generic_uniq_selection(ocb,clause,false, true,
4816 maxlcomplexavoidprednotype_weight, pred_dist);
4817 pred_dist_array_free(pred_dist);
4818 }
4819
4820
4821
4822
4823 /*-----------------------------------------------------------------------
4824 //
4825 // Function: SelectMaxLComplexAvoidPosUPred()
4826 //
4827 // As SelectMaxLComplex, but preferably select literals that do not
4828 // share the predicate symbol with a positive literal.
4829 //
4830 // Global Variables: -
4831 //
4832 // Side Effects : -
4833 //
4834 /----------------------------------------------------------------------*/
4835
4836
SelectMaxLComplexAvoidPosUPred(OCB_p ocb,Clause_p clause)4837 void SelectMaxLComplexAvoidPosUPred(OCB_p ocb, Clause_p clause)
4838 {
4839 long lit_no;
4840 PDArray_p pred_dist;
4841
4842 assert(ocb);
4843 assert(clause);
4844 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4845
4846 ClauseCondMarkMaximalTerms(ocb, clause);
4847
4848 lit_no = EqnListQueryPropNumber(clause->literals, EPIsMaximal);
4849
4850 if(lit_no <=1)
4851 {
4852 return;
4853 }
4854 pred_dist = pos_pred_dist_array_compute(clause);
4855 PDArrayAssignInt(pred_dist, 0, 0);
4856
4857 generic_uniq_selection(ocb,clause,false, true,
4858 maxlcomplexavoidpred_weight, pred_dist);
4859 pred_dist_array_free(pred_dist);
4860 }
4861
4862 /*-----------------------------------------------------------------------
4863 //
4864 // Function: complex_weight
4865 //
4866 // Implement a weight function mimicking the old SelectComplex.
4867 //
4868 // Global Variables: -
4869 //
4870 // Side Effects : -
4871 //
4872 /----------------------------------------------------------------------*/
4873
4874
complex_weight(LitEval_p lit,Clause_p clause,void * dummy)4875 static void complex_weight(LitEval_p lit, Clause_p clause,
4876 void *dummy)
4877 {
4878 if(EqnIsNegative(lit->literal))
4879 {
4880 if(EqnIsPureVar(lit->literal))
4881 {
4882 lit->w1 = 0;
4883 }
4884 else if(EqnIsGround(lit->literal))
4885 {
4886 lit->w1 = 10;
4887 lit->w2 = EqnStandardWeight(lit->literal);
4888 }
4889 else
4890 {
4891 lit->w1 = 20;
4892 lit->w2 = -lit_sel_diff_weight(lit->literal);
4893 }
4894 }
4895 }
4896
4897
4898 /*-----------------------------------------------------------------------
4899 //
4900 // Function: SelectComplexG()
4901 //
4902 // Simulate old SelectComplex() with new schema
4903 //
4904 // Global Variables: -
4905 //
4906 // Side Effects : -
4907 //
4908 /----------------------------------------------------------------------*/
4909
SelectComplexG(OCB_p ocb,Clause_p clause)4910 void SelectComplexG(OCB_p ocb, Clause_p clause)
4911 {
4912 generic_uniq_selection(ocb,clause,false, false,
4913 complex_weight,
4914 NULL);
4915 }
4916
4917
4918 /*-----------------------------------------------------------------------
4919 //
4920 // Function: complex_weight_ahp
4921 //
4922 // Implement a weight function mimicking the old SelectComplex, but,
4923 // other things being equal, avoid head predicate symbols.
4924 //
4925 // Global Variables: -
4926 //
4927 // Side Effects : -
4928 //
4929 /----------------------------------------------------------------------*/
4930
4931
complex_weight_ahp(LitEval_p lit,Clause_p clause,void * pred_dist)4932 static void complex_weight_ahp(LitEval_p lit, Clause_p clause,
4933 void *pred_dist)
4934 {
4935 PDArray_p pd = pred_dist;
4936
4937 assert(clause);
4938
4939 if(EqnIsNegative(lit->literal))
4940 {
4941 if(EqnIsPureVar(lit->literal))
4942 {
4943 lit->w1 = 0;
4944 }
4945 else if(EqnIsGround(lit->literal))
4946 {
4947 lit->w1 = 10;
4948 lit->w2 = EqnStandardWeight(lit->literal);
4949 }
4950 else
4951 {
4952 lit->w1 = 20;
4953 lit->w2 = -lit_sel_diff_weight(lit->literal);
4954 }
4955 }
4956 lit->w3 = 0;
4957 if(lit->literal->lterm->f_code > 0)
4958 {
4959 lit->w3 = PDArrayElementInt(pd, lit->literal->lterm->f_code);
4960 }
4961 }
4962
4963
4964 /*-----------------------------------------------------------------------
4965 //
4966 // Function: SelectComplexAHP()
4967 //
4968 // As SelectComplexG, but preferably select literals that do not
4969 // share the predicate symbol with a positive literal.
4970 //
4971 // Global Variables: -
4972 //
4973 // Side Effects : -
4974 //
4975 /----------------------------------------------------------------------*/
4976
4977
SelectComplexAHP(OCB_p ocb,Clause_p clause)4978 void SelectComplexAHP(OCB_p ocb, Clause_p clause)
4979 {
4980 PDArray_p pred_dist;
4981
4982 assert(ocb);
4983 assert(clause);
4984 assert(clause->neg_lit_no);
4985 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
4986
4987 pred_dist = pos_pred_dist_array_compute(clause);
4988
4989 generic_uniq_selection(ocb,clause,false, true,
4990 complex_weight_ahp, pred_dist);
4991 pred_dist_array_free(pred_dist);
4992 }
4993
4994
4995 /*-----------------------------------------------------------------------
4996 //
4997 // Function: PSelectComplexAHP()
4998 //
4999 // As SelectComplexAHP, but also select positive literals.
5000 //
5001 // Global Variables: -
5002 //
5003 // Side Effects : -
5004 //
5005 /----------------------------------------------------------------------*/
5006
5007
PSelectComplexAHP(OCB_p ocb,Clause_p clause)5008 void PSelectComplexAHP(OCB_p ocb, Clause_p clause)
5009 {
5010 PDArray_p pred_dist;
5011
5012 assert(ocb);
5013 assert(clause);
5014 assert(clause->neg_lit_no);
5015 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5016
5017 pred_dist = pos_pred_dist_array_compute(clause);
5018
5019 generic_uniq_selection(ocb,clause,true, true,
5020 complex_weight_ahp, pred_dist);
5021 pred_dist_array_free(pred_dist);
5022 }
5023
5024
5025 /*-----------------------------------------------------------------------
5026 //
5027 // Function: new_complex_notp_ahp
5028 //
5029 // Implement a weight function mimicking the old SelectNewComplex,
5030 // but, other things being equal, avoid head predicate symbols.
5031 //
5032 // Global Variables: -
5033 //
5034 // Side Effects : -
5035 //
5036 /----------------------------------------------------------------------*/
5037
5038
new_complex_notp_ahp(LitEval_p lit,Clause_p clause,void * pred_dist)5039 static void new_complex_notp_ahp(LitEval_p lit, Clause_p clause,
5040 void *pred_dist)
5041 {
5042 PDArray_p pd = pred_dist;
5043
5044 assert(clause);
5045
5046 if(EqnIsNegative(lit->literal))
5047 {
5048 if(EqnIsGround(lit->literal))
5049 {
5050 lit->w1 = 0;
5051 lit->w2 = TermStandardWeight(lit->literal->lterm);
5052 }
5053 else if(!EqnIsXTypePred(lit->literal))
5054 {
5055 lit->w1 = 10;
5056 lit->w2 = EqnMaxTermPositions(lit->literal);
5057 }
5058 else if(!EqnIsTypePred(lit->literal))
5059 {
5060 lit->w1 = 20;
5061 lit->w2 = -TermStandardWeight(lit->literal->lterm);
5062 }
5063 else
5064 {
5065 assert(EqnIsTypePred(lit->literal));
5066 lit->w1 = 100000;
5067 lit->forbidden = 1;
5068 }
5069 }
5070 lit->w3 = 0;
5071 if(!TermIsVar(lit->literal->lterm))
5072 {
5073 lit->w3 = PDArrayElementInt(pd, lit->literal->lterm->f_code);
5074 }
5075 }
5076
5077
5078
5079
5080 /*-----------------------------------------------------------------------
5081 //
5082 // Function: SelectNewComplexAHP
5083 //
5084 // Mimic SelectNewComplex(), but with the AHP property.
5085 //
5086 // Global Variables: -
5087 //
5088 // Side Effects : -
5089 //
5090 /----------------------------------------------------------------------*/
5091
SelectNewComplexAHP(OCB_p ocb,Clause_p clause)5092 void SelectNewComplexAHP(OCB_p ocb, Clause_p clause)
5093 {
5094 PDArray_p pred_dist;
5095
5096 assert(ocb);
5097 assert(clause);
5098 assert(clause->neg_lit_no);
5099 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5100
5101 pred_dist = pos_pred_dist_array_compute(clause);
5102
5103 generic_uniq_selection(ocb,clause,false, true,
5104 new_complex_notp_ahp, pred_dist);
5105 pred_dist_array_free(pred_dist);
5106 }
5107
5108
5109 /*-----------------------------------------------------------------------
5110 //
5111 // Function: PSelectNewComplexAHP
5112 //
5113 // Mimic PSelectNewComplex(), but with the AHP property.
5114 //
5115 // Global Variables: -
5116 //
5117 // Side Effects : -
5118 //
5119 /----------------------------------------------------------------------*/
5120
PSelectNewComplexAHP(OCB_p ocb,Clause_p clause)5121 void PSelectNewComplexAHP(OCB_p ocb, Clause_p clause)
5122 {
5123 PDArray_p pred_dist;
5124
5125 assert(ocb);
5126 assert(clause);
5127 assert(clause->neg_lit_no);
5128 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5129
5130 pred_dist = pos_pred_dist_array_compute(clause);
5131
5132 generic_uniq_selection(ocb,clause, true, true,
5133 new_complex_notp_ahp, pred_dist);
5134 pred_dist_array_free(pred_dist);
5135 }
5136
5137
5138
5139
5140 /*-----------------------------------------------------------------------
5141 //
5142 // Function: SelectComplexAHPExceptRRHorn()
5143 //
5144 // If a clause is Horn and range-restricted, do no select. Otherwise
5145 // use SelectComplexAHP() (above).
5146 //
5147 // Global Variables: -
5148 //
5149 // Side Effects : Changes property in literals
5150 //
5151 /----------------------------------------------------------------------*/
5152
SelectComplexAHPExceptRRHorn(OCB_p ocb,Clause_p clause)5153 void SelectComplexAHPExceptRRHorn(OCB_p ocb, Clause_p clause)
5154 {
5155 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
5156 {
5157 SelectComplexAHP(ocb, clause);
5158 }
5159 }
5160
5161
5162 /*-----------------------------------------------------------------------
5163 //
5164 // Function: PSelectComplexAHPExceptRRHorn()
5165 //
5166 // If a clause is Horn and range-restricted, do no select. Otherwise
5167 // use PSelectComplexAHP() (above).
5168 //
5169 // Global Variables: -
5170 //
5171 // Side Effects : Changes property in literals
5172 //
5173 /----------------------------------------------------------------------*/
5174
PSelectComplexAHPExceptRRHorn(OCB_p ocb,Clause_p clause)5175 void PSelectComplexAHPExceptRRHorn(OCB_p ocb, Clause_p clause)
5176 {
5177 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
5178 {
5179 PSelectComplexAHP(ocb, clause);
5180 }
5181 }
5182
5183
5184 /*-----------------------------------------------------------------------
5185 //
5186 // Function: SelectNewComplexAHPExceptRRHorn()
5187 //
5188 // If a clause is Horn and range-restricted, do no select. Otherwise
5189 // use SelectNewComplexAHP() (above).
5190 //
5191 // Global Variables: -
5192 //
5193 // Side Effects : Changes property in literals
5194 //
5195 /----------------------------------------------------------------------*/
5196
SelectNewComplexAHPExceptRRHorn(OCB_p ocb,Clause_p clause)5197 void SelectNewComplexAHPExceptRRHorn(OCB_p ocb, Clause_p clause)
5198 {
5199 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
5200 {
5201 SelectNewComplexAHP(ocb, clause);
5202 }
5203 }
5204
5205
5206 /*-----------------------------------------------------------------------
5207 //
5208 // Function: PSelectNewComplexAHPExceptRRHorn()
5209 //
5210 // If a clause is Horn and range-restricted, do no select. Otherwise
5211 // use PSelectNewComplexAHP() (above).
5212 //
5213 // Global Variables: -
5214 //
5215 // Side Effects : Changes property in literals
5216 //
5217 /----------------------------------------------------------------------*/
5218
PSelectNewComplexAHPExceptRRHorn(OCB_p ocb,Clause_p clause)5219 void PSelectNewComplexAHPExceptRRHorn(OCB_p ocb, Clause_p clause)
5220 {
5221 if(!(ClauseIsHorn(clause) && ClauseIsRangeRestricted(clause)))
5222 {
5223 PSelectNewComplexAHP(ocb, clause);
5224 }
5225 }
5226
5227
5228 /*-----------------------------------------------------------------------
5229 //
5230 // Function: SelectNewComplexAHPExceptUniqMaxHorn()
5231 //
5232 // Select literal as in SelectNewComplexAHP unless the clause is a
5233 // Horn clause with a unique maximal literal.
5234 //
5235 // Global Variables: -
5236 //
5237 // Side Effects : Changes property in literals
5238 //
5239 /----------------------------------------------------------------------*/
5240
SelectNewComplexAHPExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)5241 void SelectNewComplexAHPExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
5242 {
5243 if(ClauseIsHorn(clause))
5244 {
5245 ClauseCondMarkMaximalTerms(ocb, clause);
5246 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
5247 {
5248 return;
5249 }
5250 }
5251 SelectNewComplexAHP(ocb,clause);
5252 }
5253
5254
5255
5256 /*-----------------------------------------------------------------------
5257 //
5258 // Function: PSelectNewComplexAHPExceptUniqMaxHorn()
5259 //
5260 // Select literal as in PSelectNewComplexAHP unless the clause is a
5261 // Horn clause with a unique maximal literal.
5262 //
5263 // Global Variables: -
5264 //
5265 // Side Effects : Changes property in literals
5266 //
5267 /----------------------------------------------------------------------*/
5268
PSelectNewComplexAHPExceptUniqMaxHorn(OCB_p ocb,Clause_p clause)5269 void PSelectNewComplexAHPExceptUniqMaxHorn(OCB_p ocb, Clause_p clause)
5270 {
5271 if(ClauseIsHorn(clause))
5272 {
5273 ClauseCondMarkMaximalTerms(ocb, clause);
5274 if(EqnListQueryPropNumber(clause->literals, EPIsMaximal)==1)
5275 {
5276 return;
5277 }
5278 }
5279 PSelectNewComplexAHP(ocb,clause);
5280 }
5281
5282
5283
5284
5285
5286 /*-----------------------------------------------------------------------
5287 //
5288 // Function: new_complex_notp_ahp_ns
5289 //
5290 // Implement a weight function mimicking the old SelectNewComplex,
5291 // but, other things being equal, avoid head predicate
5292 // symbols. Always avoid split symbols.
5293 //
5294 // Global Variables: -
5295 //
5296 // Side Effects : -
5297 //
5298 /----------------------------------------------------------------------*/
5299
5300
new_complex_notp_ahp_ns(LitEval_p lit,Clause_p clause,void * pred_dist)5301 static void new_complex_notp_ahp_ns(LitEval_p lit, Clause_p clause,
5302 void *pred_dist)
5303 {
5304 PDArray_p pd = pred_dist;
5305
5306 assert(clause);
5307
5308 if(EqnIsNegative(lit->literal))
5309 {
5310 if(EqnIsSplitLit(lit->literal))
5311 {
5312 lit->w1 = 100000;
5313 lit->forbidden = 1;
5314 }
5315 else if(EqnIsGround(lit->literal))
5316 {
5317 lit->w1 = 0;
5318 lit->w2 = TermStandardWeight(lit->literal->lterm);
5319 }
5320 else if(!EqnIsXTypePred(lit->literal))
5321 {
5322 lit->w1 = 10;
5323 lit->w2 = EqnMaxTermPositions(lit->literal);
5324 }
5325 else if(!EqnIsTypePred(lit->literal))
5326 {
5327 lit->w1 = 20;
5328 lit->w2 = -TermStandardWeight(lit->literal->lterm);
5329 }
5330 else
5331 {
5332 assert(EqnIsTypePred(lit->literal));
5333 lit->w1 = 100000;
5334 lit->forbidden = 1;
5335 }
5336 }
5337 lit->w3 = 0;
5338 if(!TermIsVar(lit->literal->lterm))
5339 {
5340 lit->w3 = PDArrayElementInt(pd, lit->literal->lterm->f_code);
5341 }
5342 }
5343
5344
5345
5346
5347 /*-----------------------------------------------------------------------
5348 //
5349 // Function: SelectNewComplexAHPNS
5350 //
5351 // Mimic SelectNewComplex(), but with the AHP property and never
5352 // select split literals.
5353 //
5354 // Global Variables: -
5355 //
5356 // Side Effects : -
5357 //
5358 /----------------------------------------------------------------------*/
5359
SelectNewComplexAHPNS(OCB_p ocb,Clause_p clause)5360 void SelectNewComplexAHPNS(OCB_p ocb, Clause_p clause)
5361 {
5362 PDArray_p pred_dist;
5363
5364 assert(ocb);
5365 assert(clause);
5366 assert(clause->neg_lit_no);
5367 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5368
5369 pred_dist = pos_pred_dist_array_compute(clause);
5370
5371 generic_uniq_selection(ocb,clause,false, true,
5372 new_complex_notp_ahp_ns, pred_dist);
5373 pred_dist_array_free(pred_dist);
5374 }
5375
5376
5377 /*-----------------------------------------------------------------------
5378 //
5379 // Function: SelectVGNonCR()
5380 //
5381 // If there is a negative pure variable literal, select it.
5382 // If there is a negative ground literal, select the smallest one.
5383 // Otherwise, if there is a unique positive maximal literal, don't
5384 // select.
5385 // Otherwise select as SelectNewComplexAHPNS.
5386 //
5387 // Global Variables: -
5388 //
5389 // Side Effects : -
5390 //
5391 /----------------------------------------------------------------------*/
5392
SelectVGNonCR(OCB_p ocb,Clause_p clause)5393 void SelectVGNonCR(OCB_p ocb, Clause_p clause)
5394 {
5395 Eqn_p handle;
5396 int maxlits, maxposlits;
5397 PDArray_p pred_dist;
5398
5399 assert(ocb);
5400 assert(clause);
5401 assert(clause->neg_lit_no);
5402 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5403
5404 handle = ClauseFindNegPureVarLit(clause);
5405
5406 if(handle)
5407 {
5408 EqnSetProp(handle, EPIsSelected);
5409 return;
5410 }
5411
5412 ClauseCondMarkMaximalTerms(ocb, clause);
5413 handle = find_smallest_neg_ground_lit(clause);
5414 if(handle)
5415 {
5416 EqnSetProp(handle, EPIsSelected);
5417 return;
5418 }
5419 maxlits = EqnListQueryPropNumber(clause->literals,
5420 EPIsMaximal);
5421 if(maxlits == 1)
5422 {
5423 maxposlits = EqnListQueryPropNumber(clause->literals,
5424 EPIsMaximal|EPIsPositive);
5425 if(maxposlits == 1)
5426 {
5427 return;
5428 }
5429 }
5430 pred_dist = pos_pred_dist_array_compute(clause);
5431
5432 generic_uniq_selection(ocb,clause,false, true,
5433 new_complex_notp_ahp_ns, pred_dist);
5434 pred_dist_array_free(pred_dist);
5435 }
5436
5437
5438 /*-----------------------------------------------------------------------
5439 //
5440 // Function: select_cq_ar_eql_weight()
5441 // Function: SelectCQArEqLast()
5442 //
5443 // Select based on a total ordering on predicate symbols. Preferably
5444 // select symbols with high arity. Equality is always selected last.
5445 //
5446 // Global Variables: -
5447 //
5448 // Side Effects : -
5449 //
5450 /----------------------------------------------------------------------*/
5451
select_cq_ar_eql_weight(LitEval_p lit,Clause_p clause,void * dummy)5452 static void select_cq_ar_eql_weight(LitEval_p lit, Clause_p clause,
5453 void* dummy)
5454 {
5455 Eqn_p l = lit->literal;
5456
5457 if(EqnIsEquLit(l))
5458 {
5459 lit->w1 = 1000000;
5460 lit->w2 = 0;
5461 }
5462 else
5463 {
5464 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5465 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5466 }
5467 lit->w3 =lit_sel_diff_weight(l);
5468 }
5469
SelectCQArEqLast(OCB_p ocb,Clause_p clause)5470 void SelectCQArEqLast(OCB_p ocb, Clause_p clause)
5471 {
5472 assert(ocb);
5473 assert(clause);
5474 assert(clause->neg_lit_no);
5475 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5476
5477 generic_uniq_selection(ocb,clause,false, true,
5478 select_cq_ar_eql_weight, NULL);
5479 }
5480
5481
5482 /*-----------------------------------------------------------------------
5483 //
5484 // Function: select_cq_ar_eqf_weight()
5485 // Function: SelectCQArEqFirst()
5486 //
5487 // Select based on a total ordering on predicate symbols. Preferably
5488 // select symbols with high arity. Equality is always selected
5489 // first.
5490 //
5491 // Global Variables: -
5492 //
5493 // Side Effects : -
5494 //
5495 /----------------------------------------------------------------------*/
5496
select_cq_ar_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5497 static void select_cq_ar_eqf_weight(LitEval_p lit, Clause_p clause,
5498 void* dummy)
5499 {
5500 Eqn_p l = lit->literal;
5501
5502 if(EqnIsEquLit(l))
5503 {
5504 lit->w1 = -100000;
5505 lit->w2 = 0;
5506 }
5507 else
5508 {
5509 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5510 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5511 }
5512 lit->w3 =lit_sel_diff_weight(l);
5513 }
5514
SelectCQArEqFirst(OCB_p ocb,Clause_p clause)5515 void SelectCQArEqFirst(OCB_p ocb, Clause_p clause)
5516 {
5517 assert(ocb);
5518 assert(clause);
5519 assert(clause->neg_lit_no);
5520 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5521
5522 generic_uniq_selection(ocb,clause,false, true,
5523 select_cq_ar_eqf_weight, NULL);
5524 }
5525
5526 /*-----------------------------------------------------------------------
5527 //
5528 // Function: select_cq_iar_eql_weight()
5529 // Function: SelectCQIArEqLast()
5530 //
5531 // Select based on a total ordering on predicate symbols. Preferably
5532 // select symbols with low arity. Equality is always selected
5533 // last.
5534 //
5535 // Global Variables: -
5536 //
5537 // Side Effects : -
5538 //
5539 /----------------------------------------------------------------------*/
5540
select_cq_iar_eql_weight(LitEval_p lit,Clause_p clause,void * dummy)5541 static void select_cq_iar_eql_weight(LitEval_p lit, Clause_p clause,
5542 void* dummy)
5543 {
5544 Eqn_p l = lit->literal;
5545
5546 if(EqnIsEquLit(l))
5547 {
5548 lit->w1 = 100000;
5549 lit->w2 = 0;
5550 }
5551 else
5552 {
5553 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
5554 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5555 }
5556 lit->w3 =lit_sel_diff_weight(l);
5557 }
5558
SelectCQIArEqLast(OCB_p ocb,Clause_p clause)5559 void SelectCQIArEqLast(OCB_p ocb, Clause_p clause)
5560 {
5561 assert(ocb);
5562 assert(clause);
5563 assert(clause->neg_lit_no);
5564 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5565
5566 generic_uniq_selection(ocb,clause,false, true,
5567 select_cq_iar_eql_weight, NULL);
5568 }
5569
5570
5571 /*-----------------------------------------------------------------------
5572 //
5573 // Function: select_cq_iar_eqf_weight()
5574 // Function: SelectCQIArEqFirst()
5575 //
5576 // Select based on a total ordering on predicate symbols. Preferable
5577 // select symbols with low arity. Equality is always selected
5578 // first.
5579 //
5580 // Global Variables: -
5581 //
5582 // Side Effects : -
5583 //
5584 /----------------------------------------------------------------------*/
5585
select_cq_iar_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5586 static void select_cq_iar_eqf_weight(LitEval_p lit, Clause_p clause,
5587 void* dummy)
5588 {
5589 Eqn_p l = lit->literal;
5590
5591 if(EqnIsEquLit(l))
5592 {
5593 lit->w1 = -100000;
5594 lit->w2 = 0;
5595 }
5596 else
5597 {
5598 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
5599 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5600 }
5601 lit->w3 =lit_sel_diff_weight(l);
5602 }
5603
SelectCQIArEqFirst(OCB_p ocb,Clause_p clause)5604 void SelectCQIArEqFirst(OCB_p ocb, Clause_p clause)
5605 {
5606 assert(ocb);
5607 assert(clause);
5608 assert(clause->neg_lit_no);
5609 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5610
5611 generic_uniq_selection(ocb,clause,false, true,
5612 select_cq_iar_eqf_weight, NULL);
5613 }
5614
5615
5616
5617 /*-----------------------------------------------------------------------
5618 //
5619 // Function: select_cq_ar_weight()
5620 // Function: SelectCQAr()
5621 //
5622 // Select based on a total ordering on predicate symbols. Preferably
5623 // select symbols with high arity. Equality is treated as a normal
5624 // predicate symbol (nearly).
5625 //
5626 // Global Variables: -
5627 //
5628 // Side Effects : -
5629 //
5630 /----------------------------------------------------------------------*/
5631
5632
select_cq_ar_weight(LitEval_p lit,Clause_p clause,void * dummy)5633 static void select_cq_ar_weight(LitEval_p lit, Clause_p clause,
5634 void* dummy)
5635 {
5636 Eqn_p l = lit->literal;
5637
5638 if(EqnIsEquLit(l))
5639 {
5640 lit->w1 = -2;
5641 lit->w2 = l->lterm->f_code > 0
5642 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
5643 : 0;
5644 }
5645 else
5646 {
5647 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5648 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5649 }
5650 lit->w3 =lit_sel_diff_weight(l);
5651 }
5652
SelectCQAr(OCB_p ocb,Clause_p clause)5653 void SelectCQAr(OCB_p ocb, Clause_p clause)
5654 {
5655 assert(ocb);
5656 assert(clause);
5657 assert(clause->neg_lit_no);
5658 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5659
5660 generic_uniq_selection(ocb,clause,false, true,
5661 select_cq_ar_weight, NULL);
5662 }
5663
5664
5665
5666 /*-----------------------------------------------------------------------
5667 //
5668 // Function: select_cq_iar_weight()
5669 // Function: SelectCQIAr()
5670 //
5671 // Select based on a total ordering on predicate symbols. Preferably
5672 // select symbols with low arity. Equality is treated as a normal
5673 // predicate symbol (nearly).
5674 //
5675 // Global Variables: -
5676 //
5677 // Side Effects : -
5678 //
5679 /----------------------------------------------------------------------*/
5680
select_cq_iar_weight(LitEval_p lit,Clause_p clause,void * dummy)5681 static void select_cq_iar_weight(LitEval_p lit, Clause_p clause,
5682 void* dummy)
5683 {
5684 Eqn_p l = lit->literal;
5685
5686 if(EqnIsEquLit(l))
5687 {
5688 lit->w1 = 2;
5689 lit->w2 = l->lterm->f_code > 0
5690 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
5691 : 0;
5692 }
5693 else
5694 {
5695 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
5696 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5697 }
5698 lit->w3 =lit_sel_diff_weight(l);
5699 }
5700
5701
SelectCQIAr(OCB_p ocb,Clause_p clause)5702 void SelectCQIAr(OCB_p ocb, Clause_p clause)
5703 {
5704 assert(ocb);
5705 assert(clause);
5706 assert(clause->neg_lit_no);
5707 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5708
5709 generic_uniq_selection(ocb,clause,false, true,
5710 select_cq_iar_weight, NULL);
5711 }
5712
5713
5714 /*-----------------------------------------------------------------------
5715 //
5716 // Function: select_cq_arnp_eqf_weight()
5717 // Function: SelectCQArNpEqFirst()
5718 //
5719 // Select based on a total ordering on predicate symbols. Preferably
5720 // select symbols with high arity. Equaliy comes
5721 // first. Propositional symbols are never selected.
5722 //
5723 // Global Variables: -
5724 //
5725 // Side Effects : -
5726 //
5727 /----------------------------------------------------------------------*/
5728
select_cq_arnp_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5729 static void select_cq_arnp_eqf_weight(LitEval_p lit, Clause_p clause,
5730 void* dummy)
5731 {
5732 Eqn_p l = lit->literal;
5733
5734 if(EqnIsEquLit(l))
5735 {
5736 lit->w1 = -100000;
5737 lit->w2 = 0;
5738 }
5739 else
5740 {
5741 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5742 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5743 if(lit->w1 == 0)
5744 {
5745 lit->w1 = 100000;
5746 lit->forbidden = true;
5747 }
5748 }
5749 lit->w3 =lit_sel_diff_weight(l);
5750 }
5751
5752
SelectCQArNpEqFirst(OCB_p ocb,Clause_p clause)5753 void SelectCQArNpEqFirst(OCB_p ocb, Clause_p clause)
5754 {
5755 assert(ocb);
5756 assert(clause);
5757 assert(clause->neg_lit_no);
5758 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5759
5760 generic_uniq_selection(ocb,clause,false, true,
5761 select_cq_arnp_eqf_weight, NULL);
5762 }
5763
5764
5765
5766 /*-----------------------------------------------------------------------
5767 //
5768 // Function: select_cq_iarnp_eqf_weight()
5769 // Function: SelectCQIArNpEqFirst()
5770 //
5771 // Select based on a total ordering on predicate symbols. Preferably
5772 // select symbols with low arity. Equaliy comes
5773 // first. Propositional symbols are never selected.
5774 //
5775 // Global Variables: -
5776 //
5777 // Side Effects : -
5778 //
5779 /----------------------------------------------------------------------*/
5780
select_cq_iarnp_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5781 static void select_cq_iarnp_eqf_weight(LitEval_p lit, Clause_p clause,
5782 void* dummy)
5783 {
5784 Eqn_p l = lit->literal;
5785
5786 if(EqnIsEquLit(l))
5787 {
5788 lit->w1 = -1000000;
5789 lit->w2 = 0;
5790 }
5791 else
5792 {
5793 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
5794 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5795 if(lit->w1 == 0)
5796 {
5797 lit->w1 = 1000000;
5798 lit->forbidden = true;
5799 }
5800 }
5801 lit->w3 =lit_sel_diff_weight(l);
5802 }
5803
SelectCQIArNpEqFirst(OCB_p ocb,Clause_p clause)5804 void SelectCQIArNpEqFirst(OCB_p ocb, Clause_p clause)
5805 {
5806 assert(ocb);
5807 assert(clause);
5808 assert(clause->neg_lit_no);
5809 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5810
5811 generic_uniq_selection(ocb,clause,false, true,
5812 select_cq_iarnp_eqf_weight, NULL);
5813 }
5814
5815
5816 /*-----------------------------------------------------------------------
5817 //
5818 // Function: select_grcq_ar_eqf_weight()
5819 // Function: SelectGrCQArEqFirst()
5820 //
5821 // Select ground literals first, then others. Among
5822 // ground/nonground, select symbols with high arity. Equality is
5823 // always selected first.
5824 //
5825 // Global Variables:
5826 //
5827 // Side Effects :
5828 //
5829 /----------------------------------------------------------------------*/
5830
select_grcq_ar_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5831 static void select_grcq_ar_eqf_weight(LitEval_p lit, Clause_p clause,
5832 void* dummy)
5833 {
5834 Eqn_p l = lit->literal;
5835
5836 if(EqnIsEquLit(l))
5837 {
5838 lit->w1 = -1000000;
5839 lit->w2 = 0;
5840 }
5841 else
5842 {
5843 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5844 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5845 }
5846 lit->w3 =lit_sel_diff_weight(l);
5847 if(EqnIsGround(l))
5848 {
5849 lit->w1 -= 2000000;
5850 }
5851 }
5852
5853
SelectGrCQArEqFirst(OCB_p ocb,Clause_p clause)5854 void SelectGrCQArEqFirst(OCB_p ocb, Clause_p clause)
5855 {
5856 assert(ocb);
5857 assert(clause);
5858 assert(clause->neg_lit_no);
5859 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5860
5861 generic_uniq_selection(ocb,clause,false, true,
5862 select_grcq_ar_eqf_weight, NULL);
5863 }
5864
5865
5866 /*-----------------------------------------------------------------------
5867 //
5868 // Function: select_cqgr_ar_eqf_weight()
5869 // Function: SelectCQGrArEqFirst()
5870 //
5871 // Select based on a total ordering on predicate symbols. Preferably
5872 // select symbols with low arity. Equality is always selected
5873 // first. Among literals with the same symbol, prefer ground.
5874 //
5875 // Global Variables: -
5876 //
5877 // Side Effects : -
5878 //
5879 /----------------------------------------------------------------------*/
5880
select_cqgr_ar_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5881 static void select_cqgr_ar_eqf_weight(LitEval_p lit, Clause_p clause,
5882 void* dummy)
5883 {
5884 Eqn_p l = lit->literal;
5885
5886 if(EqnIsEquLit(l))
5887 {
5888 lit->w1 = -1000000;
5889 lit->w2 = 0;
5890 }
5891 else
5892 {
5893 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5894 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5895 }
5896 lit->w3 =lit_sel_diff_weight(l);
5897 if(EqnIsGround(l))
5898 {
5899 lit->w2 -= 2000000;
5900 }
5901 }
5902
SelectCQGrArEqFirst(OCB_p ocb,Clause_p clause)5903 void SelectCQGrArEqFirst(OCB_p ocb, Clause_p clause)
5904 {
5905 assert(ocb);
5906 assert(clause);
5907 assert(clause->neg_lit_no);
5908 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5909
5910 generic_uniq_selection(ocb,clause,false, true,
5911 select_cqgr_ar_eqf_weight, NULL);
5912 }
5913
5914
5915 /*-----------------------------------------------------------------------
5916 //
5917 // Function: select_cq_arnt_eqf_weight()
5918 // Function: SelectCQArNTEqFirst()
5919 //
5920 // Select based on a total ordering on predicate symbols. Preferably
5921 // select symbols with low arity. Equality comes
5922 // first. Type literals p(X) are never selected.
5923 //
5924 // Global Variables: -
5925 //
5926 // Side Effects : -
5927 //
5928 /----------------------------------------------------------------------*/
5929
select_cq_arnt_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5930 static void select_cq_arnt_eqf_weight(LitEval_p lit, Clause_p clause,
5931 void* dummy)
5932 {
5933 Eqn_p l = lit->literal;
5934
5935 if(EqnIsEquLit(l))
5936 {
5937 lit->w1 = -100000;
5938 lit->w2 = 0;
5939 }
5940 else
5941 {
5942 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
5943 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5944 if(EqnIsTypePred(l))
5945 {
5946 lit->w1 = 100000;
5947 lit->forbidden = true;
5948 }
5949 }
5950 lit->w3 =lit_sel_diff_weight(l);
5951 }
5952
SelectCQArNTEqFirst(OCB_p ocb,Clause_p clause)5953 void SelectCQArNTEqFirst(OCB_p ocb, Clause_p clause)
5954 {
5955 assert(ocb);
5956 assert(clause);
5957 assert(clause->neg_lit_no);
5958 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
5959
5960 generic_uniq_selection(ocb,clause,false, true,
5961 select_cq_arnt_eqf_weight, NULL);
5962 }
5963
5964
5965 /*-----------------------------------------------------------------------
5966 //
5967 // Function: select_cq_iarnt_eqf_weight()
5968 // Function: SelectCQIArNTEqFirst()
5969 //
5970 // Select based on a total ordering on predicate symbols. Preferably
5971 // select symbols with low arity. Equality comes
5972 // first. Type literals p(X) are never selected.
5973 //
5974 // Global Variables: -
5975 //
5976 // Side Effects : -
5977 //
5978 /----------------------------------------------------------------------*/
5979
select_cq_iarnt_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)5980 static void select_cq_iarnt_eqf_weight(LitEval_p lit, Clause_p clause,
5981 void* dummy)
5982 {
5983 Eqn_p l = lit->literal;
5984
5985 if(EqnIsEquLit(l))
5986 {
5987 lit->w1 = -100000;
5988 lit->w2 = 0;
5989 }
5990 else
5991 {
5992 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
5993 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
5994 if(EqnIsTypePred(l))
5995 {
5996 lit->w1 = 100000;
5997 lit->forbidden = true;
5998 }
5999 }
6000 lit->w3 =lit_sel_diff_weight(l);
6001 }
6002
SelectCQIArNTEqFirst(OCB_p ocb,Clause_p clause)6003 void SelectCQIArNTEqFirst(OCB_p ocb, Clause_p clause)
6004 {
6005 assert(ocb);
6006 assert(clause);
6007 assert(clause->neg_lit_no);
6008 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6009
6010 generic_uniq_selection(ocb,clause,false, true,
6011 select_cq_iarnt_eqf_weight, NULL);
6012 }
6013
6014
6015 /*-----------------------------------------------------------------------
6016 //
6017 // Function: select_cq_arntnp_eqf_weight()
6018 // Function: SelectCQArNTNpEqFirst()
6019 //
6020 // Select based on a total ordering on predicate symbols. Preferably
6021 // select symbols with low arity. Equality comes
6022 // first. Type literals p(X) and propositional lierals are never
6023 // selected.
6024 //
6025 // Global Variables: -
6026 //
6027 // Side Effects : -
6028 //
6029 /----------------------------------------------------------------------*/
6030
select_cq_arntnp_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)6031 static void select_cq_arntnp_eqf_weight(LitEval_p lit, Clause_p clause,
6032 void* dummy)
6033 {
6034 Eqn_p l = lit->literal;
6035
6036 if(EqnIsEquLit(l))
6037 {
6038 lit->w1 = -100000;
6039 lit->w2 = 0;
6040 }
6041 else
6042 {
6043 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
6044 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6045 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6046 {
6047 lit->w1 = 100000;
6048 lit->forbidden = true;
6049 }
6050 }
6051 lit->w3 =lit_sel_diff_weight(l);
6052 }
6053
SelectCQArNTNpEqFirst(OCB_p ocb,Clause_p clause)6054 void SelectCQArNTNpEqFirst(OCB_p ocb, Clause_p clause)
6055 {
6056 assert(ocb);
6057 assert(clause);
6058 assert(clause->neg_lit_no);
6059 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6060
6061 generic_uniq_selection(ocb,clause,false, true,
6062 select_cq_arntnp_eqf_weight, NULL);
6063 }
6064
6065
6066 /*-----------------------------------------------------------------------
6067 //
6068 // Function: select_cq_iarntnp_eqf_weight()
6069 // Function: SelectCQIArNTNpEqFirst()
6070 //
6071 // Select based on a total ordering on predicate symbols. Preferably
6072 // select symbols with low arity. Equality comes
6073 // first. Type literals p(X) and propositional lierals are never
6074 // selected.
6075 //
6076 // Global Variables: -
6077 //
6078 // Side Effects : -
6079 //
6080 /----------------------------------------------------------------------*/
6081
select_cq_iarntnp_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)6082 static void select_cq_iarntnp_eqf_weight(LitEval_p lit, Clause_p clause,
6083 void* dummy)
6084 {
6085 Eqn_p l = lit->literal;
6086
6087 if(EqnIsEquLit(l))
6088 {
6089 lit->w1 = -100000;
6090 lit->w2 = 0;
6091 }
6092 else
6093 {
6094 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
6095 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6096 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6097 {
6098 lit->w1 = 100000;
6099 lit->forbidden = true;
6100 }
6101 }
6102 lit->w3 =lit_sel_diff_weight(l);
6103 }
6104
SelectCQIArNTNpEqFirst(OCB_p ocb,Clause_p clause)6105 void SelectCQIArNTNpEqFirst(OCB_p ocb, Clause_p clause)
6106 {
6107 assert(ocb);
6108 assert(clause);
6109 assert(clause->neg_lit_no);
6110 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6111
6112 generic_uniq_selection(ocb,clause,false, true,
6113 select_cq_iarntnp_eqf_weight, NULL);
6114 }
6115
6116
6117 /*-----------------------------------------------------------------------
6118 //
6119 // Function: select_cq_arnxt_eqf_weight()
6120 // Function: SelectCQArNXTEqFirst()
6121 //
6122 // Select based on a total ordering on predicate symbols. Preferably
6123 // select symbols with low arity. Equality comes
6124 // first. XType literals p(X,Y,...) are never selected.
6125 //
6126 // Global Variables: -
6127 //
6128 // Side Effects : -
6129 //
6130 /----------------------------------------------------------------------*/
6131
select_cq_arnxt_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)6132 static void select_cq_arnxt_eqf_weight(LitEval_p lit, Clause_p clause,
6133 void* dummy)
6134 {
6135 Eqn_p l = lit->literal;
6136
6137 if(EqnIsEquLit(l))
6138 {
6139 lit->w1 = -100000;
6140 lit->w2 = 0;
6141 }
6142 else
6143 {
6144 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
6145 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6146 if(EqnIsXTypePred(l))
6147 {
6148 lit->w1 = 100000;
6149 lit->forbidden = true;
6150 }
6151 }
6152 lit->w3 =lit_sel_diff_weight(l);
6153 }
6154
SelectCQArNXTEqFirst(OCB_p ocb,Clause_p clause)6155 void SelectCQArNXTEqFirst(OCB_p ocb, Clause_p clause)
6156 {
6157 assert(ocb);
6158 assert(clause);
6159 assert(clause->neg_lit_no);
6160 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6161
6162 generic_uniq_selection(ocb,clause,false, true,
6163 select_cq_arnxt_eqf_weight, NULL);
6164 }
6165
6166
6167 /*-----------------------------------------------------------------------
6168 //
6169 // Function: select_cq_iarnxt_eqf_weight()
6170 // Function: SelectCQIArNXTEqFirst()
6171 //
6172 // Select based on a total ordering on predicate symbols. Preferably
6173 // select symbols with low arity. Equality comes
6174 // first. XType literals p(X, Y,...) are never selected.
6175 //
6176 // Global Variables: -
6177 //
6178 // Side Effects : -
6179 //
6180 /----------------------------------------------------------------------*/
6181
6182
select_cq_iarnxt_eqf_weight(LitEval_p lit,Clause_p clause,void * dummy)6183 static void select_cq_iarnxt_eqf_weight(LitEval_p lit, Clause_p clause,
6184 void* dummy)
6185 {
6186 Eqn_p l = lit->literal;
6187
6188 if(EqnIsEquLit(l))
6189 {
6190 lit->w1 = -100000;
6191 lit->w2 = 0;
6192 }
6193 else
6194 {
6195 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
6196 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6197 if(EqnIsXTypePred(l))
6198 {
6199 lit->w1 = 100000;
6200 lit->forbidden = true;
6201 }
6202 }
6203 lit->w3 =lit_sel_diff_weight(l);
6204 }
6205
SelectCQIArNXTEqFirst(OCB_p ocb,Clause_p clause)6206 void SelectCQIArNXTEqFirst(OCB_p ocb, Clause_p clause)
6207 {
6208 assert(ocb);
6209 assert(clause);
6210 assert(clause->neg_lit_no);
6211 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6212
6213 generic_uniq_selection(ocb,clause,false, true,
6214 select_cq_iarnxt_eqf_weight, NULL);
6215 }
6216
6217
6218
6219 /*-----------------------------------------------------------------------
6220 //
6221 // Function: SelectCQArNTNp()
6222 //
6223 // Select based on a total ordering on predicate symbols. Preferably
6224 // select symbols with high arity. Never select propositional and
6225 // type predicates.
6226 //
6227 // Global Variables: -
6228 //
6229 // Side Effects : -
6230 //
6231 /----------------------------------------------------------------------*/
6232
select_cq_arntnp_weight(LitEval_p lit,Clause_p clause,void * dummy)6233 static void select_cq_arntnp_weight(LitEval_p lit, Clause_p clause,
6234 void* dummy)
6235 {
6236 Eqn_p l = lit->literal;
6237
6238 if(EqnIsEquLit(l))
6239 {
6240 lit->w1 = -2;
6241 lit->w2 = l->lterm->f_code > 0
6242 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6243 : 0;
6244 }
6245 else
6246 {
6247 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
6248 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6249 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6250 {
6251 lit->w1 = 100000;
6252 lit->forbidden = true;
6253 }
6254 }
6255 lit->w3 =lit_sel_diff_weight(l);
6256 }
6257
SelectCQArNTNp(OCB_p ocb,Clause_p clause)6258 void SelectCQArNTNp(OCB_p ocb, Clause_p clause)
6259 {
6260 assert(ocb);
6261 assert(clause);
6262 assert(clause->neg_lit_no);
6263 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6264
6265 generic_uniq_selection(ocb,clause,false, true,
6266 select_cq_arntnp_weight, NULL);
6267 }
6268
6269
6270 /*-----------------------------------------------------------------------
6271 //
6272 // Function: SelectCQIArNTNp()
6273 //
6274 // Select based on a total ordering on predicate symbols. Preferably
6275 // select symbols with low arity. Never select propositional and
6276 // type predicates.
6277 //
6278 // Global Variables: -
6279 //
6280 // Side Effects : -
6281 //
6282 /----------------------------------------------------------------------*/
6283
select_cq_iarntnp_weight(LitEval_p lit,Clause_p clause,void * dummy)6284 static void select_cq_iarntnp_weight(LitEval_p lit, Clause_p clause,
6285 void* dummy)
6286 {
6287 Eqn_p l = lit->literal;
6288
6289 if(EqnIsEquLit(l))
6290 {
6291 lit->w1 = 2;
6292 lit->w2 = l->lterm->f_code > 0
6293 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6294 : 0;
6295 }
6296 else
6297 {
6298 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
6299 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6300 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6301 {
6302 lit->w1 = 100000;
6303 lit->forbidden = true;
6304 }
6305 }
6306 lit->w3 =lit_sel_diff_weight(l);
6307 }
6308
SelectCQIArNTNp(OCB_p ocb,Clause_p clause)6309 void SelectCQIArNTNp(OCB_p ocb, Clause_p clause)
6310 {
6311 assert(ocb);
6312 assert(clause);
6313 assert(clause->neg_lit_no);
6314 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6315
6316 generic_uniq_selection(ocb,clause,false, true,
6317 select_cq_iarntnp_weight, NULL);
6318 }
6319
6320
6321 /*-----------------------------------------------------------------------
6322 //
6323 // Function: SelectCQArNT()
6324 //
6325 // Select based on a total ordering on predicate symbols. Preferably
6326 // select symbols with high arity. Never select type predicates.
6327 //
6328 // Global Variables: -
6329 //
6330 // Side Effects : -
6331 //
6332 /----------------------------------------------------------------------*/
6333
select_cq_arnt_weight(LitEval_p lit,Clause_p clause,void * dummy)6334 static void select_cq_arnt_weight(LitEval_p lit, Clause_p clause,
6335 void* dummy)
6336 {
6337 Eqn_p l = lit->literal;
6338
6339 if(EqnIsEquLit(l))
6340 {
6341 lit->w1 = -2;
6342 lit->w2 = l->lterm->f_code > 0
6343 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6344 : 0;
6345 }
6346 else
6347 {
6348 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
6349 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6350 if(EqnIsTypePred(l))
6351 {
6352 lit->w1 = 100000;
6353 lit->forbidden = true;
6354 }
6355 }
6356 lit->w3 =lit_sel_diff_weight(l);
6357 }
6358
SelectCQArNT(OCB_p ocb,Clause_p clause)6359 void SelectCQArNT(OCB_p ocb, Clause_p clause)
6360 {
6361 assert(ocb);
6362 assert(clause);
6363 assert(clause->neg_lit_no);
6364 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6365
6366 generic_uniq_selection(ocb,clause,false, true,
6367 select_cq_arnt_weight, NULL);
6368 }
6369
6370
6371 /*-----------------------------------------------------------------------
6372 //
6373 // Function: SelectCQIArNT()
6374 //
6375 // Select based on a total ordering on predicate symbols. Preferably
6376 // select symbols with low arity. Never select type predicates.
6377 //
6378 // Global Variables: -
6379 //
6380 // Side Effects : -
6381 //
6382 /----------------------------------------------------------------------*/
6383
select_cq_iarnt_weight(LitEval_p lit,Clause_p clause,void * dummy)6384 static void select_cq_iarnt_weight(LitEval_p lit, Clause_p clause,
6385 void* dummy)
6386 {
6387 Eqn_p l = lit->literal;
6388
6389 if(EqnIsEquLit(l))
6390 {
6391 lit->w1 = 2;
6392 lit->w2 = l->lterm->f_code > 0
6393 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6394 : 0;
6395 }
6396 else
6397 {
6398 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
6399 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6400 if(EqnIsTypePred(l))
6401 {
6402 lit->w1 = 100000;
6403 lit->forbidden = true;
6404 }
6405 }
6406 lit->w3 =lit_sel_diff_weight(l);
6407 }
6408
SelectCQIArNT(OCB_p ocb,Clause_p clause)6409 void SelectCQIArNT(OCB_p ocb, Clause_p clause)
6410 {
6411 assert(ocb);
6412 assert(clause);
6413 assert(clause->neg_lit_no);
6414 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6415
6416 generic_uniq_selection(ocb,clause,false, true,
6417 select_cq_iarnt_weight, NULL);
6418 }
6419
6420
6421 /*-----------------------------------------------------------------------
6422 //
6423 // Function: SelectCQArNp()
6424 //
6425 // Select based on a total ordering on predicate symbols. Preferably
6426 // select symbols with high arity. Never select propositional predicates.
6427 //
6428 // Global Variables: -
6429 //
6430 // Side Effects : -
6431 //
6432 /----------------------------------------------------------------------*/
6433
select_cq_arnp_weight(LitEval_p lit,Clause_p clause,void * dummy)6434 static void select_cq_arnp_weight(LitEval_p lit, Clause_p clause,
6435 void* dummy)
6436 {
6437 Eqn_p l = lit->literal;
6438
6439 if(EqnIsEquLit(l))
6440 {
6441 lit->w1 = -2;
6442 lit->w2 = l->lterm->f_code > 0
6443 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6444 : 0;
6445 }
6446 else
6447 {
6448 lit->w1 = -SigFindArity(l->bank->sig, l->lterm->f_code);
6449 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6450 if(EqnIsPropositional(l))
6451 {
6452 lit->w1 = 100000;
6453 lit->forbidden = true;
6454 }
6455 }
6456 lit->w3 =lit_sel_diff_weight(l);
6457 }
6458
SelectCQArNp(OCB_p ocb,Clause_p clause)6459 void SelectCQArNp(OCB_p ocb, Clause_p clause)
6460 {
6461 assert(ocb);
6462 assert(clause);
6463 assert(clause->neg_lit_no);
6464 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6465
6466 generic_uniq_selection(ocb,clause,false, true,
6467 select_cq_arnp_weight, NULL);
6468 }
6469
6470
6471 /*-----------------------------------------------------------------------
6472 //
6473 // Function: SelectCQIArNp()
6474 //
6475 // Select based on a total ordering on predicate symbols. Preferably
6476 // select symbols with low arity. Never select propositional
6477 // predicates.
6478 //
6479 // Global Variables: -
6480 //
6481 // Side Effects : -
6482 //
6483 /----------------------------------------------------------------------*/
6484
select_cq_iarnp_weight(LitEval_p lit,Clause_p clause,void * dummy)6485 static void select_cq_iarnp_weight(LitEval_p lit, Clause_p clause,
6486 void* dummy)
6487 {
6488 Eqn_p l = lit->literal;
6489
6490 if(EqnIsEquLit(l))
6491 {
6492 lit->w1 = 2;
6493 lit->w2 = l->lterm->f_code > 0
6494 ? SigGetAlphaRank(l->bank->sig, l->lterm->f_code)
6495 : 0;
6496 }
6497 else
6498 {
6499 lit->w1 = SigFindArity(l->bank->sig, l->lterm->f_code);
6500 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6501 if(EqnIsPropositional(l))
6502 {
6503 lit->w1 = 100000;
6504 lit->forbidden = true;
6505 }
6506 }
6507 lit->w3 =lit_sel_diff_weight(l);
6508 }
6509
SelectCQIArNp(OCB_p ocb,Clause_p clause)6510 void SelectCQIArNp(OCB_p ocb, Clause_p clause)
6511 {
6512 assert(ocb);
6513 assert(clause);
6514 assert(clause->neg_lit_no);
6515 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6516
6517 generic_uniq_selection(ocb,clause,false, true,
6518 select_cq_iarnp_weight, NULL);
6519 }
6520
6521
6522
6523
6524 /*-----------------------------------------------------------------------
6525 //
6526 // Function: select_unless_pdom()
6527 //
6528 // If there is a maximal positive literal with the same predicate
6529 // symbol as a negative literal, don't select. Otherwise use
6530 // the provided function.
6531 //
6532 // Global Variables: -
6533 //
6534 // Side Effects : -
6535 //
6536 /----------------------------------------------------------------------*/
6537
select_unless_pdom(OCB_p ocb,Clause_p clause,LiteralSelectionFun selfun)6538 void select_unless_pdom(OCB_p ocb, Clause_p clause, LiteralSelectionFun selfun)
6539 {
6540 PStack_p neg_lits = PStackAlloc();
6541 bool *dom_array;
6542 Eqn_p lit;
6543 bool dom = false;
6544 int i;
6545 long sig_size;
6546
6547 assert(ocb);
6548 assert(clause);
6549 assert(clause->neg_lit_no);
6550 assert(clause->literals);
6551 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6552
6553 sig_size = clause->literals->bank->sig->size;
6554 dom_array = SizeMalloc(sizeof(bool)*sig_size);
6555 for(i=0; i<sig_size; i++)
6556 {
6557 dom_array[i] = false;
6558 }
6559
6560 ClauseCondMarkMaximalTerms(ocb, clause);
6561 //printf("Selection: ");
6562 //ClausePrint(stdout, clause, true);
6563 //printf("\n");
6564
6565 for(lit = clause->literals; lit; lit = lit->next)
6566 {
6567 if(EqnIsPositive(lit)&&EqnIsMaximal(lit))
6568 {
6569 // printf("Posmax: %ld\n", EqnGetPredCode(lit));
6570 dom_array[EqnGetPredCode(lit)] = true;
6571 }
6572 else if(EqnIsNegative(lit))
6573 {
6574 PStackPushP(neg_lits, lit);
6575 }
6576 }
6577 while(!PStackEmpty(neg_lits))
6578 {
6579 lit = PStackPopP(neg_lits);
6580 //printf("%p - %ld\n", lit, EqnGetPredCode(lit));
6581 if(dom_array[EqnGetPredCode(lit)])
6582 {
6583 dom = true;
6584 break;
6585 }
6586 }
6587
6588 PStackFree(neg_lits);
6589 SizeFree(dom_array, sizeof(bool)*sig_size);
6590 if(dom)
6591 {
6592 //printf("nixda\n");
6593 }
6594 else
6595 {
6596 //printf("Select\n");
6597 selfun(ocb, clause);
6598 }
6599 }
6600
6601
6602 /*-----------------------------------------------------------------------
6603 //
6604 // Function: SelectCQArNpEqFirstUnlessPDom()
6605 //
6606 // If there is a maximal positive literal with the same predicate
6607 // symbol as a negative literal, don't select. Otherwise use
6608 // SelectCQArNpEqFirst.
6609 //
6610 // Global Variables: -
6611 //
6612 // Side Effects : -
6613 //
6614 /----------------------------------------------------------------------*/
6615
SelectCQArNpEqFirstUnlessPDom(OCB_p ocb,Clause_p clause)6616 void SelectCQArNpEqFirstUnlessPDom(OCB_p ocb, Clause_p clause)
6617 {
6618 select_unless_pdom(ocb, clause, SelectCQArNpEqFirst);
6619 }
6620
6621
6622 /*-----------------------------------------------------------------------
6623 //
6624 // Function: SelectCQArNTEqFirst()
6625 //
6626 // If there is a maximal positive literal with the same predicate
6627 // symbol as a negative literal, don't select. Otherwise use
6628 // SelectCQArNpEqFirst.
6629 //
6630 // Global Variables: -
6631 //
6632 // Side Effects : -
6633 //
6634 /----------------------------------------------------------------------*/
6635
SelectCQArNTEqFirstUnlessPDom(OCB_p ocb,Clause_p clause)6636 void SelectCQArNTEqFirstUnlessPDom(OCB_p ocb, Clause_p clause)
6637 {
6638 select_unless_pdom(ocb, clause, SelectCQArNTEqFirst);
6639 }
6640
6641
6642 /*-----------------------------------------------------------------------
6643 //
6644 // Function: SelectCQPrecW()
6645 //
6646 // Select literals based on the predicate, with the order of the
6647 // predicates defined by the prec_weights (i.e. the preoder on the
6648 // function symbols). Prefer larger (?) symbols.
6649 //
6650 // Global Variables: -
6651 //
6652 // Side Effects : -
6653 //
6654 /----------------------------------------------------------------------*/
6655
select_cq_precw_weight(LitEval_p lit,Clause_p clause,void * vocb)6656 static void select_cq_precw_weight(LitEval_p lit, Clause_p clause,
6657 void* vocb)
6658 {
6659 OCB_p ocb = (OCB_p)vocb;
6660 Eqn_p l = lit->literal;
6661
6662 if(TermIsVar(l->lterm))
6663 {
6664 lit->w1 = 0;
6665 lit->w2 = 0;
6666 }
6667 else
6668 {
6669 lit->w1 = OCBFunPrecWeight(ocb, l->lterm->f_code);
6670 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6671 }
6672 lit->w3 =lit_sel_diff_weight(l);
6673 }
6674
SelectCQPrecW(OCB_p ocb,Clause_p clause)6675 void SelectCQPrecW(OCB_p ocb, Clause_p clause)
6676 {
6677 assert(ocb);
6678 assert(clause);
6679 assert(clause->neg_lit_no);
6680 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6681
6682 generic_uniq_selection(ocb,clause,false, true,
6683 select_cq_precw_weight, ocb);
6684 }
6685
6686
6687 /*-----------------------------------------------------------------------
6688 //
6689 // Function: SelectCQIPrecW()
6690 //
6691 // Select literals based on the predicate, with the order of the
6692 // predicates defined by the prec_weights (i.e. the preoder on the
6693 // function symbols). Prefere smaller (?) symbols.
6694 //
6695 // Global Variables: -
6696 //
6697 // Side Effects : -
6698 //
6699 /----------------------------------------------------------------------*/
6700
6701
select_cq_iprecw_weight(LitEval_p lit,Clause_p clause,void * vocb)6702 static void select_cq_iprecw_weight(LitEval_p lit, Clause_p clause,
6703 void* vocb)
6704 {
6705 OCB_p ocb = (OCB_p)vocb;
6706 Eqn_p l = lit->literal;
6707
6708 if(TermIsVar(l->lterm))
6709 {
6710 lit->w1 = 0;
6711 lit->w2 = 0;
6712 }
6713 else
6714 {
6715 lit->w1 = -OCBFunPrecWeight(ocb, l->lterm->f_code);
6716 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6717 }
6718 lit->w3 =lit_sel_diff_weight(l);
6719 }
6720
SelectCQIPrecW(OCB_p ocb,Clause_p clause)6721 void SelectCQIPrecW(OCB_p ocb, Clause_p clause)
6722 {
6723 assert(ocb);
6724 assert(clause);
6725 assert(clause->neg_lit_no);
6726 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6727
6728 generic_uniq_selection(ocb,clause,false, true,
6729 select_cq_iprecw_weight, ocb);
6730 }
6731
6732
6733 /*-----------------------------------------------------------------------
6734 //
6735 // Function: SelectCQPrecWNTNp()
6736 //
6737 // Select literals based on the predicate, with the order of the
6738 // predicates defined by the prec_weights (i.e. the preoder on the
6739 // function symbols). Prefere larger symbols. Never select
6740 // propostional or type predicates.
6741 //
6742 // Global Variables: -
6743 //
6744 // Side Effects : -
6745 //
6746 /----------------------------------------------------------------------*/
6747
6748
select_cq_precwntnp_weight(LitEval_p lit,Clause_p clause,void * vocb)6749 static void select_cq_precwntnp_weight(LitEval_p lit, Clause_p clause,
6750 void* vocb)
6751 {
6752 OCB_p ocb = (OCB_p)vocb;
6753 Eqn_p l = lit->literal;
6754
6755 if(TermIsVar(l->lterm))
6756 {
6757 lit->w1 = 0;
6758 lit->w2 = 0;
6759 }
6760 else
6761 {
6762 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6763 {
6764 lit->w1 = 100000;
6765 lit->forbidden = true;
6766 }
6767 else
6768 {
6769 lit->w1 = OCBFunPrecWeight(ocb, l->lterm->f_code);
6770 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6771 }
6772 }
6773 lit->w3 =lit_sel_diff_weight(l);
6774 }
6775
SelectCQPrecWNTNp(OCB_p ocb,Clause_p clause)6776 void SelectCQPrecWNTNp(OCB_p ocb, Clause_p clause)
6777 {
6778 assert(ocb);
6779 assert(clause);
6780 assert(clause->neg_lit_no);
6781 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6782
6783 generic_uniq_selection(ocb,clause,false, true,
6784 select_cq_precwntnp_weight, ocb);
6785 }
6786
6787
6788 /*-----------------------------------------------------------------------
6789 //
6790 // Function: SelectCQPrecWNTNp()
6791 //
6792 // Select literals based on the predicate, with the order of the
6793 // predicates defined by the prec_weights (i.e. the preoder on the
6794 // function symbols). Prefere larger symbols. Never select
6795 // propostional or type predicates.
6796 //
6797 // Global Variables: -
6798 //
6799 // Side Effects : -
6800 //
6801 /----------------------------------------------------------------------*/
6802
6803
select_cq_iprecwntnp_weight(LitEval_p lit,Clause_p clause,void * vocb)6804 static void select_cq_iprecwntnp_weight(LitEval_p lit, Clause_p clause,
6805 void* vocb)
6806 {
6807 OCB_p ocb = (OCB_p)vocb;
6808 Eqn_p l = lit->literal;
6809
6810 if(TermIsVar(l->lterm))
6811 {
6812 lit->w1 = 0;
6813 lit->w2 = 0;
6814 }
6815 else
6816 {
6817 if(EqnIsTypePred(l)||EqnIsPropositional(l))
6818 {
6819 lit->w1 = 100000;
6820 lit->forbidden = true;
6821 }
6822 else
6823 {
6824 lit->w1 = -OCBFunPrecWeight(ocb, l->lterm->f_code);
6825 lit->w2 = SigGetAlphaRank(l->bank->sig, l->lterm->f_code);
6826 }
6827 }
6828 lit->w3 =lit_sel_diff_weight(l);
6829 }
6830
SelectCQIPrecWNTNp(OCB_p ocb,Clause_p clause)6831 void SelectCQIPrecWNTNp(OCB_p ocb, Clause_p clause)
6832 {
6833 assert(ocb);
6834 assert(clause);
6835 assert(clause->neg_lit_no);
6836 assert(EqnListQueryPropNumber(clause->literals, EPIsSelected)==0);
6837
6838 generic_uniq_selection(ocb,clause,false, true,
6839 select_cq_iprecwntnp_weight, ocb);
6840 }
6841
6842
6843
6844
6845
6846
6847 /*---------------------------------------------------------------------*/
6848 /* End of File */
6849 /*---------------------------------------------------------------------*/
6850
6851
6852
6853
6854
6855
6856
6857
6858
6859