4 #define compilingParser
5 #include <basic/Dynamic_Array.h>
6 #include <code_gen/code_gen.h>
7 #include <code_gen/spmd.h>
8 #include <omega/library_version.h>
10 #include <omega_calc/yylex.h>
11 #include <omega/hull.h>
12 #include <omega/calc_debug.h>
13 #include <basic/Exit.h>
14 #include <omega/closure.h>
15 #include <omega/reach.h>
16 #include <code_gen/mmap-codegen.h>
17 #include <code_gen/mmap-util.h>
20 #include <sys/resource.h>
22 #include <barvinok/bernstein.h>
27 #define CALC_VERSION_STRING "Omega Calculator v1.2"
29 #define DEBUG_FILE_NAME "./oc.out"
32 Map
<Const_String
,Relation
*> relationMap
((Relation
*)0);
33 static int redundant_conj_level
;
35 #if defined BRAIN_DAMAGED_FREE
37 void *realloc
(void *p
, size_t s
);
40 #if !defined(OMIT_GETRUSAGE)
41 void start_clock
( void );
42 int clock_diff
( void );
43 bool anyTimingDone
= false
;
48 Argument_Tuple currentTuple
= Input_Tuple
;
49 char *currentVar
= NULL
;
51 Relation LexForward
(int n
);
54 reachable_information
*reachable_info
;
56 Relation
*build_relation
(tupleDescriptor
*tuple
, AST
* ast
)
58 Relation
* r
= new Relation
(tuple
->size
);
60 F_And
*f
= r
->add_and
();
62 for
(i
=1;i
<=tuple
->size
;i
++) {
63 tuple
->vars
[i
]->vid
= r
->set_var
(i
);
64 if
(!tuple
->vars
[i
]->anonymous
)
65 r
->name_set_var
(i
,tuple
->vars
[i
]->stripped_name
);
67 foreach
(e
,Exp
*,tuple
->eq_constraints
, install_eq
(f
,e
,0));
68 foreach
(e
,Exp
*,tuple
->geq_constraints
, install_geq
(f
,e
,0));
69 foreach
(c
,strideConstraint
*,tuple
->stride_constraints
, install_stride
(f
,c
));
70 if
(ast
) ast
->install
(f
);
76 Map
<Variable_Ref
*, GiNaC
::ex
> *variableMap
;
82 %token
<INT_VALUE
> INT
83 %token
<STRING_VALUE
> STRING
84 %token OPEN_BRACE CLOSE_BRACE
90 %token OMEGA_DOMAIN RANGE
91 %token DIFFERENCE DIFFERENCE_TO_RELATION
92 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
93 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
94 %token MAXIMIZE_RANGE MINIMIZE_RANGE
95 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
98 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
99 %token UNION INTERSECTION
100 %token VERTICAL_BAR SUCH_THAT
101 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
102 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
103 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
104 %token
<REL_OPERATOR
> REL_OP
105 %token RESTRICT_DOMAIN RESTRICT_RANGE
106 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
107 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
109 %token CARD RANKING COUNT_LEXSMALLER
113 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
115 %nonassoc ASSERT_UNSAT
116 %left UNION OMEGA_P1
'+' '-'
117 %nonassoc SUPERSETOF SUBSETOF
118 %left OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE
119 %left INTERSECTION OMEGA_P3
'*' '@'
124 %left COMPOSE JOIN CARRIED_BY
125 %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
130 %right CARD RANKING COUNT_LEXSMALLER
134 %type
<INT_VALUE
> effort
135 %type
<EXP
> exp simpleExp
136 %type
<EXP_LIST
> expList
137 %type
<VAR_LIST
> varList
138 %type
<ARGUMENT_TUPLE
> argumentList
139 %type
<ASTP
> formula optionalFormula
140 %type
<ASTCP
> constraintChain
141 %type
<TUPLE_DESCRIPTOR
> tupleDeclaration
142 %type
<DECLARATION_SITE
> varDecl varDeclOptBrackets
143 %type
<RELATION
> relation builtRelation context
144 %type
<RELATION
> reachable_of
145 %type
<REL_TUPLE_PAIR
> relPairList
146 %type
<REL_TUPLE_TRIPLE
> relTripList
147 %type
<RELATION_ARRAY_1D
> reachable
148 %type
<STM_INFO_TUPLE
> statementInfoList statementInfoResult
149 %type
<STM_INFO
> statementInfo
150 %type
<STM_INFO
> reads
152 %type
<READ
> partials
153 %type
<PREAD
> partial
154 %type
<MMAP
> partialwrites
155 %type
<PMMAP
> partialwrite
156 %type
<POLYFUNC
> polyfunc
157 %type
<POLYNOMIAL
> polynomial
167 Argument_Tuple ARGUMENT_TUPLE
;
168 AST_constraints
*ASTCP
;
169 Declaration_Site
* DECLARATION_SITE
;
171 tupleDescriptor
* TUPLE_DESCRIPTOR
;
172 RelTuplePair
* REL_TUPLE_PAIR
;
173 RelTupleTriple
* REL_TUPLE_TRIPLE
;
174 Dynamic_Array2
<Relation
> * RELATION_ARRAY_2D
;
175 Dynamic_Array1
<Relation
> * RELATION_ARRAY_1D
;
176 Tuple
<String
> *STRING_TUPLE
;
177 String
*STRING_VALUE
;
178 Tuple
<stm_info
> *STM_INFO_TUPLE
;
185 GiNaC
::ex
*POLYNOMIAL
;
196 inputSequence
: inputItem
197 | inputSequence
{ assert
( current_Declaration_Site
== globalDecls
);}
204 /* Kill all the local declarations -- ejr */
207 Declaration_Site
*ds1
, *ds2
;
208 for
(ds1
= current_Declaration_Site
; ds1
!= globalDecls
;) {
213 current_Declaration_Site
= globalDecls
;
214 yyerror("skipping to statement end");
216 | SYMBOLIC globVarList
';'
219 | VAR
{ currentVar
= $1; } IS_ASSIGNED relation
';'
222 $4->simplify
(min
(2,redundant_conj_level
),4);
223 Relation
*r
= relationMap
((Const_String
)$1);
225 relationMap
[(Const_String
)$1] = $4;
232 $1->simplify
(redundant_conj_level
,4);
233 $1->print_with_subs
(stdout
);
237 | TIME relation
';' {
239 #if defined(OMIT_GETRUSAGE)
240 printf
("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
248 bool SKIP_FULL_CHECK
= getenv
("OC_TIMING_SKIP_FULL_CHECK");
249 ($2)->and_with_GEQ
();
251 for
(t
=1;t
<=100;t
++) {
255 int copyTime
= clock_diff
();
257 for
(t
=1;t
<=100;t
++) {
262 int simplifyTime
= clock_diff
() -copyTime
;
264 if
(!SKIP_FULL_CHECK
)
267 for
(t
=1;t
<=100;t
++) {
273 int excessiveTime
= clock_diff
() - copyTime
;
274 printf
("Times (in microseconds): \n");
275 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
276 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
278 R.print_with_subs
(stdout
);
280 if
(!SKIP_FULL_CHECK
)
282 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
284 R2.print_with_subs
(stdout
);
287 if
(!anyTimingDone
) {
296 printf
("WARNING: The Omega calculator was compiled with options that force\n");
297 printf
("it to perform additional consistency and error checks\n");
298 printf
("that may slow it down substantially\n");
301 printf
("NOTE: These times relect the time of the current _implementation_\n");
302 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
303 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
304 printf
("request that send your test cases to us to allow us to determine if the \n");
305 printf
("times are appropriate, and if the way you are using the Omega library to \n");
306 printf
("solve your problem is the most effective way.\n");
309 printf
("Also, please be aware that over the past two years, we have focused our \n");
310 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
311 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
312 printf
("was substantially faster on the limited domain it handled.\n");
314 printf
(" Thanks, \n");
315 printf
(" the Omega Team \n");
317 anyTimingDone
= true
;
321 | TIMECLOSURE relation
';' {
323 #if defined(OMIT_GETRUSAGE)
324 printf
("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
330 ($2)->and_with_GEQ
();
332 for
(t
=1;t
<=100;t
++) {
336 int copyTime
= clock_diff
();
338 for
(t
=1;t
<=100;t
++) {
343 int simplifyTime
= clock_diff
() -copyTime
;
346 for
(t
=1;t
<=100;t
++) {
349 Rclosed
= TransitiveClosure
(Rclosed
, 1,Relation
::Null
());
351 int closureTime
= clock_diff
() - copyTime
;
354 for
(t
=1;t
<=100;t
++) {
359 int excessiveTime
= clock_diff
() - copyTime
;
360 printf
("Times (in microseconds): \n");
361 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
362 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
364 R.print_with_subs
(stdout
);
366 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
368 R2.print_with_subs
(stdout
);
369 printf
("%5d us to do the transitive closure, obtaining: \n\t",
371 Rclosed.print_with_subs
(stdout
);
373 if
(!anyTimingDone
) {
382 printf
("WARNING: The Omega calculator was compiled with options that force\n");
383 printf
("it to perform additional consistency and error checks\n");
384 printf
("that may slow it down substantially\n");
387 printf
("NOTE: These times relect the time of the current _implementation_\n");
388 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
389 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
390 printf
("request that send your test cases to us to allow us to determine if the \n");
391 printf
("times are appropriate, and if the way you are using the Omega library to \n");
392 printf
("solve your problem is the most effective way.\n");
395 printf
("Also, please be aware that over the past two years, we have focused our \n");
396 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
397 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
398 printf
("was substantially faster on the limited domain it handled.\n");
400 printf
(" Thanks, \n");
401 printf
(" the Omega Team \n");
403 anyTimingDone
= true
;
409 | relation SUBSET relation
';' {
411 int c
= Must_Be_Subset
(*$1, *$3);
412 printf
("\n%s\n", c ?
"True" : "False");
416 | CODEGEN effort relPairList context
';'
419 String s
= MMGenerateCode
($3->mappings
, $3->ispaces
,*$4,$2);
422 printf
("%s\n", (const char *) s
);
424 | TCODEGEN effort statementInfoResult context
';'
427 String s
= tcodegen
($2, *($3), *($4));
430 printf
("%s\n", (const char *) s
);
432 /* | TCODEGEN NOT effort statementInfoResult context';'
435 * String s = tcodegen($3, *($4), *($5), false);
438 * printf("%s\n", (const char *) s);
441 | SPMD blockAndProcsAndEffort relTripList
';'
443 Tuple
<Free_Var_Decl
*> lowerBounds
(0), upperBounds
(0), my_procs
(0);
444 Tuple
<spmd_stmt_info
*> names
(0);
447 int nr_statements
= $3->space.size
();
449 for
(int i
= 1; i
<= $3->space
[1].n_out
(); i
++)
451 lowerBounds.append
(new Free_Var_Decl
("lb" + itoS
(i
)));
452 upperBounds.append
(new Free_Var_Decl
("ub" + itoS
(i
)));
453 my_procs.append
(new Free_Var_Decl
("my_proc" + itoS
(i
)));
456 for
(int p
= 1; p
<= nr_statements
; p
++)
457 names.append
(new numbered_stmt_info
(p
-1, Identity
($3->time
[p
].n_out
()),
459 (char *)(const char *)("s"+itoS
(p
-1))));
461 String s
= SPMD_GenerateCode
("", $3->space
, $3->time
, $3->ispaces
,
463 lowerBounds
, upperBounds
, my_procs
,
467 printf
("%s\n", (const char *) s
);
471 Dynamic_Array1
<Relation
> &final
= *$1;
473 int i
,n_nodes
= reachable_info
->node_names.size
();
474 for
(i
= 1; i
<= n_nodes
; i
++) if
(final
[i
].is_upper_bound_satisfiable
()) {
476 fprintf
(stdout
,"Node %s: ",
477 (const char *) (reachable_info
->node_names
[i
]));
478 final
[i
].print_with_subs
(stdout
);
481 fprintf
(stdout
,"No nodes reachable.\n");
483 delete reachable_info
;
485 | CARD relation
';' {
486 evalue
*EP
= count_relation
(*$2);
488 const Variable_ID_Tuple
* globals
= $2->global_decls
();
489 const char **param_names
= new
const char *[globals
->size
()];
491 for
(int i
= 0; i
< globals
->size
(); ++i
)
492 param_names
[i
] = (*globals
)[i
+1]->char_name
();
493 print_evalue
(stdout
, EP
, param_names
);
495 delete
[] param_names
;
500 | RANKING relation
';' {
501 evalue
*EP
= rank_relation
(*$2);
503 const Variable_ID_Tuple
* globals
= $2->global_decls
();
504 int nvar
= $2->n_set
();
505 int n
= nvar
+ globals
->size
();
506 const char **names
= new
const char *[n
];
508 for
(int i
= 0; i
< nvar
; ++i
)
509 names
[i
] = $2->set_var
(i
+1)->char_name
();
510 for
(int i
= 0; i
< globals
->size
(); ++i
)
511 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
512 print_evalue
(stdout
, EP
, names
);
519 | COUNT_LEXSMALLER relation WITHIN relation
';' {
520 evalue
*EP
= count_lexsmaller
(*$2, *$4);
522 const Variable_ID_Tuple
* globals
= $4->global_decls
();
523 int nvar
= $4->n_set
();
524 int n
= nvar
+ globals
->size
();
525 const char **names
= new
const char *[n
];
527 for
(int i
= 0; i
< nvar
; ++i
)
528 names
[i
] = $4->set_var
(i
+1)->char_name
();
529 for
(int i
= 0; i
< globals
->size
(); ++i
)
530 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
531 print_evalue
(stdout
, EP
, names
);
539 | VERTICES relation
';' {
545 relationDecl
= new Declaration_Site
();
546 variableMap
= new Map
<Variable_Ref
*, GiNaC
::ex
>(0);
549 maximize
($3, *variableMap
);
551 current_Declaration_Site
= globalDecls
;
557 relTripList: relTripList
',' relation
':' relation
':' relation
559 $1->space.append
(*$3);
560 $1->time.append
(*$5);
561 $1->ispaces.append
(*$7);
567 | relation
':' relation
':' relation
569 RelTupleTriple
*rtt
= new RelTupleTriple
;
570 rtt
->space.append
(*$1);
571 rtt
->time.append
(*$3);
572 rtt
->ispaces.append
(*$5);
580 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
581 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
582 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
583 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
588 |
'-' INT
{ $$
= -$2; }
591 context
: { $$
= new Relation
();
592 *$$
= Relation
::Null
(); }
593 | GIVEN relation
{$$
= $2; }
596 relPairList: relPairList
',' relation
':' relation
598 $1->mappings.append
(*$3);
599 $1->mappings
[$1->mappings.size
()].compress
();
600 $1->ispaces.append
(*$5);
601 $1->ispaces
[$1->ispaces.size
()].compress
();
606 | relPairList
',' relation
608 $1->mappings.append
(Identity
($3->n_set
()));
609 $1->mappings
[$1->mappings.size
()].compress
();
610 $1->ispaces.append
(*$3);
611 $1->ispaces
[$1->ispaces.size
()].compress
();
615 | relation
':' relation
617 RelTuplePair
*rtp
= new RelTuplePair
;
618 rtp
->mappings.append
(*$1);
619 rtp
->mappings
[rtp
->mappings.size
()].compress
();
620 rtp
->ispaces.append
(*$3);
621 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
628 RelTuplePair
*rtp
= new RelTuplePair
;
629 rtp
->mappings.append
(Identity
($1->n_set
()));
630 rtp
->mappings
[rtp
->mappings.size
()].compress
();
631 rtp
->ispaces.append
(*$1);
632 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
638 statementInfoResult
: statementInfoList
640 /* | ASSERT_UNSAT statementInfoResult
642 * DoDebug2("Debug info requested in input", *($2));
645 | TRANS_IS relation statementInfoResult
646 { $$
= &Trans_IS
(*($3), *($2));
649 | SET_MMAP INT partialwrites statementInfoResult
650 { $$
= &Set_MMap
(*($4), $2, *($3));
653 | UNROLL_IS INT INT INT statementInfoResult
654 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
655 | PEEL_IS INT INT relation statementInfoResult
656 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
659 | PEEL_IS INT INT relation
',' relation statementInfoResult
660 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
666 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
669 | statementInfoList
',' statementInfo
{ $$
= $1;
674 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
676 $$
->stm
= *($2); delete
$2;
677 $$
->IS
= *($4); delete
$4;
678 $$
->map
= *($6); delete
$6;
680 |
'[' STRING
',' relation
',' partialwrites
']'
682 $$
->stm
= *($2); delete
$2;
683 $$
->IS
= *($4); delete
$4;
684 $$
->map
= *($6); delete
$6;
688 partialwrites
: partialwrites
',' partialwrite
690 $$
->partials.append
(*($3)); delete
$3;
692 | partialwrite
{ $$
= new MMap
;
693 $$
->partials.append
(*($1)); delete
$1;
697 partialwrite
: STRING
'[' relation
']' ',' relation
698 { $$
= new PartialMMap
;
699 $$
->mapping
= *($6); delete
$6;
700 $$
->bounds
= *($3); delete
$3;
701 $$
->var
= *($1); delete
$1;
703 | STRING
',' relation
{ $$
= new PartialMMap
;
704 $$
->mapping
= *($3); delete
$3;
705 $$
->bounds
= Relation
::True
(0);
706 $$
->var
= *($1); delete
$1;
710 reads
: reads
',' oneread
{ $$
= $1;
711 $$
->read.append
(*($3)); delete
$3;
713 | oneread
{ $$
= new stm_info
;
714 $$
->read.append
(*($1)); delete
$1;
718 oneread
: '[' partials
']' { $$
= $2; }
721 partials
: partials
',' partial
{ $$
= $1;
722 $$
->partials.append
(*($3)); delete
$3;
724 | partial
{ $$
= new Read
;
725 $$
->partials.append
(*($1)); delete
$1;
729 partial
: INT
',' relation
{ $$
= new PartialRead
;
731 $$
->dataFlow
= *($3); delete
$3;
735 globVarList: globVarList
',' globVar
739 globVar: VAR
'(' INT
')'
740 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
742 { globalDecls
->extend
($1); free
($1); }
745 polynomial
: INT
{ $$
= new GiNaC
::ex
($1); }
747 Variable_Ref
*v
= lookupScalar
($1);
750 if
((*variableMap
)(v
) == 0)
751 (*variableMap
)[v
] = GiNaC
::symbol
(std
::string(v
->name
));
752 $$
= new GiNaC
::ex
((*variableMap
)[v
]);
754 |
'(' polynomial
')' { $$
= $2; }
755 |
'-' polynomial %prec
'*' {
756 $$
= new GiNaC
::ex
(-*$2);
759 | polynomial
'+' polynomial
{
760 $$
= new GiNaC
::ex
(*$1 + *$3);
764 | polynomial
'-' polynomial
{
765 $$
= new GiNaC
::ex
(*$1 - *$3);
769 | polynomial
'/' polynomial
{
770 $$
= new GiNaC
::ex
(*$1 / *$3);
774 | polynomial
'*' polynomial
{
775 $$
= new GiNaC
::ex
(*$1 * *$3);
781 polyfunc
: OPEN_BRACE
782 tupleDeclaration GOES_TO polynomial optionalFormula CLOSE_BRACE
{
783 Relation
*r
= build_relation
($2, $5);
792 relation
: OPEN_BRACE
793 { relationDecl
= new Declaration_Site
(); }
797 if
(omega_calc_debug
) {
798 fprintf
(DebugFile
,"Built relation:\n");
799 $$
->prefix_print
(DebugFile
);
801 current_Declaration_Site
= globalDecls
;
806 if
(relationMap
(s
) == 0) {
807 fprintf
(stderr
,"Variable %s not declared\n",$1);
813 $$
= new Relation
(*relationMap
(s
));
815 |
'(' relation
')' {$$
= $2;}
816 | relation
'+' %prec OMEGA_P9
817 { $$
= new Relation
();
818 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
821 | relation
'*' %prec OMEGA_P9
822 { $$
= new Relation
();
823 int vars
= $1->n_inp
();
824 *$$
= Union
(Identity
(vars
),
825 TransitiveClosure
(*$1, 1,Relation
::Null
()));
828 | relation
'+' WITHIN relation %prec OMEGA_P9
829 {$$
= new Relation
();
830 *$$
= TransitiveClosure
(*$1, 1,*$4);
834 | MINIMIZE_RANGE relation %prec OMEGA_P8
838 r
= Join
(r
,LexForward
($2->n_out
()));
840 *$$
= Difference
(o
,r
);
843 | MAXIMIZE_RANGE relation %prec OMEGA_P8
847 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
849 *$$
= Difference
(o
,r
);
852 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
856 r
= Join
(LexForward
($2->n_inp
()),r
);
858 *$$
= Difference
(o
,r
);
861 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
865 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
867 *$$
= Difference
(o
,r
);
870 | MAXIMIZE relation %prec OMEGA_P8
875 *$$
= Cross_Product
(Relation
(*$2),c
);
877 assert
($$
->n_inp
() ==$$
->n_out
());
878 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
880 | MINIMIZE relation %prec OMEGA_P8
885 *$$
= Cross_Product
(Relation
(*$2),c
);
887 assert
($$
->n_inp
() ==$$
->n_out
());
888 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
890 | FARKAS relation %prec OMEGA_P8
893 *$$
= Farkas
(*$2, Basic_Farkas
);
896 | DECOUPLED_FARKAS relation %prec OMEGA_P8
899 *$$
= Farkas
(*$2, Decoupled_Farkas
);
902 | relation
'@' %prec OMEGA_P9
903 { $$
= new Relation
();
904 *$$
= ConicClosure
(*$1);
907 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
908 { $$
= new Relation
();
909 *$$
= Project_Sym
(*$2);
912 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
913 { $$
= new Relation
();
914 *$$
= Project_On_Sym
(*$2);
917 | DIFFERENCE relation %prec OMEGA_P8
918 { $$
= new Relation
();
922 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
923 { $$
= new Relation
();
924 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
927 | OMEGA_DOMAIN relation %prec OMEGA_P8
928 { $$
= new Relation
();
932 | VENN relation %prec OMEGA_P8
933 { $$
= new Relation
();
934 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
937 | VENN relation GIVEN relation %prec OMEGA_P8
938 { $$
= new Relation
();
939 *$$
= VennDiagramForm
(*$2,*$4);
943 | CONVEX_HULL relation %prec OMEGA_P8
944 { $$
= new Relation
();
945 *$$
= ConvexHull
(*$2);
948 | POSITIVE_COMBINATION relation %prec OMEGA_P8
949 { $$
= new Relation
();
950 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
953 | CONVEX_COMBINATION relation %prec OMEGA_P8
954 { $$
= new Relation
();
955 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
958 | PAIRWISE_CHECK relation %prec OMEGA_P8
959 { $$
= new Relation
();
960 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
963 | CONVEX_CHECK relation %prec OMEGA_P8
964 { $$
= new Relation
();
965 *$$
= CheckForConvexRepresentation
(*$2);
968 | AFFINE_HULL relation %prec OMEGA_P8
969 { $$
= new Relation
();
970 *$$
= AffineHull
(*$2);
973 | CONIC_HULL relation %prec OMEGA_P8
974 { $$
= new Relation
();
975 *$$
= ConicHull
(*$2);
978 | LINEAR_HULL relation %prec OMEGA_P8
979 { $$
= new Relation
();
980 *$$
= LinearHull
(*$2);
983 | HULL relation %prec OMEGA_P8
984 { $$
= new Relation
();
985 *$$
= Hull
(*$2,false
,1,Null_Relation
());
988 | HULL relation GIVEN relation %prec OMEGA_P8
989 { $$
= new Relation
();
990 *$$
= Hull
(*$2,false
,1,*$4);
994 | APPROX relation %prec OMEGA_P8
995 { $$
= new Relation
();
996 *$$
= Approximate
(*$2);
999 | RANGE relation %prec OMEGA_P8
1000 { $$
= new Relation
();
1004 | INVERSE relation %prec OMEGA_P8
1005 { $$
= new Relation
();
1009 | COMPLEMENT relation %prec OMEGA_P8
1010 { $$
= new Relation
();
1011 *$$
= Complement
(*$2);
1014 | GIST relation GIVEN relation %prec OMEGA_P8
1015 { $$
= new Relation
();
1016 *$$
= Gist
(*$2,*$4,1);
1020 | relation
'(' relation
')'
1021 { $$
= new Relation
();
1022 *$$
= Composition
(*$1,*$3);
1026 | relation COMPOSE relation
1027 { $$
= new Relation
();
1028 *$$
= Composition
(*$1,*$3);
1032 | relation CARRIED_BY INT
1033 { $$
= new Relation
();
1034 *$$
= After
(*$1,$3,$3);
1036 (*$$
).prefix_print
(stdout
);
1038 | relation JOIN relation
1039 { $$
= new Relation
();
1040 *$$
= Composition
(*$3,*$1);
1044 | relation RESTRICT_RANGE relation
1045 { $$
= new Relation
();
1046 *$$
= Restrict_Range
(*$1,*$3);
1050 | relation RESTRICT_DOMAIN relation
1051 { $$
= new Relation
();
1052 *$$
= Restrict_Domain
(*$1,*$3);
1056 | relation INTERSECTION relation
1057 { $$
= new Relation
();
1058 *$$
= Intersection
(*$1,*$3);
1062 | relation
'-' relation %prec INTERSECTION
1063 { $$
= new Relation
();
1064 *$$
= Difference
(*$1,*$3);
1068 | relation UNION relation
1069 { $$
= new Relation
();
1070 *$$
= Union
(*$1,*$3);
1074 | relation
'*' relation
1075 { $$
= new Relation
();
1076 *$$
= Cross_Product
(*$1,*$3);
1080 | SUPERSETOF relation
1081 { $$
= new Relation
();
1082 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
1086 { $$
= new Relation
();
1087 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
1090 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
1091 { $$
= new Relation
();
1092 *$$
= Upper_Bound
(*$2);
1095 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
1096 { $$
= new Relation
();
1097 *$$
= Lower_Bound
(*$2);
1101 { $$
= new Relation
();
1102 *$$
= Sample_Solution
(*$2);
1105 | SYM_SAMPLE relation
1106 { $$
= new Relation
();
1107 *$$
= Symbolic_Solution
(*$2);
1110 | reachable_of
{ $$
= $1; }
1111 | ASSERT_UNSAT relation
1113 if
(($2)->is_satisfiable
())
1115 fprintf
(stderr
,"assert_unsatisfiable failed on ");
1116 ($2)->print_with_subs
(stderr
);
1125 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
1126 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
1127 Relation
* r
= new Relation
($1->size
,$4->size
);
1129 F_And
*f
= r
->add_and
();
1131 for
(i
=1;i
<=$1->size
;i
++) {
1132 $1->vars
[i
]->vid
= r
->input_var
(i
);
1133 if
(!$1->vars
[i
]->anonymous
)
1134 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
1136 for
(i
=1;i
<=$4->size
;i
++) {
1137 $4->vars
[i
]->vid
= r
->output_var
(i
);
1138 if
(!$4->vars
[i
]->anonymous
)
1139 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
1141 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1142 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1143 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1144 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
1145 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
1146 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
1147 if
($6) $6->install
(f
);
1152 | tupleDeclaration optionalFormula
{
1153 $$
= build_relation
($1, $2);
1156 Relation
* r
= new Relation
(0,0);
1157 F_And
*f
= r
->add_and
();
1164 optionalFormula
: formula_sep formula
{ $$
= $2; }
1175 if
(currentTupleDescriptor
)
1176 delete currentTupleDescriptor
;
1177 currentTupleDescriptor
= new tupleDescriptor
;
1180 '[' optionalTupleVarList
']'
1181 {$$
= currentTupleDescriptor
; currentTupleDescriptor
= NULL
; }
1184 optionalTupleVarList
:
1186 | optionalTupleVarList
',' tupleVar
1190 tupleVar
: VAR %prec OMEGA_P10
1191 { Declaration_Site
*ds
= defined
($1);
1192 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1194 Variable_Ref
* v
= lookupScalar
($1);
1196 if
(ds
!= globalDecls
)
1197 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1199 currentTupleDescriptor
->extend
(new Exp
(v
));
1205 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1206 | exp %prec OMEGA_P1
1207 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1208 | exp
':' exp %prec OMEGA_P1
1209 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1210 | exp
':' exp
':' INT %prec OMEGA_P1
1211 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1215 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1216 | VAR
{ $$
= new VarList
;
1222 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1223 foreach
(s
,char *, *$1, free
(s
));
1228 /* variable declaration with optional brackets */
1230 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1231 |
'[' varDecl
']' { $$
= $2; }
1234 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1235 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1236 | constraintChain
{ $$
= $1; }
1237 |
'(' formula
')' { $$
= $2; }
1238 | NOT formula
{ $$
= new AST_Not
($2); }
1239 | start_exists varDeclOptBrackets exists_sep formula end_quant
1240 { $$
= new AST_exists
($2,$4); }
1241 | start_forall varDeclOptBrackets forall_sep formula end_quant
1242 { $$
= new AST_forall
($2,$4); }
1245 start_exists
: '(' EXISTS
1254 start_forall
: '(' FORALL
1265 expList
: exp
',' expList
1276 constraintChain
: expList REL_OP expList
1277 { $$
= new AST_constraints
($1,$2,$3); }
1278 | expList REL_OP constraintChain
1279 { $$
= new AST_constraints
($1,$2,$3); }
1284 { Variable_Ref
* v
= lookupScalar
($1);
1289 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1291 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1292 else v
= functionOfOutput
[$1];
1294 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1301 |
'(' exp
')' { $$
= $2;}
1307 argumentList
',' VAR
{
1308 Variable_Ref
* v
= lookupScalar
($3);
1311 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1312 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1318 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1321 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1322 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1330 exp
: INT
{$$
= new Exp
($1);}
1331 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1332 | simpleExp
{ $$
= $1; }
1333 |
'-' exp %prec
'*' { $$
= negate
($2);}
1334 | exp
'+' exp
{ $$
= add
($1,$3);}
1335 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1336 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1341 REACHABLE_FROM nodeNameList nodeSpecificationList
1343 Dynamic_Array1
<Relation
> *final
=
1344 Reachable_Nodes
(reachable_info
);
1350 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1352 Dynamic_Array1
<Relation
> *final
=
1353 Reachable_Nodes
(reachable_info
);
1354 int index
= reachable_info
->node_names.index
(String
($2));
1355 assert
(index
!= 0 && "No such node");
1357 *$$
= (*final
)[index
];
1359 delete reachable_info
;
1365 nodeNameList: '(' realNodeNameList
')'
1366 { int sz
= reachable_info
->node_names.size
();
1367 reachable_info
->node_arity.reallocate
(sz
);
1368 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1369 reachable_info
->start_nodes.resize
(sz
+1);
1373 realNodeNameList: realNodeNameList
',' VAR
1374 { reachable_info
->node_names.append
(String
($3));
1376 | VAR
{ reachable_info
= new reachable_information
;
1377 reachable_info
->node_names.append
(String
($1));
1382 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1385 int n_nodes
= reachable_info
->node_names.size
();
1386 Tuple
<int> &arity
= reachable_info
->node_arity
;
1387 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1389 /* fixup unspecified transitions to be false */
1391 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1392 for
(i
= 1; i
<= n_nodes
; i
++)
1393 for
(j
= 1; j
<= n_nodes
; j
++)
1394 if
(! transitions
[i
][j
].is_null
()) {
1395 int in_arity
= transitions
[i
][j
].n_inp
();
1396 int out_arity
= transitions
[i
][j
].n_out
();
1397 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1398 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1399 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1401 "Arity mismatch in node transition: %s -> %s",
1402 (const char *) reachable_info
->node_names
[i
],
1403 (const char *) reachable_info
->node_names
[j
]);
1408 for
(i
= 1; i
<= n_nodes
; i
++)
1409 if
(arity
[i
] < 0) arity
[i
] = 0;
1410 /* Fill in false relations */
1411 for
(i
= 1; i
<= n_nodes
; i
++)
1412 for
(j
= 1; j
<= n_nodes
; j
++)
1413 if
(transitions
[i
][j
].is_null
())
1414 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1417 /* fixup unused start node positions */
1418 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1419 for
(i
= 1; i
<= n_nodes
; i
++)
1420 if
(nodes
[i
].is_null
())
1421 nodes
[i
] = Relation
::False
(arity
[i
]);
1423 if
(nodes
[i
].n_set
() != arity
[i
]){
1424 fprintf
(stderr
,"Arity mismatch in start node %s",
1425 (const char *) reachable_info
->node_names
[i
]);
1432 realNodeSpecificationList:
1433 realNodeSpecificationList
',' VAR
':' relation
1434 { int n_nodes
= reachable_info
->node_names.size
();
1435 int index
= reachable_info
->node_names.index
($3);
1436 assert
(index
!= 0 && index
<= n_nodes
);
1437 reachable_info
->start_nodes
[index
] = *$5;
1441 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1442 { int n_nodes
= reachable_info
->node_names.size
();
1443 int from_index
= reachable_info
->node_names.index
($3);
1444 int to_index
= reachable_info
->node_names.index
($5);
1445 assert
(from_index
!= 0 && to_index
!= 0);
1446 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1447 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1452 | VAR GOES_TO VAR
':' relation
1453 { int n_nodes
= reachable_info
->node_names.size
();
1454 int from_index
= reachable_info
->node_names.index
($1);
1455 int to_index
= reachable_info
->node_names.index
($3);
1456 assert
(from_index
!= 0 && to_index
!= 0);
1457 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1458 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1464 { int n_nodes
= reachable_info
->node_names.size
();
1465 int index
= reachable_info
->node_names.index
($1);
1466 assert
(index
!= 0 && index
<= n_nodes
);
1467 reachable_info
->start_nodes
[index
] = *$3;
1475 #if !defined(OMIT_GETRUSAGE)
1476 #include <sys/types.h>
1477 #include <sys/time.h>
1478 #include <sys/resource.h>
1480 struct rusage start_time
;
1483 #if defined BRAIN_DAMAGED_FREE
1489 void *realloc
(void *p
, size_t s
)
1491 return realloc
((malloc_t
) p
, s
);
1495 #if ! defined(OMIT_GETRUSAGE)
1497 extern
"C" int getrusage
(int, struct rusage
*);
1500 void start_clock
( void )
1502 getrusage
(RUSAGE_SELF
, &start_time
);
1505 int clock_diff
( void )
1507 struct rusage current_time
;
1508 getrusage
(RUSAGE_SELF
, ¤t_time
);
1509 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1510 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1514 void printUsage
(FILE *outf
, char **argv
) {
1515 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
);
1518 int omega_calc_debug
;
1521 int main
(int argc
, char **argv
){
1522 redundant_conj_level
= 2;
1523 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1528 char * fileName
= 0;
1530 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1532 calc_all_debugging_off
();
1535 DebugFile
= fopen
("/dev/null","w");
1538 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1540 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1543 setbuf
(DebugFile
,0);
1546 closure_presburger_debug
= 0;
1548 setOutputFile
(DebugFile
);
1551 for
(i
=1; i
<argc
; i
++) {
1552 if
(argv
[i
][0] == '-') {
1554 while
((c
=argv
[i
][j
++]) != 0) {
1557 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1558 printUsage
(stderr
,argv
);
1564 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1565 while
(argv
[i
][j
] != 0) j
++;
1570 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1571 while
(argv
[i
][j
] != 0) j
++;
1575 redundant_conj_level
= 1;
1577 // Other future options go here
1579 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1580 printUsage
(stderr
,argv
);
1586 // Make sure this is a file name
1588 fprintf
(stderr
,"\nCan only handle a single input file\n");
1589 printUsage
(stderr
,argv
);
1593 yyin
= fopen
(fileName
, "r");
1595 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1596 printUsage
(stderr
,argv
);
1604 initializeScanBuffer
();
1605 currentTupleDescriptor
= NULL
;
1610 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1611 {delete r
; relationMap
[cs
]=0;});
1617 Relation LexForward
(int n
) {
1619 F_Or
*f
= r.add_or
();
1620 for
(int i
=1; i
<= n
; i
++) {
1621 F_And
*g
= f
->add_and
();
1622 for
(int j
=1;j
<i
;j
++) {
1623 EQ_Handle e
= g
->add_EQ
();
1624 e.update_coef
(r.input_var
(j
),-1);
1625 e.update_coef
(r.output_var
(j
),1);
1628 GEQ_Handle e
= g
->add_GEQ
();
1629 e.update_coef
(r.input_var
(i
),-1);
1630 e.update_coef
(r.output_var
(i
),1);