At the momemnt this file just provide the facilities to access 'options' unitilities

SatSolverGroup 
SatIncSolver_create_group(
  const SatIncSolver_ptr  self 
)
Creates a new group and returns its ID. To destroy a group use SatIncSolver_destroy_group or SatIncSolver_move_to_permanent_and_destroy_group

See Also SatIncSolver_destroy_group SatIncSolver_move_to_permanent_and_destroy_group
Defined in SatIncSolver.c

void 
SatIncSolver_destroy_group(
  const SatIncSolver_ptr  self, 
  SatSolverGroup  group 
)
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.

See Also SatIncSolver_create_group
Defined in SatIncSolver.c

void 
SatIncSolver_destroy(
  SatIncSolver_ptr  self 
)
Destroys an instance of a SAT incremental solver

Defined in SatIncSolver.c

void 
SatIncSolver_move_to_permanent_and_destroy_group(
  const SatIncSolver_ptr  self, 
  SatSolverGroup  group 
)
Moves all formulas from a group into the permanent group of the solver and then destroy the given group. (Permanent group may have more efficient implementation, but it can not be destroyed).

See Also SatIncSolver_create_group SatSolver_get_permanent_group
Defined in SatIncSolver.c

SatSolverResult 
SatIncSolver_solve_groups(
  const SatIncSolver_ptr  self, 
  const lsList  groups 
)
The permanent group is automatically added to the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See Also SatSolverResult SatSolver_get_permanent_group SatIncSolver_create_group SatSolver_get_model
Defined in SatIncSolver.c

SatSolverResult 
SatIncSolver_solve_without_groups(
  const SatIncSolver_ptr  self, 
  const lsList  groups 
)
The permanent group must not be in the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See Also SatSolverResult SatSolver_get_permanent_group SatIncSolver_create_group SatSolver_get_model
Defined in SatIncSolver.c

void 
SatSolver_add(
  const SatSolver_ptr  self, 
  const Be_Cnf_ptr  cnfProb, 
  SatSolverGroup  group 
)
The function does not specify the polarity of the formula. This should be done by SatSolver_set_polarity. In general, if polarity is not set any value can be assigned to the formula and its variables (this may potentially slow down the solver because there is a number of variables whose value can be any and solver will try to assign values to them though it is not necessary). Moreover, some solver (such as ZChaff) can deal with non-redundent clauses only, so the input clauses must be non-redundent: no variable can be in the same clause twice. CNF formular may be a constant.

See Also SatSolver_set_polarity
Defined in SatSolver.c

void 
SatSolver_destroy(
  SatSolver_ptr  self 
)
Destoys an instance of a SAT solver

Defined in SatSolver.c

long 
SatSolver_get_last_solving_time(
  const SatSolver_ptr  self 
)
Returns the time of last solving

Defined in SatSolver.c

const lsList 
SatSolver_get_model(
  const SatSolver_ptr  self 
)
The previous solving call should have returned SATISFIABLE. The returned list is a list of values in dimac form (positive literal is included as the variable index, negative literal as the negative variable index, if a literal has not been set its value is not included).

Defined in SatSolver.c

const char* 
SatSolver_get_name(
  const SatSolver_ptr  self 
)
Returns the name of the solver

Defined in SatSolver.c

const SatSolverGroup 
SatSolver_get_permanent_group(
  const SatSolver_ptr  self 
)
Every solver has one permanent group that can not be destroyed. This group may has more efficient representation and during invocations of any 'solve' functions, the permanent group will always be included into the groups to be solved.

Defined in SatSolver.c

void 
SatSolver_set_polarity(
  const SatSolver_ptr  self, 
  const Be_Cnf_ptr  cnfProb, 
  int  polarity, 
  SatSolverGroup  group 
)
Polarity 1 means the formula will be considered in this group as positive. Polarity -1 means the formula will be considered in this group as negative. The formula is not added to the group, just the formula's polarity. The formula can be added to a group with SatSolver_add. The formula and its polarity can be added to different groups. CNF formular may be a constant.

See Also SatSolver_add
Defined in SatSolver.c

SatSolverResult 
SatSolver_solve_all_groups(
  const SatSolver_ptr  self 
)
Solves all groups belonging to the solver and returns the flag

See Also SatSolverResult
Defined in SatSolver.c

SatSolverGroup 
sat_inc_solver_create_group(
  const SatIncSolver_ptr  self 
)
It is a pure virtual function and SatIncSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatIncSolver_add
Defined in SatIncSolver.c

void 
sat_inc_solver_deinit(
  SatIncSolver_ptr  self 
)
This function de-initializes the SatIncSolver class.

Defined in SatIncSolver.c

void 
sat_inc_solver_destroy_group(
  const SatIncSolver_ptr  self, 
  SatSolverGroup  group 
)
It is a pure virtual function and SatIncSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatIncSolver_add
Defined in SatIncSolver.c

void 
sat_inc_solver_finalize(
  Object_ptr  object, 
  void* dummy 
)
Pure virtual function. This must be refined by derived classes.

Defined in SatIncSolver.c

void 
sat_inc_solver_init(
  SatIncSolver_ptr  self, 
  const char* name 
)
This function initializes the SatIncSolver class.

Defined in SatIncSolver.c

void 
sat_inc_solver_move_to_permanent_and_destroy_group(
  const SatIncSolver_ptr  self, 
  SatSolverGroup  group 
)
It is a pure virtual function and SatIncSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatIncSolver_add
Defined in SatIncSolver.c

SatSolverResult 
sat_inc_solver_solve_groups(
  const SatIncSolver_ptr  self, 
  const lsList  groups 
)
It is a pure virtual function and SatIncSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatIncSolver_add
Defined in SatIncSolver.c

SatSolverResult 
sat_inc_solver_solve_without_groups(
  const SatIncSolver_ptr  self, 
  const lsList  groups 
)
It is a pure virtual function and SatIncSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatIncSolver_add
Defined in SatIncSolver.c

int 
sat_solver_BelongToList(
  const lsList  list, 
  const lsGeneric  element 
)
just checks all elements in the list for being equal to a given element

Defined in SatSolver.c

void 
sat_solver_RemoveFromList(
  lsList  list, 
  const lsGeneric  element 
)
If there is no such element in the list => do nothing

See Also sat_solver_BelongToList
Defined in SatSolver.c

void 
sat_solver_add(
  const SatSolver_ptr  self, 
  const Be_Cnf_ptr  cnfProb, 
  SatSolverGroup  group 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatSolver_add
Defined in SatSolver.c

void 
sat_solver_deinit(
  SatSolver_ptr  self 
)
This function de-initializes the SatSolver class.

Defined in SatSolver.c

void 
sat_solver_finalize(
  Object_ptr  object, 
  void* dummy 
)
Pure virtual function. This must be refined by derived classes.

Defined in SatSolver.c

void 
sat_solver_init(
  SatSolver_ptr  self, 
  const char* name 
)
This function initializes the SatSolver class.

Defined in SatSolver.c

lsList 
sat_solver_make_model(
  const SatSolver_ptr  self 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function. It is an error if the last solving was unsuccessful.

Defined in SatSolver.c

void 
sat_solver_set_polarity(
  const SatSolver_ptr  self, 
  const Be_Cnf_ptr  cnfProb, 
  int  polarity, 
  SatSolverGroup  group 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function.

See Also SatSolver_set_polarity
Defined in SatSolver.c

SatSolverResult 
sat_solver_solve_all_groups(
  const SatSolver_ptr  self 
)
It is a pure virtual function and SatSolver is an abstract base class. Every derived class must ovewrwrite this function.

Defined in SatSolver.c

 
(
    
)
A flag indicating that there is at least one incremental SAT solver

Defined in sat.h

 
(
    
)
Returns the number of element in a statically allocated array

Defined in satUtils.c

Last updated on 2004/12/28 16h:58