Optimization

Functions
bool	vallst_getBreadthFstOptStrat (VallstInstance *vi)
bool	vallst_maxConstraints (VallstInstance *vi, VallstFormulaNames *names, VallstFormulaN pushedConstraintPos, VallstLiteralN *constraintIncs, bool *levelCreated)
void	vallst_setBreadthFstOptStrat (VallstInstance *vi, bool b)

---

Function Documentation

bool vallst_getBreadthFstOptStrat (  VallstInstance *  vi  )

Returns the optimization strategy flag. If true, min/max formulas will be optimized in a breadth first fashion e.g. in vallst standalone. Otherwise the last min/max axiom will be the one pushed. See vallst.c. Examples: vallst.c.

bool vallst_maxConstraints (  VallstInstance *  vi, VallstFormulaNames *  names, VallstFormulaN  pushedConstraintPos, VallstLiteralN *  constraintIncs, bool *  levelCreated )

Calculates the maximum amount the constraint constants in 'names' can be raised while still maintaining the model. The calculated max amounts will be placed in constraintIncs like this: pushedConstraintPos will correspond to constraintIncs+0; prev(pushedConstraintPos) to constraintIncs+1; ... Semi-completes the model for open literals in the constraints. The literals will all be set on one level greater than the current one. Note that that is a bit of a hack since all the literals on that level will really be assumptions and not consequences. However, since the open literals set could be very many and there shouldn't be any problem with this hack, they are collected to one level. You can undo the semi-completion by moving up one level (i.e. undoing one level, moving to a lesser level). See vallst_undoLevel(). However, if no literal was set, no new level will be created. If levelCreated isn't NULL, *levelCreated will be set to true iff a new level was created; otherwise it is set to false. Returns true iff an out of memory error occurred. pushedConstraintPos must be the position of a constraint in 'names'. pushedConstraintPos will be the first position processed. Then prev(pushedConstraintPos) will be processed, and so on. The state should be a model (i.e. all axioms should be satisfied). The raise for formulas of type <\/ where the left disjunct is true will be set to 0. See vallst.c for an example. Examples: vallst.c.

void vallst_setBreadthFstOptStrat (  VallstInstance *  vi, bool  b )

Sets the optimization strategy flag. If true, min/max formulas will be optimized in a breadth first fashion e.g. in vallst standalone. Otherwise the last min/max axiom will be the one pushed. See vallst.c.

---