Allocation

Functions
VallstInstance *	vallst_newInstance (VallstLiteralN nrOfVars, VallstFormulaN nrOf3ClausesEstimate, VallstFormulaN nrOfLitOccsEstimate)
bool	vallst_propagateNrOf3ClausesEstimate (VallstInstance *vi)
bool	vallst_propagateNrOfLitOccsEstimate (VallstInstance *vi)
void	vallst_setFstNrOfLevelsAllocSize (VallstInstance *vi, VallstLiteralN size)
void	vallst_setMaxHashLoad (VallstInstance *vi, double maxLoad)
void	vallst_setNonAxChunkSizeAxDep (VallstInstance *vi, double value)
void	vallst_setNonAxChunkSizeConst (VallstInstance *vi, VallstFormulaN value)
void	vallst_setNonAxChunkSizeVarDep (VallstInstance *vi, double value)
void	vallst_setNrOf3ClausesEstimate (VallstInstance *vi, VallstFormulaN pNrOf3Clauses)
void	vallst_setNrOfFreeChunksCap (VallstInstance *vi, unsigned int cap)
void	vallst_setNrOfLitOccsEstimate (VallstInstance *vi, VallstFormulaN pNrOfLitOccs)

---

Function Documentation

VallstInstance* vallst_newInstance (  VallstLiteralN  nrOfVars, VallstFormulaN  nrOf3ClausesEstimate, VallstFormulaN  nrOfLitOccsEstimate )

Returns a new vallst problem instance. NULL is returned iff a new instance couldn't be created, 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 including 0 will work though and if you don't have any good guess of a roughly minimal upper bound just use any value as long as it isn't much larger than the largest variable to be used. If nrOfVars is 0, no variable space will be allocated. Using nrOfVars=0 is useful for memory efficiency reasons if you at first don't know how many variables that are used. If you later learn of a roughly minimal upper bound on the variables you can call vallst_extendNrOfVars(). See vallst.c for an example. nrOf3ClausesEstimate is meant to be an estimate of the number of ternary clauses. It's not important that nrOf3Clauses is exactly accurate but any fairly accurate estimate might be helpful for memory efficiency reasons. You can use nrOf3ClausesEstimate=0, and then later, before adding ternary clauses, set an estimate with vallst_setNrOf3ClausesEstimate() and propagate the value by calling vallst_propagateNrOf3ClausesEstimate(). See vallst.c for an example. If you know that there will be ternary clauses but have no idea of how many, just use any value not too large, e.g. 0. The only motive behind this number of ternary clauses estimate is to improve efficiency a little; it's not very important. nrOfLitOccsEstimate is supposed to be a possibly rough estimate of the number of literal/constant occurrences in the input theory modulo "special accounting". The special accounting works like this: Occurrences in unit formulas or binary disjunctions don't count at all; add 1 for each formula (that isn't unit or a binary disjunction); add 1 for each formula that isn't a ternary disjunction (and not unit or a binary disjunction); add 2 for each <*-formula; the count for ggcdit is exactly 4. For example, the count for c < c1*p1 + ... + cn*pn would be 1 + 2*n + 1 + 1 + 2. It's not important that the estimate is exactly accurate but any fairly accurate estimate might be helpful for memory efficiency reasons. Try to make it an upper bound. You could also set the value to some fraction of the "correct" value. Just try not to get a too low value. You can use nrOfLitOccsEstimate = VallstFormulaN_undef, and then later, before adding formulas, set an estimate with vallst_setNrOfLitOccsEstimate() and propagate the value by calling vallst_propagateNrOfLitOccsEstimate(). See vallst.c for an example. Examples: vallst.c.

bool vallst_propagateNrOf3ClausesEstimate (  VallstInstance *  vi  )

See vallst_newInstance() for a description. Returns true iff not enough memory could be allocated. Nothing is done if the nrOf3ClausesEstimate in vi is undefined, i.e. equals VallstFormulaN_undef. Examples: vallst.c.

bool vallst_propagateNrOfLitOccsEstimate (  VallstInstance *  vi  )

See vallst_newInstance() for a description. Returns true iff not enough memory could be allocated. Nothing is done if the theory memory is already set up somehow, i.e. the theory memory isn't NULL. If the nrOfLitOccsEstimate in vi is undefined, i.e. equals VallstFormulaN_undef, nrOfLitOccsEstimate in vi will be set to some value first before propagation. If it's possible, try to set the number of variables, explicitly or implicitly, before calling this function since some heuristic size value function will use that variable value. See e.g. vallst.c. Examples: vallst.c.

void vallst_setFstNrOfLevelsAllocSize (  VallstInstance *  vi, VallstLiteralN  size )

Sets the fstNrOfLevelsAlloc size. If no smaller value can be seen to be enough, like e.g. the number of variables, this value will be used as a first allocation size of nr-of-levels dependent arrays. This value can at most only have some minor memory allocation efficiency impact.

void vallst_setMaxHashLoad (  VallstInstance *  vi, double  maxLoad )

Sets max load. Decides how many hash entries are allowed before resizing. Resizing is done when maxLoad < nrOfEntries/tableSize.

void vallst_setNonAxChunkSizeAxDep (  VallstInstance *  vi, double  value )

Sets the value. It determines the size addition to the non-axiom chunk size relative to the size of the axiom chunks.

void vallst_setNonAxChunkSizeConst (  VallstInstance *  vi, VallstFormulaN  value )

Sets the value. It determines the size of a constant addition to the non-axiom chunk size.

void vallst_setNonAxChunkSizeVarDep (  VallstInstance *  vi, double  value )

Sets the value. It determines the size addition to the non-axiom chunk size relative to the number of variables allocated for.

void vallst_setNrOf3ClausesEstimate (  VallstInstance *  vi, VallstFormulaN  pNrOf3Clauses )

Sets the number of ternary clauses estimate. It's not important that the estimate is exactly accurate but any fairly accurate estimate might be helpful for memory efficiency reasons.

void vallst_setNrOfFreeChunksCap (  VallstInstance *  vi, unsigned int  cap )

Sets cap. Only 'cap' number of free chunks are guaranteed to be kept. The rest are freed occasionally, handing the memory back to the system.

void vallst_setNrOfLitOccsEstimate (  VallstInstance *  vi, VallstFormulaN  pNrOfLitOccs )

Sets the number of literal occurrences estimate, modulo special accounting. See vallst_newInstance(). It's not important that the estimate is exactly accurate but any fairly accurate estimate might be helpful for memory efficiency reasons. Try to make it an upper bound.

---