Package org.jacop.jasat.core.clauses
Interface ClauseDatabaseInterface
- All Known Implementing Classes:
AbstractClausesDatabase
,BinaryClausesDatabase
,DatabasesStore
,DefaultClausesDatabase
,DomainClausesDatabase
,LongClausesDatabase
,TernaryClausesDatabase
,UnaryClausesDatabase
public interface ClauseDatabaseInterface
Interface for clause databases or database stores. Any entity that
contains clauses and can perform different operations on them.
- Version:
- 4.8
-
Method Summary
Modifier and TypeMethodDescriptionint
addClause
(int[] clause, boolean isModelClause) It adds a clause to the database.void
assertLiteral
(int literal) It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.void
backjump
(int level) Do everything needed to return to the given level.boolean
canRemove
(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or notvoid
removeClause
(int clauseId) It removes the clause which unique ID is @param clauseId.resolutionWith
(int clauseIndex, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.int
size()
size of the databasevoid
toCNF
(BufferedWriter output) It writes the clauses of the databases in cnf format to the specified writer.
-
Method Details
-
addClause
int addClause(int[] clause, boolean isModelClause) It adds a clause to the database. This can change the state of the solver, for example if the clause is unsatisfiable in the current trail affectation, the solver will get in the conflict state.- Parameters:
clause
- the clause to addisModelClause
- defined if the clause is model clause- Returns:
- the unique ID referring to the clause
-
assertLiteral
void assertLiteral(int literal) It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.- Parameters:
literal
- the literal that is set
-
removeClause
void removeClause(int clauseId) It removes the clause which unique ID is @param clauseId.- Parameters:
clauseId
- clause id
-
canRemove
boolean canRemove(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or not- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true iff removal of clauses is possible
-
resolutionWith
It returns the clause obtained by resolution between clauseIndex and clause. It will also modify in place the given SetClause (avoid allocating).- Parameters:
clauseIndex
- the unique id of the clauseclause
- an explanation clause that is modified by resolution- Returns:
- the clause obtained by resolution
-
backjump
void backjump(int level) Do everything needed to return to the given level.- Parameters:
level
- the level to return to. Must be < solver.getCurrentLevel().
-
size
int size()size of the database- Returns:
- the number of clauses in the database
-
toCNF
It writes the clauses of the databases in cnf format to the specified writer.- Parameters:
output
- the output writer to which all the clauses will be written to.- Throws:
IOException
- execption from java.io package
-