Simplification

Functions
bool	vallst_getSubstEqus (VallstInstance *vi)
void	vallst_setConvert3ClausesIntoEqus (VallstInstance *vi, bool b)
void	vallst_setSimpTimeLimitFast (VallstInstance *vi, unsigned int ms)
void	vallst_setSimpTimeLimitSlow (VallstInstance *vi, unsigned int ms)
bool	vallst_setSimpSetting (VallstInstance *vi, VallstLiteralN level, VallstLiteralN sublevel, VallstLiteralN nrOfVars, VallstLiteralN nrOfIterations)
bool	vallst_setSimpSettingSlow (VallstInstance *vi, VallstLiteralN level, VallstLiteralN sublevel, VallstLiteralN nrOfVars, VallstLiteralN nrOfIterations)
VallstResult	vallst_simplify (VallstInstance *vi)
VallstResult	vallst_simplifySlow (VallstInstance *vi)
void	vallst_setSubstEqus (VallstInstance *vi, bool b)
unsigned char	vallst_substEqus (VallstInstance *vi)

---

Function Documentation

bool vallst_getSubstEqus (  VallstInstance *  vi  )

Returns flag. See vallst_setSubstEqus() and vallst_substEqus(). Examples: vallst.c.

void vallst_setConvert3ClausesIntoEqus (  VallstInstance *  vi, bool  b )

Sets the convert-3-clauses flag. 3-clauses on the form: p \/ q \/ r p \/ -q \/ -r -p \/ -q \/ r -p \/ q \/ -r will be converted into an equivalence <->{p,q,r} iff the convert-3-clauses flag is true. p, q and r stand for literals rather than just variables and the clauses and the literals in the clauses may be permuted in any way, clauses representing an equivalence will still be detected and converted if the 3-clause flag is true. The conversion happens at input, when the fourth clause is added. There may be other formulas added in between the four clauses.

bool vallst_setSimpSetting (  VallstInstance *  vi, VallstLiteralN  level, VallstLiteralN  sublevel, VallstLiteralN  nrOfVars, VallstLiteralN  nrOfIterations )

Sets setting for the main, bcp based, simplification, vallst_simplify(). 'level' determines which simplification case the sublevel, nrOfVars and nrOfIterations arguments pertain to. 'level' start at 1 so having level = 0 is pointless. Having nrOfIterations = 0 will traverse once, which might very well be the best strategy. The time complexity for vallst_simplify() for a level n typically is 2^n times the product of the nrOfVars values for that level, not counting iterations (nrOfIterations). Hence be mindful of the complexity explosion! However, there is a time limit in effect too. See vallst_setSimpTimeLimitFast(). 'sublevel' must be less than or equal to level. (Having sublevel=0 makes no sense.) Return true iff not enough memory could be allocated. The default setting for level 1 is a very large nrOfVars value, in effect infinite. The default nrOfIterations value for level 1 is 0. Other lower levels, especially level 2, might also have some default values that imply that simplification will be done on that level. Levels not covered thus far get default values like this: the default setting for nrOfIterations is 0; the default for nrOfVars is 0 if the sublevel is 1, otherwise it is 1.

bool vallst_setSimpSettingSlow (  VallstInstance *  vi, VallstLiteralN  level, VallstLiteralN  sublevel, VallstLiteralN  nrOfVars, VallstLiteralN  nrOfIterations )

Like vallst_setSimpSetting() but used for the slower and stronger vallst_simplifySlow(). See also vallst_setSimpTimeLimitSlow().

void vallst_setSimpTimeLimitFast (  VallstInstance *  vi, unsigned int  ms )

Sets the time limit in millisecs for fast simplification calls, vallst_simplify().

void vallst_setSimpTimeLimitSlow (  VallstInstance *  vi, unsigned int  ms )

Sets the time limit in millisecs for slow simplification calls, vallst_simplifySlow().

void vallst_setSubstEqus (  VallstInstance *  vi, bool  b )

Sets flag. If true, then at least for standalone vallst, variables p equivalent to an equivalence a (e.g. p<->a, a:=-q<->r), will be substituted in other equivalences. (Equivalences here include xors (-<->).)

VallstResult vallst_simplify (  VallstInstance *  vi  )

Simplifies the problem. BCP based. For each level k>0 and each sublevel i, 0<i<=k, in the simplification settings, the m=nrOfVars strongest variables and their negations will be assumed so that there are k nested assumptions. Then bcp will be applied and the cut inferred. This is iterated n=nrOfIterations times. See vallst_setSimpSetting() to define how much simplification is done. The default setting entails *no* simplification (for the API version; the standalone solver will do some simplifications)! VallstResult_other will be returned if no other value is applicable. VallstResult_other+1 will be returned iff the function couldn't even try to do simplifications. This can only happen if certain default compiling options are changed (in particular undefining StrHeur). Uses the simp-time-limit-fast time limit as time limit (or the overall time limit if at the time the overall time limit is smaller). See vallst_setSimpTimeLimitFast(). The fast and weak version. Uses the fast simplification settings (confer vallst_setSimpSetting()) in contrast to the slow and strong vallst_simplifySlow(), which uses the slow simplification settings (confer vallst_setSimpSettingSlow()).

VallstResult vallst_simplifySlow (  VallstInstance *  vi  )

Like vallst_simplify() but slower and stronger. Uses the slow simplification settings, confer vallst_setSimpSettingSlow(), and the slow time limit, confer vallst_setSimpTimeLimitSlow(). Examples: vallst.c.

unsigned char vallst_substEqus (  VallstInstance *  vi  )

Variables p equivalent to an equivalence a (e.g. p<->a, a:=-q<->r), will be substituted in other equivalences. (Equivalences here include xors (-<->).) Returns 1 iff a proof of false was found; 2 iff not enough memory could be allocated; 0 otherwise. Examples: vallst.c.

---