Class AsynchronousCloseSatSolverState

  • All Implemented Interfaces:
    java.lang.AutoCloseable, SatSolverState

    public class AsynchronousCloseSatSolverState
    extends java.lang.Object
    implements SatSolverState
    The cleanup after the close() call happens (possibly) in a separate thread, depending on the provided executor.
    Author:
    Mathias Hofer
    • 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 to SatSolverState.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, or null if the state is unsatisfiable.
      java.util.Set<Atom> witness​(java.util.Collection<Atom> filter)  
      • Methods inherited from class java.lang.Object

        equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • AsynchronousCloseSatSolverState

        public AsynchronousCloseSatSolverState​(SatSolverState delegate,
                                               java.util.concurrent.Executor executor)
        Parameters:
        delegate - the state
        executor - 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 interface SatSolverState
        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, or null if the state is unsatisfiable.
        Specified by:
        witness in interface SatSolverState
        Returns:
        a witness if the state is sat, else returns null
      • add

        public boolean add​(Clause clause)
        Description copied from interface: SatSolverState
        Adds the given clause to the solver state.
        Specified by:
        add in interface SatSolverState
        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 interface java.lang.AutoCloseable
        Specified by:
        close in interface SatSolverState