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>
21 #include "count_solutions.h"
23 #define CALC_VERSION_STRING "Omega Calculator v1.2"
25 #define DEBUG_FILE_NAME "./oc.out"
28 Map
<Const_String
,Relation
*> relationMap
((Relation
*)0);
29 static int redundant_conj_level
;
31 #if defined BRAIN_DAMAGED_FREE
33 void *realloc
(void *p
, size_t s
);
36 #if !defined(OMIT_GETRUSAGE)
37 void start_clock
( void );
38 int clock_diff
( void );
39 bool anyTimingDone
= false
;
44 Argument_Tuple currentTuple
= Input_Tuple
;
46 Relation LexForward
(int n
);
49 reachable_information
*reachable_info
;
55 %token
<INT_VALUE
> INT
56 %token
<STRING_VALUE
> STRING
57 %token OPEN_BRACE CLOSE_BRACE
64 %token DIFFERENCE DIFFERENCE_TO_RELATION
65 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
66 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
67 %token MAXIMIZE_RANGE MINIMIZE_RANGE
68 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
71 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
72 %token UNION INTERSECTION
73 %token VERTICAL_BAR SUCH_THAT
74 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
75 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
76 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
77 %token
<REL_OPERATOR
> REL_OP
78 %token RESTRICT_DOMAIN RESTRICT_RANGE
79 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
80 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
85 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
87 %nonassoc ASSERT_UNSAT
88 %left UNION OMEGA_P1
'+' '-'
89 %nonassoc SUPERSETOF SUBSETOF
90 %left OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE
91 %left INTERSECTION OMEGA_P3
'*' '@'
95 %left COMPOSE JOIN CARRIED_BY
96 %right NOT APPROX 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
105 %type
<INT_VALUE
> effort
106 %type
<EXP
> exp simpleExp
107 %type
<EXP_LIST
> expList
108 %type
<VAR_LIST
> varList
109 %type
<ARGUMENT_TUPLE
> argumentList
110 %type
<ASTP
> formula optionalFormula
111 %type
<ASTCP
> constraintChain
112 %type
<TUPLE_DESCRIPTOR
> tupleDeclaration
113 %type
<DECLARATION_SITE
> varDecl varDeclOptBrackets
114 %type
<RELATION
> relation builtRelation context
115 %type
<RELATION
> reachable_of
116 %type
<REL_TUPLE_PAIR
> relPairList
117 %type
<REL_TUPLE_TRIPLE
> relTripList
118 %type
<RELATION_ARRAY_1D
> reachable
119 %type
<STM_INFO_TUPLE
> statementInfoList statementInfoResult
120 %type
<STM_INFO
> statementInfo
121 %type
<STM_INFO
> reads
123 %type
<READ
> partials
124 %type
<PREAD
> partial
125 %type
<MMAP
> partialwrites
126 %type
<PMMAP
> partialwrite
136 Argument_Tuple ARGUMENT_TUPLE
;
137 AST_constraints
*ASTCP
;
138 Declaration_Site
* DECLARATION_SITE
;
140 tupleDescriptor
* TUPLE_DESCRIPTOR
;
141 RelTuplePair
* REL_TUPLE_PAIR
;
142 RelTupleTriple
* REL_TUPLE_TRIPLE
;
143 Dynamic_Array2
<Relation
> * RELATION_ARRAY_2D
;
144 Dynamic_Array1
<Relation
> * RELATION_ARRAY_1D
;
145 Tuple
<String
> *STRING_TUPLE
;
146 String
*STRING_VALUE
;
147 Tuple
<stm_info
> *STM_INFO_TUPLE
;
163 inputSequence
: inputItem
164 | inputSequence
{ assert
( current_Declaration_Site
== globalDecls
);}
171 /* Kill all the local declarations -- ejr */
172 Declaration_Site
*ds1
, *ds2
;
173 for
(ds1
= current_Declaration_Site
; ds1
!= globalDecls
;) {
178 current_Declaration_Site
= globalDecls
;
179 yyerror("skipping to statement end");
181 | SYMBOLIC globVarList
';'
184 | VAR IS_ASSIGNED relation
';'
187 $3->simplify
(min
(2,redundant_conj_level
),4);
188 Relation
*r
= relationMap
((Const_String
)$1);
190 relationMap
[(Const_String
)$1] = $3;
196 $1->simplify
(redundant_conj_level
,4);
197 $1->print_with_subs
(stdout
);
201 | TIME relation
';' {
203 #if defined(OMIT_GETRUSAGE)
204 printf
("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
212 bool SKIP_FULL_CHECK
= getenv
("OC_TIMING_SKIP_FULL_CHECK");
213 ($2)->and_with_GEQ
();
215 for
(t
=1;t
<=100;t
++) {
219 int copyTime
= clock_diff
();
221 for
(t
=1;t
<=100;t
++) {
226 int simplifyTime
= clock_diff
() -copyTime
;
228 if
(!SKIP_FULL_CHECK
)
231 for
(t
=1;t
<=100;t
++) {
237 int excessiveTime
= clock_diff
() - copyTime
;
238 printf
("Times (in microseconds): \n");
239 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
240 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
242 R.print_with_subs
(stdout
);
244 if
(!SKIP_FULL_CHECK
)
246 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
248 R2.print_with_subs
(stdout
);
251 if
(!anyTimingDone
) {
260 printf
("WARNING: The Omega calculator was compiled with options that force\n");
261 printf
("it to perform additional consistency and error checks\n");
262 printf
("that may slow it down substantially\n");
265 printf
("NOTE: These times relect the time of the current _implementation_\n");
266 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
267 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
268 printf
("request that send your test cases to us to allow us to determine if the \n");
269 printf
("times are appropriate, and if the way you are using the Omega library to \n");
270 printf
("solve your problem is the most effective way.\n");
273 printf
("Also, please be aware that over the past two years, we have focused our \n");
274 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
275 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
276 printf
("was substantially faster on the limited domain it handled.\n");
278 printf
(" Thanks, \n");
279 printf
(" the Omega Team \n");
281 anyTimingDone
= true
;
285 | TIMECLOSURE relation
';' {
287 #if defined(OMIT_GETRUSAGE)
288 printf
("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
294 ($2)->and_with_GEQ
();
296 for
(t
=1;t
<=100;t
++) {
300 int copyTime
= clock_diff
();
302 for
(t
=1;t
<=100;t
++) {
307 int simplifyTime
= clock_diff
() -copyTime
;
310 for
(t
=1;t
<=100;t
++) {
313 Rclosed
= TransitiveClosure
(Rclosed
, 1,Relation
::Null
());
315 int closureTime
= clock_diff
() - copyTime
;
318 for
(t
=1;t
<=100;t
++) {
323 int excessiveTime
= clock_diff
() - copyTime
;
324 printf
("Times (in microseconds): \n");
325 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
326 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
328 R.print_with_subs
(stdout
);
330 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
332 R2.print_with_subs
(stdout
);
333 printf
("%5d us to do the transitive closure, obtaining: \n\t",
335 Rclosed.print_with_subs
(stdout
);
337 if
(!anyTimingDone
) {
346 printf
("WARNING: The Omega calculator was compiled with options that force\n");
347 printf
("it to perform additional consistency and error checks\n");
348 printf
("that may slow it down substantially\n");
351 printf
("NOTE: These times relect the time of the current _implementation_\n");
352 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
353 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
354 printf
("request that send your test cases to us to allow us to determine if the \n");
355 printf
("times are appropriate, and if the way you are using the Omega library to \n");
356 printf
("solve your problem is the most effective way.\n");
359 printf
("Also, please be aware that over the past two years, we have focused our \n");
360 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
361 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
362 printf
("was substantially faster on the limited domain it handled.\n");
364 printf
(" Thanks, \n");
365 printf
(" the Omega Team \n");
367 anyTimingDone
= true
;
373 | relation SUBSET relation
';' {
375 int c
= Must_Be_Subset
(*$1, *$3);
376 printf
("\n%s\n", c ?
"True" : "False");
380 | CODEGEN effort relPairList context
';'
383 String s
= MMGenerateCode
($3->mappings
, $3->ispaces
,*$4,$2);
386 printf
("%s\n", (const char *) s
);
388 | TCODEGEN effort statementInfoResult context
';'
391 String s
= tcodegen
($2, *($3), *($4));
394 printf
("%s\n", (const char *) s
);
396 /* | TCODEGEN NOT effort statementInfoResult context';'
399 * String s = tcodegen($3, *($4), *($5), false);
402 * printf("%s\n", (const char *) s);
405 | SPMD blockAndProcsAndEffort relTripList
';'
407 Tuple
<Free_Var_Decl
*> lowerBounds
(0), upperBounds
(0), my_procs
(0);
408 Tuple
<spmd_stmt_info
*> names
(0);
411 int nr_statements
= $3->space.size
();
413 for
(int i
= 1; i
<= $3->space
[1].n_out
(); i
++)
415 lowerBounds.append
(new Free_Var_Decl
("lb" + itoS
(i
)));
416 upperBounds.append
(new Free_Var_Decl
("ub" + itoS
(i
)));
417 my_procs.append
(new Free_Var_Decl
("my_proc" + itoS
(i
)));
420 for
(int p
= 1; p
<= nr_statements
; p
++)
421 names.append
(new numbered_stmt_info
(p
-1, Identity
($3->time
[p
].n_out
()),
423 (char *)(const char *)("s"+itoS
(p
-1))));
425 String s
= SPMD_GenerateCode
("", $3->space
, $3->time
, $3->ispaces
,
427 lowerBounds
, upperBounds
, my_procs
,
431 printf
("%s\n", (const char *) s
);
435 Dynamic_Array1
<Relation
> &final
= *$1;
437 int i
,n_nodes
= reachable_info
->node_names.size
();
438 for
(i
= 1; i
<= n_nodes
; i
++) if
(final
[i
].is_upper_bound_satisfiable
()) {
440 fprintf
(stdout
,"Node %s: ",
441 (const char *) (reachable_info
->node_names
[i
]));
442 final
[i
].print_with_subs
(stdout
);
445 fprintf
(stdout
,"No nodes reachable.\n");
447 delete reachable_info
;
449 | COUNT relation
';' {
450 double c
= count_solutions
(*$2);
451 fprintf
(stdout
, "%.0f\n", c
);
455 relTripList: relTripList
',' relation
':' relation
':' relation
457 $1->space.append
(*$3);
458 $1->time.append
(*$5);
459 $1->ispaces.append
(*$7);
465 | relation
':' relation
':' relation
467 RelTupleTriple
*rtt
= new RelTupleTriple
;
468 rtt
->space.append
(*$1);
469 rtt
->time.append
(*$3);
470 rtt
->ispaces.append
(*$5);
478 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
479 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
480 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
481 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
486 |
'-' INT
{ $$
= -$2; }
489 context
: { $$
= new Relation
();
490 *$$
= Relation
::Null
(); }
491 | GIVEN relation
{$$
= $2; }
494 relPairList: relPairList
',' relation
':' relation
496 $1->mappings.append
(*$3);
497 $1->mappings
[$1->mappings.size
()].compress
();
498 $1->ispaces.append
(*$5);
499 $1->ispaces
[$1->ispaces.size
()].compress
();
504 | relPairList
',' relation
506 $1->mappings.append
(Identity
($3->n_set
()));
507 $1->mappings
[$1->mappings.size
()].compress
();
508 $1->ispaces.append
(*$3);
509 $1->ispaces
[$1->ispaces.size
()].compress
();
513 | relation
':' relation
515 RelTuplePair
*rtp
= new RelTuplePair
;
516 rtp
->mappings.append
(*$1);
517 rtp
->mappings
[rtp
->mappings.size
()].compress
();
518 rtp
->ispaces.append
(*$3);
519 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
526 RelTuplePair
*rtp
= new RelTuplePair
;
527 rtp
->mappings.append
(Identity
($1->n_set
()));
528 rtp
->mappings
[rtp
->mappings.size
()].compress
();
529 rtp
->ispaces.append
(*$1);
530 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
536 statementInfoResult
: statementInfoList
538 /* | ASSERT_UNSAT statementInfoResult
540 * DoDebug2("Debug info requested in input", *($2));
543 | TRANS_IS relation statementInfoResult
544 { $$
= &Trans_IS
(*($3), *($2));
547 | SET_MMAP INT partialwrites statementInfoResult
548 { $$
= &Set_MMap
(*($4), $2, *($3));
551 | UNROLL_IS INT INT INT statementInfoResult
552 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
553 | PEEL_IS INT INT relation statementInfoResult
554 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
557 | PEEL_IS INT INT relation
',' relation statementInfoResult
558 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
564 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
567 | statementInfoList
',' statementInfo
{ $$
= $1;
572 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
574 $$
->stm
= *($2); delete
$2;
575 $$
->IS
= *($4); delete
$4;
576 $$
->map
= *($6); delete
$6;
578 |
'[' STRING
',' relation
',' partialwrites
']'
580 $$
->stm
= *($2); delete
$2;
581 $$
->IS
= *($4); delete
$4;
582 $$
->map
= *($6); delete
$6;
586 partialwrites
: partialwrites
',' partialwrite
588 $$
->partials.append
(*($3)); delete
$3;
590 | partialwrite
{ $$
= new MMap
;
591 $$
->partials.append
(*($1)); delete
$1;
595 partialwrite
: STRING
'[' relation
']' ',' relation
596 { $$
= new PartialMMap
;
597 $$
->mapping
= *($6); delete
$6;
598 $$
->bounds
= *($3); delete
$3;
599 $$
->var
= *($1); delete
$1;
601 | STRING
',' relation
{ $$
= new PartialMMap
;
602 $$
->mapping
= *($3); delete
$3;
603 $$
->bounds
= Relation
::True
(0);
604 $$
->var
= *($1); delete
$1;
608 reads
: reads
',' oneread
{ $$
= $1;
609 $$
->read.append
(*($3)); delete
$3;
611 | oneread
{ $$
= new stm_info
;
612 $$
->read.append
(*($1)); delete
$1;
616 oneread
: '[' partials
']' { $$
= $2; }
619 partials
: partials
',' partial
{ $$
= $1;
620 $$
->partials.append
(*($3)); delete
$3;
622 | partial
{ $$
= new Read
;
623 $$
->partials.append
(*($1)); delete
$1;
627 partial
: INT
',' relation
{ $$
= new PartialRead
;
629 $$
->dataFlow
= *($3); delete
$3;
633 globVarList: globVarList
',' globVar
637 globVar: VAR
'(' INT
')'
638 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
640 { globalDecls
->extend
($1); free
($1); }
643 relation
: OPEN_BRACE
644 { relationDecl
= new Declaration_Site
(); }
648 if
(omega_calc_debug
) {
649 fprintf
(DebugFile
,"Built relation:\n");
650 $$
->prefix_print
(DebugFile
);
652 current_Declaration_Site
= globalDecls
;
658 if
(relationMap
(s
) == 0) {
659 fprintf
(stderr
,"Variable %s not declared\n",$1);
663 $$
= new Relation
(*relationMap
(s
));
665 |
'(' relation
')' {$$
= $2;}
666 | relation
'+' %prec OMEGA_P9
667 { $$
= new Relation
();
668 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
671 | relation
'*' %prec OMEGA_P9
672 { $$
= new Relation
();
673 int vars
= $1->n_inp
();
674 *$$
= Union
(Identity
(vars
),
675 TransitiveClosure
(*$1, 1,Relation
::Null
()));
678 | relation
'+' WITHIN relation %prec OMEGA_P9
679 {$$
= new Relation
();
680 *$$
= TransitiveClosure
(*$1, 1,*$4);
684 | MINIMIZE_RANGE relation %prec OMEGA_P8
688 r
= Join
(r
,LexForward
($2->n_out
()));
690 *$$
= Difference
(o
,r
);
693 | MAXIMIZE_RANGE relation %prec OMEGA_P8
697 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
699 *$$
= Difference
(o
,r
);
702 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
706 r
= Join
(LexForward
($2->n_inp
()),r
);
708 *$$
= Difference
(o
,r
);
711 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
715 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
717 *$$
= Difference
(o
,r
);
720 | MAXIMIZE relation %prec OMEGA_P8
725 *$$
= Cross_Product
(Relation
(*$2),c
);
727 assert
($$
->n_inp
() ==$$
->n_out
());
728 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
730 | MINIMIZE relation %prec OMEGA_P8
735 *$$
= Cross_Product
(Relation
(*$2),c
);
737 assert
($$
->n_inp
() ==$$
->n_out
());
738 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
740 | FARKAS relation %prec OMEGA_P8
743 *$$
= Farkas
(*$2, Basic_Farkas
);
746 | DECOUPLED_FARKAS relation %prec OMEGA_P8
749 *$$
= Farkas
(*$2, Decoupled_Farkas
);
752 | relation
'@' %prec OMEGA_P9
753 { $$
= new Relation
();
754 *$$
= ConicClosure
(*$1);
757 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
758 { $$
= new Relation
();
759 *$$
= Project_Sym
(*$2);
762 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
763 { $$
= new Relation
();
764 *$$
= Project_On_Sym
(*$2);
767 | DIFFERENCE relation %prec OMEGA_P8
768 { $$
= new Relation
();
772 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
773 { $$
= new Relation
();
774 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
777 | DOMAIN relation %prec OMEGA_P8
778 { $$
= new Relation
();
782 | VENN relation %prec OMEGA_P8
783 { $$
= new Relation
();
784 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
787 | VENN relation GIVEN relation %prec OMEGA_P8
788 { $$
= new Relation
();
789 *$$
= VennDiagramForm
(*$2,*$4);
793 | CONVEX_HULL relation %prec OMEGA_P8
794 { $$
= new Relation
();
795 *$$
= ConvexHull
(*$2);
798 | POSITIVE_COMBINATION relation %prec OMEGA_P8
799 { $$
= new Relation
();
800 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
803 | CONVEX_COMBINATION relation %prec OMEGA_P8
804 { $$
= new Relation
();
805 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
808 | PAIRWISE_CHECK relation %prec OMEGA_P8
809 { $$
= new Relation
();
810 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
813 | CONVEX_CHECK relation %prec OMEGA_P8
814 { $$
= new Relation
();
815 *$$
= CheckForConvexRepresentation
(*$2);
818 | AFFINE_HULL relation %prec OMEGA_P8
819 { $$
= new Relation
();
820 *$$
= AffineHull
(*$2);
823 | CONIC_HULL relation %prec OMEGA_P8
824 { $$
= new Relation
();
825 *$$
= ConicHull
(*$2);
828 | LINEAR_HULL relation %prec OMEGA_P8
829 { $$
= new Relation
();
830 *$$
= LinearHull
(*$2);
833 | HULL relation %prec OMEGA_P8
834 { $$
= new Relation
();
835 *$$
= Hull
(*$2,false
,1,Null_Relation
());
838 | HULL relation GIVEN relation %prec OMEGA_P8
839 { $$
= new Relation
();
840 *$$
= Hull
(*$2,false
,1,*$4);
844 | APPROX relation %prec OMEGA_P8
845 { $$
= new Relation
();
846 *$$
= Approximate
(*$2);
849 | RANGE relation %prec OMEGA_P8
850 { $$
= new Relation
();
854 | INVERSE relation %prec OMEGA_P8
855 { $$
= new Relation
();
859 | COMPLEMENT relation %prec OMEGA_P8
860 { $$
= new Relation
();
861 *$$
= Complement
(*$2);
864 | GIST relation GIVEN relation %prec OMEGA_P8
865 { $$
= new Relation
();
866 *$$
= Gist
(*$2,*$4,1);
870 | relation
'(' relation
')'
871 { $$
= new Relation
();
872 *$$
= Composition
(*$1,*$3);
876 | relation COMPOSE relation
877 { $$
= new Relation
();
878 *$$
= Composition
(*$1,*$3);
882 | relation CARRIED_BY INT
883 { $$
= new Relation
();
884 *$$
= After
(*$1,$3,$3);
886 (*$$
).prefix_print
(stdout
);
888 | relation JOIN relation
889 { $$
= new Relation
();
890 *$$
= Composition
(*$3,*$1);
894 | relation RESTRICT_RANGE relation
895 { $$
= new Relation
();
896 *$$
= Restrict_Range
(*$1,*$3);
900 | relation RESTRICT_DOMAIN relation
901 { $$
= new Relation
();
902 *$$
= Restrict_Domain
(*$1,*$3);
906 | relation INTERSECTION relation
907 { $$
= new Relation
();
908 *$$
= Intersection
(*$1,*$3);
912 | relation
'-' relation %prec INTERSECTION
913 { $$
= new Relation
();
914 *$$
= Difference
(*$1,*$3);
918 | relation UNION relation
919 { $$
= new Relation
();
920 *$$
= Union
(*$1,*$3);
924 | relation
'*' relation
925 { $$
= new Relation
();
926 *$$
= Cross_Product
(*$1,*$3);
930 | SUPERSETOF relation
931 { $$
= new Relation
();
932 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
936 { $$
= new Relation
();
937 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
940 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
941 { $$
= new Relation
();
942 *$$
= Upper_Bound
(*$2);
945 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
946 { $$
= new Relation
();
947 *$$
= Lower_Bound
(*$2);
951 { $$
= new Relation
();
952 *$$
= Sample_Solution
(*$2);
955 | SYM_SAMPLE relation
956 { $$
= new Relation
();
957 *$$
= Symbolic_Solution
(*$2);
960 | reachable_of
{ $$
= $1; }
961 | ASSERT_UNSAT relation
963 if
(($2)->is_satisfiable
())
965 fprintf
(stderr
,"assert_unsatisfiable failed on ");
966 ($2)->print_with_subs
(stderr
);
975 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
976 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
977 Relation
* r
= new Relation
($1->size
,$4->size
);
979 F_And
*f
= r
->add_and
();
981 for
(i
=1;i
<=$1->size
;i
++) {
982 $1->vars
[i
]->vid
= r
->input_var
(i
);
983 if
(!$1->vars
[i
]->anonymous
)
984 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
986 for
(i
=1;i
<=$4->size
;i
++) {
987 $4->vars
[i
]->vid
= r
->output_var
(i
);
988 if
(!$4->vars
[i
]->anonymous
)
989 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
991 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
992 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
993 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
994 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
995 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
996 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
997 if
($6) $6->install
(f
);
1002 | tupleDeclaration optionalFormula
{
1003 Relation
* r
= new Relation
($1->size
);
1005 F_And
*f
= r
->add_and
();
1007 for
(i
=1;i
<=$1->size
;i
++) {
1008 $1->vars
[i
]->vid
= r
->set_var
(i
);
1009 if
(!$1->vars
[i
]->anonymous
)
1010 r
->name_set_var
(i
,$1->vars
[i
]->stripped_name
);
1012 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1013 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1014 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1015 if
($2) $2->install
(f
);
1020 Relation
* r
= new Relation
(0,0);
1021 F_And
*f
= r
->add_and
();
1028 optionalFormula
: formula_sep formula
{ $$
= $2; }
1038 { currentTupleDescriptor
= new tupleDescriptor
; tuplePos
= 1; }
1039 '[' optionalTupleVarList
']'
1040 {$$
= currentTupleDescriptor
; }
1043 optionalTupleVarList
:
1045 | optionalTupleVarList
',' tupleVar
1049 tupleVar
: VAR %prec OMEGA_P10
1050 { Declaration_Site
*ds
= defined
($1);
1051 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1053 Variable_Ref
* v
= lookupScalar
($1);
1055 if
(ds
!= globalDecls
)
1056 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1058 currentTupleDescriptor
->extend
(new Exp
(v
));
1064 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1065 | exp %prec OMEGA_P1
1066 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1067 | exp
':' exp %prec OMEGA_P1
1068 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1069 | exp
':' exp
':' INT %prec OMEGA_P1
1070 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1074 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1075 | VAR
{ $$
= new VarList
;
1081 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1082 foreach
(s
,char *, *$1, delete s
);
1087 /* variable declaration with optional brackets */
1089 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1090 |
'[' varDecl
']' { $$
= $2; }
1093 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1094 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1095 | constraintChain
{ $$
= $1; }
1096 |
'(' formula
')' { $$
= $2; }
1097 | NOT formula
{ $$
= new AST_Not
($2); }
1098 | start_exists varDeclOptBrackets exists_sep formula end_quant
1099 { $$
= new AST_exists
($2,$4); }
1100 | start_forall varDeclOptBrackets forall_sep formula end_quant
1101 { $$
= new AST_forall
($2,$4); }
1104 start_exists
: '(' EXISTS
1113 start_forall
: '(' FORALL
1124 expList
: exp
',' expList
1135 constraintChain
: expList REL_OP expList
1136 { $$
= new AST_constraints
($1,$2,$3); }
1137 | expList REL_OP constraintChain
1138 { $$
= new AST_constraints
($1,$2,$3); }
1143 { Variable_Ref
* v
= lookupScalar
($1);
1148 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1150 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1151 else v
= functionOfOutput
[$1];
1154 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1159 |
'(' exp
')' { $$
= $2;}
1165 argumentList
',' VAR
{
1166 Variable_Ref
* v
= lookupScalar
($3);
1169 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1170 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1176 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1179 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1180 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1188 exp
: INT
{$$
= new Exp
($1);}
1189 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1190 | simpleExp
{ $$
= $1; }
1191 |
'-' exp %prec
'*' { $$
= negate
($2);}
1192 | exp
'+' exp
{ $$
= add
($1,$3);}
1193 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1194 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1199 REACHABLE_FROM nodeNameList nodeSpecificationList
1201 Dynamic_Array1
<Relation
> *final
=
1202 Reachable_Nodes
(reachable_info
);
1208 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1210 Dynamic_Array1
<Relation
> *final
=
1211 Reachable_Nodes
(reachable_info
);
1212 int index
= reachable_info
->node_names.index
(String
($2));
1213 assert
(index
!= 0 && "No such node");
1215 *$$
= (*final
)[index
];
1217 delete reachable_info
;
1223 nodeNameList: '(' realNodeNameList
')'
1224 { int sz
= reachable_info
->node_names.size
();
1225 reachable_info
->node_arity.reallocate
(sz
);
1226 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1227 reachable_info
->start_nodes.resize
(sz
+1);
1231 realNodeNameList: realNodeNameList
',' VAR
1232 { reachable_info
->node_names.append
(String
($3));
1234 | VAR
{ reachable_info
= new reachable_information
;
1235 reachable_info
->node_names.append
(String
($1));
1240 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1243 int n_nodes
= reachable_info
->node_names.size
();
1244 Tuple
<int> &arity
= reachable_info
->node_arity
;
1245 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1247 /* fixup unspecified transitions to be false */
1249 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1250 for
(i
= 1; i
<= n_nodes
; i
++)
1251 for
(j
= 1; j
<= n_nodes
; j
++)
1252 if
(! transitions
[i
][j
].is_null
()) {
1253 int in_arity
= transitions
[i
][j
].n_inp
();
1254 int out_arity
= transitions
[i
][j
].n_out
();
1255 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1256 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1257 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1259 "Arity mismatch in node transition: %s -> %s",
1260 (const char *) reachable_info
->node_names
[i
],
1261 (const char *) reachable_info
->node_names
[j
]);
1266 for
(i
= 1; i
<= n_nodes
; i
++)
1267 if
(arity
[i
] < 0) arity
[i
] = 0;
1268 /* Fill in false relations */
1269 for
(i
= 1; i
<= n_nodes
; i
++)
1270 for
(j
= 1; j
<= n_nodes
; j
++)
1271 if
(transitions
[i
][j
].is_null
())
1272 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1275 /* fixup unused start node positions */
1276 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1277 for
(i
= 1; i
<= n_nodes
; i
++)
1278 if
(nodes
[i
].is_null
())
1279 nodes
[i
] = Relation
::False
(arity
[i
]);
1281 if
(nodes
[i
].n_set
() != arity
[i
]){
1282 fprintf
(stderr
,"Arity mismatch in start node %s",
1283 (const char *) reachable_info
->node_names
[i
]);
1290 realNodeSpecificationList:
1291 realNodeSpecificationList
',' VAR
':' relation
1292 { int n_nodes
= reachable_info
->node_names.size
();
1293 int index
= reachable_info
->node_names.index
($3);
1294 assert
(index
!= 0 && index
<= n_nodes
);
1295 reachable_info
->start_nodes
[index
] = *$5;
1299 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1300 { int n_nodes
= reachable_info
->node_names.size
();
1301 int from_index
= reachable_info
->node_names.index
($3);
1302 int to_index
= reachable_info
->node_names.index
($5);
1303 assert
(from_index
!= 0 && to_index
!= 0);
1304 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1305 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1310 | VAR GOES_TO VAR
':' relation
1311 { int n_nodes
= reachable_info
->node_names.size
();
1312 int from_index
= reachable_info
->node_names.index
($1);
1313 int to_index
= reachable_info
->node_names.index
($3);
1314 assert
(from_index
!= 0 && to_index
!= 0);
1315 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1316 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1322 { int n_nodes
= reachable_info
->node_names.size
();
1323 int index
= reachable_info
->node_names.index
($1);
1324 assert
(index
!= 0 && index
<= n_nodes
);
1325 reachable_info
->start_nodes
[index
] = *$3;
1333 #if !defined(OMIT_GETRUSAGE)
1334 #include <sys/types.h>
1335 #include <sys/time.h>
1336 #include <sys/resource.h>
1338 struct rusage start_time
;
1341 #if defined BRAIN_DAMAGED_FREE
1347 void *realloc
(void *p
, size_t s
)
1349 return realloc
((malloc_t
) p
, s
);
1353 #if ! defined(OMIT_GETRUSAGE)
1355 extern
"C" int getrusage
(int, struct rusage
*);
1358 void start_clock
( void )
1360 getrusage
(RUSAGE_SELF
, &start_time
);
1363 int clock_diff
( void )
1365 struct rusage current_time
;
1366 getrusage
(RUSAGE_SELF
, ¤t_time
);
1367 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1368 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1372 void printUsage
(FILE *outf
, char **argv
) {
1373 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
);
1376 int omega_calc_debug
;
1379 int main
(int argc
, char **argv
){
1380 redundant_conj_level
= 2;
1381 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1386 char * fileName
= 0;
1388 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1390 calc_all_debugging_off
();
1393 DebugFile
= fopen
("/dev/null","w");
1396 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1398 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1401 setbuf
(DebugFile
,0);
1404 closure_presburger_debug
= 0;
1406 setOutputFile
(DebugFile
);
1409 for
(i
=1; i
<argc
; i
++) {
1410 if
(argv
[i
][0] == '-') {
1412 while
((c
=argv
[i
][j
++]) != 0) {
1415 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1416 printUsage
(stderr
,argv
);
1422 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1423 while
(argv
[i
][j
] != 0) j
++;
1428 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1429 while
(argv
[i
][j
] != 0) j
++;
1433 redundant_conj_level
= 1;
1435 // Other future options go here
1437 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1438 printUsage
(stderr
,argv
);
1444 // Make sure this is a file name
1446 fprintf
(stderr
,"\nCan only handle a single input file\n");
1447 printUsage
(stderr
,argv
);
1451 yyin
= fopen
(fileName
, "r");
1453 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1454 printUsage
(stderr
,argv
);
1462 initializeScanBuffer
();
1467 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1468 {delete r
; relationMap
[cs
]=0;});
1474 Relation LexForward
(int n
) {
1476 F_Or
*f
= r.add_or
();
1477 for
(int i
=1; i
<= n
; i
++) {
1478 F_And
*g
= f
->add_and
();
1479 for
(int j
=1;j
<i
;j
++) {
1480 EQ_Handle e
= g
->add_EQ
();
1481 e.update_coef
(r.input_var
(j
),-1);
1482 e.update_coef
(r.output_var
(j
),1);
1485 GEQ_Handle e
= g
->add_GEQ
();
1486 e.update_coef
(r.input_var
(i
),-1);
1487 e.update_coef
(r.output_var
(i
),1);