1 /*-----------------------------------------------------------------------
2
3 File : ccl_freqvectors.c
4
5 Author: Stephan Schulz
6
7 Contents
8
9 Algorithms for frequency count vectors.
10
11 Copyright 1998-2011 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Tue Jul 8 21:50:44 CEST 2003
20 New (separated functionality from ccl_fcvindexing.c)
21
22 -----------------------------------------------------------------------*/
23
24 #include "ccl_freqvectors.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32 PERF_CTR_DEFINE(FreqVecTimer);
33
34 /*---------------------------------------------------------------------*/
35 /* Forward Declarations */
36 /*---------------------------------------------------------------------*/
37
38
39 /*---------------------------------------------------------------------*/
40 /* Internal Functions */
41 /*---------------------------------------------------------------------*/
42
43 /*-----------------------------------------------------------------------
44 //
45 // Function: tuple_3_compare_23lex()
46 //
47 // Compare 2 tuple-2 cells lexicographically, with diff more
48 // significant than value, which is more significant than pos.
49 //
50 // Global Variables: -
51 //
52 // Side Effects : -
53 //
54 /----------------------------------------------------------------------*/
55
tuple3_compare_23lex(const void * tuple1,const void * tuple2)56 int tuple3_compare_23lex(const void* tuple1, const void* tuple2)
57 {
58 const Tuple3Cell *t1 = (const Tuple3Cell *)tuple1;
59 const Tuple3Cell *t2 = (const Tuple3Cell *)tuple2;
60
61 if(t1->diff < t2->diff)
62 {
63 return -1;
64 }
65 if(t1->diff > t2->diff)
66 {
67 return 1;
68 }
69 if(t1->value < t2->value)
70 {
71 return -1;
72 }
73 if(t1->value > t2->value)
74 {
75 return 1;
76 }
77 if(t1->pos > t2->pos)
78 {
79 return -1;
80 }
81 if(t1->pos < t2->pos)
82 {
83 return 1;
84 }
85 return 0;
86 }
87
88
89 /*-----------------------------------------------------------------------
90 //
91 // Function: gather_feature_vec()
92 //
93 // Gather a feature from a full feature vector according to
94 // cspec.
95 //
96 // Global Variables: -
97 //
98 // Side Effects : -
99 //
100 /----------------------------------------------------------------------*/
101
gather_feature_vec(FVCollect_p cspec,long * full_vec,FreqVector_p vec,long findex)102 static void gather_feature_vec(FVCollect_p cspec, long* full_vec,
103 FreqVector_p vec, long findex)
104 {
105 long resindex = -1, base = 0, offset = 0, mod = 0;
106
107 if(findex < cspec->ass_vec_len)
108 {
109 resindex = cspec->assembly_vector[findex];
110 }
111 else
112 {
113 switch(findex%4)
114 {
115 case 0:
116 base = cspec->pos_count_base;
117 offset = cspec->pos_count_offset;
118 mod = cspec->pos_count_mod;
119 break;
120 case 1:
121 base = cspec->pos_depth_base;
122 offset = cspec->pos_depth_offset;
123 mod = cspec->pos_depth_mod;
124 break;
125 case 2:
126 base = cspec->neg_count_base;
127 offset = cspec->neg_count_offset;
128 mod = cspec->neg_count_mod;
129 break;
130 case 3:
131 base = cspec->neg_depth_base;
132 offset = cspec->neg_depth_offset;
133 mod = cspec->neg_depth_mod;
134 break;
135 default:
136 assert(false);
137 break;
138 }
139 if(mod)
140 {
141 resindex = base+(offset+(findex/4))%mod;
142 }
143 }
144 if(resindex != -1)
145 {
146 vec->array[resindex]+=full_vec[findex];
147 }
148 }
149
150
151 /*---------------------------------------------------------------------*/
152 /* Exported Functions */
153 /*---------------------------------------------------------------------*/
154
155 /*-----------------------------------------------------------------------
156 //
157 // Function: PermVectorComputeInternal()
158 //
159 // Find a "good" permutation (and selection) vector for
160 // FVIndexing by:
161 // - Ordering features from lesser to higher informativity
162 // - Selecting the best max_len features
163 // - Optionally drop features that have no projected informational
164 // value.
165 //
166 // Global Variables: -
167 //
168 // Side Effects : Memory operations
169 //
170 /----------------------------------------------------------------------*/
171
PermVectorComputeInternal(FreqVector_p fmax,FreqVector_p fmin,FreqVector_p fsum,long max_len,bool eliminate_uninformative)172 PermVector_p PermVectorComputeInternal(FreqVector_p fmax, FreqVector_p fmin,
173 FreqVector_p fsum,
174 long max_len,
175 bool eliminate_uninformative)
176 {
177 Tuple3Cell *array;
178 long i, size, start=0, start1=0, diff;
179 PermVector_p handle;
180
181 assert(fsum->size == fmax->size);
182 assert(fsum->size == fmin->size);
183
184 array = SizeMalloc(fsum->size * sizeof(Tuple3Cell));
185 for(i=0; i<fsum->size; i++)
186 {
187 array[i].pos = i;
188 diff = fmax->array[i]-fmin->array[i];
189 array[i].diff = diff;
190 array[i].value = fsum->array[i];
191 }
192 qsort(array, fsum->size, sizeof(Tuple3Cell), tuple3_compare_23lex);
193
194 if(fsum->size > max_len)
195 {
196 start = fsum->size - max_len;
197 }
198 if(eliminate_uninformative)
199 {
200 for(i=0; i<fsum->size && !array[i].diff; i++)
201 {
202 /* Intentionally empty */
203 };
204 start1 = i;
205 }
206 start = MAX(start, start1);
207 if(start == fsum->size)
208 {
209 start--;
210 }
211 size = fsum->size - start;
212
213 handle = PermVectorAlloc(size);
214
215 for(i=0; i < size; i++)
216 {
217 handle->array[i] = array[i+start].pos;
218 }
219 SizeFree(array, fsum->size * sizeof(Tuple3Cell));
220 /* PermVectorPrint(GlobalOut, handle); */
221 return handle;
222 }
223
224
225 /*-----------------------------------------------------------------------
226 //
227 // Function: FreqVectorAlloc()
228 //
229 // Allocate a frequency vector that can hold up to sig_start
230 // non function symbol count features and sig_count function symbol
231 // counts (in both positive and negative variety).
232 //
233 // Global Variables: -
234 //
235 // Side Effects : Memory operations.
236 //
237 /----------------------------------------------------------------------*/
238
FreqVectorAlloc(long size)239 FreqVector_p FreqVectorAlloc(long size)
240 {
241 FreqVector_p handle = FreqVectorCellAlloc();
242
243 /* printf("Size: %ld\n", size); */
244 handle->size = size;
245 handle->array = SizeMalloc(sizeof(long)*handle->size);
246 FreqVectorInitialize(handle, 0);
247 handle->clause = NULL;
248 return handle;
249 }
250
251
252 /*-----------------------------------------------------------------------
253 //
254 // Function: FreqVectorFree()
255 //
256 // Free a frequency vector.
257 //
258 // Global Variables: -
259 //
260 // Side Effects : Memory operations
261 //
262 /----------------------------------------------------------------------*/
263
FreqVectorFreeReal(FreqVector_p junk)264 void FreqVectorFreeReal(FreqVector_p junk)
265 {
266 assert(junk);
267
268 if(junk->array)
269 {
270 SizeFree(junk->array, sizeof(long)*junk->size);
271 #ifndef NDEBUG
272 junk->array = NULL;
273 junk->clause = NULL;
274 #endif
275 }
276 FreqVectorCellFree(junk);
277 }
278
279
280 /*-----------------------------------------------------------------------
281 //
282 // Function: FreqVectorInitialize()
283 //
284 // Store value in all fields of vec.
285 //
286 // Global Variables: -
287 //
288 // Side Effects : -
289 //
290 /----------------------------------------------------------------------*/
291
FreqVectorInitialize(FreqVector_p vec,long value)292 void FreqVectorInitialize(FreqVector_p vec, long value)
293 {
294 long i;
295
296 for(i=0; i<vec->size;i++)
297 {
298 vec->array[i] = value;
299 }
300 }
301
302 /*-----------------------------------------------------------------------
303 //
304 // Function: FreqVectorPrint()
305 //
306 // Print a frequency vector.
307 //
308 // Global Variables: -
309 //
310 // Side Effects : Output
311 //
312 /----------------------------------------------------------------------*/
313
FreqVectorPrint(FILE * out,FreqVector_p vec)314 void FreqVectorPrint(FILE* out, FreqVector_p vec)
315 {
316 long i;
317
318 assert(vec);
319 if(vec->clause)
320 {
321 fprintf(out, "# FV for: ");
322 ClausePrint(out, vec->clause, true);
323 fprintf(out, "\n");
324 }
325 else
326 {
327 fprintf(out, "# FV, no clause given.\n");
328 }
329 fprintf(out, "# FV(len=%ld):", vec->size);
330 for(i=0; i<vec->size; i++)
331
332 {
333 fprintf(out, " %ld", vec->array[i]);
334 }
335 fprintf(out, "\n");
336 }
337
338
339 /*-----------------------------------------------------------------------
340 //
341 // Function: VarFreqVectorAddVals()
342 //
343 // Add values for up to symbol type features to the freq vector.
344 //
345 // Global Variables: -
346 //
347 // Side Effects : Memory operations
348 //
349 /----------------------------------------------------------------------*/
350
VarFreqVectorAddVals(FreqVector_p vec,long symbols,FVIndexType features,Clause_p clause)351 void VarFreqVectorAddVals(FreqVector_p vec, long symbols, FVIndexType features,
352 Clause_p clause)
353 {
354 long *unused, *pfreqstart, *nfreqstart, *pdepthstart, *ndepthstart;
355 long unused_size = 0;
356 Eqn_p handle;
357
358 assert(clause);
359 assert((features == FVIACFeatures) ||
360 (features == FVISSFeatures) ||
361 (features == FVIAllFeatures));
362 assert(vec);
363 assert(vec->size == FVSize(symbols, features));
364
365 switch(features)
366 {
367 case FVIACFeatures:
368 vec->array[0] += clause->pos_lit_no;
369 vec->array[1] += clause->neg_lit_no;
370 unused_size = symbols+1;
371 unused = SizeMalloc(sizeof(long)*unused_size);
372 pdepthstart = ndepthstart = unused;
373 nfreqstart = &(vec->array[FV_CLAUSE_FEATURES]);
374 pfreqstart = &(vec->array[FV_CLAUSE_FEATURES+1*(symbols+1)]);
375 break;
376 case FVISSFeatures:
377 unused_size = symbols+1;
378 unused = SizeMalloc(sizeof(long)*unused_size);
379 pfreqstart = nfreqstart = unused;
380 ndepthstart = &(vec->array[0]);
381 pdepthstart = &(vec->array[0+1*(symbols+1)]);
382 break;
383 case FVIAllFeatures:
384 vec->array[0] += clause->pos_lit_no;
385 vec->array[1] += clause->neg_lit_no;
386 unused = NULL;
387 nfreqstart = &(vec->array[FV_CLAUSE_FEATURES]);
388 pfreqstart = &(vec->array[FV_CLAUSE_FEATURES+1*(symbols+1)]);
389 pdepthstart = &(vec->array[FV_CLAUSE_FEATURES+2*(symbols+1)]);
390 ndepthstart = &(vec->array[FV_CLAUSE_FEATURES+3*(symbols+1)]);
391 break;
392 default:
393 assert(features == FVINoFeatures);
394 assert(false);
395 return; /* Cheapest way to fix compiler warning */
396 }
397 if(unused)
398 { /* Stiffle insure warnings - we don't use unused (duh!), but
399 insure does not know that */
400 long i;
401
402 for(i=0; i<unused_size; i++)
403 {
404 unused[i] = 0;
405 }
406 }
407 for(handle = clause->literals; handle; handle = handle->next)
408 {
409 if(EqnIsPositive(handle))
410 {
411 EqnAddSymbolFeaturesLimited(handle,
412 pfreqstart,
413 pdepthstart,
414 symbols);
415 }
416 else
417 {
418 EqnAddSymbolFeaturesLimited(handle,
419 nfreqstart,
420 ndepthstart,
421 symbols);
422 }
423 }
424 if(unused)
425 {
426 SizeFree(unused, sizeof(long)*unused_size);
427 }
428 }
429
430
431 /*-----------------------------------------------------------------------
432 //
433 // Function: VarFreqVectorCompute()
434 //
435 // Allocate and return a frequency vector for clause based on the
436 // other supplied parameters.
437 //
438 // Global Variables: -
439 //
440 // Side Effects : Memory allocation.
441 //
442 /----------------------------------------------------------------------*/
443
VarFreqVectorCompute(Clause_p clause,FVCollect_p cspec)444 FreqVector_p VarFreqVectorCompute(Clause_p clause, FVCollect_p cspec)
445 {
446 long size;
447 FreqVector_p vec;
448
449 assert(clause);
450
451 assert((cspec->features == FVIACFeatures) ||
452 (cspec->features == FVISSFeatures) ||
453 (cspec->features == FVIAllFeatures) ||
454 (cspec->features == FVICollectFeatures));
455
456 if(cspec->features == FVICollectFeatures)
457 {
458 vec = FVCollectFreqVectorCompute(clause, cspec);
459 }
460 else
461 {
462 size = FVSize(cspec->max_symbols, cspec->features);
463
464 vec = FreqVectorAlloc(size);
465 vec->clause = clause;
466 FreqVectorInitialize(vec, 0);
467 VarFreqVectorAddVals(vec, cspec->max_symbols,
468 cspec->features, clause);
469 }
470 return vec;
471 }
472
473
474 /*-----------------------------------------------------------------------
475 //
476 // Function: OptimizedVarFreqVectorCompute()
477 //
478 // Compute an "optimized" frequency count vector, based on a given
479 // permutation vector. If no permutation vector is given, return a
480 // VarFreqVector.
481 //
482 // Global Variables: -
483 //
484 // Side Effects : Memory operations
485 //
486 /----------------------------------------------------------------------*/
487
OptimizedVarFreqVectorCompute(Clause_p clause,PermVector_p perm,FVCollect_p cspec)488 FreqVector_p OptimizedVarFreqVectorCompute(Clause_p clause,
489 PermVector_p perm,
490 FVCollect_p cspec)
491 {
492 FreqVector_p vec, res;
493
494 assert((cspec->features == FVIACFeatures) ||
495 (cspec->features == FVISSFeatures) ||
496 (cspec->features == FVIAllFeatures) ||
497 (cspec->features == FVICollectFeatures));
498
499 PERF_CTR_ENTRY(FreqVecTimer);
500
501
502 /* printf("Symbols used: %ld\n", sig_symbols); */
503 vec = VarFreqVectorCompute(clause, cspec);
504 /* FreqVectorPrint(GlobalOut, vec); */
505 if(perm)
506 {
507 long i;
508
509 res = FreqVectorAlloc(perm->size);
510 for(i=0; i<perm->size; i++)
511 {
512 assert(perm->array[i]>=0);
513 assert(perm->array[i]<vec->size);
514 res->array[i] = vec->array[perm->array[i]];
515 }
516 res->clause = clause;
517 FreqVectorFree(vec);
518 PERF_CTR_EXIT(FreqVecTimer);
519 return res;
520 }
521 PERF_CTR_EXIT(FreqVecTimer);
522 return vec;
523 }
524
525
526 /*-----------------------------------------------------------------------
527 //
528 // Function: FVCollectInit()
529 //
530 // Initialize an FVCollectCell.
531 //
532 // Global Variables: -
533 //
534 // Side Effects : Memory operations
535 //
536 /----------------------------------------------------------------------*/
537
FVCollectInit(FVCollect_p handle,FVIndexType features,bool use_litcount,long ass_vec_len,long res_vec_len,long pos_count_base,long pos_count_offset,long pos_count_mod,long neg_count_base,long neg_count_offset,long neg_count_mod,long pos_depth_base,long pos_depth_offset,long pos_depth_mod,long neg_depth_base,long neg_depth_offset,long neg_depth_mod)538 void FVCollectInit(FVCollect_p handle,
539 FVIndexType features,
540 bool use_litcount,
541 long ass_vec_len,
542 long res_vec_len,
543 long pos_count_base,
544 long pos_count_offset,
545 long pos_count_mod,
546 long neg_count_base,
547 long neg_count_offset,
548 long neg_count_mod,
549 long pos_depth_base,
550 long pos_depth_offset,
551 long pos_depth_mod,
552 long neg_depth_base,
553 long neg_depth_offset,
554 long neg_depth_mod)
555 {
556 long i;
557
558 handle->features = features;
559 handle->use_litcount = use_litcount;
560 handle->ass_vec_len = ass_vec_len;
561 handle->res_vec_len = res_vec_len;
562 handle->assembly_vector = SizeMalloc(sizeof(long)*ass_vec_len);
563 for(i=0; i< ass_vec_len; i++)
564 {
565 handle->assembly_vector[i] = -1;
566 }
567 handle->pos_count_base = pos_count_base;
568 handle->pos_count_offset = pos_count_offset;
569 handle->pos_count_mod = pos_count_mod;
570 handle->neg_count_base = neg_count_base;
571 handle->neg_count_offset = neg_count_offset;
572 handle->neg_count_mod = neg_count_mod;
573 handle->pos_depth_base = pos_depth_base;
574 handle->pos_depth_offset = pos_depth_offset;
575 handle->pos_depth_mod = pos_depth_mod;
576 handle->neg_depth_base = neg_depth_base;
577 handle->neg_depth_offset = neg_depth_offset;
578 handle->neg_depth_mod = neg_depth_mod;
579
580 handle->max_symbols = FVINDEX_MAX_FEATURES_DEFAULT;
581 }
582
583
584 /*-----------------------------------------------------------------------
585 //
586 // Function: FVCollectAlloc()
587 //
588 // Allocate an initialized FVCollectCell.
589 //
590 // Global Variables: -
591 //
592 // Side Effects : Memory operations
593 //
594 /----------------------------------------------------------------------*/
595
FVCollectAlloc(FVIndexType features,bool use_litcount,long ass_vec_len,long res_vec_len,long pos_count_base,long pos_count_offset,long pos_count_mod,long neg_count_base,long neg_count_offset,long neg_count_mod,long pos_depth_base,long pos_depth_offset,long pos_depth_mod,long neg_depth_base,long neg_depth_offset,long neg_depth_mod)596 FVCollect_p FVCollectAlloc(FVIndexType features,
597 bool use_litcount,
598 long ass_vec_len,
599 long res_vec_len,
600 long pos_count_base,
601 long pos_count_offset,
602 long pos_count_mod,
603 long neg_count_base,
604 long neg_count_offset,
605 long neg_count_mod,
606 long pos_depth_base,
607 long pos_depth_offset,
608 long pos_depth_mod,
609 long neg_depth_base,
610 long neg_depth_offset,
611 long neg_depth_mod)
612 {
613 FVCollect_p handle = FVCollectCellAlloc();
614
615 FVCollectInit(handle,
616 features,
617 use_litcount,
618 ass_vec_len,
619 res_vec_len,
620 pos_count_base,
621 pos_count_offset,
622 pos_count_mod,
623 neg_count_base,
624 neg_count_offset,
625 neg_count_mod,
626 pos_depth_base,
627 pos_depth_offset,
628 pos_depth_mod,
629 neg_depth_base,
630 neg_depth_offset,
631 neg_depth_mod);
632 return handle;
633 }
634
635
636 /*-----------------------------------------------------------------------
637 //
638 // Function: FVCollectFree()
639 //
640 // Free a FVCollectCell.
641 //
642 // Global Variables: -
643 //
644 // Side Effects : Memory operations
645 //
646 /----------------------------------------------------------------------*/
647
FVCollectFree(FVCollect_p junk)648 void FVCollectFree(FVCollect_p junk)
649 {
650 SizeFree(junk->assembly_vector,sizeof(long)*junk->ass_vec_len);
651 FVCollectCellFree(junk);
652 }
653
654
655
656 /*-----------------------------------------------------------------------
657 //
658 // Function: FVCollectFreqVectorCompute()
659 //
660 // Compute a Feature Vector for the clause based on cspec.
661 //
662 // Global Variables:
663 //
664 // Side Effects :
665 //
666 /----------------------------------------------------------------------*/
667
FVCollectFreqVectorCompute(Clause_p clause,FVCollect_p cspec)668 FreqVector_p FVCollectFreqVectorCompute(Clause_p clause, FVCollect_p cspec)
669 {
670 static size_t full_vec_len = 0;
671 static long* full_vec = NULL;
672
673 FreqVector_p vec = FreqVectorAlloc(cspec->res_vec_len);
674
675 vec->clause = clause;
676 FreqVectorInitialize(vec, 0);
677
678 if(!ClauseIsEmpty(clause))
679 {
680 PStack_p mod_stack = PStackAlloc();
681 long max_fun = clause->literals->bank->sig->f_count;
682 long findex;
683
684 if(cspec->use_litcount)
685 {
686 vec->array[0] = clause->pos_lit_no;
687 vec->array[1] = clause->neg_lit_no;
688 }
689 full_vec = RegMemProvide(full_vec, &full_vec_len, sizeof(long)*(max_fun+1)*4);
690
691 ClauseAddSymbolFeatures(clause, mod_stack, full_vec);
692
693 while(!PStackEmpty(mod_stack))
694 {
695 findex = PStackPopInt(mod_stack);
696 gather_feature_vec(cspec, full_vec, vec, findex);
697 full_vec[findex] = 0;
698 gather_feature_vec(cspec, full_vec, vec, findex+1);
699 full_vec[findex+1] = 0;
700 }
701
702 PStackFree(mod_stack);
703 }
704 return vec;
705 }
706
707
708
709 /*-----------------------------------------------------------------------
710 //
711 // Function: BillFeaturesCollectAlloc()
712 //
713 // Generate a CollectSpec as follows
714 // - positive literals
715 // - negative literals
716 // foreach relation symbol
717 // positive occurrences
718 // negative occurrences
719 // foreach function symbol
720 // positive occurrences
721 // negative occurrences
722 // positive maxdepth
723 // negative maxdepth
724 //
725 // Global Variables: -
726 //
727 // Side Effects : Memory operations
728 //
729 /----------------------------------------------------------------------*/
730
BillFeaturesCollectAlloc(Sig_p sig,long len)731 FVCollect_p BillFeaturesCollectAlloc(Sig_p sig, long len)
732 {
733 long p_no = SigCountSymbols(sig, true);
734 long f_no = SigCountSymbols(sig, false);
735 FunCode i, pos;
736 FVCollect_p cspec;
737
738 assert(len>2);
739
740 while((2+2*p_no+4*f_no) > len)
741 {
742 if(p_no > f_no)
743 {
744 p_no--;
745 }
746 else
747 {
748 f_no--;
749 }
750 }
751
752 cspec = FVCollectAlloc(FVICollectFeatures,
753 true,
754 (sig->f_count+1)*4+2,
755 len,
756 0, 0, 0,
757 0, 0, 0,
758 0, 0, 0,
759 0, 0, 0);
760 pos = 2;
761 for(i=sig->internal_symbols+1; p_no; i++)
762 {
763 /* printf("p = %ld (%s)\n", i, SigFindName(sig,i)); */
764 if(!SigIsSpecial(sig, i) && SigIsPredicate(sig, i))
765 {
766 cspec->assembly_vector[4*i] = pos;
767 pos++;
768 cspec->assembly_vector[4*i+1] = pos;
769 pos++;
770 p_no--;
771 }
772 }
773
774 for(i=sig->internal_symbols+1; f_no; i++)
775 {
776 /* printf("f = %ld (%s)\n", i, SigFindName(sig,i)); */
777 if(!SigIsSpecial(sig, i) && SigIsFunction(sig,i))
778 {
779 cspec->assembly_vector[4*i] = pos;
780 pos++;
781 cspec->assembly_vector[4*i+1] = pos;
782 pos++;
783 cspec->assembly_vector[4*i+2] = pos;
784 pos++;
785 cspec->assembly_vector[4*i+3] = pos;
786 pos++;
787 f_no--;
788 }
789 }
790 return cspec;
791 }
792
793 /*-----------------------------------------------------------------------
794 //
795 // Function: BillPlusFeaturesCollectAlloc()
796 //
797 // Generate a CollectSpec as follows
798 // - positive literals
799 // - negative literals
800 // foreach relation symbol
801 // positive occurrences
802 // negative occurrences
803 // foreach function symbol
804 // positive occurrences
805 // negative occurrences
806 // positive maxdepth
807 // negative maxdepth
808 // All overflow counts
809 // All overflow depths
810 //
811 // Global Variables: -
812 //
813 // Side Effects : Memory operations
814 //
815 /----------------------------------------------------------------------*/
816
BillPlusFeaturesCollectAlloc(Sig_p sig,long len)817 FVCollect_p BillPlusFeaturesCollectAlloc(Sig_p sig, long len)
818 {
819 long p_no = SigCountSymbols(sig, true);
820 long f_no = SigCountSymbols(sig, false);
821 FunCode i, pos;
822 FVCollect_p cspec;
823
824 assert(len>2);
825
826 while((6+2*p_no+4*f_no) > len)
827 {
828 if(p_no > f_no)
829 {
830 p_no--;
831 }
832 else
833 {
834 f_no--;
835 }
836 }
837
838 cspec = FVCollectAlloc(FVICollectFeatures,
839 true,
840 (sig->f_count+1)*4+2,
841 len,
842 len-4, 0, 1,
843 len-3, 0, 1,
844 len-2, 0, 1,
845 len-1, 0, 1);
846 pos = 2;
847 for(i=sig->internal_symbols+1; p_no; i++)
848 {
849 /* printf("p = %ld (%s)\n", i, SigFindName(sig,i)); */
850 if(!SigIsSpecial(sig, i) && SigIsPredicate(sig, i))
851 {
852 cspec->assembly_vector[4*i] = pos;
853 pos++;
854 cspec->assembly_vector[4*i+1] = pos;
855 pos++;
856 p_no--;
857 }
858 }
859
860 for(i=sig->internal_symbols+1; f_no; i++)
861 {
862 /* printf("f = %ld (%s)\n", i, SigFindName(sig,i)); */
863 if(!SigIsSpecial(sig, i) && SigIsFunction(sig,i))
864 {
865 cspec->assembly_vector[4*i] = pos;
866 pos++;
867 cspec->assembly_vector[4*i+1] = pos;
868 pos++;
869 cspec->assembly_vector[4*i+2] = pos;
870 pos++;
871 cspec->assembly_vector[4*i+3] = pos;
872 pos++;
873 f_no--;
874 }
875 }
876 return cspec;
877 }
878
879
880
881 /*-----------------------------------------------------------------------
882 //
883 // Function: FVPackClause()
884 //
885 // If index is an index, compute and return a StandardFreqVector for
886 // clause, otherwise pack clause into a dummy frequency vector cell
887 // and return than.
888 //
889 // Global Variables: -
890 //
891 // Side Effects : Memory operations
892 //
893 /----------------------------------------------------------------------*/
894
FVPackClause(Clause_p clause,PermVector_p perm,FVCollect_p cspec)895 FVPackedClause_p FVPackClause(Clause_p clause, PermVector_p perm,
896 FVCollect_p cspec)
897 {
898 FVPackedClause_p res;
899
900 if(cspec && (cspec->features != FVINoFeatures))
901 {
902 return OptimizedVarFreqVectorCompute(clause, perm, cspec);
903 }
904 res = FreqVectorCellAlloc();
905 res->array = NULL;
906 res->clause = clause;
907
908 return res;
909 }
910
911
912 /*-----------------------------------------------------------------------
913 //
914 // Function: FVUnpackClause()
915 //
916 // Unpack a packed clause, i.e. return the clause and throw away the
917 // container.
918 //
919 // Global Variables: -
920 //
921 // Side Effects : Memory operations
922 //
923 /----------------------------------------------------------------------*/
924
FVUnpackClause(FVPackedClause_p pack)925 Clause_p FVUnpackClause(FVPackedClause_p pack)
926 {
927 Clause_p res = pack->clause;
928
929 #ifndef NDEBUG
930 pack->clause = NULL;
931 #endif
932 FreqVectorFree(pack);
933
934 return res;
935 }
936
937
938 /*-----------------------------------------------------------------------
939 //
940 // Function: FVPackedClauseFreeReal()
941 //
942 // Fully free a packed clause.
943 //
944 // Global Variables:
945 //
946 // Side Effects :
947 //
948 /----------------------------------------------------------------------*/
949
FVPackedClauseFreeReal(FVPackedClause_p pack)950 void FVPackedClauseFreeReal(FVPackedClause_p pack)
951 {
952 if(pack->clause)
953 {
954 ClauseFree(pack->clause);
955 }
956 FreqVectorFree(pack);
957 }
958
959
960 /*-----------------------------------------------------------------------
961 //
962 // Function: FreqVectorAdd()
963 //
964 // Component-wise addition of both sources. Guaranteed to work if
965 // dest is a source (but not maximally efficient - who cares). Yes,
966 // it's worth mentioning it ;-)
967 //
968 // Global Variables: -
969 //
970 // Side Effects : -
971 //
972 /----------------------------------------------------------------------*/
973
FreqVectorAdd(FreqVector_p dest,FreqVector_p s1,FreqVector_p s2)974 void FreqVectorAdd(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2)
975 {
976 long i;
977
978 assert(s1 && s2 && dest);
979 assert(s1->size == dest->size);
980 assert(s2->size == dest->size);
981
982 for(i=0; i<dest->size; i++)
983 {
984 dest->array[i] = s1->array[i]+s2->array[i];
985 }
986 }
987
988
989 /*-----------------------------------------------------------------------
990 //
991 // Function: FreqVectorMulAdd()
992 //
993 // Component-wise addition of both weighted sources. Guaranteed to
994 // work if dest is a source (but not maximally efficient - who
995 // cares). Yes, it's worth mentioning it ;-)
996 //
997 // Global Variables: -
998 //
999 // Side Effects : -
1000 //
1001 /----------------------------------------------------------------------*/
1002
FreqVectorMulAdd(FreqVector_p dest,FreqVector_p s1,long f1,FreqVector_p s2,long f2)1003 void FreqVectorMulAdd(FreqVector_p dest, FreqVector_p s1, long f1,
1004 FreqVector_p s2, long f2)
1005 {
1006 long i;
1007
1008 assert(s1 && s2 && dest);
1009 assert(s1->size == dest->size);
1010 assert(s2->size == dest->size);
1011
1012 for(i=0; i<dest->size; i++)
1013 {
1014 dest->array[i] = f1*s1->array[i]+f2*s2->array[i];
1015 }
1016 }
1017
1018
1019 /*-----------------------------------------------------------------------
1020 //
1021 // Function: FreqVectorMax()
1022 //
1023 // Compute componentwise max of vectors. See above.
1024 //
1025 // Global Variables: -
1026 //
1027 // Side Effects : -
1028 //
1029 /----------------------------------------------------------------------*/
1030
FreqVectorMax(FreqVector_p dest,FreqVector_p s1,FreqVector_p s2)1031 void FreqVectorMax(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2)
1032 {
1033 long i;
1034
1035 assert(s1 && s2 && dest);
1036 assert(s1->size == dest->size);
1037 assert(s2->size == dest->size);
1038
1039 for(i=0; i<dest->size; i++)
1040 {
1041 dest->array[i] = MAX(s1->array[i],s2->array[i]);
1042 }
1043 }
1044
1045
1046 /*-----------------------------------------------------------------------
1047 //
1048 // Function: FreqVectorMin()
1049 //
1050 // Compute componentwise min of vectors. See above.
1051 //
1052 // Global Variables: -
1053 //
1054 // Side Effects : -
1055 //
1056 /----------------------------------------------------------------------*/
1057
FreqVectorMin(FreqVector_p dest,FreqVector_p s1,FreqVector_p s2)1058 void FreqVectorMin(FreqVector_p dest, FreqVector_p s1, FreqVector_p s2)
1059 {
1060 long i;
1061
1062 assert(s1 && s2 && dest);
1063 assert(s1->size == dest->size);
1064 assert(s2->size == dest->size);
1065
1066 for(i=0; i<dest->size; i++)
1067 {
1068 dest->array[i] = MIN(s1->array[i],s2->array[i]);
1069 }
1070 }
1071
1072
1073 /*---------------------------------------------------------------------*/
1074 /* End of File */
1075 /*---------------------------------------------------------------------*/
1076
1077
1078