|
|
Returns value. Search will be aborted after this many new variables have been set, to a truth value or to an other equ class. (Aborted that is provided that enough time has passed. See vallst_getNoAbortTime().) Search will also be aborted if fewer vars are set but more time has passed. |
|
|
Returns the current search level.
|
|
|
Returns limit. Given that enough vars are set, search will not abort until no-abort-time seconds have passed. See vallst_getAbortThreshold(). |
|
|
Makes all search assumptions into onetime search suggestions. Used for suggesting a model/state. Suggestions will be chosen as assumptions at the lowest levels in a search. The suggestions will be emptied/reset as soon as one literal suggestion is false. Search assumptions take precedence over search suggestions. Returns true iff not enough memory could be allocated. Any previous suggestions will be emptied/reset.
|
|
||||||||||||
|
Makes a search assumption that will affect vallst_search(). If p is already true, VallstResult_other is returned. If p is already false, VallstResult_proofOfFalseGivenSearchAssumptions is returned. If not enough memory could be allocated, VallstResult_notEnoughMemory is returned. Otherwise VallstResult_other+1 is returned. If p is already true or false, a call to vallst_makeSearchAssumption() will have no effect. |
|
|
Moves the current search state to level 0. Also resets the buffers if the level isn't 0 already.
|
|
|
Removes all search assumptions.
|
|
|
Removes the last search assumption.
|
|
|
Searches for a proof of false or a model. Returns the result of the search. VallstResult_other will be returned if the level isn't 0. If there are search assumptions, VallstResult_proofOfFalseGivenSearchAssumptions and VallstResult_modelOfSearchAssumptions may be returned. If it's determined that there is no model where the extra search assumptions are true as well as the axioms, VallstResult_proofOfFalseGivenSearchAssumptions is returned, except that if a proof of false was found not using the extra search assumptions, VallstResult_proofOfFalse will be returned rather than VallstResult_proofOfFalseGivenSearchAssumptions. Note also that VallstResult_model may be returned instead VallstResult_proofOfFalseGivenSearchAssumptions if it's proved that there is no model satisfying the extra search assumptions but a model to the axioms was in fact found.
|
|
||||||||||||
|
Sets value. Search will be aborted after this many new variables have been set, to a truth value or to an other equ class. (Aborted that is provided that enough time has passed. See vallst_getNoAbortTime().) Search will also be aborted if fewer vars are set but more time has passed. |
|
||||||||||||
|
Sets the frequency. The buffers will be emptied every bufferResetFrequency-th time the search is restarted. You might want to synchronize this value with metaPruneFrequency and perhaps with metaMetaPruneFrequency too so that metaPruneFrequency is a multiple of bufferResetFrequency and metaMetaPruneFrequency is a multiple of metaPruneFrequency. |
|
||||||||||||
|
Sets the value. It determines the size of a constant addition to the buffer size. |
|
||||||||||||
|
Sets the value. It determines the size addition to the buffer size relative to the size of some non-axiom chunk. |
|
||||||||||||
|
Sets the value. It determines the size addition to the buffer size relative to the number of variables allocated for. |
|
||||||||||||
|
Sets the proof improvement leeway. Conflict clause size ccSize1 is considered as good as ccSize2 if ccSize1/ccSize2 <= ccLeeway. Used when the 1-uips are the same. Should probably be 1.0 or slightly greater. |
|
||||||||||||
|
Sets the create-phantom-conflict-clauses flag. Conflict clauses will be marked as deleted iff createPhantomConflictClauses is true and they aren't short. False by default. If you change this flag from false to true after a search has been made the buffers will also reset. This flag, if set to true, might interact with the improveProofLevel and keepConflictClauseLengthThreshold options to affect proof improvement in a perhaps subtle way. See the note on vallst_setImproveProofLevel(). |
|
||||||||||||
|
Sets the base/initial restart size. Typically used as the initial number of end nodes until the first restart is made. Restarts may be postponed for other reasons during the search batch. The value is supposed to be the least size that is sensible to have as a search batch size and is used as a base for restart strategies. If the Luby-Sinclair-Zuckerman restart strategy is used, all batch sizes will be multiples of this value. See vallst_setRestartPredefFunc(). |
|
||||||||||||
|
Sets what's to be considered good. Clause sizes <= goodClauseSize are considered good. If a conflict clause size is good the next restart will be postponed. |
|
||||||||||||
|
Sets what's to be considered good. Levels <= goodLevel are considered good. If the search backtracks to a good level the next restart will be postponed. |
|
||||||||||||
|
Sets how many axioms, starting from the last one, that should be checked to see if they are open, in some branching heuristics. Binary clauses don't count! |
|
||||||||||||
|
Sets the level threshold. The solver will try to improve proofs if the current level is less than improveProofLevel. Hence, setting it to 0 will turn off proof improvements. There are situations where the algorithm won't make an effort to improve proofs even if the level is less than improveProofLevel. Note that trying to improve proofs while createPhantomConflictClauses is true might give rise to a situation where the prover during a proof improvement attempt can't re-prove what it just proved: Let |-0 stand for closure under bcp. Assume that improveProofLevel is large enough and keepConflictClauseLengthThreshold is small enough. Assume that ...+p+q+r|-0 0, where 0 stands for a contradiction. Then ...+p+q proves -r with reason c_r and say that c_r is a phantom clause. Assume that ...+p+q+-r|-0 0. Then ...+p|- -q but this proof depends on c_r and it's not necessarily the case that we now have ...+p+q|-0 0. In this situation, i.e. when the proof improvement attempt fails to even find a proof of false, the proof path is aborted and the state is reverted back to the first proof before proof improvement was last attempted. Hence, if you want to try to improve proofs while creating phantom conflict clauses, you still might want to lower the improve-proof-level in order to get the proof improvement to work more effectively. Ideally one might want to somehow synchronize improveProofLevel and vallst_setKeepConflictClauseLengthThreshold(). |
|
||||||||||||
|
Sets the keep-conflict-clause-length meta meta threshold. keepCCMetaMetaThreshold functions as a lower bound for various non-axiom pruning thresholds. Non-axioms of size less than or equal to keepCCMetaMetaThreshold will be kept. The intended use is to have:
Furthermore, the tight thresholds are intended to be less than or equal to the loose ones (where it makes sense):
It is also the intention that the below meta-meta, meta, object relations hold:
|
|
||||||||||||
|
Sets the keep-conflict-clause-length threshold. Conflict clauses less than or equal to keepConflictClauseLengthThreshold will be fully added even if the createPhantomConflictClauses flag is true. Also, when using conflict clause buffers, if the conflict clause is less than or equal to keepConflictClauseLengthThreshold the clause will be added, to the non-axioms, as a proper first class clause. Note though that a doppelganger may be created too. A threshold of less than 2 will have the same effects as a threshold of 2. Therefore any value lower than 2 will be raised to 2. This flag might interact with the improveProofLevel and createPhantomConflictClauses options, if the latter is set to true, to affect proof improvement in a perhaps subtle way. See the note on vallst_setImproveProofLevel(). The intention is to have tightKeepCCThreshold <= keepConflictClauseLengthThreshold. |
|
||||||||||||||||
|
Sets the function defining the strength of literal pairs (p,-p) given the strength of the literals p and -p. The litPairStrFunc function should return a measure of the combined strength of p and -p given the individual strength of p and -p. varStrPtr[0] will be the strength of the unnegated variable (p), varStrPtr[1] will be the strength of the negated variable (-p). The default function looks something like this: static Strength litPairStrF( Strength * varStrPtr )
{
return varStrPtr[0] * varStrPtr[1];
} Unfortunately, because the Strength type isn't (for various reasons) part of the interface/library, you have to provide two versions of the function: 1) a version with type double as the Strength type, 2) a version with type long double as the Strength type. |
|
||||||||||||
|
Sets meta leeway. Like vallst_setLooseTheorySizeLeeway() but used after meta pruning. The intention is to have tightTheoryMetaSizeLeeway <= looseTheoryMetaSizeLeeway. |
|
||||||||||||
|
Sets meta meta leeway. The nr of non-axioms is allowed to grow in loose mode to at most nrOf(non-erased)Axioms * looseTheorySizeLeeway before relevant parameters are tightened in order to bring the size of the theory back down again. Used after meta meta pruning. The intention is to have tightTheorySizeLeeway <= looseTheorySizeLeeway. See also vallst_setKeepCCMetaMetaThreshold(). |
|
||||||||||||
|
Sets leeway. Like vallst_setLooseTheorySizeLeeway() but used before meta meta pruning. The intention is to have tightTheorySizeLeewayKeep <= looseTheorySizeLeewayKeep. |
|
||||||||||||
|
Sets the looseTimeLimitBase parameter to k. The heuristic mode timers will be something like looseTimeLimitBase * looseBias + nrOfRestarts * looseTimeLimitMod. |
|
||||||||||||
|
Sets the looseTimeLimitMod parameter to k. The heuristic mode timers will be something like looseTimeLimitBase * looseBias + nrOfRestarts * looseTimeLimitMod. |
|
||||||||||||
|
Sets the value. The value determines the maximal number of times the simplify call during search can be skipped (because the theory didn't become sufficently much stronger from the last time simplification was made). |
|
||||||||||||
|
Sets the value. These start and end values determine which clauses are kept during pruning. A clause is kept iff it's on or below the line starting at the start value and ending at the end value. The actual end point used will be the minimum of meta(Meta)PruneEnd and (tight) keep-cc-length-threshold. The idea is to keep the meta meta pruning more restrictive and rarer than the meta pruning although that's not required. See vallst_setKeepCCMetaMetaThreshold() for more on the intended relation between different thresholds. |
|
||||||||||||
|
Sets the frequency. The proper non-axioms will be meta meta pruned, using metaMetaPruneStart and metaMetaPruneEnd, every metaMetaPruneFrequency-th time the search is restarted. You might want to synchronize this value with bufferResetFrequency and perhaps also with metaPruneFrequency so that metaPruneFrequency is a multiple of bufferResetFrequency and metaMetaPruneFrequency is a multiple of metaPruneFrequency. |
|
||||||||||||
|
Sets the value. See vallst_setMetaMetaPruneEnd().
|
|
||||||||||||
|
Sets the value. See vallst_setMetaMetaPruneEnd(). Not that relevant since tightKeepCCThreshold and keepConflictClauseLengthThreshold are used as endpoints instead of this metaPruneEnd value if metaPruneEnd is larger. Hence you might want to leave metaPruneEnd at the default infinite value. |
|
||||||||||||
|
Sets the frequency. The proper non-axioms will be (meta) pruned, using metaPruneStart and metaPruneEnd, every metaPruneFrequency-th time the search is restarted provided that it's not time for a meta meta pruning. You might want to synchronize this value with bufferResetFrequency and perhaps also metaMetaPruneFrequency so that metaPruneFrequency is a multiple of bufferResetFrequency and metaMetaPruneFrequency is a multiple of metaPruneFrequency. |
|
||||||||||||
|
Sets the value. See vallst_setMetaMetaPruneEnd().
|
|
||||||||||||
|
Sets the next-batch-size-const value. The restart batch size will possibly increase with nextBatchSizeConst, depending on the restart strategy. (The restart batch size may depend on other things too.) |
|
||||||||||||
|
Sets value. Given that enough vars are set, search will not abort until secs seconds have passed. See vallst_getAbortThreshold(). |
|
||||||||||||
|
If positiveHeurAxSign is true, the sign of the branching literal will be the sign it has in the formula from where it was derived, if it is derived from an axiom in the sos-like heuristic set (i.e. if the axiom comes late) (see vallst_setHeurAxSize()). This can be useful e.g. if you don't want to set the positiveSign to true but still want the literals picked from the last axiom to be true, e.g. when solving an optimization problem with a large driving last axiom to optimize. |
|
||||||||||||
|
Depending on other settings as well, if positiveSign is true, the sign of the branching literal will be the sign it has in the formula from where it was derived. |
|
||||||||||||
|
With prob/1000 probability the sign of the literal to branch on will be chosen randomly. (This will not affect any added search assumptions of course.) |
|
||||||||||||
|
With prob/1000 probability the open literal to branch on in a formula will be chosen randomly. |
|
||||||||||||
|
Moved temporary causes no longer active will be removed iff the removeTmpCauses flag is true. This flag will have no very large impact but left-over causes no longer active might screw up some heuristics.(???) |
|
||||||||||||
|
The flag tells whether buffers should be reset when moving up to level 0 between searches. |
|
||||||||||||
|
Sets restart batch size function. The restart batch size function should return the next batch size, which should be greater than 0. lastSize is the last batch size. At the very first invocation of each search, the value provided will be taken to be firstRestart. nrOfRestarts is the number of restarts made so far. Is 0 at each search start. |
|
||||||||||||
|
Sets the restart batch size function used to the fth function below: 0: Luby-Sinclair-Zuckerman restart strategy (1,1,2,1,1,2,4,1,1,2,1...) with firstRestart used as a base size. 1: Starting at firstRestart size, the sizes will be incremented using nextBatchSizeConst. Returns true iff f doesn't designate a legitimate function, i.e. iff f>1. To set firstRestart, see vallst_setFirstRestart(). |
|
||||||||||||
|
Sets the restart batch prolong cap. A restart batch won't be prolonged to be (much) more than the value at the start of the batch times restartProlongCap. |
|
||||||||||||
|
Sets the start phase size. A restart time strictly less than restartStart belongs to the start phase of a restart search batch which will possibly imply a different branching heuristic from the main phase. |
|
||||||||||||
|
Sets flag. Decides which bcp function should be applied first. The other bcp function will then be used if a proof improvement is attempted. |
|
||||||||||||
|
Will be greater than or equal to 1. Heuristic strength str is considered to be maximal iff leeway * str >= maxStr where maxStr is the real maximal strength. The Formula variant of leeway (see vallst_setStrengthLeewayFormula() below) is used for formula based heuristics. This non-formula variant is used elsewhere for absolute heuristics. |
|
||||||||||||
|
Will be greater than or equal to 1. Heuristic strength str is considered to be maximal iff leeway * str >= maxStr where maxStr is the real maximal strength. This Formula variant of leeway is used for formula based heuristics. The non-formula variant (see vallst_setStrengthLeeway() above) is used elsewhere for absolute heuristics. |
|
||||||||||||
|
Sets a hard cap of the maximal number of strengths to be considered maximal by the strength-leeway construction (see vallst_setStrengthLeeway()). Will be greater than or equal to 1. |
|
||||||||||||
|
Sets a hard cap of the maximal number of strengths to be considered maximal by the strength-leeway-formula construction (see vallst_setStrengthLeewayFormula()). Will be greater than or equal to 1. |
|
||||||||||||
|
Sets the tight proof improvement leeway. Like the normal ccLeeway but used when the 1-uips differ. Should probably be 1.0 or slightly greater. |
|
||||||||||||
|
Like vallst_setKeepConflictClauseLengthThreshold() but for when the search heuristic is in tight mode. The intention is to have tightKeepCCThreshold <= keepConflictClauseLengthThreshold. |
|
||||||||||||
|
Like vallst_setMetaMetaPruneEnd() but for when the search heuristic is in tight mode. |
|
||||||||||||
|
Like vallst_setMetaMetaPruneStart() but for when the search heuristic is in tight mode. |
|
||||||||||||
|
Like vallst_setMetaPruneStart() but for when the search heuristic is in tight mode. |
|
||||||||||||
|
Sets meta leeway. Like vallst_setTightTheorySizeLeeway() but used after meta pruning. The intention is to have tightTheoryMetaSizeLeeway <= looseTheoryMetaSizeLeeway. |
|
||||||||||||
|
Sets meta meta leeway. The nr of non-axioms is allowed to grow in tight mode to at most nrOf(non-erased)Axioms * tightTheorySizeLeeway before relevant parameters are tightened in order to bring the size of the theory back down again. Used after meta meta pruning. The intention is to have tightTheorySizeLeeway <= looseTheorySizeLeeway. See also vallst_setKeepCCMetaMetaThreshold(). |
|
||||||||||||
|
Sets leeway. Like vallst_setTightTheorySizeLeeway() but used before meta meta pruning. The intention is to have tightTheorySizeLeewayKeep <= looseTheorySizeLeewayKeep. |
|
||||||||||||
|
Sets the tightTimeLimitBase parameter to k. The heuristic mode timers will be something like tightTimeLimitBase * tightBias + nrOfRestarts * tightTimeLimitMod. |
|
||||||||||||
|
Sets the tightTimeLimitMod parameter to k. The heuristic mode timers will be something like tightTimeLimitBase * tightBias + nrOfRestarts * tightTimeLimitMod. |
|
||||||||||||
|
Sets the useDoppelganger flag. Determines if, when the conflict clause is saved in a non-buffer as a proper non-axiom, an extra copy phantom clause should be added to a buffer in order to preserve clause order for branching heuristics. |
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.