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.

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

Last updated on 2009/03/04 12h:51