- Added more fine-grained control for the associativity of tupling:
--tupling=n * 0: right-associative; 1: left-associative; others are reserved for future use. --ra-tupling * Sets the default, but is there for symmetry.
This commit is contained in:
parent
cb315aafc8
commit
2e9e43742e
@ -39,7 +39,7 @@ switchesInit (int argc, char **argv)
|
|||||||
switches.engine = POR_ENGINE; // default is partial ordering engine
|
switches.engine = POR_ENGINE; // default is partial ordering engine
|
||||||
switches.match = 0; // default matching
|
switches.match = 0; // default matching
|
||||||
switches.clp = 0;
|
switches.clp = 0;
|
||||||
switches.la_tupling = false;
|
switches.tupling = 0;
|
||||||
|
|
||||||
// Pruning and Bounding
|
// Pruning and Bounding
|
||||||
switches.prune = 2; // default pruning method
|
switches.prune = 2; // default pruning method
|
||||||
@ -379,21 +379,52 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect (' ', "ra-tupling", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
/* for experts only
|
||||||
|
helptext ("--ra-tupling", "compile using right-associative tupling");
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.tupling = 0;
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
if (detect (' ', "la-tupling", 0))
|
if (detect (' ', "la-tupling", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
/* not very important
|
/* for experts only
|
||||||
helptext ("--la-tupling", "compile using left-associative tupling");
|
helptext ("--la-tupling", "compile using left-associative tupling");
|
||||||
*/
|
*/
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
switches.la_tupling = true;
|
switches.tupling = 1;
|
||||||
return index;
|
return index;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect (' ', "tupling", 1))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
/* for experts only
|
||||||
|
helptext ("--tupling", "tupling type to use");
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.tupling = integer_argument ();
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
/* ==================
|
/* ==================
|
||||||
* Modelchecker only
|
* Modelchecker only
|
||||||
*/
|
*/
|
||||||
|
@ -18,7 +18,7 @@ struct switchdata
|
|||||||
int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE)
|
int engine; //!< Engine type (POR_ENGINE,ARACHNE_ENGINE)
|
||||||
int match; //!< Matching type.
|
int match; //!< Matching type.
|
||||||
int clp; //!< Do we use clp?
|
int clp; //!< Do we use clp?
|
||||||
int la_tupling; //!< Tupling is by default right-associative, optionally left-associative.
|
int tupling; //!< Tupling is by default 0: right-associative, optionally 1: left-associative.
|
||||||
|
|
||||||
// Pruning and Bounding
|
// Pruning and Bounding
|
||||||
int prune; //!< Type of pruning.
|
int prune; //!< Type of pruning.
|
||||||
|
16
src/tac.c
16
src/tac.c
@ -167,17 +167,19 @@ tacTuple (Tac taclist)
|
|||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
if (switches.la_tupling)
|
switch (switches.tupling)
|
||||||
{
|
|
||||||
/* switch --la-tupling */
|
|
||||||
/* left-associative */
|
|
||||||
return tacTupleLa (taclist);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
{
|
||||||
|
case 0:
|
||||||
|
/* case 0: as well as */
|
||||||
/* DEFAULT behaviour */
|
/* DEFAULT behaviour */
|
||||||
/* right-associative */
|
/* right-associative */
|
||||||
return tacTupleRa (taclist);
|
return tacTupleRa (taclist);
|
||||||
|
case 1:
|
||||||
|
/* switch --la-tupling */
|
||||||
|
/* left-associative */
|
||||||
|
return tacTupleLa (taclist);
|
||||||
|
default:
|
||||||
|
error ("Unknown tupling mode (--tupling=%i)", switches.tupling);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user