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
;
496 free_evalue_refs
(EP
);
501 | RANKING relation
';' {
502 evalue
*EP
= rank_relation
(*$2);
504 const Variable_ID_Tuple
* globals
= $2->global_decls
();
505 int nvar
= $2->n_set
();
506 int n
= nvar
+ globals
->size
();
507 const char **names
= new
const char *[n
];
509 for
(int i
= 0; i
< nvar
; ++i
)
510 names
[i
] = $2->set_var
(i
+1)->char_name
();
511 for
(int i
= 0; i
< globals
->size
(); ++i
)
512 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
513 print_evalue
(stdout
, EP
, names
);
516 free_evalue_refs
(EP
);
521 | COUNT_LEXSMALLER relation WITHIN relation
';' {
522 evalue
*EP
= count_lexsmaller
(*$2, *$4);
524 const Variable_ID_Tuple
* globals
= $4->global_decls
();
525 int nvar
= $4->n_set
();
526 int n
= nvar
+ globals
->size
();
527 const char **names
= new
const char *[n
];
529 for
(int i
= 0; i
< nvar
; ++i
)
530 names
[i
] = $4->set_var
(i
+1)->char_name
();
531 for
(int i
= 0; i
< globals
->size
(); ++i
)
532 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
533 print_evalue
(stdout
, EP
, names
);
536 free_evalue_refs
(EP
);
542 | VERTICES relation
';' {
548 relationDecl
= new Declaration_Site
();
549 variableMap
= new Map
<Variable_Ref
*, GiNaC
::ex
>(0);
552 maximize
($3, *variableMap
);
554 current_Declaration_Site
= globalDecls
;
560 relTripList: relTripList
',' relation
':' relation
':' relation
562 $1->space.append
(*$3);
563 $1->time.append
(*$5);
564 $1->ispaces.append
(*$7);
570 | relation
':' relation
':' relation
572 RelTupleTriple
*rtt
= new RelTupleTriple
;
573 rtt
->space.append
(*$1);
574 rtt
->time.append
(*$3);
575 rtt
->ispaces.append
(*$5);
583 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
584 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
585 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
586 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
591 |
'-' INT
{ $$
= -$2; }
594 context
: { $$
= new Relation
();
595 *$$
= Relation
::Null
(); }
596 | GIVEN relation
{$$
= $2; }
599 relPairList: relPairList
',' relation
':' relation
601 $1->mappings.append
(*$3);
602 $1->mappings
[$1->mappings.size
()].compress
();
603 $1->ispaces.append
(*$5);
604 $1->ispaces
[$1->ispaces.size
()].compress
();
609 | relPairList
',' relation
611 $1->mappings.append
(Identity
($3->n_set
()));
612 $1->mappings
[$1->mappings.size
()].compress
();
613 $1->ispaces.append
(*$3);
614 $1->ispaces
[$1->ispaces.size
()].compress
();
618 | relation
':' relation
620 RelTuplePair
*rtp
= new RelTuplePair
;
621 rtp
->mappings.append
(*$1);
622 rtp
->mappings
[rtp
->mappings.size
()].compress
();
623 rtp
->ispaces.append
(*$3);
624 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
631 RelTuplePair
*rtp
= new RelTuplePair
;
632 rtp
->mappings.append
(Identity
($1->n_set
()));
633 rtp
->mappings
[rtp
->mappings.size
()].compress
();
634 rtp
->ispaces.append
(*$1);
635 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
641 statementInfoResult
: statementInfoList
643 /* | ASSERT_UNSAT statementInfoResult
645 * DoDebug2("Debug info requested in input", *($2));
648 | TRANS_IS relation statementInfoResult
649 { $$
= &Trans_IS
(*($3), *($2));
652 | SET_MMAP INT partialwrites statementInfoResult
653 { $$
= &Set_MMap
(*($4), $2, *($3));
656 | UNROLL_IS INT INT INT statementInfoResult
657 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
658 | PEEL_IS INT INT relation statementInfoResult
659 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
662 | PEEL_IS INT INT relation
',' relation statementInfoResult
663 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
669 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
672 | statementInfoList
',' statementInfo
{ $$
= $1;
677 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
679 $$
->stm
= *($2); delete
$2;
680 $$
->IS
= *($4); delete
$4;
681 $$
->map
= *($6); delete
$6;
683 |
'[' STRING
',' relation
',' partialwrites
']'
685 $$
->stm
= *($2); delete
$2;
686 $$
->IS
= *($4); delete
$4;
687 $$
->map
= *($6); delete
$6;
691 partialwrites
: partialwrites
',' partialwrite
693 $$
->partials.append
(*($3)); delete
$3;
695 | partialwrite
{ $$
= new MMap
;
696 $$
->partials.append
(*($1)); delete
$1;
700 partialwrite
: STRING
'[' relation
']' ',' relation
701 { $$
= new PartialMMap
;
702 $$
->mapping
= *($6); delete
$6;
703 $$
->bounds
= *($3); delete
$3;
704 $$
->var
= *($1); delete
$1;
706 | STRING
',' relation
{ $$
= new PartialMMap
;
707 $$
->mapping
= *($3); delete
$3;
708 $$
->bounds
= Relation
::True
(0);
709 $$
->var
= *($1); delete
$1;
713 reads
: reads
',' oneread
{ $$
= $1;
714 $$
->read.append
(*($3)); delete
$3;
716 | oneread
{ $$
= new stm_info
;
717 $$
->read.append
(*($1)); delete
$1;
721 oneread
: '[' partials
']' { $$
= $2; }
724 partials
: partials
',' partial
{ $$
= $1;
725 $$
->partials.append
(*($3)); delete
$3;
727 | partial
{ $$
= new Read
;
728 $$
->partials.append
(*($1)); delete
$1;
732 partial
: INT
',' relation
{ $$
= new PartialRead
;
734 $$
->dataFlow
= *($3); delete
$3;
738 globVarList: globVarList
',' globVar
742 globVar: VAR
'(' INT
')'
743 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
745 { globalDecls
->extend
($1); free
($1); }
748 polynomial
: INT
{ $$
= new GiNaC
::ex
($1); }
750 Variable_Ref
*v
= lookupScalar
($1);
753 if
((*variableMap
)(v
) == 0)
754 (*variableMap
)[v
] = GiNaC
::symbol
(std
::string(v
->name
));
755 $$
= new GiNaC
::ex
((*variableMap
)[v
]);
757 |
'(' polynomial
')' { $$
= $2; }
758 |
'-' polynomial %prec
'*' {
759 $$
= new GiNaC
::ex
(-*$2);
762 | polynomial
'+' polynomial
{
763 $$
= new GiNaC
::ex
(*$1 + *$3);
767 | polynomial
'-' polynomial
{
768 $$
= new GiNaC
::ex
(*$1 - *$3);
772 | polynomial
'/' polynomial
{
773 $$
= new GiNaC
::ex
(*$1 / *$3);
777 | polynomial
'*' polynomial
{
778 $$
= new GiNaC
::ex
(*$1 * *$3);
784 polyfunc
: OPEN_BRACE
785 tupleDeclaration GOES_TO polynomial optionalFormula CLOSE_BRACE
{
786 Relation
*r
= build_relation
($2, $5);
795 relation
: OPEN_BRACE
796 { relationDecl
= new Declaration_Site
(); }
800 if
(omega_calc_debug
) {
801 fprintf
(DebugFile
,"Built relation:\n");
802 $$
->prefix_print
(DebugFile
);
804 current_Declaration_Site
= globalDecls
;
809 if
(relationMap
(s
) == 0) {
810 fprintf
(stderr
,"Variable %s not declared\n",$1);
816 $$
= new Relation
(*relationMap
(s
));
818 |
'(' relation
')' {$$
= $2;}
819 | relation
'+' %prec OMEGA_P9
820 { $$
= new Relation
();
821 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
824 | relation
'*' %prec OMEGA_P9
825 { $$
= new Relation
();
826 int vars
= $1->n_inp
();
827 *$$
= Union
(Identity
(vars
),
828 TransitiveClosure
(*$1, 1,Relation
::Null
()));
831 | relation
'+' WITHIN relation %prec OMEGA_P9
832 {$$
= new Relation
();
833 *$$
= TransitiveClosure
(*$1, 1,*$4);
837 | MINIMIZE_RANGE relation %prec OMEGA_P8
841 r
= Join
(r
,LexForward
($2->n_out
()));
843 *$$
= Difference
(o
,r
);
846 | MAXIMIZE_RANGE relation %prec OMEGA_P8
850 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
852 *$$
= Difference
(o
,r
);
855 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
859 r
= Join
(LexForward
($2->n_inp
()),r
);
861 *$$
= Difference
(o
,r
);
864 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
868 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
870 *$$
= Difference
(o
,r
);
873 | MAXIMIZE relation %prec OMEGA_P8
878 *$$
= Cross_Product
(Relation
(*$2),c
);
880 assert
($$
->n_inp
() ==$$
->n_out
());
881 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
883 | MINIMIZE relation %prec OMEGA_P8
888 *$$
= Cross_Product
(Relation
(*$2),c
);
890 assert
($$
->n_inp
() ==$$
->n_out
());
891 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
893 | FARKAS relation %prec OMEGA_P8
896 *$$
= Farkas
(*$2, Basic_Farkas
);
899 | DECOUPLED_FARKAS relation %prec OMEGA_P8
902 *$$
= Farkas
(*$2, Decoupled_Farkas
);
905 | relation
'@' %prec OMEGA_P9
906 { $$
= new Relation
();
907 *$$
= ConicClosure
(*$1);
910 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
911 { $$
= new Relation
();
912 *$$
= Project_Sym
(*$2);
915 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
916 { $$
= new Relation
();
917 *$$
= Project_On_Sym
(*$2);
920 | DIFFERENCE relation %prec OMEGA_P8
921 { $$
= new Relation
();
925 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
926 { $$
= new Relation
();
927 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
930 | OMEGA_DOMAIN relation %prec OMEGA_P8
931 { $$
= new Relation
();
935 | VENN relation %prec OMEGA_P8
936 { $$
= new Relation
();
937 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
940 | VENN relation GIVEN relation %prec OMEGA_P8
941 { $$
= new Relation
();
942 *$$
= VennDiagramForm
(*$2,*$4);
946 | CONVEX_HULL relation %prec OMEGA_P8
947 { $$
= new Relation
();
948 *$$
= ConvexHull
(*$2);
951 | POSITIVE_COMBINATION relation %prec OMEGA_P8
952 { $$
= new Relation
();
953 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
956 | CONVEX_COMBINATION relation %prec OMEGA_P8
957 { $$
= new Relation
();
958 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
961 | PAIRWISE_CHECK relation %prec OMEGA_P8
962 { $$
= new Relation
();
963 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
966 | CONVEX_CHECK relation %prec OMEGA_P8
967 { $$
= new Relation
();
968 *$$
= CheckForConvexRepresentation
(*$2);
971 | AFFINE_HULL relation %prec OMEGA_P8
972 { $$
= new Relation
();
973 *$$
= AffineHull
(*$2);
976 | CONIC_HULL relation %prec OMEGA_P8
977 { $$
= new Relation
();
978 *$$
= ConicHull
(*$2);
981 | LINEAR_HULL relation %prec OMEGA_P8
982 { $$
= new Relation
();
983 *$$
= LinearHull
(*$2);
986 | HULL relation %prec OMEGA_P8
987 { $$
= new Relation
();
988 *$$
= Hull
(*$2,false
,1,Null_Relation
());
991 | HULL relation GIVEN relation %prec OMEGA_P8
992 { $$
= new Relation
();
993 *$$
= Hull
(*$2,false
,1,*$4);
997 | APPROX relation %prec OMEGA_P8
998 { $$
= new Relation
();
999 *$$
= Approximate
(*$2);
1002 | RANGE relation %prec OMEGA_P8
1003 { $$
= new Relation
();
1007 | INVERSE relation %prec OMEGA_P8
1008 { $$
= new Relation
();
1012 | COMPLEMENT relation %prec OMEGA_P8
1013 { $$
= new Relation
();
1014 *$$
= Complement
(*$2);
1017 | GIST relation GIVEN relation %prec OMEGA_P8
1018 { $$
= new Relation
();
1019 *$$
= Gist
(*$2,*$4,1);
1023 | relation
'(' relation
')'
1024 { $$
= new Relation
();
1025 *$$
= Composition
(*$1,*$3);
1029 | relation COMPOSE relation
1030 { $$
= new Relation
();
1031 *$$
= Composition
(*$1,*$3);
1035 | relation CARRIED_BY INT
1036 { $$
= new Relation
();
1037 *$$
= After
(*$1,$3,$3);
1039 (*$$
).prefix_print
(stdout
);
1041 | relation JOIN relation
1042 { $$
= new Relation
();
1043 *$$
= Composition
(*$3,*$1);
1047 | relation RESTRICT_RANGE relation
1048 { $$
= new Relation
();
1049 *$$
= Restrict_Range
(*$1,*$3);
1053 | relation RESTRICT_DOMAIN relation
1054 { $$
= new Relation
();
1055 *$$
= Restrict_Domain
(*$1,*$3);
1059 | relation INTERSECTION relation
1060 { $$
= new Relation
();
1061 *$$
= Intersection
(*$1,*$3);
1065 | relation
'-' relation %prec INTERSECTION
1066 { $$
= new Relation
();
1067 *$$
= Difference
(*$1,*$3);
1071 | relation UNION relation
1072 { $$
= new Relation
();
1073 *$$
= Union
(*$1,*$3);
1077 | relation
'*' relation
1078 { $$
= new Relation
();
1079 *$$
= Cross_Product
(*$1,*$3);
1083 | SUPERSETOF relation
1084 { $$
= new Relation
();
1085 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
1089 { $$
= new Relation
();
1090 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
1093 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
1094 { $$
= new Relation
();
1095 *$$
= Upper_Bound
(*$2);
1098 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
1099 { $$
= new Relation
();
1100 *$$
= Lower_Bound
(*$2);
1104 { $$
= new Relation
();
1105 *$$
= Sample_Solution
(*$2);
1108 | SYM_SAMPLE relation
1109 { $$
= new Relation
();
1110 *$$
= Symbolic_Solution
(*$2);
1113 | reachable_of
{ $$
= $1; }
1114 | ASSERT_UNSAT relation
1116 if
(($2)->is_satisfiable
())
1118 fprintf
(stderr
,"assert_unsatisfiable failed on ");
1119 ($2)->print_with_subs
(stderr
);
1128 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
1129 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
1130 Relation
* r
= new Relation
($1->size
,$4->size
);
1132 F_And
*f
= r
->add_and
();
1134 for
(i
=1;i
<=$1->size
;i
++) {
1135 $1->vars
[i
]->vid
= r
->input_var
(i
);
1136 if
(!$1->vars
[i
]->anonymous
)
1137 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
1139 for
(i
=1;i
<=$4->size
;i
++) {
1140 $4->vars
[i
]->vid
= r
->output_var
(i
);
1141 if
(!$4->vars
[i
]->anonymous
)
1142 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
1144 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1145 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1146 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1147 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
1148 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
1149 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
1150 if
($6) $6->install
(f
);
1155 | tupleDeclaration optionalFormula
{
1156 $$
= build_relation
($1, $2);
1159 Relation
* r
= new Relation
(0,0);
1160 F_And
*f
= r
->add_and
();
1167 optionalFormula
: formula_sep formula
{ $$
= $2; }
1178 if
(currentTupleDescriptor
)
1179 delete currentTupleDescriptor
;
1180 currentTupleDescriptor
= new tupleDescriptor
;
1183 '[' optionalTupleVarList
']'
1184 {$$
= currentTupleDescriptor
; currentTupleDescriptor
= NULL
; }
1187 optionalTupleVarList
:
1189 | optionalTupleVarList
',' tupleVar
1193 tupleVar
: VAR %prec OMEGA_P10
1194 { Declaration_Site
*ds
= defined
($1);
1195 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1197 Variable_Ref
* v
= lookupScalar
($1);
1199 if
(ds
!= globalDecls
)
1200 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1202 currentTupleDescriptor
->extend
(new Exp
(v
));
1208 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1209 | exp %prec OMEGA_P1
1210 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1211 | exp
':' exp %prec OMEGA_P1
1212 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1213 | exp
':' exp
':' INT %prec OMEGA_P1
1214 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1218 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1219 | VAR
{ $$
= new VarList
;
1225 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1226 foreach
(s
,char *, *$1, free
(s
));
1231 /* variable declaration with optional brackets */
1233 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1234 |
'[' varDecl
']' { $$
= $2; }
1237 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1238 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1239 | constraintChain
{ $$
= $1; }
1240 |
'(' formula
')' { $$
= $2; }
1241 | NOT formula
{ $$
= new AST_Not
($2); }
1242 | start_exists varDeclOptBrackets exists_sep formula end_quant
1243 { $$
= new AST_exists
($2,$4); }
1244 | start_forall varDeclOptBrackets forall_sep formula end_quant
1245 { $$
= new AST_forall
($2,$4); }
1248 start_exists
: '(' EXISTS
1257 start_forall
: '(' FORALL
1268 expList
: exp
',' expList
1279 constraintChain
: expList REL_OP expList
1280 { $$
= new AST_constraints
($1,$2,$3); }
1281 | expList REL_OP constraintChain
1282 { $$
= new AST_constraints
($1,$2,$3); }
1287 { Variable_Ref
* v
= lookupScalar
($1);
1292 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1294 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1295 else v
= functionOfOutput
[$1];
1297 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1304 |
'(' exp
')' { $$
= $2;}
1310 argumentList
',' VAR
{
1311 Variable_Ref
* v
= lookupScalar
($3);
1314 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1315 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1321 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1324 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1325 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1333 exp
: INT
{$$
= new Exp
($1);}
1334 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1335 | simpleExp
{ $$
= $1; }
1336 |
'-' exp %prec
'*' { $$
= negate
($2);}
1337 | exp
'+' exp
{ $$
= add
($1,$3);}
1338 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1339 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1344 REACHABLE_FROM nodeNameList nodeSpecificationList
1346 Dynamic_Array1
<Relation
> *final
=
1347 Reachable_Nodes
(reachable_info
);
1353 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1355 Dynamic_Array1
<Relation
> *final
=
1356 Reachable_Nodes
(reachable_info
);
1357 int index
= reachable_info
->node_names.index
(String
($2));
1358 assert
(index
!= 0 && "No such node");
1360 *$$
= (*final
)[index
];
1362 delete reachable_info
;
1368 nodeNameList: '(' realNodeNameList
')'
1369 { int sz
= reachable_info
->node_names.size
();
1370 reachable_info
->node_arity.reallocate
(sz
);
1371 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1372 reachable_info
->start_nodes.resize
(sz
+1);
1376 realNodeNameList: realNodeNameList
',' VAR
1377 { reachable_info
->node_names.append
(String
($3));
1379 | VAR
{ reachable_info
= new reachable_information
;
1380 reachable_info
->node_names.append
(String
($1));
1385 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1388 int n_nodes
= reachable_info
->node_names.size
();
1389 Tuple
<int> &arity
= reachable_info
->node_arity
;
1390 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1392 /* fixup unspecified transitions to be false */
1394 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1395 for
(i
= 1; i
<= n_nodes
; i
++)
1396 for
(j
= 1; j
<= n_nodes
; j
++)
1397 if
(! transitions
[i
][j
].is_null
()) {
1398 int in_arity
= transitions
[i
][j
].n_inp
();
1399 int out_arity
= transitions
[i
][j
].n_out
();
1400 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1401 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1402 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1404 "Arity mismatch in node transition: %s -> %s",
1405 (const char *) reachable_info
->node_names
[i
],
1406 (const char *) reachable_info
->node_names
[j
]);
1411 for
(i
= 1; i
<= n_nodes
; i
++)
1412 if
(arity
[i
] < 0) arity
[i
] = 0;
1413 /* Fill in false relations */
1414 for
(i
= 1; i
<= n_nodes
; i
++)
1415 for
(j
= 1; j
<= n_nodes
; j
++)
1416 if
(transitions
[i
][j
].is_null
())
1417 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1420 /* fixup unused start node positions */
1421 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1422 for
(i
= 1; i
<= n_nodes
; i
++)
1423 if
(nodes
[i
].is_null
())
1424 nodes
[i
] = Relation
::False
(arity
[i
]);
1426 if
(nodes
[i
].n_set
() != arity
[i
]){
1427 fprintf
(stderr
,"Arity mismatch in start node %s",
1428 (const char *) reachable_info
->node_names
[i
]);
1435 realNodeSpecificationList:
1436 realNodeSpecificationList
',' VAR
':' relation
1437 { int n_nodes
= reachable_info
->node_names.size
();
1438 int index
= reachable_info
->node_names.index
($3);
1439 assert
(index
!= 0 && index
<= n_nodes
);
1440 reachable_info
->start_nodes
[index
] = *$5;
1444 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1445 { int n_nodes
= reachable_info
->node_names.size
();
1446 int from_index
= reachable_info
->node_names.index
($3);
1447 int to_index
= reachable_info
->node_names.index
($5);
1448 assert
(from_index
!= 0 && to_index
!= 0);
1449 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1450 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1455 | VAR GOES_TO VAR
':' relation
1456 { int n_nodes
= reachable_info
->node_names.size
();
1457 int from_index
= reachable_info
->node_names.index
($1);
1458 int to_index
= reachable_info
->node_names.index
($3);
1459 assert
(from_index
!= 0 && to_index
!= 0);
1460 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1461 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1467 { int n_nodes
= reachable_info
->node_names.size
();
1468 int index
= reachable_info
->node_names.index
($1);
1469 assert
(index
!= 0 && index
<= n_nodes
);
1470 reachable_info
->start_nodes
[index
] = *$3;
1478 #if !defined(OMIT_GETRUSAGE)
1479 #include <sys/types.h>
1480 #include <sys/time.h>
1481 #include <sys/resource.h>
1483 struct rusage start_time
;
1486 #if defined BRAIN_DAMAGED_FREE
1492 void *realloc
(void *p
, size_t s
)
1494 return realloc
((malloc_t
) p
, s
);
1498 #if ! defined(OMIT_GETRUSAGE)
1500 extern
"C" int getrusage
(int, struct rusage
*);
1503 void start_clock
( void )
1505 getrusage
(RUSAGE_SELF
, &start_time
);
1508 int clock_diff
( void )
1510 struct rusage current_time
;
1511 getrusage
(RUSAGE_SELF
, ¤t_time
);
1512 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1513 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1517 void printUsage
(FILE *outf
, char **argv
) {
1518 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
);
1521 int omega_calc_debug
;
1524 int main
(int argc
, char **argv
){
1525 redundant_conj_level
= 2;
1526 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1531 char * fileName
= 0;
1533 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1535 calc_all_debugging_off
();
1538 DebugFile
= fopen
("/dev/null","w");
1541 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1543 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1546 setbuf
(DebugFile
,0);
1549 closure_presburger_debug
= 0;
1551 setOutputFile
(DebugFile
);
1554 for
(i
=1; i
<argc
; i
++) {
1555 if
(argv
[i
][0] == '-') {
1557 while
((c
=argv
[i
][j
++]) != 0) {
1560 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1561 printUsage
(stderr
,argv
);
1567 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1568 while
(argv
[i
][j
] != 0) j
++;
1573 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1574 while
(argv
[i
][j
] != 0) j
++;
1578 redundant_conj_level
= 1;
1580 // Other future options go here
1582 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1583 printUsage
(stderr
,argv
);
1589 // Make sure this is a file name
1591 fprintf
(stderr
,"\nCan only handle a single input file\n");
1592 printUsage
(stderr
,argv
);
1596 yyin
= fopen
(fileName
, "r");
1598 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1599 printUsage
(stderr
,argv
);
1607 initializeScanBuffer
();
1608 currentTupleDescriptor
= NULL
;
1613 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1614 {delete r
; relationMap
[cs
]=0;});
1620 Relation LexForward
(int n
) {
1622 F_Or
*f
= r.add_or
();
1623 for
(int i
=1; i
<= n
; i
++) {
1624 F_And
*g
= f
->add_and
();
1625 for
(int j
=1;j
<i
;j
++) {
1626 EQ_Handle e
= g
->add_EQ
();
1627 e.update_coef
(r.input_var
(j
),-1);
1628 e.update_coef
(r.output_var
(j
),1);
1631 GEQ_Handle e
= g
->add_GEQ
();
1632 e.update_coef
(r.input_var
(i
),-1);
1633 e.update_coef
(r.output_var
(i
),1);