int
Sim_DllAddLit(
int clId,
int lit
)
- If there is no pending clause in SimClauses,
or `lit' is not within reasonable bounds, exit
with error condition -1.
Check for tautologies and duplications using the list of
occurrences for the proposition corresponding to `lit'.
Return 0 on tautologies, 1 on duplications.
If the literal is ok, add it to the clause and update
the lists of occurrences of the corresponding proposition.
- Side Effects none
- See Also
Sim_DllNewCl
Sim_DllNewClSize
void
Sim_DllClear(
)
- Destroys the internal data structure.
- Side Effects none
- See Also
Sim_DllInit
int
Sim_DllCommitCl(
int clId
)
- If there is no pending clause in SimClauses or it has
not the same `clId', return -1.
If the current clause is empty, reset the state and
return 0.
If the pending clause is ok, it is confirmed in the
main clause index: if unary, it is pushed in the bcp
stack. If HORN_RELAXATION is defined, non-Horn clauses
are detected and pushed in the non-Horn index.
- Side Effects none
- See Also
Sim_DllInit
int *
Sim_DllGetSolution(
)
- Allocate `result' to contain all propositions
indexes; scan the main propositions index and store in
`result' the value of the corresponing literals.
- Side Effects none
- See Also
Sim_DllGetStack
int *
Sim_DllGetStack(
)
- Allocate `result' to contain all the propositions; scan
the stack and store in `result' the id
of the literal with the sign of propagation.
- Side Effects none
- See Also
Sim_DllGetStack
void
Sim_DllInit(
int * params
)
- Perform several initializations.
- the solver working parameters are set using the values
in the input array `params';
- timeout and memory out are fixed;
- counters, statistics and timers are resetted;
- the random seed is initialized;
- the main propositions index and the propositions
look-up table are initialized
(the look-up table is to accomodate up to the
biggest variable index);
- the model propositions index is initialized to a
fraction (25%) of the number of propositions;
- if PURE_LITERAL is defined, the pure literal stack
is initialized to the number of propositions;
- the main clause index and the unit clauses stack
are initialized to the number of clauses;
- if HORN_RELAXATION is defined, the non-Horn
clauses index is initialized to the number of clauses.
- Side Effects none
- See Also
Sim_DllClear
int
Sim_DllNewClSize(
short size
)
- If there is a pending clause in SimClauses,
return -1, a failure code.
Otherwise, create a new empty clause and reference it
with the last available index in SimClauses. The size
of the clause will be `size'.
Return the clause index (to be used in future operations with
the clause).
- Side Effects none
- See Also
Sim_DllAddLit
Sim_DllCommitCl
int
Sim_DllNewCl(
)
- If there is a pending clause in SimClauses,
return -1, a failure code.
Otherwise, create a new empty one and reference it
with the last available index in SimClauses. The size
of the clause will be the default SIMCL_SIZE.
Return the clause index (to be used in future operations with
the clause).
- Side Effects none
- See Also
Sim_DllAddLit
Sim_DllCommitCl
int
Sim_DllParseDimacs(
FILE * inFile,
int * params
)
- Takes a pointer to a file and tries to parse (using
DIMACS format) a cnf problem. Takes also the initialization
parameters for the dll module. Returns a pointer to a
DLL module if successfull; NULL if (i) the file does
not exists, or (ii) there is no line starting with p,
or (iii) such line does not define a DIMACS cnf
problem.
- Side Effects none
- See Also
Sim_DllInit
void
Sim_DllPrintFormulaDimacs(
)
- Print the formula in the DLL module using DIMACS format.
- Side Effects None
void
Sim_DllPrintModel(
)
- Print the model.
- Side Effects None
- See Also
Sim_DllPrintStack
void
Sim_DllPrintParams(
)
- Prints parameters (configuration).
- Side Effects None
- See Also
Sim_DllPrintModel
void
Sim_DllPrintResult(
int res
)
- Prints the result (formatted).
- Side Effects None
- See Also
Sim_DllPrintModel
void
Sim_DllPrintStats(
)
- Prints internal statistics.
- Side Effects None
- See Also
Sim_DllPrintModel
void
Sim_DllPrintTimers(
)
- Prints internal timers.
- Side Effects None
- See Also
Sim_DllPrintModel
void
Sim_DllPropMakeIndep(
int prop
)
- If `prop' is a sensible value, then if the
corresponding proposition is not there, it is created and
inserted in the main proposition index. If the
proposition was not declared as a model proposition,
set its back reference and push it in the model
propositions index.
- Side Effects none
int
Sim_DllSolve(
)
- A heuristic function (SimDllChooseLiteral) is used to choose
a literal at each node of the search tree;
SimDllCheckConsistency is used to (i) declare a formula
satisfiable, and (ii) stop the search at some point;
the SimDllBacktracking function is responsible for
restoring to a
previous choice point (if any) in the search tree when
a dead end (SIM_UNSAT subproblem) is reached.
Returns SIM_SAT if the formula is satisifable;
SIM_UNSAT otherwise.
- Side Effects none
- See Also
SimDllCheckConsistency
SimDllChooseLiteral
SimDllBacktrack
Sim_ErrCode_c
Sim_GetErrorCode(
)
- Returns the error code (if any).
- Side Effects none
Sim_ErrLocation_c
Sim_GetErrorLocation(
)
- Returns the error location (if any).
- Side Effects none
int *
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.
- Side Effects none
- See Also
Sim_ParamSet
int *
Sim_ParamSet(
int * param,
int pName,
int pValue
)
- Changes the value of a specific parameter.
- Side Effects none
- See Also
Sim_ParamInit