API functions grouped

Here is a list of all API functions grouped into categories.

Allocation

• vallst_deleteInstance() -- Deletes a vallst instance.
• vallst_extendNrOfVars() -- Extends the number of variables ready to be used.
• vallst_newInstance() -- Creates a new vallst problem instance.
• vallst_propagateNrOf3ClausesEstimate() -- Propagates value.
• vallst_propagateNrOfLitOccsEstimate() -- Propagates value.
• vallst_setFstNrOfLevelsAllocSize() -- Sets flag.
• vallst_setMaxHashLoad() -- Sets max load.
• vallst_setNonAxChunkSizeAxDep() -- Sets value.
• vallst_setNonAxChunkSizeConst() -- Sets value.
• vallst_setNonAxChunkSizeVarDep() -- Sets value.
• vallst_setNrOf3ClausesEstimate() -- Sets the number of ternary clauses estimate.
• vallst_setNrOfFreeChunksCap() -- Sets cap.
• vallst_setNrOfLitOccsEstimate() -- Sets estimate of the number of literal occurrences, modulo special accounting.

Formulas and variables

• vallst_addAxiom() -- Adds an axiom.
• vallst_addConsequence() -- Adds a formula that should be a consequence of the axioms since the formula might be removed.
• vallst_addNamedAxiom() -- Adds a named axiom.
• vallst_alterAxiomIncMT() -- Adds to the constant in a more-than* axiom.
• vallst_alterAxiomIncMTMKeepAboves() -- Adds to the constant in a <*-axiom keeping "aboves".
• vallst_extendNrOfVars() -- Extends the number of variables ready to be used.
• vallst_formulaType() -- Returns the type given a formula name.
• vallst_getConst() -- Returns the constant in a constraint.
• vallst_getFullLitValue() -- Returns the full status of a literal.
• vallst_getKeepAboves() -- Returns the keep-aboves flag.
• vallst_getLitValue() -- Returns the status of a literal.
• vallst_getNrOfVarsAllocated() -- Returns the number of vars allocated for.
• vallst_getTotalSum() -- Returns the sum of the literal constants in a more-than-mult (<*) formula.
• vallst_isConstraint() -- Returns true iff a name is a constraint.
• vallst_lessThanEqMultToMoreThanMult() -- Tranforms a >=*-formula into a <*-formula.
• vallst_lessThanEqToMoreThan() -- Tranforms a >=-formula into a <-formula.
• vallst_neg() -- Returns the negation of a literal.
• vallst_newVar() -- Returns a new variable ready to be used.
• vallst_setKeepAboves() -- Sets flag.
• vallst_setStartConst() -- Sets value.
• vallst_sumOpenTrue() -- Sums up true and open lits in a constraint.
• vallst_sumTrue() -- Sums up true lits in a constraint.

Search

• vallst_getAbortThreshold() -- Returns nr of vars set to abort value.
• vallst_getLevel() -- Returns the current search level.
• vallst_getNoAbortTime() -- Returns time limit for no aborts.
• vallst_makeCurrentAssumptionsSuggestions() -- Sets suggestions.
• vallst_makeSearchAssumption() -- Makes a search assumption.
• vallst_moveToLevel0() -- Moves the current search state to level 0.
• vallst_removeAssumptions() -- Removes all search assumptions.
• vallst_removeLastAssumption() -- Removes the last search assumption.
• vallst_search() -- Searches for a proof of false or a model.
• vallst_setAbortThreshold() -- Sets nr of vars set to abort.
• vallst_setBufferResetFrequency() -- Sets the frequency.
• vallst_setBufferSizeConst() -- Sets value.
• vallst_setBufferSizeNonAxDep() -- Sets value.
• vallst_setBufferSizeVarDep() -- Sets value.
• vallst_setCCLeeway() -- Sets proof improvement leeway.
• vallst_setCreatePhantomConflictClauses() -- Sets the create-phantom-conflict-clauses flag.
• vallst_setFirstRestart() -- Sets the base/initial restart size.
• vallst_setFstNrOfLevelsAllocSize() -- Sets flag.
• vallst_setGoodClauseSize() -- Sets what's to be considered good.
• vallst_setGoodLevel() -- Sets what's to be considered good.
• vallst_setHeurAxSize() -- Sets size.
• vallst_setImproveProofLevel() -- Sets level threshold.
• vallst_setKeepCCMetaMetaThreshold() -- Sets threshold.
• vallst_setKeepConflictClauseLengthThreshold() -- Sets threshold.
• vallst_setLooseTheoryMetaSizeLeeway() -- Set meta leeway used in loose mode.
• vallst_setLooseTheorySizeLeeway() -- Set meta meta leeway used in loose mode.
• vallst_setLooseTheorySizeLeewayKeep() -- Set leeway used in loose mode.
• vallst_setLooseTimeLimitBase() -- Sets mode limit parameter.
• vallst_setLooseTimeLimitMod() -- Sets mode limit parameter.
• vallst_setMaxSkippedSimps() -- Sets max skipped search simplifications.
• vallst_setMetaMetaPruneEnd() -- Sets the value.
• vallst_setMetaMetaPruneFrequency() -- Sets the frequency.
• vallst_setMetaMetaPruneStart() -- Sets the value.
• vallst_setMetaPruneEnd() -- Sets the value.
• vallst_setMetaPruneFrequency() -- Sets the frequency.
• vallst_setMetaPruneStart() -- Sets the value.
• vallst_setNextBatchSizeConst() -- Sets value.
• vallst_setNoAbortTime() -- Sets time limit for no aborts.
• vallst_setPositiveHeurAxSign() -- Sets value.
• vallst_setPositiveSign() -- Sets value.
• vallst_setPruningFunction() -- Sets the pruning function.
• vallst_setRandomBranchSign() -- Sets random sign choice likelihood.
• vallst_setRandomFormulaLit() -- Sets random formula lit choice likelihood.
• vallst_setRemoveTmpCauses() -- Sets this flag.
• vallst_setResetBuffersBetweenSearches() -- Sets flag.
• vallst_setRestartFunc() -- Sets restart batch size function.
• vallst_setRestartPredefFunc() -- Chooses a predef. restart batch size function.
• vallst_setRestartProlongCap() -- Sets cap.
• vallst_setRestartStart() -- Sets the start phase size.
• vallst_setStartWithBinFstBcp() -- Sets flag.
• vallst_setStrengthLeeway() -- Sets the heuristic strength leeway.
• vallst_setStrengthLeewayFormula() -- Sets the heuristic strength leeway for formulas.
• vallst_setStrengthLeewaySize() -- Sets a hard strength leeway space size cap.
• vallst_setStrengthLeewaySizeFormula() -- Sets a hard strength leeway space size cap for formulas.
• vallst_setTightCCLeeway() -- Sets tight proof improvement leeway.
• vallst_setTightKeepCCThreshold() -- Set value used in tight mode.
• vallst_setTightMetaMetaPruneEnd() -- Set value used in tight mode.
• vallst_setTightMetaMetaPruneStart() -- Set value used in tight mode.
• vallst_setTightMetaPruneStart() -- Set value used in tight mode.
• vallst_setTightTheoryMetaSizeLeeway() -- Set meta leeway used in tight mode.
• vallst_setTightTheorySizeLeeway() -- Set meta meta leeway used in tight mode.
• vallst_setTightTheorySizeLeewayKeep() -- Set leeway used in tight mode.
• vallst_setTightTimeLimitBase() -- Sets mode limit parameter.
• vallst_setTightTimeLimitMod() -- Sets mode limit parameter.
• vallst_setUseDoppelganger() -- Sets flag.

Simplification

• vallst_compactifyVars() -- Removes gaps in the variables.
• vallst_getSubstEqus() -- Returns flag.
• vallst_permuteVars() -- Permute the variables moving related variables closer together.
• vallst_pruneTheory() -- Prunes the theory.
• vallst_setConvert3ClausesIntoEqus() -- Sets the convert-3-clauses flag.
• vallst_setSimpTimeLimitFast() -- Sets time limit for fast simplifications.
• vallst_setSimpTimeLimitSlow() -- Sets time limit for slow simplifications.
• vallst_setSimpSetting() -- Setting for main bcp based fast simplification.
• vallst_setSimpSettingSlow() -- Setting for main bcp based slow simplification.
• vallst_setSubstEqus() -- Sets flag.
• vallst_simplify() -- Simplifies the problem fast. BCP based.
• vallst_simplifySlow() -- Simplifies the problem slow. BCP based.
• vallst_substEqus() -- Substitutes vars p<->a in equivalences.

Symmetry detection

• vallst_symmetrySearch() -- Searches for symmetries.

Parsing

• vallst_closeInTheoryFile() -- Closes the in-theory file.
• vallst_getInTheoryFile() -- Returns the in-theory file.
• vallst_getInTheoryFileName() -- Returns the in-theory file name.
• vallst_setPBVarPrefixChar() -- Sets flag.
• vallst_getProblemType -- Returns the problem type.
• vallst_parseCommandLineOptions() -- Parses options.
• vallst_readInTheoryBody() -- Reads the body of the in-theory.
• vallst_readInTheoryHead() -- Reads the head (i.e. the prologue) of the in-theory.
• vallst_setIgnorePrologue() -- Sets the ignore-prologue flag.
• vallst_setInTheoryFile() -- Sets the in-theory file.
• vallst_setInTheoryFileName() -- Sets the in-theory file name.
• vallst_setProblemType -- Sets the problem type.
• vallst_setVarMapFile() -- Sets the pb variable map file.
• vallst_setVarMapFileName() -- Sets the pb variable map file name.

Printing

• vallst_closeChangingSettingFile() -- Closes the changing-setting file.
• vallst_closeOutTheoryFile() -- Closes the out-theory file.
• vallst_getChangingSettingFile() -- Returns the changing-setting file.
• vallst_getChangingSettingFileName() -- Returns the changing-setting file name.
• vallst_getCompleteModel() -- Returns the complete-model flag.
• vallst_getOutTheoryFile() -- Returns the out-theory file.
• vallst_getOutTheoryFileName() -- Returns the out-theory file name.
• vallst_getPrintChangingSetting() -- Returns the print-changing-setting flag.
• vallst_getPrintOutTheory() -- Returns the print-out-theory flag.
• vallst_getResultFile() -- Returns the result file.
• vallst_getResultFileName() -- Returns the result file name.
• vallst_getVerbosityVector() -- Returns the verbosity vector.
• vallst_hashStateCheck() -- Prints detailed hash info.
• vallst_printAllGgcditTours() -- Prints all ggcdit tours.
• vallst_printChangingSetting() -- Prints changing settings.
• vallst_printChangingSettingToFile() -- Prints changing settings to supplied file.
• vallst_printEstimatedPrologues() -- Prints estimated prologue values.
• vallst_printGgcditTour() -- Prints a tour.
• vallst_printHashInfo() -- Prints easily obtainable hash info.
• vallst_printModel() -- Prints the current value of variables.
• vallst_printNrOfUncheckedVars() -- Prints nr of unchecked vars.
• vallst_printNrOfVarsSet() -- Prints nr of vars set.
• vallst_printOpenTheory() -- Prints the current theory but without the variable history.
• vallst_printPrologues() -- Prints hindsighted prologue values.
• vallst_printSettings() -- Prints option settings.
• vallst_printTheory() -- Prints the current theory.
• vallst_printTheoryToFile() -- Prints the theory to a supplied file.
• vallst_printTimePassed() -- Prints the cpu time used.
• vallst_printVallstResult() -- Prints a short string corresponding to a VallstResult.
• vallst_printVarHistory() -- Prints the variable history.
• vallst_setChangingSettingFile() -- Sets the changing-setting file.
• vallst_setChangingSettingFileName() -- Sets the changing-setting file name.
• vallst_setCompleteModel() -- Sets the complete-model flag.
• vallst_setOutTheoryFile() -- Sets the out-theory file.
• vallst_setOutTheoryFileName() -- Sets the out-theory file name.
• vallst_setPrintChangingSetting() -- Sets the print-changing-setting flag.
• vallst_setPrintOutTheory() -- Sets the print-out-theory flag.
• vallst_setResultFile() -- Sets the result file.
• vallst_setResultFileName() -- Sets the result file name.
• vallst_setVerbosityLevel() -- Sets the verbosity level.
• vallst_setVerbosityVector() -- Sets the verbosity vector.

Callback

• vallst_setCallback() -- Sets the callback function.

Formula name allocation

• vallst_extendFormulaNameArray() -- Extends a name array.
• vallst_newFormulaNameArray() -- Returns a new formula name array.

Graph coding

• vallst_ggcditEdgeToLit() -- Maps an (i,j) edge to a vallst literal.
• vallst_ggcditLitToEdge() -- Maps a literal to the corresponding edge.
• vallst_ggcditLitToEdgeFst() -- Maps a literal to first node of edge.

Optimization

• vallst_getBreadthFstOptStrat() -- Returns the optimization strategy flag.
• vallst_maxConstraints() -- Maximizes constraint constants.
• vallst_setBreadthFstOptStrat() -- Sets the optimization strategy flag.

Seed

• vallst_getSeed() -- Gets the seed used.
• vallst_setSeed() -- Sets the seed.

Timers

• vallst_setTimeLimitInMilliSec() -- Sets the overall time limit in milliseconds.
• vallst_setTimeLimitInSec() -- Sets the overall time limit in seconds.

---