Package org.tweetyproject.arg.adf.sat
Class AsynchronousCloseSatSolverState
- java.lang.Object
-
- org.tweetyproject.arg.adf.sat.AsynchronousCloseSatSolverState
-
- All Implemented Interfaces:
java.lang.AutoCloseable
,SatSolverState
public class AsynchronousCloseSatSolverState extends java.lang.Object implements SatSolverState
The cleanup after theclose()
call happens (possibly) in a separate thread, depending on the provided executor.- Author:
- Mathias Hofer
-
-
Constructor Summary
Constructors Constructor Description AsynchronousCloseSatSolverState(SatSolverState delegate, java.util.concurrent.Executor executor)
-
Method Summary
Modifier and Type Method Description boolean
add(Clause clause)
Adds the given clause to the solver state.void
assume(Atom proposition, boolean value)
Assumes the truth value of the given proposition for the next call toSatSolverState.satisfiable()
.void
close()
boolean
satisfiable()
Computes if the current state is satisfiable.java.util.Set<Atom>
witness()
Returns a witness of the satisfiability of all the clauses in the state, ornull
if the state is unsatisfiable.java.util.Set<Atom>
witness(java.util.Collection<Atom> filter)
-
-
-
Constructor Detail
-
AsynchronousCloseSatSolverState
public AsynchronousCloseSatSolverState(SatSolverState delegate, java.util.concurrent.Executor executor)
- Parameters:
delegate
- the stateexecutor
- the executor which is used to execute the calls to the delegate state
-
-
Method Detail
-
satisfiable
public boolean satisfiable()
Description copied from interface:SatSolverState
Computes if the current state is satisfiable. Also takes made assumptions into account.Note that it is up to the implementation if the current satisfiability status is cached or if it is computed for every call.
- Specified by:
satisfiable
in interfaceSatSolverState
- Returns:
- true if the state is satisfiable, false if it is not
-
witness
public java.util.Set<Atom> witness()
Description copied from interface:SatSolverState
Returns a witness of the satisfiability of all the clauses in the state, ornull
if the state is unsatisfiable.- Specified by:
witness
in interfaceSatSolverState
- Returns:
- a witness if the state is sat, else returns
null
-
witness
public java.util.Set<Atom> witness(java.util.Collection<Atom> filter)
- Specified by:
witness
in interfaceSatSolverState
-
assume
public void assume(Atom proposition, boolean value)
Description copied from interface:SatSolverState
Assumes the truth value of the given proposition for the next call toSatSolverState.satisfiable()
. There can be multiple assumptions, all of them are gone after the nextSatSolverState.satisfiable()
call.- Specified by:
assume
in interfaceSatSolverState
- Parameters:
proposition
- the atom for which we assume a valuevalue
- the value we assume
-
add
public boolean add(Clause clause)
Description copied from interface:SatSolverState
Adds the given clause to the solver state.- Specified by:
add
in interfaceSatSolverState
- Parameters:
clause
- a clause containing only literals - no constants!- Returns:
- true if the clause could be added to the state, false if it failed
-
close
public void close()
- Specified by:
close
in interfacejava.lang.AutoCloseable
- Specified by:
close
in interfaceSatSolverState
-
-