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>
30 #define CALC_VERSION_STRING "Omega Counting Calculator v1.2"
32 #define DEBUG_FILE_NAME "./oc.out"
35 Map
<Const_String
,Relation
*> relationMap
((Relation
*)0);
36 static int redundant_conj_level
;
38 #if defined BRAIN_DAMAGED_FREE
40 void *realloc
(void *p
, size_t s
);
43 #if !defined(OMIT_GETRUSAGE)
44 void start_clock
( void );
45 int clock_diff
( void );
46 bool anyTimingDone
= false
;
51 Argument_Tuple currentTuple
= Input_Tuple
;
52 char *currentVar
= NULL
;
54 Relation LexForward
(int n
);
57 reachable_information
*reachable_info
;
59 Relation
*build_relation
(tupleDescriptor
*tuple
, AST
* ast
)
61 Relation
* r
= new Relation
(tuple
->size
);
63 F_And
*f
= r
->add_and
();
65 for
(i
=1;i
<=tuple
->size
;i
++) {
66 tuple
->vars
[i
]->vid
= r
->set_var
(i
);
67 if
(!tuple
->vars
[i
]->anonymous
)
68 r
->name_set_var
(i
,tuple
->vars
[i
]->stripped_name
);
70 foreach
(e
,Exp
*,tuple
->eq_constraints
, install_eq
(f
,e
,0));
71 foreach
(e
,Exp
*,tuple
->geq_constraints
, install_geq
(f
,e
,0));
72 foreach
(c
,strideConstraint
*,tuple
->stride_constraints
, install_stride
(f
,c
));
73 if
(ast
) ast
->install
(f
);
79 Map
<Variable_Ref
*, GiNaC
::ex
> *variableMap
;
82 static void evalue_print_and_free
(Relation
*r
, evalue
*EP
)
87 const Variable_ID_Tuple
* globals
= r
->global_decls
();
88 const char **param_names
= new
const char *[globals
->size
()];
90 for
(int i
= 0; i
< globals
->size
(); ++i
)
91 param_names
[i
] = (*globals
)[i
+1]->char_name
();
92 print_evalue
(stdout
, EP
, param_names
);
94 delete
[] param_names
;
101 %token
<VAR_NAME
> VAR
102 %token
<INT_VALUE
> INT
103 %token
<STRING_VALUE
> STRING
104 %token OPEN_BRACE CLOSE_BRACE
110 %token OMEGA_DOMAIN RANGE
111 %token DIFFERENCE DIFFERENCE_TO_RELATION
112 %token GIST GIVEN HULL WITHIN MAXIMIZE MINIMIZE
113 %token AFFINE_HULL VENN CONVEX_COMBINATION POSITIVE_COMBINATION CONVEX_HULL CONIC_HULL LINEAR_HULL PAIRWISE_CHECK CONVEX_CHECK
114 %token MAXIMIZE_RANGE MINIMIZE_RANGE
115 %token MAXIMIZE_DOMAIN MINIMIZE_DOMAIN
118 %token COMPOSE JOIN INVERSE COMPLEMENT IN CARRIED_BY TIME TIMECLOSURE
119 %token UNION INTERSECTION
120 %token VERTICAL_BAR SUCH_THAT
121 %token SUBSET ITERATIONS SPMD CODEGEN DECOUPLED_FARKAS FARKAS
122 %token TCODEGEN TRANS_IS SET_MMAP UNROLL_IS PEEL_IS
123 %token MAKE_UPPER_BOUND MAKE_LOWER_BOUND
124 %token
<REL_OPERATOR
> REL_OP
125 %token RESTRICT_DOMAIN RESTRICT_RANGE
126 %token SUPERSETOF SUBSETOF SAMPLE SYM_SAMPLE
127 %token PROJECT_AWAY_SYMBOLS PROJECT_ON_SYMBOLS REACHABLE_FROM REACHABLE_OF
129 %token CARD USING BARVINOK PARKER RANKING COUNT_LEXSMALLER
135 %token PARSE_EXPRESSION PARSE_FORMULA PARSE_RELATION
137 %nonassoc ASSERT_UNSAT
138 %left UNION OMEGA_P1
'+' '-'
139 %nonassoc SUPERSETOF SUBSETOF
140 %left OMEGA_P2 RESTRICT_DOMAIN RESTRICT_RANGE
141 %left INTERSECTION OMEGA_P3
'*' '@'
146 %left COMPOSE JOIN CARRIED_BY
147 %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
152 %right CARD USING RANKING COUNT_LEXSMALLER
158 %type
<INT_VALUE
> effort
159 %type
<EXP
> exp simpleExp
160 %type
<EXP_LIST
> expList
161 %type
<VAR_LIST
> varList
162 %type
<ARGUMENT_TUPLE
> argumentList
163 %type
<ASTP
> formula optionalFormula
164 %type
<ASTCP
> constraintChain
165 %type
<TUPLE_DESCRIPTOR
> tupleDeclaration
166 %type
<DECLARATION_SITE
> varDecl varDeclOptBrackets
167 %type
<RELATION
> relation builtRelation context
168 %type
<RELATION
> reachable_of
169 %type
<REL_TUPLE_PAIR
> relPairList
170 %type
<REL_TUPLE_TRIPLE
> relTripList
171 %type
<RELATION_ARRAY_1D
> reachable
172 %type
<STM_INFO_TUPLE
> statementInfoList statementInfoResult
173 %type
<STM_INFO
> statementInfo
174 %type
<STM_INFO
> reads
176 %type
<READ
> partials
177 %type
<PREAD
> partial
178 %type
<MMAP
> partialwrites
179 %type
<PMMAP
> partialwrite
180 %type
<POLYFUNC
> polyfunc
181 %type
<POLYNOMIAL
> polynomial
182 %type
<INT_VALUE
> counting_method
192 Argument_Tuple ARGUMENT_TUPLE
;
193 AST_constraints
*ASTCP
;
194 Declaration_Site
* DECLARATION_SITE
;
196 tupleDescriptor
* TUPLE_DESCRIPTOR
;
197 RelTuplePair
* REL_TUPLE_PAIR
;
198 RelTupleTriple
* REL_TUPLE_TRIPLE
;
199 Dynamic_Array2
<Relation
> * RELATION_ARRAY_2D
;
200 Dynamic_Array1
<Relation
> * RELATION_ARRAY_1D
;
201 Tuple
<String
> *STRING_TUPLE
;
202 String
*STRING_VALUE
;
203 Tuple
<stm_info
> *STM_INFO_TUPLE
;
210 GiNaC
::ex
*POLYNOMIAL
;
221 inputSequence
: inputItem
222 | inputSequence
{ assert
( current_Declaration_Site
== globalDecls
);}
229 /* Kill all the local declarations -- ejr */
232 Declaration_Site
*ds1
, *ds2
;
233 for
(ds1
= current_Declaration_Site
; ds1
!= globalDecls
;) {
238 current_Declaration_Site
= globalDecls
;
239 yyerror("skipping to statement end");
241 | SYMBOLIC globVarList
';'
244 | VAR
{ currentVar
= $1; } IS_ASSIGNED relation
';'
247 $4->simplify
(min
(2,redundant_conj_level
),4);
248 Relation
*r
= relationMap
((Const_String
)$1);
250 relationMap
[(Const_String
)$1] = $4;
257 $1->simplify
(redundant_conj_level
,4);
258 $1->print_with_subs
(stdout
);
262 | TIME relation
';' {
264 #if defined(OMIT_GETRUSAGE)
265 printf
("'time' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
273 bool SKIP_FULL_CHECK
= getenv
("OC_TIMING_SKIP_FULL_CHECK");
274 ($2)->and_with_GEQ
();
276 for
(t
=1;t
<=100;t
++) {
280 int copyTime
= clock_diff
();
282 for
(t
=1;t
<=100;t
++) {
287 int simplifyTime
= clock_diff
() -copyTime
;
289 if
(!SKIP_FULL_CHECK
)
292 for
(t
=1;t
<=100;t
++) {
298 int excessiveTime
= clock_diff
() - copyTime
;
299 printf
("Times (in microseconds): \n");
300 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
301 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
303 R.print_with_subs
(stdout
);
305 if
(!SKIP_FULL_CHECK
)
307 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
309 R2.print_with_subs
(stdout
);
312 if
(!anyTimingDone
) {
321 printf
("WARNING: The Omega calculator was compiled with options that force\n");
322 printf
("it to perform additional consistency and error checks\n");
323 printf
("that may slow it down substantially\n");
326 printf
("NOTE: These times relect the time of the current _implementation_\n");
327 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
328 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
329 printf
("request that send your test cases to us to allow us to determine if the \n");
330 printf
("times are appropriate, and if the way you are using the Omega library to \n");
331 printf
("solve your problem is the most effective way.\n");
334 printf
("Also, please be aware that over the past two years, we have focused our \n");
335 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
336 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
337 printf
("was substantially faster on the limited domain it handled.\n");
339 printf
(" Thanks, \n");
340 printf
(" the Omega Team \n");
342 anyTimingDone
= true
;
346 | TIMECLOSURE relation
';' {
348 #if defined(OMIT_GETRUSAGE)
349 printf
("'timeclosure' requires getrusage, but the omega calclator was compiled with OMIT_GETRUSAGE set!\n");
355 ($2)->and_with_GEQ
();
357 for
(t
=1;t
<=100;t
++) {
361 int copyTime
= clock_diff
();
363 for
(t
=1;t
<=100;t
++) {
368 int simplifyTime
= clock_diff
() -copyTime
;
371 for
(t
=1;t
<=100;t
++) {
374 Rclosed
= TransitiveClosure
(Rclosed
, 1,Relation
::Null
());
376 int closureTime
= clock_diff
() - copyTime
;
379 for
(t
=1;t
<=100;t
++) {
384 int excessiveTime
= clock_diff
() - copyTime
;
385 printf
("Times (in microseconds): \n");
386 printf
("%5d us to copy original set of constraints\n",copyTime
/100);
387 printf
("%5d us to do the default amount of simplification, obtaining: \n\t",
389 R.print_with_subs
(stdout
);
391 printf
("%5d us to do the maximum (i.e., excessive) amount of simplification, obtaining: \n\t",
393 R2.print_with_subs
(stdout
);
394 printf
("%5d us to do the transitive closure, obtaining: \n\t",
396 Rclosed.print_with_subs
(stdout
);
398 if
(!anyTimingDone
) {
407 printf
("WARNING: The Omega calculator was compiled with options that force\n");
408 printf
("it to perform additional consistency and error checks\n");
409 printf
("that may slow it down substantially\n");
412 printf
("NOTE: These times relect the time of the current _implementation_\n");
413 printf
("of our algorithms. Performance bugs do exist. If you intend to publish or \n");
414 printf
("report on the performance on the Omega test, we respectfully but strongly \n");
415 printf
("request that send your test cases to us to allow us to determine if the \n");
416 printf
("times are appropriate, and if the way you are using the Omega library to \n");
417 printf
("solve your problem is the most effective way.\n");
420 printf
("Also, please be aware that over the past two years, we have focused our \n");
421 printf
("efforts on the expressive power of the Omega library, sometimes at the\n");
422 printf
("expensive of raw speed. Our original implementation of the Omega test\n");
423 printf
("was substantially faster on the limited domain it handled.\n");
425 printf
(" Thanks, \n");
426 printf
(" the Omega Team \n");
428 anyTimingDone
= true
;
434 | relation SUBSET relation
';' {
436 int c
= Must_Be_Subset
(*$1, *$3);
437 printf
("\n%s\n", c ?
"True" : "False");
441 | CODEGEN effort relPairList context
';'
444 String s
= MMGenerateCode
($3->mappings
, $3->ispaces
,*$4,$2);
447 printf
("%s\n", (const char *) s
);
449 | TCODEGEN effort statementInfoResult context
';'
452 String s
= tcodegen
($2, *($3), *($4));
455 printf
("%s\n", (const char *) s
);
457 /* | TCODEGEN NOT effort statementInfoResult context';'
460 * String s = tcodegen($3, *($4), *($5), false);
463 * printf("%s\n", (const char *) s);
466 | SPMD blockAndProcsAndEffort relTripList
';'
468 Tuple
<Free_Var_Decl
*> lowerBounds
(0), upperBounds
(0), my_procs
(0);
469 Tuple
<spmd_stmt_info
*> names
(0);
472 int nr_statements
= $3->space.size
();
474 for
(int i
= 1; i
<= $3->space
[1].n_out
(); i
++)
476 lowerBounds.append
(new Free_Var_Decl
("lb" + itoS
(i
)));
477 upperBounds.append
(new Free_Var_Decl
("ub" + itoS
(i
)));
478 my_procs.append
(new Free_Var_Decl
("my_proc" + itoS
(i
)));
481 for
(int p
= 1; p
<= nr_statements
; p
++)
482 names.append
(new numbered_stmt_info
(p
-1, Identity
($3->time
[p
].n_out
()),
484 (char *)(const char *)("s"+itoS
(p
-1))));
486 String s
= SPMD_GenerateCode
("", $3->space
, $3->time
, $3->ispaces
,
488 lowerBounds
, upperBounds
, my_procs
,
492 printf
("%s\n", (const char *) s
);
496 Dynamic_Array1
<Relation
> &final
= *$1;
498 int i
,n_nodes
= reachable_info
->node_names.size
();
499 for
(i
= 1; i
<= n_nodes
; i
++) if
(final
[i
].is_upper_bound_satisfiable
()) {
501 fprintf
(stdout
,"Node %s: ",
502 (const char *) (reachable_info
->node_names
[i
]));
503 final
[i
].print_with_subs
(stdout
);
506 fprintf
(stdout
,"No nodes reachable.\n");
508 delete reachable_info
;
510 | CARD relation
';' {
511 evalue
*EP
= count_relation
(*$2, COUNT_RELATION_BARVINOK
);
512 evalue_print_and_free
($2, EP
);
515 | CARD relation USING counting_method
';' {
516 evalue
*EP
= count_relation
(*$2, $4);
517 evalue_print_and_free
($2, EP
);
520 | RANKING relation
';' {
521 evalue
*EP
= rank_relation
(*$2);
523 const Variable_ID_Tuple
* globals
= $2->global_decls
();
524 int nvar
= $2->n_set
();
525 int n
= nvar
+ globals
->size
();
526 const char **names
= new
const char *[n
];
528 for
(int i
= 0; i
< nvar
; ++i
)
529 names
[i
] = $2->set_var
(i
+1)->char_name
();
530 for
(int i
= 0; i
< globals
->size
(); ++i
)
531 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
532 print_evalue
(stdout
, EP
, names
);
539 | COUNT_LEXSMALLER relation WITHIN relation
';' {
540 evalue
*EP
= count_lexsmaller
(*$2, *$4);
542 const Variable_ID_Tuple
* globals
= $4->global_decls
();
543 int nvar
= $4->n_set
();
544 int n
= nvar
+ globals
->size
();
545 const char **names
= new
const char *[n
];
547 for
(int i
= 0; i
< nvar
; ++i
)
548 names
[i
] = $4->set_var
(i
+1)->char_name
();
549 for
(int i
= 0; i
< globals
->size
(); ++i
)
550 names
[nvar
+i
] = (*globals
)[i
+1]->char_name
();
551 print_evalue
(stdout
, EP
, names
);
559 | VERTICES relation
';' {
565 relationDecl
= new Declaration_Site
();
566 variableMap
= new Map
<Variable_Ref
*, GiNaC
::ex
>(0);
569 maximize
($3, *variableMap
);
571 current_Declaration_Site
= globalDecls
;
577 relationDecl
= new Declaration_Site
();
578 variableMap
= new Map
<Variable_Ref
*, GiNaC
::ex
>(0);
581 evalue
*s
= summate
($3, *variableMap
);
582 evalue_print_and_free
(&$3->domain
, s
);
584 current_Declaration_Site
= globalDecls
;
588 | DUMP relation
';' {
593 relTripList: relTripList
',' relation
':' relation
':' relation
595 $1->space.append
(*$3);
596 $1->time.append
(*$5);
597 $1->ispaces.append
(*$7);
603 | relation
':' relation
':' relation
605 RelTupleTriple
*rtt
= new RelTupleTriple
;
606 rtt
->space.append
(*$1);
607 rtt
->time.append
(*$3);
608 rtt
->ispaces.append
(*$5);
616 blockAndProcsAndEffort
: { Block_Size
= 0; Num_Procs
= 0; overheadEffort
=0; }
617 | INT
{ Block_Size
= $1; Num_Procs
= 0; overheadEffort
=0;}
618 | INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=0;}
619 | INT INT INT
{ Block_Size
= $1; Num_Procs
= $2; overheadEffort
=$3;}
623 BARVINOK
{ $$
= COUNT_RELATION_BARVINOK
; }
624 | PARKER
{ $$
= COUNT_RELATION_PARKER
; }
629 |
'-' INT
{ $$
= -$2; }
632 context
: { $$
= new Relation
();
633 *$$
= Relation
::Null
(); }
634 | GIVEN relation
{$$
= $2; }
637 relPairList: relPairList
',' relation
':' relation
639 $1->mappings.append
(*$3);
640 $1->mappings
[$1->mappings.size
()].compress
();
641 $1->ispaces.append
(*$5);
642 $1->ispaces
[$1->ispaces.size
()].compress
();
647 | relPairList
',' relation
649 $1->mappings.append
(Identity
($3->n_set
()));
650 $1->mappings
[$1->mappings.size
()].compress
();
651 $1->ispaces.append
(*$3);
652 $1->ispaces
[$1->ispaces.size
()].compress
();
656 | relation
':' relation
658 RelTuplePair
*rtp
= new RelTuplePair
;
659 rtp
->mappings.append
(*$1);
660 rtp
->mappings
[rtp
->mappings.size
()].compress
();
661 rtp
->ispaces.append
(*$3);
662 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
669 RelTuplePair
*rtp
= new RelTuplePair
;
670 rtp
->mappings.append
(Identity
($1->n_set
()));
671 rtp
->mappings
[rtp
->mappings.size
()].compress
();
672 rtp
->ispaces.append
(*$1);
673 rtp
->ispaces
[rtp
->ispaces.size
()].compress
();
679 statementInfoResult
: statementInfoList
681 /* | ASSERT_UNSAT statementInfoResult
683 * DoDebug2("Debug info requested in input", *($2));
686 | TRANS_IS relation statementInfoResult
687 { $$
= &Trans_IS
(*($3), *($2));
690 | SET_MMAP INT partialwrites statementInfoResult
691 { $$
= &Set_MMap
(*($4), $2, *($3));
694 | UNROLL_IS INT INT INT statementInfoResult
695 { $$
= &Unroll_One_IS
(*($5), $2, $3, $4);}
696 | PEEL_IS INT INT relation statementInfoResult
697 { $$
= &Peel_One_IS
(*($5), $2, $3, *($4));
700 | PEEL_IS INT INT relation
',' relation statementInfoResult
701 { $$
= &Peel_One_IS
(*($7), $2, $3, *($4), *($6));
707 statementInfoList
: statementInfo
{ $$
= new Tuple
<stm_info
>;
710 | statementInfoList
',' statementInfo
{ $$
= $1;
715 statementInfo
: '[' STRING
',' relation
',' partialwrites
',' reads
']'
717 $$
->stm
= *($2); delete
$2;
718 $$
->IS
= *($4); delete
$4;
719 $$
->map
= *($6); delete
$6;
721 |
'[' STRING
',' relation
',' partialwrites
']'
723 $$
->stm
= *($2); delete
$2;
724 $$
->IS
= *($4); delete
$4;
725 $$
->map
= *($6); delete
$6;
729 partialwrites
: partialwrites
',' partialwrite
731 $$
->partials.append
(*($3)); delete
$3;
733 | partialwrite
{ $$
= new MMap
;
734 $$
->partials.append
(*($1)); delete
$1;
738 partialwrite
: STRING
'[' relation
']' ',' relation
739 { $$
= new PartialMMap
;
740 $$
->mapping
= *($6); delete
$6;
741 $$
->bounds
= *($3); delete
$3;
742 $$
->var
= *($1); delete
$1;
744 | STRING
',' relation
{ $$
= new PartialMMap
;
745 $$
->mapping
= *($3); delete
$3;
746 $$
->bounds
= Relation
::True
(0);
747 $$
->var
= *($1); delete
$1;
751 reads
: reads
',' oneread
{ $$
= $1;
752 $$
->read.append
(*($3)); delete
$3;
754 | oneread
{ $$
= new stm_info
;
755 $$
->read.append
(*($1)); delete
$1;
759 oneread
: '[' partials
']' { $$
= $2; }
762 partials
: partials
',' partial
{ $$
= $1;
763 $$
->partials.append
(*($3)); delete
$3;
765 | partial
{ $$
= new Read
;
766 $$
->partials.append
(*($1)); delete
$1;
770 partial
: INT
',' relation
{ $$
= new PartialRead
;
772 $$
->dataFlow
= *($3); delete
$3;
776 globVarList: globVarList
',' globVar
780 globVar: VAR
'(' INT
')'
781 { globalDecls
->extend_both_tuples
($1, $3); free
($1); }
783 { globalDecls
->extend
($1); free
($1); }
786 polynomial
: INT
{ $$
= new GiNaC
::ex
($1); }
788 Variable_Ref
*v
= lookupScalar
($1);
791 if
((*variableMap
)(v
) == 0)
792 (*variableMap
)[v
] = GiNaC
::symbol
(std
::string(v
->name
));
793 $$
= new GiNaC
::ex
((*variableMap
)[v
]);
795 |
'(' polynomial
')' { $$
= $2; }
796 |
'-' polynomial %prec
'*' {
797 $$
= new GiNaC
::ex
(-*$2);
800 | polynomial
'+' polynomial
{
801 $$
= new GiNaC
::ex
(*$1 + *$3);
805 | polynomial
'-' polynomial
{
806 $$
= new GiNaC
::ex
(*$1 - *$3);
810 | polynomial
'/' polynomial
{
811 $$
= new GiNaC
::ex
(*$1 / *$3);
815 | polynomial
'*' polynomial
{
816 $$
= new GiNaC
::ex
(*$1 * *$3);
822 polyfunc
: OPEN_BRACE
823 tupleDeclaration GOES_TO polynomial optionalFormula CLOSE_BRACE
{
824 Relation
*r
= build_relation
($2, $5);
833 relation
: OPEN_BRACE
834 { relationDecl
= new Declaration_Site
(); }
838 if
(omega_calc_debug
) {
839 fprintf
(DebugFile
,"Built relation:\n");
840 $$
->prefix_print
(DebugFile
);
842 current_Declaration_Site
= globalDecls
;
847 if
(relationMap
(s
) == 0) {
848 fprintf
(stderr
,"Variable %s not declared\n",$1);
854 $$
= new Relation
(*relationMap
(s
));
856 |
'(' relation
')' {$$
= $2;}
857 | relation
'+' %prec OMEGA_P9
858 { $$
= new Relation
();
859 *$$
= TransitiveClosure
(*$1, 1,Relation
::Null
());
862 | relation
'*' %prec OMEGA_P9
863 { $$
= new Relation
();
864 int vars
= $1->n_inp
();
865 *$$
= Union
(Identity
(vars
),
866 TransitiveClosure
(*$1, 1,Relation
::Null
()));
869 | relation
'+' WITHIN relation %prec OMEGA_P9
870 {$$
= new Relation
();
871 *$$
= TransitiveClosure
(*$1, 1,*$4);
875 | MINIMIZE_RANGE relation %prec OMEGA_P8
879 r
= Join
(r
,LexForward
($2->n_out
()));
881 *$$
= Difference
(o
,r
);
884 | MAXIMIZE_RANGE relation %prec OMEGA_P8
888 r
= Join
(r
,Inverse
(LexForward
($2->n_out
())));
890 *$$
= Difference
(o
,r
);
893 | MINIMIZE_DOMAIN relation %prec OMEGA_P8
897 r
= Join
(LexForward
($2->n_inp
()),r
);
899 *$$
= Difference
(o
,r
);
902 | MAXIMIZE_DOMAIN relation %prec OMEGA_P8
906 r
= Join
(Inverse
(LexForward
($2->n_inp
())),r
);
908 *$$
= Difference
(o
,r
);
911 | MAXIMIZE relation %prec OMEGA_P8
916 *$$
= Cross_Product
(Relation
(*$2),c
);
918 assert
($$
->n_inp
() ==$$
->n_out
());
919 *$$
= Difference
(r
,Domain
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
921 | MINIMIZE relation %prec OMEGA_P8
926 *$$
= Cross_Product
(Relation
(*$2),c
);
928 assert
($$
->n_inp
() ==$$
->n_out
());
929 *$$
= Difference
(r
,Range
(Intersection
(*$$
,LexForward
($$
->n_inp
()))));
931 | FARKAS relation %prec OMEGA_P8
934 *$$
= Farkas
(*$2, Basic_Farkas
);
937 | DECOUPLED_FARKAS relation %prec OMEGA_P8
940 *$$
= Farkas
(*$2, Decoupled_Farkas
);
943 | relation
'@' %prec OMEGA_P9
944 { $$
= new Relation
();
945 *$$
= ConicClosure
(*$1);
948 | PROJECT_AWAY_SYMBOLS relation %prec OMEGA_P8
949 { $$
= new Relation
();
950 *$$
= Project_Sym
(*$2);
953 | PROJECT_ON_SYMBOLS relation %prec OMEGA_P8
954 { $$
= new Relation
();
955 *$$
= Project_On_Sym
(*$2);
958 | DIFFERENCE relation %prec OMEGA_P8
959 { $$
= new Relation
();
963 | DIFFERENCE_TO_RELATION relation %prec OMEGA_P8
964 { $$
= new Relation
();
965 *$$
= DeltasToRelation
(*$2,$2->n_set
(),$2->n_set
());
968 | OMEGA_DOMAIN relation %prec OMEGA_P8
969 { $$
= new Relation
();
973 | VENN relation %prec OMEGA_P8
974 { $$
= new Relation
();
975 *$$
= VennDiagramForm
(*$2,Relation
::True
(*$2));
978 | VENN relation GIVEN relation %prec OMEGA_P8
979 { $$
= new Relation
();
980 *$$
= VennDiagramForm
(*$2,*$4);
984 | CONVEX_HULL relation %prec OMEGA_P8
985 { $$
= new Relation
();
986 *$$
= ConvexHull
(*$2);
989 | POSITIVE_COMBINATION relation %prec OMEGA_P8
990 { $$
= new Relation
();
991 *$$
= Farkas
(*$2,Positive_Combination_Farkas
);
994 | CONVEX_COMBINATION relation %prec OMEGA_P8
995 { $$
= new Relation
();
996 *$$
= Farkas
(*$2,Convex_Combination_Farkas
);
999 | PAIRWISE_CHECK relation %prec OMEGA_P8
1000 { $$
= new Relation
();
1001 *$$
= CheckForConvexRepresentation
(CheckForConvexPairs
(*$2));
1004 | CONVEX_CHECK relation %prec OMEGA_P8
1005 { $$
= new Relation
();
1006 *$$
= CheckForConvexRepresentation
(*$2);
1009 | AFFINE_HULL relation %prec OMEGA_P8
1010 { $$
= new Relation
();
1011 *$$
= AffineHull
(*$2);
1014 | CONIC_HULL relation %prec OMEGA_P8
1015 { $$
= new Relation
();
1016 *$$
= ConicHull
(*$2);
1019 | LINEAR_HULL relation %prec OMEGA_P8
1020 { $$
= new Relation
();
1021 *$$
= LinearHull
(*$2);
1024 | HULL relation %prec OMEGA_P8
1025 { $$
= new Relation
();
1026 *$$
= Hull
(*$2,false
,1,Null_Relation
());
1029 | HULL relation GIVEN relation %prec OMEGA_P8
1030 { $$
= new Relation
();
1031 *$$
= Hull
(*$2,false
,1,*$4);
1035 | APPROX relation %prec OMEGA_P8
1036 { $$
= new Relation
();
1037 *$$
= Approximate
(*$2);
1040 | RANGE relation %prec OMEGA_P8
1041 { $$
= new Relation
();
1045 | INVERSE relation %prec OMEGA_P8
1046 { $$
= new Relation
();
1050 | COMPLEMENT relation %prec OMEGA_P8
1051 { $$
= new Relation
();
1052 *$$
= Complement
(*$2);
1055 | GIST relation GIVEN relation %prec OMEGA_P8
1056 { $$
= new Relation
();
1057 *$$
= Gist
(*$2,*$4,1);
1061 | relation
'(' relation
')'
1062 { $$
= new Relation
();
1063 *$$
= Composition
(*$1,*$3);
1067 | relation COMPOSE relation
1068 { $$
= new Relation
();
1069 *$$
= Composition
(*$1,*$3);
1073 | relation CARRIED_BY INT
1074 { $$
= new Relation
();
1075 *$$
= After
(*$1,$3,$3);
1077 (*$$
).prefix_print
(stdout
);
1079 | relation JOIN relation
1080 { $$
= new Relation
();
1081 *$$
= Composition
(*$3,*$1);
1085 | relation RESTRICT_RANGE relation
1086 { $$
= new Relation
();
1087 *$$
= Restrict_Range
(*$1,*$3);
1091 | relation RESTRICT_DOMAIN relation
1092 { $$
= new Relation
();
1093 *$$
= Restrict_Domain
(*$1,*$3);
1097 | relation INTERSECTION relation
1098 { $$
= new Relation
();
1099 *$$
= Intersection
(*$1,*$3);
1103 | relation
'-' relation %prec INTERSECTION
1104 { $$
= new Relation
();
1105 *$$
= Difference
(*$1,*$3);
1109 | relation UNION relation
1110 { $$
= new Relation
();
1111 *$$
= Union
(*$1,*$3);
1115 | relation
'*' relation
1116 { $$
= new Relation
();
1117 *$$
= Cross_Product
(*$1,*$3);
1121 | SUPERSETOF relation
1122 { $$
= new Relation
();
1123 *$$
= Union
(*$2, Relation
::Unknown
(*$2));
1127 { $$
= new Relation
();
1128 *$$
= Intersection
(*$2, Relation
::Unknown
(*$2));
1131 | MAKE_UPPER_BOUND relation %prec OMEGA_P8
1132 { $$
= new Relation
();
1133 *$$
= Upper_Bound
(*$2);
1136 | MAKE_LOWER_BOUND relation %prec OMEGA_P8
1137 { $$
= new Relation
();
1138 *$$
= Lower_Bound
(*$2);
1142 { $$
= new Relation
();
1143 *$$
= Sample_Solution
(*$2);
1146 | SYM_SAMPLE relation
1147 { $$
= new Relation
();
1148 *$$
= Symbolic_Solution
(*$2);
1151 | reachable_of
{ $$
= $1; }
1152 | ASSERT_UNSAT relation
1154 if
(($2)->is_satisfiable
())
1156 fprintf
(stderr
,"assert_unsatisfiable failed on ");
1157 ($2)->print_with_subs
(stderr
);
1166 tupleDeclaration GOES_TO
{currentTuple
= Output_Tuple
;}
1167 tupleDeclaration
{currentTuple
= Input_Tuple
;} optionalFormula
{
1168 Relation
* r
= new Relation
($1->size
,$4->size
);
1170 F_And
*f
= r
->add_and
();
1172 for
(i
=1;i
<=$1->size
;i
++) {
1173 $1->vars
[i
]->vid
= r
->input_var
(i
);
1174 if
(!$1->vars
[i
]->anonymous
)
1175 r
->name_input_var
(i
,$1->vars
[i
]->stripped_name
);
1177 for
(i
=1;i
<=$4->size
;i
++) {
1178 $4->vars
[i
]->vid
= r
->output_var
(i
);
1179 if
(!$4->vars
[i
]->anonymous
)
1180 r
->name_output_var
(i
,$4->vars
[i
]->stripped_name
);
1182 foreach
(e
,Exp
*,$1->eq_constraints
, install_eq
(f
,e
,0));
1183 foreach
(e
,Exp
*,$1->geq_constraints
, install_geq
(f
,e
,0));
1184 foreach
(c
,strideConstraint
*,$1->stride_constraints
, install_stride
(f
,c
));
1185 foreach
(e
,Exp
*,$4->eq_constraints
, install_eq
(f
,e
,0));
1186 foreach
(e
,Exp
*,$4->geq_constraints
, install_geq
(f
,e
,0));
1187 foreach
(c
,strideConstraint
*,$4->stride_constraints
, install_stride
(f
,c
));
1188 if
($6) $6->install
(f
);
1193 | tupleDeclaration optionalFormula
{
1194 $$
= build_relation
($1, $2);
1197 Relation
* r
= new Relation
(0,0);
1198 F_And
*f
= r
->add_and
();
1205 optionalFormula
: formula_sep formula
{ $$
= $2; }
1216 if
(currentTupleDescriptor
)
1217 delete currentTupleDescriptor
;
1218 currentTupleDescriptor
= new tupleDescriptor
;
1221 '[' optionalTupleVarList
']'
1222 {$$
= currentTupleDescriptor
; currentTupleDescriptor
= NULL
; }
1225 optionalTupleVarList
:
1227 | optionalTupleVarList
',' tupleVar
1231 tupleVar
: VAR %prec OMEGA_P10
1232 { Declaration_Site
*ds
= defined
($1);
1233 if
(!ds
) currentTupleDescriptor
->extend
($1,currentTuple
,tuplePos
);
1235 Variable_Ref
* v
= lookupScalar
($1);
1237 if
(ds
!= globalDecls
)
1238 currentTupleDescriptor
->extend
($1, new Exp
(v
));
1240 currentTupleDescriptor
->extend
(new Exp
(v
));
1246 {currentTupleDescriptor
->extend
(); tuplePos
++; }
1247 | exp %prec OMEGA_P1
1248 {currentTupleDescriptor
->extend
($1); tuplePos
++; }
1249 | exp
':' exp %prec OMEGA_P1
1250 {currentTupleDescriptor
->extend
($1,$3); tuplePos
++; }
1251 | exp
':' exp
':' INT %prec OMEGA_P1
1252 {currentTupleDescriptor
->extend
($1,$3,$5); tuplePos
++; }
1256 varList: varList
',' VAR
{$$
= $1; $$
->insert
($3); }
1257 | VAR
{ $$
= new VarList
;
1263 $$
= current_Declaration_Site
= new Declaration_Site
($1);
1264 foreach
(s
,char *, *$1, free
(s
));
1269 /* variable declaration with optional brackets */
1271 varDeclOptBrackets
: varDecl
{ $$
= $1; }
1272 |
'[' varDecl
']' { $$
= $2; }
1275 formula
: formula AND formula
{ $$
= new AST_And
($1,$3); }
1276 | formula OR formula
{ $$
= new AST_Or
($1,$3); }
1277 | constraintChain
{ $$
= $1; }
1278 |
'(' formula
')' { $$
= $2; }
1279 | NOT formula
{ $$
= new AST_Not
($2); }
1280 | start_exists varDeclOptBrackets exists_sep formula end_quant
1281 { $$
= new AST_exists
($2,$4); }
1282 | start_forall varDeclOptBrackets forall_sep formula end_quant
1283 { $$
= new AST_forall
($2,$4); }
1286 start_exists
: '(' EXISTS
1295 start_forall
: '(' FORALL
1306 expList
: exp
',' expList
1317 constraintChain
: expList REL_OP expList
1318 { $$
= new AST_constraints
($1,$2,$3); }
1319 | expList REL_OP constraintChain
1320 { $$
= new AST_constraints
($1,$2,$3); }
1325 { Variable_Ref
* v
= lookupScalar
($1);
1330 | VAR
'(' {argCount
= 1;} argumentList
')' %prec OMEGA_P9
1332 if
($4 == Input_Tuple
) v
= functionOfInput
[$1];
1333 else v
= functionOfOutput
[$1];
1335 fprintf
(stderr
,"Function %s(...) not declared\n",$1);
1342 |
'(' exp
')' { $$
= $2;}
1348 argumentList
',' VAR
{
1349 Variable_Ref
* v
= lookupScalar
($3);
1352 if
(v
->pos
!= argCount || v
->of
!= $1 || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1353 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1359 | VAR
{ Variable_Ref
* v
= lookupScalar
($1);
1362 if
(v
->pos
!= argCount || v
->of
!= Input_Tuple
&& v
->of
!= Output_Tuple
) {
1363 fprintf
(stderr
,"arguments to function must be prefix of input or output tuple\n");
1371 exp
: INT
{$$
= new Exp
($1);}
1372 | INT simpleExp %prec
'*' {$$
= multiply
($1,$2);}
1373 | simpleExp
{ $$
= $1; }
1374 |
'-' exp %prec
'*' { $$
= omega
::negate
($2);}
1375 | exp
'+' exp
{ $$
= add
($1,$3);}
1376 | exp
'-' exp
{ $$
= subtract
($1,$3);}
1377 | exp
'*' exp
{ $$
= multiply
($1,$3);}
1382 REACHABLE_FROM nodeNameList nodeSpecificationList
1384 Dynamic_Array1
<Relation
> *final
=
1385 Reachable_Nodes
(reachable_info
);
1391 REACHABLE_OF VAR IN nodeNameList nodeSpecificationList
1393 Dynamic_Array1
<Relation
> *final
=
1394 Reachable_Nodes
(reachable_info
);
1395 int index
= reachable_info
->node_names.index
(String
($2));
1396 assert
(index
!= 0 && "No such node");
1398 *$$
= (*final
)[index
];
1400 delete reachable_info
;
1406 nodeNameList: '(' realNodeNameList
')'
1407 { int sz
= reachable_info
->node_names.size
();
1408 reachable_info
->node_arity.reallocate
(sz
);
1409 reachable_info
->transitions.resize
(sz
+1,sz
+1);
1410 reachable_info
->start_nodes.resize
(sz
+1);
1414 realNodeNameList: realNodeNameList
',' VAR
1415 { reachable_info
->node_names.append
(String
($3));
1417 | VAR
{ reachable_info
= new reachable_information
;
1418 reachable_info
->node_names.append
(String
($1));
1423 nodeSpecificationList: OPEN_BRACE realNodeSpecificationList CLOSE_BRACE
1426 int n_nodes
= reachable_info
->node_names.size
();
1427 Tuple
<int> &arity
= reachable_info
->node_arity
;
1428 Dynamic_Array2
<Relation
> &transitions
= reachable_info
->transitions
;
1430 /* fixup unspecified transitions to be false */
1432 for
(i
= 1; i
<= n_nodes
; i
++) arity
[i
] = -1;
1433 for
(i
= 1; i
<= n_nodes
; i
++)
1434 for
(j
= 1; j
<= n_nodes
; j
++)
1435 if
(! transitions
[i
][j
].is_null
()) {
1436 int in_arity
= transitions
[i
][j
].n_inp
();
1437 int out_arity
= transitions
[i
][j
].n_out
();
1438 if
(arity
[i
] < 0) arity
[i
] = in_arity
;
1439 if
(arity
[j
] < 0) arity
[j
] = out_arity
;
1440 if
(in_arity
!= arity
[i
] || out_arity
!= arity
[j
]) {
1442 "Arity mismatch in node transition: %s -> %s",
1443 (const char *) reachable_info
->node_names
[i
],
1444 (const char *) reachable_info
->node_names
[j
]);
1449 for
(i
= 1; i
<= n_nodes
; i
++)
1450 if
(arity
[i
] < 0) arity
[i
] = 0;
1451 /* Fill in false relations */
1452 for
(i
= 1; i
<= n_nodes
; i
++)
1453 for
(j
= 1; j
<= n_nodes
; j
++)
1454 if
(transitions
[i
][j
].is_null
())
1455 transitions
[i
][j
] = Relation
::False
(arity
[i
],arity
[j
]);
1458 /* fixup unused start node positions */
1459 Dynamic_Array1
<Relation
> &nodes
= reachable_info
->start_nodes
;
1460 for
(i
= 1; i
<= n_nodes
; i
++)
1461 if
(nodes
[i
].is_null
())
1462 nodes
[i
] = Relation
::False
(arity
[i
]);
1464 if
(nodes
[i
].n_set
() != arity
[i
]){
1465 fprintf
(stderr
,"Arity mismatch in start node %s",
1466 (const char *) reachable_info
->node_names
[i
]);
1473 realNodeSpecificationList:
1474 realNodeSpecificationList
',' VAR
':' relation
1475 { int n_nodes
= reachable_info
->node_names.size
();
1476 int index
= reachable_info
->node_names.index
($3);
1477 assert
(index
!= 0 && index
<= n_nodes
);
1478 reachable_info
->start_nodes
[index
] = *$5;
1482 | realNodeSpecificationList
',' VAR GOES_TO VAR
':' relation
1483 { int n_nodes
= reachable_info
->node_names.size
();
1484 int from_index
= reachable_info
->node_names.index
($3);
1485 int to_index
= reachable_info
->node_names.index
($5);
1486 assert
(from_index
!= 0 && to_index
!= 0);
1487 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1488 reachable_info
->transitions
[from_index
][to_index
] = *$7;
1493 | VAR GOES_TO VAR
':' relation
1494 { int n_nodes
= reachable_info
->node_names.size
();
1495 int from_index
= reachable_info
->node_names.index
($1);
1496 int to_index
= reachable_info
->node_names.index
($3);
1497 assert
(from_index
!= 0 && to_index
!= 0);
1498 assert
(from_index
<= n_nodes
&& to_index
<= n_nodes
);
1499 reachable_info
->transitions
[from_index
][to_index
] = *$5;
1505 { int n_nodes
= reachable_info
->node_names.size
();
1506 int index
= reachable_info
->node_names.index
($1);
1507 assert
(index
!= 0 && index
<= n_nodes
);
1508 reachable_info
->start_nodes
[index
] = *$3;
1516 #if !defined(OMIT_GETRUSAGE)
1517 #include <sys/types.h>
1518 #include <sys/time.h>
1519 #include <sys/resource.h>
1521 struct rusage start_time
;
1524 #if defined BRAIN_DAMAGED_FREE
1530 void *realloc
(void *p
, size_t s
)
1532 return realloc
((malloc_t
) p
, s
);
1536 #if ! defined(OMIT_GETRUSAGE)
1538 extern
"C" int getrusage
(int, struct rusage
*);
1541 void start_clock
( void )
1543 getrusage
(RUSAGE_SELF
, &start_time
);
1546 int clock_diff
( void )
1548 struct rusage current_time
;
1549 getrusage
(RUSAGE_SELF
, ¤t_time
);
1550 return
(current_time.ru_utime.tv_sec
-start_time.ru_utime.tv_sec
)*1000000 +
1551 (current_time.ru_utime.tv_usec
-start_time.ru_utime.tv_usec
);
1555 void printUsage
(FILE *outf
, char **argv
) {
1556 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
);
1561 int omega_calc_debug
;
1570 #define ANY_DEBUG any_debug
1573 int main
(int argc
, char **argv
){
1574 redundant_conj_level
= 2;
1575 current_Declaration_Site
= globalDecls
= new Global_Declaration_Site
();
1580 char * fileName
= 0;
1583 printf
("# %s\n", GIT_HEAD_ID
);
1584 printf
("# %s (based on %s, %s):\n",CALC_VERSION_STRING
, Omega_Library_Version
, Omega_Library_Date
);
1586 calc_all_debugging_off
();
1588 closure_presburger_debug
= 0;
1591 for
(i
=1; i
<argc
; i
++) {
1592 if
(argv
[i
][0] == '-') {
1594 while
((c
=argv
[i
][j
++]) != 0) {
1598 if
(! process_calc_debugging_flags
(argv
[i
],j
)) {
1599 printUsage
(stderr
,argv
);
1605 fprintf
(stderr
,"Note: specifying number of GEQ's is no longer useful.\n");
1606 while
(argv
[i
][j
] != 0) j
++;
1611 fprintf
(stderr
,"Note: specifying number of EQ's is no longer useful.\n");
1612 while
(argv
[i
][j
] != 0) j
++;
1616 redundant_conj_level
= 1;
1618 // Other future options go here
1620 fprintf
(stderr
, "\nUnknown flag -%c\n", c
);
1621 printUsage
(stderr
,argv
);
1627 // Make sure this is a file name
1629 fprintf
(stderr
,"\nCan only handle a single input file\n");
1630 printUsage
(stderr
,argv
);
1634 yyin
= fopen
(fileName
, "r");
1636 fprintf
(stderr
, "\nCan't open input file %s\n",fileName
);
1637 printUsage
(stderr
,argv
);
1644 DebugFile
= fopen
("/dev/null","w");
1647 DebugFile
= fopen
(DEBUG_FILE_NAME
, "w");
1649 fprintf
(stderr
, "Can't open debug file %s\n", DEBUG_FILE_NAME
);
1652 setbuf
(DebugFile
,0);
1655 setOutputFile
(DebugFile
);
1658 initializeScanBuffer
();
1659 currentTupleDescriptor
= NULL
;
1664 foreach_map
(cs
,Const_String
,r
,Relation
*,relationMap
,
1665 {delete r
; relationMap
[cs
]=0;});
1671 Relation LexForward
(int n
) {
1673 F_Or
*f
= r.add_or
();
1674 for
(int i
=1; i
<= n
; i
++) {
1675 F_And
*g
= f
->add_and
();
1676 for
(int j
=1;j
<i
;j
++) {
1677 EQ_Handle e
= g
->add_EQ
();
1678 e.update_coef
(r.input_var
(j
),-1);
1679 e.update_coef
(r.output_var
(j
),1);
1682 GEQ_Handle e
= g
->add_GEQ
();
1683 e.update_coef
(r.input_var
(i
),-1);
1684 e.update_coef
(r.output_var
(i
),1);