Source

z3 / src / muz_qe / dl_relation_manager.h

Full commit
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
/*++
Copyright (c) 2006 Microsoft Corporation

Module Name:

    dl_remation_manager.h

Abstract:

    <abstract>

Author:

    Krystof Hoder (t-khoder) 2010-09-24.

Revision History:

--*/
#ifndef _DL_RELATION_MANAGER_H_
#define _DL_RELATION_MANAGER_H_


#include"map.h"
#include"vector.h"

#include"dl_base.h"

namespace datalog {

    class context;
    class dl_decl_util;
    class table_relation;
    class table_relation_plugin;
    class finite_product_relation;
    class finite_product_relation_plugin;
    class sieve_relation;
    class sieve_relation_plugin;

    typedef hashtable<func_decl * , ptr_hash<func_decl>, ptr_eq<func_decl> > decl_set;

    class relation_manager {
        class empty_signature_relation_join_fn;
        class default_relation_join_project_fn;
        class default_relation_select_equal_and_project_fn;
        class default_relation_intersection_filter_fn;

        class auxiliary_table_transformer_fn;
        class auxiliary_table_filter_fn;

        class default_table_join_fn;
        class default_table_project_fn;
        class null_signature_table_project_fn;
        class default_table_join_project_fn;
        class default_table_rename_fn;
        class default_table_union_fn;
        class default_table_filter_equal_fn;
        class default_table_filter_identical_fn;
        class default_table_filter_interpreted_fn;
        class default_table_negation_filter_fn;
        class default_table_filter_not_equal_fn;
        class default_table_select_equal_and_project_fn;
        class default_table_map_fn;
        class default_table_project_with_reduce_fn;

        typedef obj_map<func_decl, family_id> decl2kind_map;

        typedef u_map<relation_plugin *> kind2plugin_map;

        typedef map<const table_plugin *, table_relation_plugin *, ptr_hash<const table_plugin>, 
            ptr_eq<const table_plugin> > tp2trp_map;
        typedef map<const relation_plugin *, finite_product_relation_plugin *, ptr_hash<const relation_plugin>, 
            ptr_eq<const relation_plugin> > rp2fprp_map;

        typedef map<func_decl *, relation_base *, ptr_hash<func_decl>, ptr_eq<func_decl> > relation_map;
        typedef ptr_vector<table_plugin> table_plugin_vector;
        typedef ptr_vector<relation_plugin> relation_plugin_vector;

        context & m_context;
        table_plugin_vector m_table_plugins;
        relation_plugin_vector m_relation_plugins;
        //table_relation_plugins corresponding to table_plugins
        tp2trp_map m_table_relation_plugins;
        rp2fprp_map m_finite_product_relation_plugins;

        kind2plugin_map m_kind2plugin;

        table_plugin * m_favourite_table_plugin;

        relation_plugin * m_favourite_relation_plugin;

        relation_map m_relations;

        decl_set m_saturated_rels;

        family_id m_next_table_fid;
        family_id m_next_relation_fid;

        /**
           Map specifying what kind of relation should be used to represent particular predicate.
        */
        decl2kind_map m_pred_kinds;

        void register_relation_plugin_impl(relation_plugin * plugin);

        relation_manager(const relation_manager &); //private and undefined copy constructor
        relation_manager & operator=(const relation_manager &); //private and undefined operator=
    public:
        relation_manager(context & ctx) : 
          m_context(ctx), 
          m_favourite_table_plugin(0),
          m_favourite_relation_plugin(0),
          m_next_table_fid(0),
          m_next_relation_fid(0) {}

        virtual ~relation_manager();

        void reset();
        void reset_relations();

        context & get_context() const { return m_context; }
        dl_decl_util & get_decl_util() const;

        family_id get_next_table_fid() { return m_next_table_fid++; }
        family_id get_next_relation_fid(relation_plugin & claimer);


        /**
           Set what kind of relation is going to be used to represent the predicate \c pred.

           This function can be called only before the relation object for \c pred is created
           (i.e. before the \c get_relation function is called with \c pred as argument for the
           first time).
        */
        void set_predicate_kind(func_decl * pred, family_id kind);
        /**
           Return the relation kind that was requested to represent the predicate \c pred by 
           \c set_predicate_kind. If there was no such request, return \c null_family_id.
        */
        family_id get_requested_predicate_kind(func_decl * pred);
        relation_base & get_relation(func_decl * pred);
        relation_base * try_get_relation(func_decl * pred) const;
        /**
           \brief Store the relation \c rel under the predicate \c pred. The \c relation_manager
           takes over the relation object.
        */
        void store_relation(func_decl * pred, relation_base * rel);

        bool is_saturated(func_decl * pred) const { return m_saturated_rels.contains(pred); }
        void mark_saturated(func_decl * pred) { m_saturated_rels.insert(pred); }
        void reset_saturated_marks() { 
            if(!m_saturated_rels.empty()) {
                m_saturated_rels.reset();
            }
        }

        void collect_predicates(decl_set & res) const;
        void collect_non_empty_predicates(decl_set & res) const;
        void restrict_predicates(const decl_set & preds);

        void register_plugin(table_plugin * plugin);
        /**
           table_relation_plugins should not be passed to this function since they are
           created automatically when registering a table plugin.
        */
        void register_plugin(relation_plugin * plugin) {
            SASSERT(!plugin->from_table());
            register_relation_plugin_impl(plugin);
        }

        table_plugin & get_appropriate_plugin(const table_signature & t);
        relation_plugin & get_appropriate_plugin(const relation_signature & t);
        table_plugin * try_get_appropriate_plugin(const table_signature & t);
        relation_plugin * try_get_appropriate_plugin(const relation_signature & t);

        table_plugin * get_table_plugin(symbol const& s);
        relation_plugin * get_relation_plugin(symbol const& s);
        relation_plugin & get_relation_plugin(family_id kind);
        table_relation_plugin & get_table_relation_plugin(table_plugin & tp);
        bool try_get_finite_product_relation_plugin(const relation_plugin & inner, 
            finite_product_relation_plugin * & res);

        table_base * mk_empty_table(const table_signature & s);
        relation_base * mk_implicit_relation(const relation_signature & s, app * expr);

        relation_base * mk_empty_relation(const relation_signature & s, family_id kind);
        relation_base * mk_empty_relation(const relation_signature & s, func_decl* pred);

        relation_base * mk_full_relation(const relation_signature & s, func_decl* pred, family_id kind);
        relation_base * mk_full_relation(const relation_signature & s, func_decl* pred);

        relation_base * mk_table_relation(const relation_signature & s, table_base * table);
        bool mk_empty_table_relation(const relation_signature & s, relation_base * & result);

        bool is_non_explanation(relation_signature const& s) const;


        /**
           \brief Convert relation value to table one.

           This function can be called only for the relation sorts that have a table counterpart.
         */
        void relation_to_table(const relation_sort & sort, const relation_element & from, table_element & to);

        void table_to_relation(const relation_sort & sort, const table_element & from, relation_element & to);
        void table_to_relation(const relation_sort & sort, const table_element & from, 
            const relation_fact::el_proxy & to);
        void table_to_relation(const relation_sort & sort, const table_element & from, 
            relation_element_ref & to);

        bool relation_sort_to_table(const relation_sort & from, table_sort & to);
        void from_predicate(func_decl * pred, unsigned arg_index, relation_sort & result);
        void from_predicate(func_decl * pred, relation_signature & result);

        /**
           \brief Convert relation signature to table signature and return true if successful. If false
           is returned, the value of \c to is undefined.
        */
        bool relation_signature_to_table(const relation_signature & from, table_signature & to);

        void relation_fact_to_table(const relation_signature & s, const relation_fact & from, 
                table_fact & to);
        void table_fact_to_relation(const relation_signature & s, const table_fact & from, 
            relation_fact & to);




        // -----------------------------------
        //
        // relation operations
        //
        // -----------------------------------

        //TODO: If multiple operation implementations are available, we may want to do something to 
        //select the best one here.

        /**
           If \c allow_product_relation is true, we will create a join that builds a product relation, 
           if there is no other way to do the join. If \c allow_product_relation is false, we will return 
           zero in that case.
        */
        relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, bool allow_product_relation=true);

        relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
                const unsigned_vector & cols1, const unsigned_vector & cols2, bool allow_product_relation=true) { 
            SASSERT(cols1.size()==cols2.size());
            return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation);
        }

        /**
            \brief Return functor that transforms a table into one that lacks columns listed in
            \c removed_cols array.

            The \c removed_cols cotains columns of table \c t in strictly ascending order.
            */
        relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 
            const unsigned * removed_cols);

        relation_transformer_fn * mk_project_fn(const relation_base & t, const unsigned_vector & removed_cols) { 
            return mk_project_fn(t, removed_cols.size(), removed_cols.c_ptr()); 
        }

        /**
            \brief Return an operation that is a composition of a join an a project operation.
        */
        relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2,
                unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
                unsigned removed_col_cnt, const unsigned * removed_cols, bool allow_product_relation_join=true);

        relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2,
                const unsigned_vector & cols1, const unsigned_vector & cols2, 
                const unsigned_vector & removed_cols, bool allow_product_relation_join=true) {
            return mk_join_project_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), removed_cols.size(), 
                removed_cols.c_ptr(), allow_product_relation_join);
        }

        relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 
            const unsigned * permutation_cycle);
        relation_transformer_fn * mk_rename_fn(const relation_base & t, const unsigned_vector & permutation_cycle) { 
            return mk_rename_fn(t, permutation_cycle.size(), permutation_cycle.c_ptr());
        }

        /**
           Like \c mk_rename_fn, only the permutation is not specified by cycle, but by a permutated array
           of column number.
        */
        relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
            const unsigned * permutation);
        relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
                const unsigned_vector permutation) {
            SASSERT(t.get_signature().size()==permutation.size());
            return mk_permutation_rename_fn(t, permutation.c_ptr());
        }


        /**
            The post-condition for an ideal union operation is be

            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                delta_1== delta_0 \union ( tgt_1 \setminus tgt_0 )

            A required post-condition is

            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                tgt_1==tgt_0 => delta_1==delta_0
                delta_0 \subset delta_1
                delta_1 \subset (delta_0 \union tgt_1)
                ( tgt_1 \setminus tgt_0 ) \subset delta_1

            So that a sufficient implementation is

            Union(tgt, src, delta) {
                oldTgt:=tgt.clone();
                tgt:=tgt \union src
                if(tgt!=oldTgt) {
                    delta:=delta \union src    //also �delta \union tgt� would work
                }
            }

            If rules are compiled with all_or_nothing_deltas parameter set to true, a sufficient 
            post-condition is
            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                (tgt_1==tgt_0 ||  delta_0 is non-empty) <=> delta_1 is non-empty
            */
        relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 
            const relation_base * delta);

        relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src) { 
            return mk_union_fn(tgt, src, static_cast<relation_base *>(0));
        }

        /**
            Similar to union, but this one should be used inside loops to allow for abstract 
            domain convergence.
        */
        relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src, 
            const relation_base * delta); 

        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
            const unsigned * identical_cols);
        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector identical_cols) {
            return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
        }

        relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, 
            unsigned col);

        relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition);

        /**
            \brief Operations that returns all rows of \c t for which is column \c col equal to \c value
            with the column \c col removed.

            This operation can often be efficiently implemented and is useful for evaluating rules 
            of the form

            F(x):-P("c",x).
            */
        relation_transformer_fn * mk_select_equal_and_project_fn(const relation_base & t, 
                const relation_element & value, unsigned col);


        relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & tgt, 
            const relation_base & src, unsigned joined_col_cnt, 
            const unsigned * tgt_cols, const unsigned * src_cols);
        relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & tgt, 
                const relation_base & src, const unsigned_vector & tgt_cols, const unsigned_vector & src_cols) { 
            SASSERT(tgt_cols.size()==src_cols.size());
            return mk_filter_by_intersection_fn(tgt, src, tgt_cols.size(), tgt_cols.c_ptr(), src_cols.c_ptr());
        }
        relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & tgt, 
                const relation_base & src);

        /**
            The filter_by_negation postcondition:
            filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, 
                                            corresponding columns in neg: d1,...,dN):
            tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
            */
        relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, 
            const relation_base & negated_obj, unsigned joined_col_cnt, 
            const unsigned * t_cols, const unsigned * negated_cols);
        relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, 
                const relation_base & negated_obj, const unsigned_vector & t_cols, 
                const unsigned_vector & negated_cols) {
            SASSERT(t_cols.size()==negated_cols.size());
            return mk_filter_by_negation_fn(t, negated_obj, t_cols.size(), t_cols.c_ptr(), negated_cols.c_ptr());
        }


        // -----------------------------------
        //
        // table operations
        //
        // -----------------------------------


        table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2,
            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);

        table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2,
                const unsigned_vector & cols1, const unsigned_vector & cols2) { 
            SASSERT(cols1.size()==cols2.size());
            return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr());
        }

        /**
            \brief Return functor that transforms a table into one that lacks columns listed in
            \c removed_cols array.

            The \c removed_cols cotains columns of table \c t in strictly ascending order.

            If a project operation removes a non-functional column, all functional columns become 
            non-functional (so that none of the values in functional columns are lost)
            */
        table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, 
            const unsigned * removed_cols);

        table_transformer_fn * mk_project_fn(const table_base & t, const unsigned_vector & removed_cols) { 
            return mk_project_fn(t, removed_cols.size(), removed_cols.c_ptr()); 
        }

        /**
            \brief Return an operation that is a composition of a join an a project operation.

            This operation is equivalent to the two operations performed separately, unless functional 
            columns are involved.
               
            The ordinary project would make all of the functional columns into non-functional if any 
            non-functional column was removed. In function, however, we group columns into equivalence 
            classes (according to the equalities in \c cols1 and \c cols2) and make everything non-functional 
            only if some equivalence class of non-functional columns would have no non-functional columns 
            remain after the removal. 
            
            This behavior is implemented in the \c table_signature::from_join_project function.
        */
        table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2,
                unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
                unsigned removed_col_cnt, const unsigned * removed_cols);

        table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2,
                const unsigned_vector & cols1, const unsigned_vector & cols2, 
                const unsigned_vector & removed_cols) {
            return mk_join_project_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), removed_cols.size(), 
                removed_cols.c_ptr());
        }

        table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, 
            const unsigned * permutation_cycle);
        table_transformer_fn * mk_rename_fn(const table_base & t, const unsigned_vector & permutation_cycle) { 
            return mk_rename_fn(t, permutation_cycle.size(), permutation_cycle.c_ptr());
        }

        /**
           Like \c mk_rename_fn, only the permutation is not specified by cycle, but by a permutated array
           of column number.
        */
        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned * permutation);
        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector permutation) {
            SASSERT(t.get_signature().size()==permutation.size());
            return mk_permutation_rename_fn(t, permutation.c_ptr());
        }


        /**
            The post-condition for an ideal union operation is be

            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                delta_1== delta_0 \union ( tgt_1 \setminus tgt_0 )

            A required post-condition is

            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                tgt_1==tgt_0 => delta_1==delta_0
                delta_0 \subset delta_1
                delta_1 \subset (delta_0 \union tgt_1)
                ( tgt_1 \setminus tgt_0 ) \subset delta_1

            So that a sufficient implementation is

            Union(tgt, src, delta) {
                oldTgt:=tgt.clone();
                tgt:=tgt \union src
                if(tgt!=oldTgt) {
                    delta:=delta \union src    //also �delta \union tgt� would work
                }
            }

            If rules are compiled with all_or_nothing_deltas parameter set to true, a sufficient 
            post-condition is
            Union(tgt, src, delta):
                tgt_1==tgt_0 \union src
                (tgt_1==tgt_0 ||  delta_0 is non-empty) <=> delta_1 is non-empty
            */
        table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, 
            const table_base * delta);

        table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src) { 
            return mk_union_fn(tgt, src, static_cast<table_base *>(0));
        }

        /**
            Similar to union, but this one should be used inside loops to allow for abstract 
            domain convergence.
        */
        table_union_fn * mk_widen_fn(const table_base & tgt, const table_base & src, 
            const table_base * delta); 

        table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, 
            const unsigned * identical_cols);
        table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector identical_cols) {
            return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
        }

        table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, 
            unsigned col);

        table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition);

        /**
            \brief Operations that returns all rows of \c t for which is column \c col equal to \c value
            with the column \c col removed.

            This operation can often be efficiently implemented and is useful for evaluating rules 
            of the form

            F(x):-P("c",x).
            */
        table_transformer_fn * mk_select_equal_and_project_fn(const table_base & t, 
                const table_element & value, unsigned col);

        table_intersection_filter_fn * mk_filter_by_intersection_fn(const table_base & t, 
            const table_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols);
        table_intersection_filter_fn * mk_filter_by_intersection_fn(const table_base & t, 
                const table_base & src, const unsigned_vector & t_cols, const unsigned_vector & src_cols) { 
            SASSERT(t_cols.size()==src_cols.size());
            return mk_filter_by_intersection_fn(t, src, t_cols.size(), t_cols.c_ptr(), src_cols.c_ptr());
        }

        /**
            The filter_by_negation postcondition:
            filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, 
                                            corresponding columns in neg: d1,...,dN):
            tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
            */
        table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, const table_base & negated_obj, 
            unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * negated_cols);
        table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, const table_base & negated_obj, 
                const unsigned_vector & t_cols, const unsigned_vector & negated_cols) {
            SASSERT(t_cols.size()==negated_cols.size());
            return mk_filter_by_negation_fn(t, negated_obj, t_cols.size(), t_cols.c_ptr(), negated_cols.c_ptr());
        }

        /**
            \c t must contain at least one functional column.

            Created object takes ownership of the \c mapper object.
        */
        virtual table_mutator_fn * mk_map_fn(const table_base & t, table_row_mutator_fn * mapper);

        /**
            \c t must contain at least one functional column.

            Created object takes ownership of the \c mapper object.
        */
        virtual table_transformer_fn * mk_project_with_reduce_fn(const table_base & t, unsigned col_cnt, 
            const unsigned * removed_cols, table_row_pair_reduce_fn * reducer);




        // -----------------------------------
        //
        // output functions
        //
        // -----------------------------------


        std::string to_nice_string(const relation_element & el) const;
        /**
           This one may give a nicer representation of \c el than the 
           \c to_nice_string(const relation_element & el) function, by unsing the information about the sort
           of the element.
        */
        std::string to_nice_string(const relation_sort & s, const relation_element & el) const;
        std::string to_nice_string(const relation_sort & s) const;
        std::string to_nice_string(const relation_signature & s) const;

        void display(std::ostream & out) const;
        void display_relation_sizes(std::ostream & out) const;
        void display_output_tables(std::ostream & out) const;

    private:
        relation_intersection_filter_fn * try_mk_default_filter_by_intersection_fn(const relation_base & t, 
            const relation_base & src, unsigned joined_col_cnt, 
            const unsigned * t_cols, const unsigned * src_cols);

    };

    /**
       This is a helper class for relation_plugins whose relations can be of various kinds.
    */
    template<class Spec, class Hash=int_vector_hash_proc<Spec>, class Eq=vector_eq_proc<Spec> >
    class rel_spec_store {
        typedef relation_signature::hash r_hash;
        typedef relation_signature::eq r_eq;

        typedef map<Spec, unsigned, Hash, Eq > family_id_idx_store;
        typedef map<relation_signature, family_id_idx_store *, r_hash, r_eq> sig2store;

        typedef u_map<Spec> family_id2spec;
        typedef map<relation_signature, family_id2spec *, r_hash, r_eq> sig2spec_store;

        relation_plugin &  m_parent;
        svector<family_id> m_allocated_kinds;
        sig2store          m_kind_assignment;
        sig2spec_store     m_kind_specs;


        relation_manager & get_manager() { return m_parent.get_manager(); }

        void add_new_kind() {
            add_available_kind(get_manager().get_next_relation_fid(m_parent));
        }

    public:
        rel_spec_store(relation_plugin & parent) : m_parent(parent) {}

        ~rel_spec_store() {
            reset_dealloc_values(m_kind_assignment);
            reset_dealloc_values(m_kind_specs);
        }

        void add_available_kind(family_id k) {
            m_allocated_kinds.push_back(k);
        }

        bool contains_signature(relation_signature const& sig) const {
            return m_kind_assignment.contains(sig);
        }

        family_id get_relation_kind(const relation_signature & sig, const Spec & spec) {
            typename sig2store::entry * e = m_kind_assignment.find_core(sig);
            if(!e) {
                e = m_kind_assignment.insert_if_not_there2(sig, alloc(family_id_idx_store));
                m_kind_specs.insert(sig, alloc(family_id2spec));
            }
            family_id_idx_store & ids = *e->get_data().m_value;
            
            unsigned res_idx;
            if(!ids.find(spec, res_idx)) {
                res_idx = ids.size();
                if(res_idx==m_allocated_kinds.size()) {
                    add_new_kind();
                }
                SASSERT(res_idx<m_allocated_kinds.size());
                ids.insert(spec, res_idx);

                family_id2spec * idspecs;
                VERIFY( m_kind_specs.find(sig, idspecs) );
                idspecs->insert(m_allocated_kinds[res_idx], spec);
            }
            return m_allocated_kinds[res_idx];
        }

        void get_relation_spec(const relation_signature & sig, family_id kind, Spec & spec) {
            family_id2spec * idspecs;
            VERIFY( m_kind_specs.find(sig, idspecs) );
            VERIFY( idspecs->find(kind, spec) );
        }

    };

};

#endif /* _DL_RELATION_MANAGER_H_ */