Sim_DllAddLit()
Add a literal `lit' to the current clause. `lit' must be an integer such that its absolute value is greater than 0 and smaller than or equal to the biggest allowed variable index. A positive (negative) integer denotes a positive (negative) occurrence of the corresponding variable. If `lit' does not fulfill the above conditions, or if there is no pending clause to add `lit' to, -1 is returned. The function returns 0 if the pending clause becomes tautologous, and 1 otherwise. Redundant literals are always discarded.
Sim_DllClear()
Destroys the internal data structure.
Sim_DllCommitCl()
Commit the pending clause. If there is no such clause, or the given `clId' is differente from the current one, -1 is returned. If the committed clause is empty, 0 is returned and the function resets the state (no pending clause). On success, `clId' is returned.
Sim_DllGetSolution()
Get the current assignment to propositions. The returned object is an array of integers indexed on propositions. For each proposition, the values SIM_TT, SIM_FF, SIM_DC are given, meaning that the proposition was assigned to true, false or not assigned at all (Don't Care). Propositions that did not occur in the formula receive a default value of SIM_DC. The first location of the returned array contains the biggest proposition index.
Sim_DllGetStack()
Get the current search stack contents. The returned object is an array representing truth assignment to propositions encoded as literals (negative value if the proposition was assigned to false and vice versa). The first location of the returned array is the cardinality of the truth assignment.
Sim_DllInit()
Initialize the DLL module. The array `params' must be suitably initialized.
Sim_DllNewClSize()
Create a new (empty) clause and return its unique id, (an integer code greater than or equal to 0). The clause is dimensioned to accomodate `size' literals without reallocations. Trying to add a new clause without committing any pending one yields -1 as a return value.
Sim_DllNewCl()
Create a new (empty) clause and return its unique id (an integer code greater than or equal to 0). Trying to add a new clause without committing any pending one yields -1 as a return value.
Sim_DllParseDimacs()
Parses a DIMACS cnf problem file into a DLL module.
Sim_DllPrintFormulaDimacs()
Print the formula in the DLL module using DIMACS format.
Sim_DllPrintModel()
Print the model.
Sim_DllPrintParams()
Prints parameters (configuration).
Sim_DllPrintResult()
Prints the result (formatted).
Sim_DllPrintStats()
Prints internal statistics.
Sim_DllPrintTimers()
Prints internal timers.
Sim_DllPropMakeIndep()
State model membership, i.e., a proposition that is not dependent or defined. 'prop` must be a positive non-zero integer smaller than or equal to the biggest allowed variable index.
Sim_DllSolve()
Solves a formula using the Davis-Logemann-Loveland algorithm.
Sim_GetErrorCode()
Returns the error code (if any).
Sim_GetErrorLocation()
Returns the error location (if any).
Sim_ParamInit()
Creates a default parameter setup as follows:
Idx Default value Parameter Notes -------------------------------------------------------------- 0 unlimited SIM_TIMEOUT seconds 1 unlimited SIM_MEMOUT megabytes 2 SIM_BOEHM_HEUR SIM_HEURISTICS 0..SIM_HEUR_NUM 3 1 SIM_SOL_NUM N >= 1 4 3 SIM_LEARN_ORDER N >= 2 5 SIM_RELEVANCE SIM_LEARN_TYPE SIM_RELEVANCE/SIM_SIZE 6 0 SIM_MODEL_PROPS 0/1 7 SIM_NONE SIM_PPROC_STRENGTH 0..SIM_RESOLVE 8 0 SIM_RND_SEED N >= 0 9 0 SIM_VERBOSITY 0/1 10 0 SIM_HEUR_PARAM N >= 0 11 100 SIM_MAX_VAR_NUM N > 1 12 1000 SIM_MAX_CL_NUM N > 1 -------------------------------------------------------------- Notice that the actual number of variables and clauses in the formula *cannot* be greater than SIM_MAX_VAR_NUM and SIM_MAX_CL_NUM respectively. Failing to dimension these parameters correctly will cause the solver to crash.
Sim_ParamSet()
Changes the value of a specific parameter.

Last updated on 2009/03/04 13h:34