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>
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
;
45 char *currentVar
= NULL
;
47 Relation LexForward
(int n
);
50 reachable_information
*reachable_info
;
56 %token
<INT_VALUE
> INT
57 %token
<STRING_VALUE
> STRING
58 %token OPEN_BRACE CLOSE_BRACE
64 %token OMEGA_DOMAIN RANGE
65 %token DIFFERENCE DIFFERENCE_TO_RELATION
66 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
67 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
68 %token MAXIMIZE_RANGE MINIMIZE_RANGE
69 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
72 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
73 %token UNION INTERSECTION
74 %token VERTICAL_BAR SUCH_THAT
75 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
76 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
77 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
78 %token
<REL_OPERATOR
> REL_OP
79 %token RESTRICT_DOMAIN RESTRICT_RANGE
80 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
81 %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 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
104 %type
<INT_VALUE
> effort
105 %type
<EXP
> exp simpleExp
106 %type
<EXP_LIST
> expList
107 %type
<VAR_LIST
> varList
108 %type
<ARGUMENT_TUPLE
> argumentList
109 %type
<ASTP
> formula optionalFormula
110 %type
<ASTCP
> constraintChain
111 %type
<TUPLE_DESCRIPTOR
> tupleDeclaration
112 %type
<DECLARATION_SITE
> varDecl varDeclOptBrackets
113 %type
<RELATION
> relation builtRelation context
114 %type
<RELATION
> reachable_of
115 %type
<REL_TUPLE_PAIR
> relPairList
116 %type
<REL_TUPLE_TRIPLE
> relTripList
117 %type
<RELATION_ARRAY_1D
> reachable
118 %type
<STM_INFO_TUPLE
> statementInfoList statementInfoResult
119 %type
<STM_INFO
> statementInfo
120 %type
<STM_INFO
> reads
122 %type
<READ
> partials
123 %type
<PREAD
> partial
124 %type
<MMAP
> partialwrites
125 %type
<PMMAP
> partialwrite
135 Argument_Tuple ARGUMENT_TUPLE
;
136 AST_constraints
*ASTCP
;
137 Declaration_Site
* DECLARATION_SITE
;
139 tupleDescriptor
* TUPLE_DESCRIPTOR
;
140 RelTuplePair
* REL_TUPLE_PAIR
;
141 RelTupleTriple
* REL_TUPLE_TRIPLE
;
142 Dynamic_Array2
<Relation
> * RELATION_ARRAY_2D
;
143 Dynamic_Array1
<Relation
> * RELATION_ARRAY_1D
;
144 Tuple
<String
> *STRING_TUPLE
;
145 String
*STRING_VALUE
;
146 Tuple
<stm_info
> *STM_INFO_TUPLE
;
162 inputSequence
: inputItem
163 | inputSequence
{ assert
( current_Declaration_Site
== globalDecls
);}
170 /* Kill all the local declarations -- ejr */
173 Declaration_Site
*ds1
, *ds2
;
174 for
(ds1
= current_Declaration_Site
; ds1
!= globalDecls
;) {
179 current_Declaration_Site
= globalDecls
;
180 yyerror("skipping to statement end");
182 | SYMBOLIC globVarList
';'
185 | VAR
{ currentVar
= $1; } IS_ASSIGNED relation
';'
188 $4->simplify
(min
(2,redundant_conj_level
),4);
189 Relation
*r
= relationMap
((Const_String
)$1);
191 relationMap
[(Const_String
)$1] = $4;
198 $1->simplify
(redundant_conj_level
,4);
199 $1->print_with_subs
(stdout
);
203 | TIME relation
';' {
205 #if defined(OMIT_GETRUSAGE)
206 printf
("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
214 bool SKIP_FULL_CHECK
= getenv
("OC_TIMING_SKIP_FULL_CHECK");
215 ($2)->and_with_GEQ
();
217 for
(t
=1;t
<=100;t
++) {
221 int copyTime
= clock_diff
();
223 for
(t
=1;t
<=100;t
++) {
228 int simplifyTime
= clock_diff
() -copyTime
;
230 if
(!SKIP_FULL_CHECK
)
233 for
(t
=1;t
<=100;t
++) {
239 int excessiveTime
= clock_diff
() - copyTime
;
240 printf
("Times (in microseconds): \n");
241 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
242 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
244 R.print_with_subs
(stdout
);
246 if
(!SKIP_FULL_CHECK
)
248 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
250 R2.print_with_subs
(stdout
);
253 if
(!anyTimingDone
) {
262 printf
("WARNING: The Omega calculator was compiled with options that force\n");
263 printf
("it to perform additional consistency and error checks\n");
264 printf
("that may slow it down substantially\n");
267 printf
("NOTE: These times relect the time of the current _implementation_\n");
268 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
269 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
270 printf
("request that send your test cases to us to allow us to determine if the \n");
271 printf
("times are appropriate, and if the way you are using the Omega library to \n");
272 printf
("solve your problem is the most effective way.\n");
275 printf
("Also, please be aware that over the past two years, we have focused our \n");
276 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
277 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
278 printf
("was substantially faster on the limited domain it handled.\n");
280 printf
(" Thanks, \n");
281 printf
(" the Omega Team \n");
283 anyTimingDone
= true
;
287 | TIMECLOSURE relation
';' {
289 #if defined(OMIT_GETRUSAGE)
290 printf
("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
296 ($2)->and_with_GEQ
();
298 for
(t
=1;t
<=100;t
++) {
302 int copyTime
= clock_diff
();
304 for
(t
=1;t
<=100;t
++) {
309 int simplifyTime
= clock_diff
() -copyTime
;
312 for
(t
=1;t
<=100;t
++) {
315 Rclosed
= TransitiveClosure
(Rclosed
, 1,Relation
::Null
());
317 int closureTime
= clock_diff
() - copyTime
;
320 for
(t
=1;t
<=100;t
++) {
325 int excessiveTime
= clock_diff
() - copyTime
;
326 printf
("Times (in microseconds): \n");
327 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
328 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
330 R.print_with_subs
(stdout
);
332 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
334 R2.print_with_subs
(stdout
);
335 printf
("%5d us to do the transitive closure, obtaining: \n\t",
337 Rclosed.print_with_subs
(stdout
);
339 if
(!anyTimingDone
) {
348 printf
("WARNING: The Omega calculator was compiled with options that force\n");
349 printf
("it to perform additional consistency and error checks\n");
350 printf
("that may slow it down substantially\n");
353 printf
("NOTE: These times relect the time of the current _implementation_\n");
354 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
355 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
356 printf
("request that send your test cases to us to allow us to determine if the \n");
357 printf
("times are appropriate, and if the way you are using the Omega library to \n");
358 printf
("solve your problem is the most effective way.\n");
361 printf
("Also, please be aware that over the past two years, we have focused our \n");
362 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
363 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
364 printf
("was substantially faster on the limited domain it handled.\n");
366 printf
(" Thanks, \n");
367 printf
(" the Omega Team \n");
369 anyTimingDone
= true
;
375 | relation SUBSET relation
';' {
377 int c
= Must_Be_Subset
(*$1, *$3);
378 printf
("\n%s\n", c ?
"True" : "False");
382 | CODEGEN effort relPairList context
';'
385 String s
= MMGenerateCode
($3->mappings
, $3->ispaces
,*$4,$2);
388 printf
("%s\n", (const char *) s
);
390 | TCODEGEN effort statementInfoResult context
';'
393 String s
= tcodegen
($2, *($3), *($4));
396 printf
("%s\n", (const char *) s
);
398 /* | TCODEGEN NOT effort statementInfoResult context';'
401 * String s = tcodegen($3, *($4), *($5), false);
404 * printf("%s\n", (const char *) s);
407 | SPMD blockAndProcsAndEffort relTripList
';'
409 Tuple
<Free_Var_Decl
*> lowerBounds
(0), upperBounds
(0), my_procs
(0);
410 Tuple
<spmd_stmt_info
*> names
(0);
413 int nr_statements
= $3->space.size
();
415 for
(int i
= 1; i
<= $3->space
[1].n_out
(); i
++)
417 lowerBounds.append
(new Free_Var_Decl
("lb" + itoS
(i
)));
418 upperBounds.append
(new Free_Var_Decl
("ub" + itoS
(i
)));
419 my_procs.append
(new Free_Var_Decl
("my_proc" + itoS
(i
)));
422 for
(int p
= 1; p
<= nr_statements
; p
++)
423 names.append
(new numbered_stmt_info
(p
-1, Identity
($3->time
[p
].n_out
()),
425 (char *)(const char *)("s"+itoS
(p
-1))));
427 String s
= SPMD_GenerateCode
("", $3->space
, $3->time
, $3->ispaces
,
429 lowerBounds
, upperBounds
, my_procs
,
433 printf
("%s\n", (const char *) s
);
437 Dynamic_Array1
<Relation
> &final
= *$1;
439 int i
,n_nodes
= reachable_info
->node_names.size
();
440 for
(i
= 1; i
<= n_nodes
; i
++) if
(final
[i
].is_upper_bound_satisfiable
()) {
442 fprintf
(stdout
,"Node %s: ",
443 (const char *) (reachable_info
->node_names
[i
]));
444 final
[i
].print_with_subs
(stdout
);
447 fprintf
(stdout
,"No nodes reachable.\n");
449 delete reachable_info
;
451 | CARD relation
';' {
452 evalue
*EP
= count_relation
(*$2);
454 const Variable_ID_Tuple
* globals
= $2->global_decls
();
455 const char **param_names
= new
(const char *)[globals
->size
()];
456 for
(int i
= 0; i
< globals
->size
(); ++i
)
457 param_names
[i
] = (*globals
)[i
+1]->char_name
();
458 print_evalue
(stdout
, EP
, (char**)param_names
);
460 delete
[] param_names
;
461 free_evalue_refs
(EP
);
466 | RANKING relation
';' {
467 evalue
*EP
= rank_relation
(*$2);
469 const Variable_ID_Tuple
* globals
= $2->global_decls
();
470 int nvar
= $2->n_set
();
471 int n
= nvar
+ globals
->size
();
472 const char **names
= new
(const char *)[n
];
474 for
(int i
= 0; i
< nvar
; ++i
)
475 names
[i
] = $2->set_var
(i
+1)->char_name
();
476 for
(int i
= 0; i
< globals
->size
(); ++i
)
477 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
478 print_evalue
(stdout
, EP
, (char**)names
);
481 free_evalue_refs
(EP
);
488 relTripList: relTripList
',' relation
':' relation
':' relation
490 $1->space.append
(*$3);
491 $1->time.append
(*$5);
492 $1->ispaces.append
(*$7);
498 | relation
':' relation
':' relation
500 RelTupleTriple
*rtt
= new RelTupleTriple
;
501 rtt
->space.append
(*$1);
502 rtt
->time.append
(*$3);
503 rtt
->ispaces.append
(*$5);
511 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
512 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
513 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
514 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
519 |
'-' INT
{ $$
= -$2; }
522 context
: { $$
= new Relation
();
523 *$$
= Relation
::Null
(); }
524 | GIVEN relation
{$$
= $2; }
527 relPairList: relPairList
',' relation
':' relation
529 $1->mappings.append
(*$3);
530 $1->mappings
[$1->mappings.size
()].compress
();
531 $1->ispaces.append
(*$5);
532 $1->ispaces
[$1->ispaces.size
()].compress
();
537 | relPairList
',' relation
539 $1->mappings.append
(Identity
($3->n_set
()));
540 $1->mappings
[$1->mappings.size
()].compress
();
541 $1->ispaces.append
(*$3);
542 $1->ispaces
[$1->ispaces.size
()].compress
();
546 | relation
':' relation
548 RelTuplePair
*rtp
= new RelTuplePair
;
549 rtp
->mappings.append
(*$1);
550 rtp
->mappings
[rtp
->mappings.size
()].compress
();
551 rtp
->ispaces.append
(*$3);
552 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
559 RelTuplePair
*rtp
= new RelTuplePair
;
560 rtp
->mappings.append
(Identity
($1->n_set
()));
561 rtp
->mappings
[rtp
->mappings.size
()].compress
();
562 rtp
->ispaces.append
(*$1);
563 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
569 statementInfoResult
: statementInfoList
571 /* | ASSERT_UNSAT statementInfoResult
573 * DoDebug2("Debug info requested in input", *($2));
576 | TRANS_IS relation statementInfoResult
577 { $$
= &Trans_IS
(*($3), *($2));
580 | SET_MMAP INT partialwrites statementInfoResult
581 { $$
= &Set_MMap
(*($4), $2, *($3));
584 | UNROLL_IS INT INT INT statementInfoResult
585 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
586 | PEEL_IS INT INT relation statementInfoResult
587 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
590 | PEEL_IS INT INT relation
',' relation statementInfoResult
591 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
597 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
600 | statementInfoList
',' statementInfo
{ $$
= $1;
605 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
607 $$
->stm
= *($2); delete
$2;
608 $$
->IS
= *($4); delete
$4;
609 $$
->map
= *($6); delete
$6;
611 |
'[' STRING
',' relation
',' partialwrites
']'
613 $$
->stm
= *($2); delete
$2;
614 $$
->IS
= *($4); delete
$4;
615 $$
->map
= *($6); delete
$6;
619 partialwrites
: partialwrites
',' partialwrite
621 $$
->partials.append
(*($3)); delete
$3;
623 | partialwrite
{ $$
= new MMap
;
624 $$
->partials.append
(*($1)); delete
$1;
628 partialwrite
: STRING
'[' relation
']' ',' relation
629 { $$
= new PartialMMap
;
630 $$
->mapping
= *($6); delete
$6;
631 $$
->bounds
= *($3); delete
$3;
632 $$
->var
= *($1); delete
$1;
634 | STRING
',' relation
{ $$
= new PartialMMap
;
635 $$
->mapping
= *($3); delete
$3;
636 $$
->bounds
= Relation
::True
(0);
637 $$
->var
= *($1); delete
$1;
641 reads
: reads
',' oneread
{ $$
= $1;
642 $$
->read.append
(*($3)); delete
$3;
644 | oneread
{ $$
= new stm_info
;
645 $$
->read.append
(*($1)); delete
$1;
649 oneread
: '[' partials
']' { $$
= $2; }
652 partials
: partials
',' partial
{ $$
= $1;
653 $$
->partials.append
(*($3)); delete
$3;
655 | partial
{ $$
= new Read
;
656 $$
->partials.append
(*($1)); delete
$1;
660 partial
: INT
',' relation
{ $$
= new PartialRead
;
662 $$
->dataFlow
= *($3); delete
$3;
666 globVarList: globVarList
',' globVar
670 globVar: VAR
'(' INT
')'
671 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
673 { globalDecls
->extend
($1); free
($1); }
676 relation
: OPEN_BRACE
677 { relationDecl
= new Declaration_Site
(); }
681 if
(omega_calc_debug
) {
682 fprintf
(DebugFile
,"Built relation:\n");
683 $$
->prefix_print
(DebugFile
);
685 current_Declaration_Site
= globalDecls
;
690 if
(relationMap
(s
) == 0) {
691 fprintf
(stderr
,"Variable %s not declared\n",$1);
697 $$
= new Relation
(*relationMap
(s
));
699 |
'(' relation
')' {$$
= $2;}
700 | relation
'+' %prec OMEGA_P9
701 { $$
= new Relation
();
702 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
705 | relation
'*' %prec OMEGA_P9
706 { $$
= new Relation
();
707 int vars
= $1->n_inp
();
708 *$$
= Union
(Identity
(vars
),
709 TransitiveClosure
(*$1, 1,Relation
::Null
()));
712 | relation
'+' WITHIN relation %prec OMEGA_P9
713 {$$
= new Relation
();
714 *$$
= TransitiveClosure
(*$1, 1,*$4);
718 | MINIMIZE_RANGE relation %prec OMEGA_P8
722 r
= Join
(r
,LexForward
($2->n_out
()));
724 *$$
= Difference
(o
,r
);
727 | MAXIMIZE_RANGE relation %prec OMEGA_P8
731 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
733 *$$
= Difference
(o
,r
);
736 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
740 r
= Join
(LexForward
($2->n_inp
()),r
);
742 *$$
= Difference
(o
,r
);
745 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
749 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
751 *$$
= Difference
(o
,r
);
754 | MAXIMIZE relation %prec OMEGA_P8
759 *$$
= Cross_Product
(Relation
(*$2),c
);
761 assert
($$
->n_inp
() ==$$
->n_out
());
762 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
764 | MINIMIZE relation %prec OMEGA_P8
769 *$$
= Cross_Product
(Relation
(*$2),c
);
771 assert
($$
->n_inp
() ==$$
->n_out
());
772 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
774 | FARKAS relation %prec OMEGA_P8
777 *$$
= Farkas
(*$2, Basic_Farkas
);
780 | DECOUPLED_FARKAS relation %prec OMEGA_P8
783 *$$
= Farkas
(*$2, Decoupled_Farkas
);
786 | relation
'@' %prec OMEGA_P9
787 { $$
= new Relation
();
788 *$$
= ConicClosure
(*$1);
791 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
792 { $$
= new Relation
();
793 *$$
= Project_Sym
(*$2);
796 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
797 { $$
= new Relation
();
798 *$$
= Project_On_Sym
(*$2);
801 | DIFFERENCE relation %prec OMEGA_P8
802 { $$
= new Relation
();
806 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
807 { $$
= new Relation
();
808 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
811 | OMEGA_DOMAIN relation %prec OMEGA_P8
812 { $$
= new Relation
();
816 | VENN relation %prec OMEGA_P8
817 { $$
= new Relation
();
818 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
821 | VENN relation GIVEN relation %prec OMEGA_P8
822 { $$
= new Relation
();
823 *$$
= VennDiagramForm
(*$2,*$4);
827 | CONVEX_HULL relation %prec OMEGA_P8
828 { $$
= new Relation
();
829 *$$
= ConvexHull
(*$2);
832 | POSITIVE_COMBINATION relation %prec OMEGA_P8
833 { $$
= new Relation
();
834 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
837 | CONVEX_COMBINATION relation %prec OMEGA_P8
838 { $$
= new Relation
();
839 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
842 | PAIRWISE_CHECK relation %prec OMEGA_P8
843 { $$
= new Relation
();
844 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
847 | CONVEX_CHECK relation %prec OMEGA_P8
848 { $$
= new Relation
();
849 *$$
= CheckForConvexRepresentation
(*$2);
852 | AFFINE_HULL relation %prec OMEGA_P8
853 { $$
= new Relation
();
854 *$$
= AffineHull
(*$2);
857 | CONIC_HULL relation %prec OMEGA_P8
858 { $$
= new Relation
();
859 *$$
= ConicHull
(*$2);
862 | LINEAR_HULL relation %prec OMEGA_P8
863 { $$
= new Relation
();
864 *$$
= LinearHull
(*$2);
867 | HULL relation %prec OMEGA_P8
868 { $$
= new Relation
();
869 *$$
= Hull
(*$2,false
,1,Null_Relation
());
872 | HULL relation GIVEN relation %prec OMEGA_P8
873 { $$
= new Relation
();
874 *$$
= Hull
(*$2,false
,1,*$4);
878 | APPROX relation %prec OMEGA_P8
879 { $$
= new Relation
();
880 *$$
= Approximate
(*$2);
883 | RANGE relation %prec OMEGA_P8
884 { $$
= new Relation
();
888 | INVERSE relation %prec OMEGA_P8
889 { $$
= new Relation
();
893 | COMPLEMENT relation %prec OMEGA_P8
894 { $$
= new Relation
();
895 *$$
= Complement
(*$2);
898 | GIST relation GIVEN relation %prec OMEGA_P8
899 { $$
= new Relation
();
900 *$$
= Gist
(*$2,*$4,1);
904 | relation
'(' relation
')'
905 { $$
= new Relation
();
906 *$$
= Composition
(*$1,*$3);
910 | relation COMPOSE relation
911 { $$
= new Relation
();
912 *$$
= Composition
(*$1,*$3);
916 | relation CARRIED_BY INT
917 { $$
= new Relation
();
918 *$$
= After
(*$1,$3,$3);
920 (*$$
).prefix_print
(stdout
);
922 | relation JOIN relation
923 { $$
= new Relation
();
924 *$$
= Composition
(*$3,*$1);
928 | relation RESTRICT_RANGE relation
929 { $$
= new Relation
();
930 *$$
= Restrict_Range
(*$1,*$3);
934 | relation RESTRICT_DOMAIN relation
935 { $$
= new Relation
();
936 *$$
= Restrict_Domain
(*$1,*$3);
940 | relation INTERSECTION relation
941 { $$
= new Relation
();
942 *$$
= Intersection
(*$1,*$3);
946 | relation
'-' relation %prec INTERSECTION
947 { $$
= new Relation
();
948 *$$
= Difference
(*$1,*$3);
952 | relation UNION relation
953 { $$
= new Relation
();
954 *$$
= Union
(*$1,*$3);
958 | relation
'*' relation
959 { $$
= new Relation
();
960 *$$
= Cross_Product
(*$1,*$3);
964 | SUPERSETOF relation
965 { $$
= new Relation
();
966 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
970 { $$
= new Relation
();
971 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
974 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
975 { $$
= new Relation
();
976 *$$
= Upper_Bound
(*$2);
979 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
980 { $$
= new Relation
();
981 *$$
= Lower_Bound
(*$2);
985 { $$
= new Relation
();
986 *$$
= Sample_Solution
(*$2);
989 | SYM_SAMPLE relation
990 { $$
= new Relation
();
991 *$$
= Symbolic_Solution
(*$2);
994 | reachable_of
{ $$
= $1; }
995 | ASSERT_UNSAT relation
997 if
(($2)->is_satisfiable
())
999 fprintf
(stderr
,"assert_unsatisfiable failed on ");
1000 ($2)->print_with_subs
(stderr
);
1009 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
1010 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
1011 Relation
* r
= new Relation
($1->size
,$4->size
);
1013 F_And
*f
= r
->add_and
();
1015 for
(i
=1;i
<=$1->size
;i
++) {
1016 $1->vars
[i
]->vid
= r
->input_var
(i
);
1017 if
(!$1->vars
[i
]->anonymous
)
1018 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
1020 for
(i
=1;i
<=$4->size
;i
++) {
1021 $4->vars
[i
]->vid
= r
->output_var
(i
);
1022 if
(!$4->vars
[i
]->anonymous
)
1023 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
1025 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1026 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1027 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1028 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
1029 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
1030 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
1031 if
($6) $6->install
(f
);
1036 | tupleDeclaration optionalFormula
{
1037 Relation
* r
= new Relation
($1->size
);
1039 F_And
*f
= r
->add_and
();
1041 for
(i
=1;i
<=$1->size
;i
++) {
1042 $1->vars
[i
]->vid
= r
->set_var
(i
);
1043 if
(!$1->vars
[i
]->anonymous
)
1044 r
->name_set_var
(i
,$1->vars
[i
]->stripped_name
);
1046 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1047 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1048 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1049 if
($2) $2->install
(f
);
1054 Relation
* r
= new Relation
(0,0);
1055 F_And
*f
= r
->add_and
();
1062 optionalFormula
: formula_sep formula
{ $$
= $2; }
1073 if
(currentTupleDescriptor
)
1074 delete currentTupleDescriptor
;
1075 currentTupleDescriptor
= new tupleDescriptor
;
1078 '[' optionalTupleVarList
']'
1079 {$$
= currentTupleDescriptor
; currentTupleDescriptor
= NULL
; }
1082 optionalTupleVarList
:
1084 | optionalTupleVarList
',' tupleVar
1088 tupleVar
: VAR %prec OMEGA_P10
1089 { Declaration_Site
*ds
= defined
($1);
1090 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1092 Variable_Ref
* v
= lookupScalar
($1);
1094 if
(ds
!= globalDecls
)
1095 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1097 currentTupleDescriptor
->extend
(new Exp
(v
));
1103 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1104 | exp %prec OMEGA_P1
1105 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1106 | exp
':' exp %prec OMEGA_P1
1107 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1108 | exp
':' exp
':' INT %prec OMEGA_P1
1109 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1113 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1114 | VAR
{ $$
= new VarList
;
1120 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1121 foreach
(s
,char *, *$1, delete s
);
1126 /* variable declaration with optional brackets */
1128 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1129 |
'[' varDecl
']' { $$
= $2; }
1132 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1133 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1134 | constraintChain
{ $$
= $1; }
1135 |
'(' formula
')' { $$
= $2; }
1136 | NOT formula
{ $$
= new AST_Not
($2); }
1137 | start_exists varDeclOptBrackets exists_sep formula end_quant
1138 { $$
= new AST_exists
($2,$4); }
1139 | start_forall varDeclOptBrackets forall_sep formula end_quant
1140 { $$
= new AST_forall
($2,$4); }
1143 start_exists
: '(' EXISTS
1152 start_forall
: '(' FORALL
1163 expList
: exp
',' expList
1174 constraintChain
: expList REL_OP expList
1175 { $$
= new AST_constraints
($1,$2,$3); }
1176 | expList REL_OP constraintChain
1177 { $$
= new AST_constraints
($1,$2,$3); }
1182 { Variable_Ref
* v
= lookupScalar
($1);
1187 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1189 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1190 else v
= functionOfOutput
[$1];
1192 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1199 |
'(' exp
')' { $$
= $2;}
1205 argumentList
',' VAR
{
1206 Variable_Ref
* v
= lookupScalar
($3);
1209 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1210 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1216 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1219 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1220 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1228 exp
: INT
{$$
= new Exp
($1);}
1229 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1230 | simpleExp
{ $$
= $1; }
1231 |
'-' exp %prec
'*' { $$
= negate
($2);}
1232 | exp
'+' exp
{ $$
= add
($1,$3);}
1233 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1234 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1239 REACHABLE_FROM nodeNameList nodeSpecificationList
1241 Dynamic_Array1
<Relation
> *final
=
1242 Reachable_Nodes
(reachable_info
);
1248 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1250 Dynamic_Array1
<Relation
> *final
=
1251 Reachable_Nodes
(reachable_info
);
1252 int index
= reachable_info
->node_names.index
(String
($2));
1253 assert
(index
!= 0 && "No such node");
1255 *$$
= (*final
)[index
];
1257 delete reachable_info
;
1263 nodeNameList: '(' realNodeNameList
')'
1264 { int sz
= reachable_info
->node_names.size
();
1265 reachable_info
->node_arity.reallocate
(sz
);
1266 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1267 reachable_info
->start_nodes.resize
(sz
+1);
1271 realNodeNameList: realNodeNameList
',' VAR
1272 { reachable_info
->node_names.append
(String
($3));
1274 | VAR
{ reachable_info
= new reachable_information
;
1275 reachable_info
->node_names.append
(String
($1));
1280 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1283 int n_nodes
= reachable_info
->node_names.size
();
1284 Tuple
<int> &arity
= reachable_info
->node_arity
;
1285 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1287 /* fixup unspecified transitions to be false */
1289 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1290 for
(i
= 1; i
<= n_nodes
; i
++)
1291 for
(j
= 1; j
<= n_nodes
; j
++)
1292 if
(! transitions
[i
][j
].is_null
()) {
1293 int in_arity
= transitions
[i
][j
].n_inp
();
1294 int out_arity
= transitions
[i
][j
].n_out
();
1295 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1296 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1297 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1299 "Arity mismatch in node transition: %s -> %s",
1300 (const char *) reachable_info
->node_names
[i
],
1301 (const char *) reachable_info
->node_names
[j
]);
1306 for
(i
= 1; i
<= n_nodes
; i
++)
1307 if
(arity
[i
] < 0) arity
[i
] = 0;
1308 /* Fill in false relations */
1309 for
(i
= 1; i
<= n_nodes
; i
++)
1310 for
(j
= 1; j
<= n_nodes
; j
++)
1311 if
(transitions
[i
][j
].is_null
())
1312 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1315 /* fixup unused start node positions */
1316 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1317 for
(i
= 1; i
<= n_nodes
; i
++)
1318 if
(nodes
[i
].is_null
())
1319 nodes
[i
] = Relation
::False
(arity
[i
]);
1321 if
(nodes
[i
].n_set
() != arity
[i
]){
1322 fprintf
(stderr
,"Arity mismatch in start node %s",
1323 (const char *) reachable_info
->node_names
[i
]);
1330 realNodeSpecificationList:
1331 realNodeSpecificationList
',' VAR
':' relation
1332 { int n_nodes
= reachable_info
->node_names.size
();
1333 int index
= reachable_info
->node_names.index
($3);
1334 assert
(index
!= 0 && index
<= n_nodes
);
1335 reachable_info
->start_nodes
[index
] = *$5;
1339 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1340 { int n_nodes
= reachable_info
->node_names.size
();
1341 int from_index
= reachable_info
->node_names.index
($3);
1342 int to_index
= reachable_info
->node_names.index
($5);
1343 assert
(from_index
!= 0 && to_index
!= 0);
1344 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1345 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1350 | VAR GOES_TO VAR
':' relation
1351 { int n_nodes
= reachable_info
->node_names.size
();
1352 int from_index
= reachable_info
->node_names.index
($1);
1353 int to_index
= reachable_info
->node_names.index
($3);
1354 assert
(from_index
!= 0 && to_index
!= 0);
1355 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1356 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1362 { int n_nodes
= reachable_info
->node_names.size
();
1363 int index
= reachable_info
->node_names.index
($1);
1364 assert
(index
!= 0 && index
<= n_nodes
);
1365 reachable_info
->start_nodes
[index
] = *$3;
1373 #if !defined(OMIT_GETRUSAGE)
1374 #include <sys/types.h>
1375 #include <sys/time.h>
1376 #include <sys/resource.h>
1378 struct rusage start_time
;
1381 #if defined BRAIN_DAMAGED_FREE
1387 void *realloc
(void *p
, size_t s
)
1389 return realloc
((malloc_t
) p
, s
);
1393 #if ! defined(OMIT_GETRUSAGE)
1395 extern
"C" int getrusage
(int, struct rusage
*);
1398 void start_clock
( void )
1400 getrusage
(RUSAGE_SELF
, &start_time
);
1403 int clock_diff
( void )
1405 struct rusage current_time
;
1406 getrusage
(RUSAGE_SELF
, ¤t_time
);
1407 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1408 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1412 void printUsage
(FILE *outf
, char **argv
) {
1413 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
);
1416 int omega_calc_debug
;
1419 int main
(int argc
, char **argv
){
1420 redundant_conj_level
= 2;
1421 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1426 char * fileName
= 0;
1428 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1430 calc_all_debugging_off
();
1433 DebugFile
= fopen
("/dev/null","w");
1436 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1438 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1441 setbuf
(DebugFile
,0);
1444 closure_presburger_debug
= 0;
1446 setOutputFile
(DebugFile
);
1449 for
(i
=1; i
<argc
; i
++) {
1450 if
(argv
[i
][0] == '-') {
1452 while
((c
=argv
[i
][j
++]) != 0) {
1455 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1456 printUsage
(stderr
,argv
);
1462 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1463 while
(argv
[i
][j
] != 0) j
++;
1468 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1469 while
(argv
[i
][j
] != 0) j
++;
1473 redundant_conj_level
= 1;
1475 // Other future options go here
1477 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1478 printUsage
(stderr
,argv
);
1484 // Make sure this is a file name
1486 fprintf
(stderr
,"\nCan only handle a single input file\n");
1487 printUsage
(stderr
,argv
);
1491 yyin
= fopen
(fileName
, "r");
1493 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1494 printUsage
(stderr
,argv
);
1502 initializeScanBuffer
();
1503 currentTupleDescriptor
= NULL
;
1508 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1509 {delete r
; relationMap
[cs
]=0;});
1515 Relation LexForward
(int n
) {
1517 F_Or
*f
= r.add_or
();
1518 for
(int i
=1; i
<= n
; i
++) {
1519 F_And
*g
= f
->add_and
();
1520 for
(int j
=1;j
<i
;j
++) {
1521 EQ_Handle e
= g
->add_EQ
();
1522 e.update_coef
(r.input_var
(j
),-1);
1523 e.update_coef
(r.output_var
(j
),1);
1526 GEQ_Handle e
= g
->add_GEQ
();
1527 e.update_coef
(r.input_var
(i
),-1);
1528 e.update_coef
(r.output_var
(i
),1);