3 #define compilingParser
4 #include <basic/Dynamic_Array.h>
5 #include <code_gen/code_gen.h>
6 #include <code_gen/spmd.h>
7 #include <omega/library_version.h>
9 #include <omega_calc/yylex.h>
10 #include <omega/hull.h>
11 #include <omega/calc_debug.h>
12 #include <basic/Exit.h>
13 #include <omega/closure.h>
14 #include <omega/reach.h>
15 #include <code_gen/mmap-codegen.h>
16 #include <code_gen/mmap-util.h>
19 #include <sys/resource.h>
24 #define CALC_VERSION_STRING "Omega Calculator v1.2"
26 #define DEBUG_FILE_NAME "./oc.out"
29 Map
<Const_String
,Relation
*> relationMap
((Relation
*)0);
30 static int redundant_conj_level
;
32 #if defined BRAIN_DAMAGED_FREE
34 void *realloc
(void *p
, size_t s
);
37 #if !defined(OMIT_GETRUSAGE)
38 void start_clock
( void );
39 int clock_diff
( void );
40 bool anyTimingDone
= false
;
45 Argument_Tuple currentTuple
= Input_Tuple
;
46 char *currentVar
= NULL
;
48 Relation LexForward
(int n
);
51 reachable_information
*reachable_info
;
57 %token
<INT_VALUE
> INT
58 %token
<STRING_VALUE
> STRING
59 %token OPEN_BRACE CLOSE_BRACE
65 %token OMEGA_DOMAIN RANGE
66 %token DIFFERENCE DIFFERENCE_TO_RELATION
67 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
68 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
69 %token MAXIMIZE_RANGE MINIMIZE_RANGE
70 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
73 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
74 %token UNION INTERSECTION
75 %token VERTICAL_BAR SUCH_THAT
76 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
77 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
78 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
79 %token
<REL_OPERATOR
> REL_OP
80 %token RESTRICT_DOMAIN RESTRICT_RANGE
81 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
82 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
84 %token CARD RANKING COUNT_LEXSMALLER
87 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
89 %nonassoc ASSERT_UNSAT
90 %left UNION OMEGA_P1
'+' '-'
91 %nonassoc SUPERSETOF SUBSETOF
92 %left OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE
93 %left INTERSECTION OMEGA_P3
'*' '@'
97 %left COMPOSE JOIN CARRIED_BY
98 %right NOT APPROX OMEGA_DOMAIN RANGE HULL PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS DIFFERENCE DIFFERENCE_TO_RELATION INVERSE COMPLEMENT FARKAS SAMPLE SYM_SAMPLE MAKE_UPPER_BOUND MAKE_LOWER_BOUND OMEGA_P7
103 %right CARD RANKING COUNT_LEXSMALLER
107 %type
<INT_VALUE
> effort
108 %type
<EXP
> exp simpleExp
109 %type
<EXP_LIST
> expList
110 %type
<VAR_LIST
> varList
111 %type
<ARGUMENT_TUPLE
> argumentList
112 %type
<ASTP
> formula optionalFormula
113 %type
<ASTCP
> constraintChain
114 %type
<TUPLE_DESCRIPTOR
> tupleDeclaration
115 %type
<DECLARATION_SITE
> varDecl varDeclOptBrackets
116 %type
<RELATION
> relation builtRelation context
117 %type
<RELATION
> reachable_of
118 %type
<REL_TUPLE_PAIR
> relPairList
119 %type
<REL_TUPLE_TRIPLE
> relTripList
120 %type
<RELATION_ARRAY_1D
> reachable
121 %type
<STM_INFO_TUPLE
> statementInfoList statementInfoResult
122 %type
<STM_INFO
> statementInfo
123 %type
<STM_INFO
> reads
125 %type
<READ
> partials
126 %type
<PREAD
> partial
127 %type
<MMAP
> partialwrites
128 %type
<PMMAP
> partialwrite
138 Argument_Tuple ARGUMENT_TUPLE
;
139 AST_constraints
*ASTCP
;
140 Declaration_Site
* DECLARATION_SITE
;
142 tupleDescriptor
* TUPLE_DESCRIPTOR
;
143 RelTuplePair
* REL_TUPLE_PAIR
;
144 RelTupleTriple
* REL_TUPLE_TRIPLE
;
145 Dynamic_Array2
<Relation
> * RELATION_ARRAY_2D
;
146 Dynamic_Array1
<Relation
> * RELATION_ARRAY_1D
;
147 Tuple
<String
> *STRING_TUPLE
;
148 String
*STRING_VALUE
;
149 Tuple
<stm_info
> *STM_INFO_TUPLE
;
165 inputSequence
: inputItem
166 | inputSequence
{ assert
( current_Declaration_Site
== globalDecls
);}
173 /* Kill all the local declarations -- ejr */
176 Declaration_Site
*ds1
, *ds2
;
177 for
(ds1
= current_Declaration_Site
; ds1
!= globalDecls
;) {
182 current_Declaration_Site
= globalDecls
;
183 yyerror("skipping to statement end");
185 | SYMBOLIC globVarList
';'
188 | VAR
{ currentVar
= $1; } IS_ASSIGNED relation
';'
191 $4->simplify
(min
(2,redundant_conj_level
),4);
192 Relation
*r
= relationMap
((Const_String
)$1);
194 relationMap
[(Const_String
)$1] = $4;
201 $1->simplify
(redundant_conj_level
,4);
202 $1->print_with_subs
(stdout
);
206 | TIME relation
';' {
208 #if defined(OMIT_GETRUSAGE)
209 printf
("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
217 bool SKIP_FULL_CHECK
= getenv
("OC_TIMING_SKIP_FULL_CHECK");
218 ($2)->and_with_GEQ
();
220 for
(t
=1;t
<=100;t
++) {
224 int copyTime
= clock_diff
();
226 for
(t
=1;t
<=100;t
++) {
231 int simplifyTime
= clock_diff
() -copyTime
;
233 if
(!SKIP_FULL_CHECK
)
236 for
(t
=1;t
<=100;t
++) {
242 int excessiveTime
= clock_diff
() - copyTime
;
243 printf
("Times (in microseconds): \n");
244 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
245 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
247 R.print_with_subs
(stdout
);
249 if
(!SKIP_FULL_CHECK
)
251 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
253 R2.print_with_subs
(stdout
);
256 if
(!anyTimingDone
) {
265 printf
("WARNING: The Omega calculator was compiled with options that force\n");
266 printf
("it to perform additional consistency and error checks\n");
267 printf
("that may slow it down substantially\n");
270 printf
("NOTE: These times relect the time of the current _implementation_\n");
271 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
272 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
273 printf
("request that send your test cases to us to allow us to determine if the \n");
274 printf
("times are appropriate, and if the way you are using the Omega library to \n");
275 printf
("solve your problem is the most effective way.\n");
278 printf
("Also, please be aware that over the past two years, we have focused our \n");
279 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
280 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
281 printf
("was substantially faster on the limited domain it handled.\n");
283 printf
(" Thanks, \n");
284 printf
(" the Omega Team \n");
286 anyTimingDone
= true
;
290 | TIMECLOSURE relation
';' {
292 #if defined(OMIT_GETRUSAGE)
293 printf
("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
299 ($2)->and_with_GEQ
();
301 for
(t
=1;t
<=100;t
++) {
305 int copyTime
= clock_diff
();
307 for
(t
=1;t
<=100;t
++) {
312 int simplifyTime
= clock_diff
() -copyTime
;
315 for
(t
=1;t
<=100;t
++) {
318 Rclosed
= TransitiveClosure
(Rclosed
, 1,Relation
::Null
());
320 int closureTime
= clock_diff
() - copyTime
;
323 for
(t
=1;t
<=100;t
++) {
328 int excessiveTime
= clock_diff
() - copyTime
;
329 printf
("Times (in microseconds): \n");
330 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
331 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
333 R.print_with_subs
(stdout
);
335 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
337 R2.print_with_subs
(stdout
);
338 printf
("%5d us to do the transitive closure, obtaining: \n\t",
340 Rclosed.print_with_subs
(stdout
);
342 if
(!anyTimingDone
) {
351 printf
("WARNING: The Omega calculator was compiled with options that force\n");
352 printf
("it to perform additional consistency and error checks\n");
353 printf
("that may slow it down substantially\n");
356 printf
("NOTE: These times relect the time of the current _implementation_\n");
357 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
358 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
359 printf
("request that send your test cases to us to allow us to determine if the \n");
360 printf
("times are appropriate, and if the way you are using the Omega library to \n");
361 printf
("solve your problem is the most effective way.\n");
364 printf
("Also, please be aware that over the past two years, we have focused our \n");
365 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
366 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
367 printf
("was substantially faster on the limited domain it handled.\n");
369 printf
(" Thanks, \n");
370 printf
(" the Omega Team \n");
372 anyTimingDone
= true
;
378 | relation SUBSET relation
';' {
380 int c
= Must_Be_Subset
(*$1, *$3);
381 printf
("\n%s\n", c ?
"True" : "False");
385 | CODEGEN effort relPairList context
';'
388 String s
= MMGenerateCode
($3->mappings
, $3->ispaces
,*$4,$2);
391 printf
("%s\n", (const char *) s
);
393 | TCODEGEN effort statementInfoResult context
';'
396 String s
= tcodegen
($2, *($3), *($4));
399 printf
("%s\n", (const char *) s
);
401 /* | TCODEGEN NOT effort statementInfoResult context';'
404 * String s = tcodegen($3, *($4), *($5), false);
407 * printf("%s\n", (const char *) s);
410 | SPMD blockAndProcsAndEffort relTripList
';'
412 Tuple
<Free_Var_Decl
*> lowerBounds
(0), upperBounds
(0), my_procs
(0);
413 Tuple
<spmd_stmt_info
*> names
(0);
416 int nr_statements
= $3->space.size
();
418 for
(int i
= 1; i
<= $3->space
[1].n_out
(); i
++)
420 lowerBounds.append
(new Free_Var_Decl
("lb" + itoS
(i
)));
421 upperBounds.append
(new Free_Var_Decl
("ub" + itoS
(i
)));
422 my_procs.append
(new Free_Var_Decl
("my_proc" + itoS
(i
)));
425 for
(int p
= 1; p
<= nr_statements
; p
++)
426 names.append
(new numbered_stmt_info
(p
-1, Identity
($3->time
[p
].n_out
()),
428 (char *)(const char *)("s"+itoS
(p
-1))));
430 String s
= SPMD_GenerateCode
("", $3->space
, $3->time
, $3->ispaces
,
432 lowerBounds
, upperBounds
, my_procs
,
436 printf
("%s\n", (const char *) s
);
440 Dynamic_Array1
<Relation
> &final
= *$1;
442 int i
,n_nodes
= reachable_info
->node_names.size
();
443 for
(i
= 1; i
<= n_nodes
; i
++) if
(final
[i
].is_upper_bound_satisfiable
()) {
445 fprintf
(stdout
,"Node %s: ",
446 (const char *) (reachable_info
->node_names
[i
]));
447 final
[i
].print_with_subs
(stdout
);
450 fprintf
(stdout
,"No nodes reachable.\n");
452 delete reachable_info
;
454 | CARD relation
';' {
455 evalue
*EP
= count_relation
(*$2);
457 const Variable_ID_Tuple
* globals
= $2->global_decls
();
458 const char **param_names
= new
(const char *)[globals
->size
()];
459 for
(int i
= 0; i
< globals
->size
(); ++i
)
460 param_names
[i
] = (*globals
)[i
+1]->char_name
();
461 print_evalue
(stdout
, EP
, (char**)param_names
);
463 delete
[] param_names
;
464 free_evalue_refs
(EP
);
469 | RANKING relation
';' {
470 evalue
*EP
= rank_relation
(*$2);
472 const Variable_ID_Tuple
* globals
= $2->global_decls
();
473 int nvar
= $2->n_set
();
474 int n
= nvar
+ globals
->size
();
475 const char **names
= new
(const char *)[n
];
477 for
(int i
= 0; i
< nvar
; ++i
)
478 names
[i
] = $2->set_var
(i
+1)->char_name
();
479 for
(int i
= 0; i
< globals
->size
(); ++i
)
480 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
481 print_evalue
(stdout
, EP
, (char**)names
);
484 free_evalue_refs
(EP
);
489 | COUNT_LEXSMALLER relation WITHIN relation
';' {
490 evalue
*EP
= count_lexsmaller
(*$2, *$4);
492 const Variable_ID_Tuple
* globals
= $4->global_decls
();
493 int nvar
= $4->n_set
();
494 int n
= nvar
+ globals
->size
();
495 const char **names
= new
(const char *)[n
];
497 for
(int i
= 0; i
< nvar
; ++i
)
498 names
[i
] = $4->set_var
(i
+1)->char_name
();
499 for
(int i
= 0; i
< globals
->size
(); ++i
)
500 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
501 print_evalue
(stdout
, EP
, (char**)names
);
504 free_evalue_refs
(EP
);
510 | VERTICES relation
';' {
516 relTripList: relTripList
',' relation
':' relation
':' relation
518 $1->space.append
(*$3);
519 $1->time.append
(*$5);
520 $1->ispaces.append
(*$7);
526 | relation
':' relation
':' relation
528 RelTupleTriple
*rtt
= new RelTupleTriple
;
529 rtt
->space.append
(*$1);
530 rtt
->time.append
(*$3);
531 rtt
->ispaces.append
(*$5);
539 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
540 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
541 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
542 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
547 |
'-' INT
{ $$
= -$2; }
550 context
: { $$
= new Relation
();
551 *$$
= Relation
::Null
(); }
552 | GIVEN relation
{$$
= $2; }
555 relPairList: relPairList
',' relation
':' relation
557 $1->mappings.append
(*$3);
558 $1->mappings
[$1->mappings.size
()].compress
();
559 $1->ispaces.append
(*$5);
560 $1->ispaces
[$1->ispaces.size
()].compress
();
565 | relPairList
',' relation
567 $1->mappings.append
(Identity
($3->n_set
()));
568 $1->mappings
[$1->mappings.size
()].compress
();
569 $1->ispaces.append
(*$3);
570 $1->ispaces
[$1->ispaces.size
()].compress
();
574 | relation
':' relation
576 RelTuplePair
*rtp
= new RelTuplePair
;
577 rtp
->mappings.append
(*$1);
578 rtp
->mappings
[rtp
->mappings.size
()].compress
();
579 rtp
->ispaces.append
(*$3);
580 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
587 RelTuplePair
*rtp
= new RelTuplePair
;
588 rtp
->mappings.append
(Identity
($1->n_set
()));
589 rtp
->mappings
[rtp
->mappings.size
()].compress
();
590 rtp
->ispaces.append
(*$1);
591 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
597 statementInfoResult
: statementInfoList
599 /* | ASSERT_UNSAT statementInfoResult
601 * DoDebug2("Debug info requested in input", *($2));
604 | TRANS_IS relation statementInfoResult
605 { $$
= &Trans_IS
(*($3), *($2));
608 | SET_MMAP INT partialwrites statementInfoResult
609 { $$
= &Set_MMap
(*($4), $2, *($3));
612 | UNROLL_IS INT INT INT statementInfoResult
613 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
614 | PEEL_IS INT INT relation statementInfoResult
615 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
618 | PEEL_IS INT INT relation
',' relation statementInfoResult
619 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
625 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
628 | statementInfoList
',' statementInfo
{ $$
= $1;
633 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
635 $$
->stm
= *($2); delete
$2;
636 $$
->IS
= *($4); delete
$4;
637 $$
->map
= *($6); delete
$6;
639 |
'[' STRING
',' relation
',' partialwrites
']'
641 $$
->stm
= *($2); delete
$2;
642 $$
->IS
= *($4); delete
$4;
643 $$
->map
= *($6); delete
$6;
647 partialwrites
: partialwrites
',' partialwrite
649 $$
->partials.append
(*($3)); delete
$3;
651 | partialwrite
{ $$
= new MMap
;
652 $$
->partials.append
(*($1)); delete
$1;
656 partialwrite
: STRING
'[' relation
']' ',' relation
657 { $$
= new PartialMMap
;
658 $$
->mapping
= *($6); delete
$6;
659 $$
->bounds
= *($3); delete
$3;
660 $$
->var
= *($1); delete
$1;
662 | STRING
',' relation
{ $$
= new PartialMMap
;
663 $$
->mapping
= *($3); delete
$3;
664 $$
->bounds
= Relation
::True
(0);
665 $$
->var
= *($1); delete
$1;
669 reads
: reads
',' oneread
{ $$
= $1;
670 $$
->read.append
(*($3)); delete
$3;
672 | oneread
{ $$
= new stm_info
;
673 $$
->read.append
(*($1)); delete
$1;
677 oneread
: '[' partials
']' { $$
= $2; }
680 partials
: partials
',' partial
{ $$
= $1;
681 $$
->partials.append
(*($3)); delete
$3;
683 | partial
{ $$
= new Read
;
684 $$
->partials.append
(*($1)); delete
$1;
688 partial
: INT
',' relation
{ $$
= new PartialRead
;
690 $$
->dataFlow
= *($3); delete
$3;
694 globVarList: globVarList
',' globVar
698 globVar: VAR
'(' INT
')'
699 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
701 { globalDecls
->extend
($1); free
($1); }
704 relation
: OPEN_BRACE
705 { relationDecl
= new Declaration_Site
(); }
709 if
(omega_calc_debug
) {
710 fprintf
(DebugFile
,"Built relation:\n");
711 $$
->prefix_print
(DebugFile
);
713 current_Declaration_Site
= globalDecls
;
718 if
(relationMap
(s
) == 0) {
719 fprintf
(stderr
,"Variable %s not declared\n",$1);
725 $$
= new Relation
(*relationMap
(s
));
727 |
'(' relation
')' {$$
= $2;}
728 | relation
'+' %prec OMEGA_P9
729 { $$
= new Relation
();
730 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
733 | relation
'*' %prec OMEGA_P9
734 { $$
= new Relation
();
735 int vars
= $1->n_inp
();
736 *$$
= Union
(Identity
(vars
),
737 TransitiveClosure
(*$1, 1,Relation
::Null
()));
740 | relation
'+' WITHIN relation %prec OMEGA_P9
741 {$$
= new Relation
();
742 *$$
= TransitiveClosure
(*$1, 1,*$4);
746 | MINIMIZE_RANGE relation %prec OMEGA_P8
750 r
= Join
(r
,LexForward
($2->n_out
()));
752 *$$
= Difference
(o
,r
);
755 | MAXIMIZE_RANGE relation %prec OMEGA_P8
759 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
761 *$$
= Difference
(o
,r
);
764 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
768 r
= Join
(LexForward
($2->n_inp
()),r
);
770 *$$
= Difference
(o
,r
);
773 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
777 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
779 *$$
= Difference
(o
,r
);
782 | MAXIMIZE relation %prec OMEGA_P8
787 *$$
= Cross_Product
(Relation
(*$2),c
);
789 assert
($$
->n_inp
() ==$$
->n_out
());
790 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
792 | MINIMIZE relation %prec OMEGA_P8
797 *$$
= Cross_Product
(Relation
(*$2),c
);
799 assert
($$
->n_inp
() ==$$
->n_out
());
800 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
802 | FARKAS relation %prec OMEGA_P8
805 *$$
= Farkas
(*$2, Basic_Farkas
);
808 | DECOUPLED_FARKAS relation %prec OMEGA_P8
811 *$$
= Farkas
(*$2, Decoupled_Farkas
);
814 | relation
'@' %prec OMEGA_P9
815 { $$
= new Relation
();
816 *$$
= ConicClosure
(*$1);
819 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
820 { $$
= new Relation
();
821 *$$
= Project_Sym
(*$2);
824 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
825 { $$
= new Relation
();
826 *$$
= Project_On_Sym
(*$2);
829 | DIFFERENCE relation %prec OMEGA_P8
830 { $$
= new Relation
();
834 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
835 { $$
= new Relation
();
836 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
839 | OMEGA_DOMAIN relation %prec OMEGA_P8
840 { $$
= new Relation
();
844 | VENN relation %prec OMEGA_P8
845 { $$
= new Relation
();
846 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
849 | VENN relation GIVEN relation %prec OMEGA_P8
850 { $$
= new Relation
();
851 *$$
= VennDiagramForm
(*$2,*$4);
855 | CONVEX_HULL relation %prec OMEGA_P8
856 { $$
= new Relation
();
857 *$$
= ConvexHull
(*$2);
860 | POSITIVE_COMBINATION relation %prec OMEGA_P8
861 { $$
= new Relation
();
862 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
865 | CONVEX_COMBINATION relation %prec OMEGA_P8
866 { $$
= new Relation
();
867 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
870 | PAIRWISE_CHECK relation %prec OMEGA_P8
871 { $$
= new Relation
();
872 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
875 | CONVEX_CHECK relation %prec OMEGA_P8
876 { $$
= new Relation
();
877 *$$
= CheckForConvexRepresentation
(*$2);
880 | AFFINE_HULL relation %prec OMEGA_P8
881 { $$
= new Relation
();
882 *$$
= AffineHull
(*$2);
885 | CONIC_HULL relation %prec OMEGA_P8
886 { $$
= new Relation
();
887 *$$
= ConicHull
(*$2);
890 | LINEAR_HULL relation %prec OMEGA_P8
891 { $$
= new Relation
();
892 *$$
= LinearHull
(*$2);
895 | HULL relation %prec OMEGA_P8
896 { $$
= new Relation
();
897 *$$
= Hull
(*$2,false
,1,Null_Relation
());
900 | HULL relation GIVEN relation %prec OMEGA_P8
901 { $$
= new Relation
();
902 *$$
= Hull
(*$2,false
,1,*$4);
906 | APPROX relation %prec OMEGA_P8
907 { $$
= new Relation
();
908 *$$
= Approximate
(*$2);
911 | RANGE relation %prec OMEGA_P8
912 { $$
= new Relation
();
916 | INVERSE relation %prec OMEGA_P8
917 { $$
= new Relation
();
921 | COMPLEMENT relation %prec OMEGA_P8
922 { $$
= new Relation
();
923 *$$
= Complement
(*$2);
926 | GIST relation GIVEN relation %prec OMEGA_P8
927 { $$
= new Relation
();
928 *$$
= Gist
(*$2,*$4,1);
932 | relation
'(' relation
')'
933 { $$
= new Relation
();
934 *$$
= Composition
(*$1,*$3);
938 | relation COMPOSE relation
939 { $$
= new Relation
();
940 *$$
= Composition
(*$1,*$3);
944 | relation CARRIED_BY INT
945 { $$
= new Relation
();
946 *$$
= After
(*$1,$3,$3);
948 (*$$
).prefix_print
(stdout
);
950 | relation JOIN relation
951 { $$
= new Relation
();
952 *$$
= Composition
(*$3,*$1);
956 | relation RESTRICT_RANGE relation
957 { $$
= new Relation
();
958 *$$
= Restrict_Range
(*$1,*$3);
962 | relation RESTRICT_DOMAIN relation
963 { $$
= new Relation
();
964 *$$
= Restrict_Domain
(*$1,*$3);
968 | relation INTERSECTION relation
969 { $$
= new Relation
();
970 *$$
= Intersection
(*$1,*$3);
974 | relation
'-' relation %prec INTERSECTION
975 { $$
= new Relation
();
976 *$$
= Difference
(*$1,*$3);
980 | relation UNION relation
981 { $$
= new Relation
();
982 *$$
= Union
(*$1,*$3);
986 | relation
'*' relation
987 { $$
= new Relation
();
988 *$$
= Cross_Product
(*$1,*$3);
992 | SUPERSETOF relation
993 { $$
= new Relation
();
994 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
998 { $$
= new Relation
();
999 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
1002 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
1003 { $$
= new Relation
();
1004 *$$
= Upper_Bound
(*$2);
1007 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
1008 { $$
= new Relation
();
1009 *$$
= Lower_Bound
(*$2);
1013 { $$
= new Relation
();
1014 *$$
= Sample_Solution
(*$2);
1017 | SYM_SAMPLE relation
1018 { $$
= new Relation
();
1019 *$$
= Symbolic_Solution
(*$2);
1022 | reachable_of
{ $$
= $1; }
1023 | ASSERT_UNSAT relation
1025 if
(($2)->is_satisfiable
())
1027 fprintf
(stderr
,"assert_unsatisfiable failed on ");
1028 ($2)->print_with_subs
(stderr
);
1037 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
1038 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
1039 Relation
* r
= new Relation
($1->size
,$4->size
);
1041 F_And
*f
= r
->add_and
();
1043 for
(i
=1;i
<=$1->size
;i
++) {
1044 $1->vars
[i
]->vid
= r
->input_var
(i
);
1045 if
(!$1->vars
[i
]->anonymous
)
1046 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
1048 for
(i
=1;i
<=$4->size
;i
++) {
1049 $4->vars
[i
]->vid
= r
->output_var
(i
);
1050 if
(!$4->vars
[i
]->anonymous
)
1051 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
1053 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1054 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1055 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1056 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
1057 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
1058 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
1059 if
($6) $6->install
(f
);
1064 | tupleDeclaration optionalFormula
{
1065 Relation
* r
= new Relation
($1->size
);
1067 F_And
*f
= r
->add_and
();
1069 for
(i
=1;i
<=$1->size
;i
++) {
1070 $1->vars
[i
]->vid
= r
->set_var
(i
);
1071 if
(!$1->vars
[i
]->anonymous
)
1072 r
->name_set_var
(i
,$1->vars
[i
]->stripped_name
);
1074 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1075 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1076 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1077 if
($2) $2->install
(f
);
1082 Relation
* r
= new Relation
(0,0);
1083 F_And
*f
= r
->add_and
();
1090 optionalFormula
: formula_sep formula
{ $$
= $2; }
1101 if
(currentTupleDescriptor
)
1102 delete currentTupleDescriptor
;
1103 currentTupleDescriptor
= new tupleDescriptor
;
1106 '[' optionalTupleVarList
']'
1107 {$$
= currentTupleDescriptor
; currentTupleDescriptor
= NULL
; }
1110 optionalTupleVarList
:
1112 | optionalTupleVarList
',' tupleVar
1116 tupleVar
: VAR %prec OMEGA_P10
1117 { Declaration_Site
*ds
= defined
($1);
1118 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1120 Variable_Ref
* v
= lookupScalar
($1);
1122 if
(ds
!= globalDecls
)
1123 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1125 currentTupleDescriptor
->extend
(new Exp
(v
));
1131 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1132 | exp %prec OMEGA_P1
1133 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1134 | exp
':' exp %prec OMEGA_P1
1135 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1136 | exp
':' exp
':' INT %prec OMEGA_P1
1137 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1141 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1142 | VAR
{ $$
= new VarList
;
1148 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1149 foreach
(s
,char *, *$1, delete s
);
1154 /* variable declaration with optional brackets */
1156 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1157 |
'[' varDecl
']' { $$
= $2; }
1160 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1161 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1162 | constraintChain
{ $$
= $1; }
1163 |
'(' formula
')' { $$
= $2; }
1164 | NOT formula
{ $$
= new AST_Not
($2); }
1165 | start_exists varDeclOptBrackets exists_sep formula end_quant
1166 { $$
= new AST_exists
($2,$4); }
1167 | start_forall varDeclOptBrackets forall_sep formula end_quant
1168 { $$
= new AST_forall
($2,$4); }
1171 start_exists
: '(' EXISTS
1180 start_forall
: '(' FORALL
1191 expList
: exp
',' expList
1202 constraintChain
: expList REL_OP expList
1203 { $$
= new AST_constraints
($1,$2,$3); }
1204 | expList REL_OP constraintChain
1205 { $$
= new AST_constraints
($1,$2,$3); }
1210 { Variable_Ref
* v
= lookupScalar
($1);
1215 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1217 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1218 else v
= functionOfOutput
[$1];
1220 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1227 |
'(' exp
')' { $$
= $2;}
1233 argumentList
',' VAR
{
1234 Variable_Ref
* v
= lookupScalar
($3);
1237 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1238 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1244 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1247 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1248 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1256 exp
: INT
{$$
= new Exp
($1);}
1257 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1258 | simpleExp
{ $$
= $1; }
1259 |
'-' exp %prec
'*' { $$
= negate
($2);}
1260 | exp
'+' exp
{ $$
= add
($1,$3);}
1261 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1262 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1267 REACHABLE_FROM nodeNameList nodeSpecificationList
1269 Dynamic_Array1
<Relation
> *final
=
1270 Reachable_Nodes
(reachable_info
);
1276 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1278 Dynamic_Array1
<Relation
> *final
=
1279 Reachable_Nodes
(reachable_info
);
1280 int index
= reachable_info
->node_names.index
(String
($2));
1281 assert
(index
!= 0 && "No such node");
1283 *$$
= (*final
)[index
];
1285 delete reachable_info
;
1291 nodeNameList: '(' realNodeNameList
')'
1292 { int sz
= reachable_info
->node_names.size
();
1293 reachable_info
->node_arity.reallocate
(sz
);
1294 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1295 reachable_info
->start_nodes.resize
(sz
+1);
1299 realNodeNameList: realNodeNameList
',' VAR
1300 { reachable_info
->node_names.append
(String
($3));
1302 | VAR
{ reachable_info
= new reachable_information
;
1303 reachable_info
->node_names.append
(String
($1));
1308 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1311 int n_nodes
= reachable_info
->node_names.size
();
1312 Tuple
<int> &arity
= reachable_info
->node_arity
;
1313 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1315 /* fixup unspecified transitions to be false */
1317 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1318 for
(i
= 1; i
<= n_nodes
; i
++)
1319 for
(j
= 1; j
<= n_nodes
; j
++)
1320 if
(! transitions
[i
][j
].is_null
()) {
1321 int in_arity
= transitions
[i
][j
].n_inp
();
1322 int out_arity
= transitions
[i
][j
].n_out
();
1323 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1324 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1325 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1327 "Arity mismatch in node transition: %s -> %s",
1328 (const char *) reachable_info
->node_names
[i
],
1329 (const char *) reachable_info
->node_names
[j
]);
1334 for
(i
= 1; i
<= n_nodes
; i
++)
1335 if
(arity
[i
] < 0) arity
[i
] = 0;
1336 /* Fill in false relations */
1337 for
(i
= 1; i
<= n_nodes
; i
++)
1338 for
(j
= 1; j
<= n_nodes
; j
++)
1339 if
(transitions
[i
][j
].is_null
())
1340 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1343 /* fixup unused start node positions */
1344 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1345 for
(i
= 1; i
<= n_nodes
; i
++)
1346 if
(nodes
[i
].is_null
())
1347 nodes
[i
] = Relation
::False
(arity
[i
]);
1349 if
(nodes
[i
].n_set
() != arity
[i
]){
1350 fprintf
(stderr
,"Arity mismatch in start node %s",
1351 (const char *) reachable_info
->node_names
[i
]);
1358 realNodeSpecificationList:
1359 realNodeSpecificationList
',' VAR
':' relation
1360 { int n_nodes
= reachable_info
->node_names.size
();
1361 int index
= reachable_info
->node_names.index
($3);
1362 assert
(index
!= 0 && index
<= n_nodes
);
1363 reachable_info
->start_nodes
[index
] = *$5;
1367 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1368 { int n_nodes
= reachable_info
->node_names.size
();
1369 int from_index
= reachable_info
->node_names.index
($3);
1370 int to_index
= reachable_info
->node_names.index
($5);
1371 assert
(from_index
!= 0 && to_index
!= 0);
1372 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1373 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1378 | VAR GOES_TO VAR
':' relation
1379 { int n_nodes
= reachable_info
->node_names.size
();
1380 int from_index
= reachable_info
->node_names.index
($1);
1381 int to_index
= reachable_info
->node_names.index
($3);
1382 assert
(from_index
!= 0 && to_index
!= 0);
1383 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1384 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1390 { int n_nodes
= reachable_info
->node_names.size
();
1391 int index
= reachable_info
->node_names.index
($1);
1392 assert
(index
!= 0 && index
<= n_nodes
);
1393 reachable_info
->start_nodes
[index
] = *$3;
1401 #if !defined(OMIT_GETRUSAGE)
1402 #include <sys/types.h>
1403 #include <sys/time.h>
1404 #include <sys/resource.h>
1406 struct rusage start_time
;
1409 #if defined BRAIN_DAMAGED_FREE
1415 void *realloc
(void *p
, size_t s
)
1417 return realloc
((malloc_t
) p
, s
);
1421 #if ! defined(OMIT_GETRUSAGE)
1423 extern
"C" int getrusage
(int, struct rusage
*);
1426 void start_clock
( void )
1428 getrusage
(RUSAGE_SELF
, &start_time
);
1431 int clock_diff
( void )
1433 struct rusage current_time
;
1434 getrusage
(RUSAGE_SELF
, ¤t_time
);
1435 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1436 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1440 void printUsage
(FILE *outf
, char **argv
) {
1441 fprintf
(outf
, "usage: %s {-R} {-D[facility][level]...} infile\n -R means skip redundant conjunct elimination\n -D sets debugging level as follows:\n a = all debugging flags\n g = code generation\n l = calculator\n c = omega core\n p = presburger functions\n r = relational operators\n t = transitive closure\nAll debugging output goes to %s\n",argv
[0],DEBUG_FILE_NAME
);
1444 int omega_calc_debug
;
1447 int main
(int argc
, char **argv
){
1448 redundant_conj_level
= 2;
1449 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1454 char * fileName
= 0;
1456 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1458 calc_all_debugging_off
();
1461 DebugFile
= fopen
("/dev/null","w");
1464 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1466 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1469 setbuf
(DebugFile
,0);
1472 closure_presburger_debug
= 0;
1474 setOutputFile
(DebugFile
);
1477 for
(i
=1; i
<argc
; i
++) {
1478 if
(argv
[i
][0] == '-') {
1480 while
((c
=argv
[i
][j
++]) != 0) {
1483 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1484 printUsage
(stderr
,argv
);
1490 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1491 while
(argv
[i
][j
] != 0) j
++;
1496 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1497 while
(argv
[i
][j
] != 0) j
++;
1501 redundant_conj_level
= 1;
1503 // Other future options go here
1505 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1506 printUsage
(stderr
,argv
);
1512 // Make sure this is a file name
1514 fprintf
(stderr
,"\nCan only handle a single input file\n");
1515 printUsage
(stderr
,argv
);
1519 yyin
= fopen
(fileName
, "r");
1521 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1522 printUsage
(stderr
,argv
);
1530 initializeScanBuffer
();
1531 currentTupleDescriptor
= NULL
;
1536 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1537 {delete r
; relationMap
[cs
]=0;});
1543 Relation LexForward
(int n
) {
1545 F_Or
*f
= r.add_or
();
1546 for
(int i
=1; i
<= n
; i
++) {
1547 F_And
*g
= f
->add_and
();
1548 for
(int j
=1;j
<i
;j
++) {
1549 EQ_Handle e
= g
->add_EQ
();
1550 e.update_coef
(r.input_var
(j
),-1);
1551 e.update_coef
(r.output_var
(j
),1);
1554 GEQ_Handle e
= g
->add_GEQ
();
1555 e.update_coef
(r.input_var
(i
),-1);
1556 e.update_coef
(r.output_var
(i
),1);