|
||||||||||||||||||||
|
Adds an axiom. New unit clauses will be put as unchecked w.r.t bcp. Literals are represented by 2, 3, 4,... 2 is the first variable. 3 is the negation of the first variable. In general 2n is the nth variable and 2n+1 is the negation of the nth variable. 'size' is the size of the formula to add, i.e. the length of 'axiom'. E.g. if the formula is a ternary clause 3\/6\/8, 'size' should be 3, type should be VallstFormulaType_clause and axiom should be [3,6,8]. E.g. 1 < p+q+r is represented as [1,p,q,r] (where p, q and r are numbers representing literals) and the size is 4. 2 < 3*p + 2*q + r + s is represented as [2,3,p,2,q,1,r,1,s] with size 9. p \/ c<q+r+s is represented as [p,c,q,r,s] with size 5. The axiom array might be altered. VallstResult_other is returned if no other value is applicable. VallstResult_model is never returned. Neither is VallstResult_modelOfSearchAssumptions, nor VallstResult_proofOfFalseGivenSearchAssumptions. For <*-formulas a variable p is allowed to occur as many times as you like, both positively and negatively. I.e. the literal list may look like ...d*p...e*p...f*-p...g*p...h*-p... For more-than and more-than-dis formulas it's an error if a literal occurs twice with the same sign, i.e. if the literal list looks like ...p...p... or ...-p...-p... where p is a variable. ...p...-p... is allowed though. If the type is more-than-dis and the formula is p\/a, then p and -p are allowed to occur in a. Literal constants in <*-formulas may be 0, like e.g. in c < ...0*p.... You may use 0 and 1 as false and true constants if you like. (This of course only works here and not for the file parser where 0 marks the end of formulas.) If you have unit-clauses to add it might be slightly more efficient to supply them first. You might want to add the more important axioms, like e.g. a conclusion if there is something like that, last. This is for efficiency reasons since some heuristics go through the axioms from the last one to the first one. There might also be some sort of sos-like strategy in use where only the last n axioms will be considered. It might be good to have strong (short) formulas before weak (long) ones. (Consider though also the above paragraph.) |
|
||||||||||||||||||||
|
Adds a formula that should be a consequence of the axioms since the formula might be removed. (It's guaranteed though that formulas with less than 4(?) literals won't be removed.) The formula must be a cnf clause, otherwise VallstResult_parseError is return. Otherwise it works like vallst_addAxiom(). |
|
||||||||||||||||||||||||
|
Adds a named axiom. Works like vallst_addAxiom() except that a name of the axiom is placed in namePtr for future reference. The return value might also be different, see below. If namePtr is NULL, nothing extra is done at all and vallst_addNamedAxiom() will work exactly like vallst_addAxiom(). Note that even if you successfully called vallst_addNamedAxiom() creating a new axiom, the axiom might internally have been tranformed into something you might not have expected. E.g. even if you input a long more-than-dis axiom, this might be turned into a binary clause. If a new axiom b was created, and b isn't a binary disjunction, then VallstResult_other will be returned and namePtr will be updated if it isn't NULL. Important to note is that binary clauses are treated in a special way because it's not very convenient or feasible to give them names like for other formulas. Instead, if a new axiom b was created, and b is a binary disjunction, either because the input was a binary clause or the input was transformed into a binary clause internally, then when a name is requested for b, *namePtr will be assigned 'axiom' (*namePtr = axiom) and the two disjuncts in the binary clause will be placed at the first two positions, [0..1], in the *namePtr/axiom array. VallstResult_other is returned. If no axiom was created and no already existing formula was found to be equivalent to 'axiom', (e.g. because the axiom was found inconsistent and vallst_addNamedAxiom() therefor returned VallstResult_proofOfFalse), namePtr will be assigned NULL. If no axiom was created because 'axiom' was found to already be true, namePtr will be assigned NULL and VallstResult_other+1 will be returned. If no axiom was created but, or rather because, 'axiom' was found to be equivalent to a literal, p, *namePtr will be assigned 'axiom' (*namePtr = axiom), p will be placed in the first position ([0]) in the *namePtr/axiom array (axiom[0] = p) and VallstResult_other+2 will be returned (and p will of course be set to true). If no axiom was created because 'axiom' was found to be equivalent to an already existing axiom b, then *namePtr will be assigned 'axiom' (*namePtr = axiom) when b is a binary clause; *namePtr will be a name of b when b isn't a binary clause. The equivalent axiom b is a disjunction and the disjuncts in b are placed in the first positions, [0..k], in the namePtr/axiom array. Also, vallst_addNamedAxiom() will return VallstResult_other+1+size where size is the number of literals in b so that e.g. VallstResult_other+1+2 will be returned when 'axiom' is found to be equivalent to a binary disjunction. Here is a summary:
Note that in the above summary, [...] denotes the 'axiom' array provided as an argument to the function. Hence it is of a temporary nature and may very well be overwritten (by the owner of the axiom array; indeed, overwriting it is probably the natural and common thing to do eventually). As things are at the moment, no value greater than VallstResult_other+4 will ever be returned; 'axiom' will not be found to be equivalent to e.g. a disjunction with 4 disjuncts. You can use vallst_formulaType() to find out the type of a formula name. Getting a name for an axiom is useful e.g. for axiom strengthening: Assume e.g. that you have got a model for a theory and want to make the theory stronger, e.g. by incrementing the constant in a more-than axiom, to see if the stronger theory has a model or not. To do that you can just call some alter-axiom function to make the theory stronger and keep everything else, including all derived consequences of the previous theory, as it is. |
|
||||||||||||||||
|
Adds c to the constant in a more-than (<), more-than-mult (<*) or more-than-dis (<\/) axiom. Returns VallstResult_parseError if 'name' isn't a name of a formula of more-than* type or if the level isn't 0. VallstResult_notEnoughMemory is returned in case not enough memory could be allocated. VallstResult_proofOfFalse may also be returned. Otherwise, Vallst_other is returned. Note that only strengthening of axioms is supported. As a consequence you can't keep Tseitin names of <*-axioms that you alter because the p\/-a part would get weaker when the constant is increased. (Intuitively, if you strengthen a and have p<->a and -p is used positively elsewhere, that would weaken the theory, which isn't supported.) (If you want to weaken/undo something you can either use search assumptions; or you can save the theory/state and then later revert back to the saved theory/state.)
|
|
||||||||||||||||
|
Like vallst_alterAxiomIncMT() but also adds c to any literal constant d in 'name' that is greater than the current constraint constant. 'name' must be of <* type.
|
|
||||||||||||
|
Extends the number of variables ready to be used. true is returned iff the extension failed --- which can only happen due to insufficient memory. nrOfVars is meant to be a roughly minimal upper bound for the number of variables, like in the DIMACS cnf prologue. Any value will work though and if you don't have any good guess of a roughly minimal upper bound don't use this function. This function only exists for memory efficiency purposes and you are never required to use it. If nrOfVars is less than or equal to the current value, nothing will be done. You should, for efficiency reasons, try to use this function if you have an already built theory (that you e.g. just have decided) and you now want to extend or change the theory with a known number of variables.
|
|
|
Returns the type of the formula with name formulaName. To follow vallst_addNamedAxiom(), vallst_formulaType() will return 1, representing the true constant, if formulaName is NULL. It will return VallstFormulaType_clause if *formulaName isn't a type (refer to the vallst_addNamedAxiom() case where formulaName = axiom = [p,...] where p is a literal and not a type).
|
|
|
Returns the constant in a formula of type <, <\/ or <*. Returns VallstLiteralN_parseError if the formula is of wrong type.
|
|
||||||||||||
|
Returns the full status of literal p. 0 is returned iff p is held false (i.e. -p is true). 1 is returned iff p is held true. Otherwise p is open and 2 is returned. |
|
|
Returns the keep-aboves flag. If true, constant-aboves will be kept aboves e.g. in vallst standalone if constraint constants are to be increased. See vallst_alterAxiomIncMTMKeepAboves() and vallst.c.
|
|
||||||||||||
|
Returns the status of literal p. true is returned iff p is held true. Otherwise false is returned. |
|
|
Returns the number of variables that has been allocated for.
|
|
|
Returns the sum of the literal constants in a more-than-mult (<*) formula. Takes constant time. Returns VallstLiteralN_parseError if the formula is of the wrong type.
|
|
|
Returns true iff name is a constraint (i.e. of type <, <* or <\/). If name is NULL, false will be returned.
|
|
||||||||||||
|
Tranforms a >=*-formula into a <*-formula using c >= +{di*pi} <=> +{di}-c-1 < +{di*-pi}. For example, [3,2,p,3,q,1,r] (size=7) with type >=*, representing 3 >= 2p+3q+1r, is transformed into the equivalent [2,2,-p,3,-q,1,-r] with type <*, representing 2 < 2*'-p'+3*'-q'+1*'-r', where p, q,... are numbers. Returns true iff +{di}-c-1 < 0, i.e. c >= +{di}, in which case a isn't altered. I.e. if true is returned, the formula a is a tautology and can be ignored. |
|
||||||||||||
|
Tranforms a >=-formula into a <-formula using c >= p1+...+pn <=> n-c-1 < +{-pi}. For example, [2,p,q,r] (size=4) with type >=, representing 2 >= p+q+r, is transformed into the equivalent [0,-p,-q,-r] with type <, representing 0 < '-p'+'-q'+'-r', where p, q,... are numbers. Returns true iff n-c-1 < 0, i.e. c >= n, in which case a isn't altered. I.e. if true is returned, the formula a is a tautology and can be ignored. |
|
|
Returns -p, i.e. the negation of the literal p.
|
|
||||||||||||
|
Sets flag. If true, constant-aboves will be kept aboves e.g. in vallst standalone if constraint constants are to be increased. See vallst_alterAxiomIncMTMKeepAboves() and vallst.c. |
|
||||||||||||
|
Sets the main constant for an (a)tsp. This value will be used when the formula is parsed and nowhere else. The edge sum formula will be (min) c >= d0*p0 + ... + dn*pn. Any value larger than or equal to the total sum s = d0+...+dn will reduce to s-1. |
|
||||||||||||
|
Evaluates the summation side in a more-than* formula given the current state. Open literals will count as true. Returns the sum. Returns VallstLiteralN_parseError if the formula isn't a more-than* formula. See vallst_sumTrue() for the intended use. |
|
||||||||||||
|
Evaluates the summation side in a more-than* formula given the current state. Open literals will count as false. Returns the sum. Returns VallstLiteralN_parseError if the formula isn't a more-than* formula. The intended use of this function is like this: Assume that you have found a model to a problem which contains constraint formulas a_k := c_k < +{d_i*p_i}. Then you can call this function for all a_k to know of a lower bound of how high you can raise the c_k constants and still have a model. Then you can carry out the increase of the constants --- possible after that you have moved up to level 0 --- and then maybe strengthen the theory further to see if the constants found were optimal. (See the various axiom altering functions on how to increase constants in constraints.) Since open variables can be interpreted either way you can use vallst_sumOpenTrue() instead if you know that the variables in the formulas you are interested in are disjoint. If the variables aren't disjoint, some caution is of course needed. Assume e.g. a_0 := c_0 < ...d_j*p_j... and a_1 := c_m < ...d_k*-p_j... where p_j is open. Then you can't of course count both p_j and -p_j as true. But you can always use vallst_sumOpenTrue() on at least one formula a_i. |
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.