SatIncSolver_create_group()
Creates a new group and returns its ID. To destroy a group use SatIncSolver_destroy_group or SatIncSolver_move_to_permanent_and_destroy_group
SatIncSolver_destroy_group()
Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
SatIncSolver_destroy()
Destroys an instance of a SAT incremental solver
SatIncSolver_move_to_permanent_and_destroy_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).
SatIncSolver_solve_groups()
Tries to solve formulas from the groups in the list.
SatIncSolver_solve_without_groups()
Tries to solve formulas in groups belonging to the solver except the groups in the list.
SatSolver_add()
Adds a CNF formula to a group
SatSolver_destroy()
Destoys an instance of a SAT solver
SatSolver_get_last_solving_time()
Returns the time of last solving
SatSolver_get_model()
Returns the model (of previous solving)
SatSolver_get_name()
Returns the name of the solver
SatSolver_get_permanent_group()
Returns the permanent group of this class instance.
SatSolver_set_polarity()
Sets the polarity of a CNF formula in a group
SatSolver_solve_all_groups()
Solves all groups belonging to the solver and returns the flag
sat_inc_solver_create_group()
Pure virtual function, create a new group
sat_inc_solver_deinit()
This function de-initializes the SatIncSolver class.
sat_inc_solver_destroy_group()
Pure virtual function, destroys existing group
sat_inc_solver_finalize()
Finalize method of SatIncSolver class.
sat_inc_solver_init()
This function initializes the SatIncSolver class.
sat_inc_solver_move_to_permanent_and_destroy_group()
Pure virtual function, moves all formulas from a given group into the permanent one, and then destroys the given group
sat_inc_solver_solve_groups()
Pure virtual function, tries to solve formulas from the groups in the list. the permanent group is automatically added to the list
sat_inc_solver_solve_without_groups()
Pure virtual function, tries to solve formulas from the groups belonging to the solver except the groups in the list. the permanent group must not be in the list
sat_solver_BelongToList()
returns 1 if an element belongs to the list and 0 otherwise.
sat_solver_RemoveFromList()
removes an element from the list
sat_solver_add()
Pure virtual function, adds a formula to a group
sat_solver_deinit()
This function de-initializes the SatSolver class.
sat_solver_finalize()
Finalize method of SatSolver class.
sat_solver_init()
This function initializes the SatSolver class.
sat_solver_make_model()
Pure virtual function, creates a model for last successful solving
sat_solver_set_polarity()
Pure virtual function, sets the polarity of a formula
sat_solver_solve_all_groups()
Pure virtual function, tries to solve formulas in the group and the permanent group
()
A flag indicating that there is at least one incremental SAT solver
()
Returns the number of element in a statically allocated array

Last updated on 2005/07/18 15h:57