-
SatMinisat_create()
- Creates a Minisat SAT solver and initializes it.
-
SatMinisat_destroy()
- Destroys an instance of a MiniSat SAT solver
-
SatZchaff_create()
- Creates a Zchaff SAT solver and initializes it.
-
SatZchaff_destroy()
- Destroys a Zchaff SAT solver instence
-
_get_clause_size()
- Computes the size of a clause.
-
_get_clause_size()
- Computes the size of a clause.
-
sat_minisat_add()
- Adds a clause to the solver database.
-
sat_minisat_clear_preferred_variables()
- Clears preferred variables in the solver
-
sat_minisat_cnfLiteral2minisatLiteral()
- Convert a cnf literal into an internal literal used by minisat
-
sat_minisat_create_group()
- Creates a new group and returns its ID
-
sat_minisat_curr_itp_group()
-
-
sat_minisat_deinit()
- Deinitializes SatMinisat object.
-
sat_minisat_destroy_group()
- Destroy an existing group (which has been returned by
SatIncSolver_create_group) and all formulas in it.
-
sat_minisat_enlarge_minisatClause()
- Enlarge minisatClause, adapt minisatClauseSize
-
sat_minisat_extract_interpolant()
-
-
sat_minisat_finalize()
- Finalize method of SatMinisat class.
-
sat_minisat_get_conflicts()
- Returns set of conflicting assumptions
-
sat_minisat_get_minisatClauseSize()
- Getter for minisatClauseSize
-
sat_minisat_get_minisatClause()
- Getter for minisatClause
-
sat_minisat_get_polarity_mode()
- Pure virtual function, returns currently set polarity mode.
-
sat_minisat_init()
- Initializes Sat Minisat object.
-
sat_minisat_make_conflicts()
- Obtains the set of conflicting assumptions from MiniSat
-
sat_minisat_make_model()
- This function creates a model (in the original CNF variables)
-
sat_minisat_minisatLiteral2cnfLiteral()
- Convert an internal minisat literal into a cnf literal
-
sat_minisat_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.
-
sat_minisat_new_itp_group()
-
-
sat_minisat_set_polarity_mode()
- Pure virtual function, sets polarity mode accordingly to the
passed value.
-
sat_minisat_set_polarity()
- Sets the polarity of the formula.
-
sat_minisat_set_preferred_variables()
- Sets preferred variables in the solver
-
sat_minisat_set_random_mode()
- Pure virtual function, sets random polarity mode if seed is
not zero, otherwise sets default non-random polarity mode.
-
sat_minisat_solve_all_groups()
- Tries to solve all added formulas
-
sat_minisat_solve_groups()
- Tries to solve formulas from the groups in the list.
-
sat_minisat_solve_permanent_group_assume()
- Solves the permanent group under set of assumptions
-
sat_minisat_solve_without_groups()
- Tries to solve formulas in groups belonging to the solver
except the groups in the list.
-
sat_zchaff_add()
- Adds a clause to the solver database.
-
sat_zchaff_clear_preferred_variables()
- Clears preferred variables in the solver
-
sat_zchaff_cnfLiteral2zchaffLiteral()
- Convert a cnf literal into an internal literal used by zchaff
-
sat_zchaff_create_group()
- Creates a new group and returns its ID
-
sat_zchaff_deinit()
- Deinitializes SatZchaff object.
-
sat_zchaff_destroy_group()
- Destroy an existing group (which has been returned by
SatIncSolver_create_group) and all formulas in it.
-
sat_zchaff_finalize()
- Finalize method of SatZchaff class.
-
sat_zchaff_get_conflicts()
- Returns set of conflicting assumptions
-
sat_zchaff_init()
- Initializes Sat Zchaff object.
-
sat_zchaff_make_conflicts()
- Obtains the set of conflicting assumptions from zCahdd
-
sat_zchaff_make_model()
- This function creates a model (in the original cnf variables)
-
sat_zchaff_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.
-
sat_zchaff_set_polarity()
- Sets the polarity of the formula.
-
sat_zchaff_set_preferred_variables()
- Sets preferred variables in the solver
-
sat_zchaff_solve_all_groups()
- Tries to solve all added formulas
-
sat_zchaff_solve_groups()
- Tries to solve formulas from the groups in the list.
-
sat_zchaff_solve_permanent_group_assume()
- Solves the permanent group under set of assumptions
-
sat_zchaff_solve_without_groups()
- Tries to solve formulas in groups belonging to the solver
except the groups in the list.
-
sat_zchaff_zchaffLiteral2cnfLiteral()
- Convert an internal zchaff literal into a cnf literal
Last updated on 2012/11/18 14h:37