Packages

  • package root
    Definition Classes
    root
  • package jp
    Definition Classes
    root
  • package kobe_u
    Definition Classes
    jp
  • package copris

    Provides classes for Constraint Programming in Scala.

    Provides classes for Constraint Programming in Scala.

    OVERVIEW

    The following is a sample program in Copris DSL (Domain Specific Language).

    object FirstStep {
      import jp.kobe_u.copris._
      import jp.kobe_u.copris.dsl._
    
      def main(args: Array[String]) = {
        val x = int('x, 0, 7)
        val y = int('y, 0, 7)
        add(x + y === 7)
        add(x * 2 + y * 4 === 20)
        if (find) {
          println(solution)
        }
      }
    }
    Definition Classes
    kobe_u
  • package smt
    Definition Classes
    copris
  • Encoder
  • SMT
  • SmtSolver
  • SmtSolverLogger
  • Solver
  • Translator
  • Z3
  • dsl

class Solver extends AbstractSolver

Class for SMT solver

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Solver
  2. AbstractSolver
  3. SolverTrait
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Solver(csp: CSP, smtSolver: SmtSolver = Z3)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def addSolverInfo(key: String, value: String): Unit

    Adds the info

    Adds the info

    Definition Classes
    AbstractSolver
  5. def addSolverStat(name: String, key: String, value: Number): Unit

    Adds the current status of name (experimental)

    Adds the current status of name (experimental)

    Definition Classes
    AbstractSolver
  6. def addSolverStat(name: String, stat: Map[String, Number]): Unit

    Sets the current status of name (experimental)

    Sets the current status of name (experimental)

    Definition Classes
    AbstractSolver
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def cancel: Unit
    Definition Classes
    SolverSolverTrait
  9. def checkTimeout: Unit

    Checks the timeout (experimental)

    Checks the timeout (experimental)

    Definition Classes
    AbstractSolver
  10. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate() @throws( ... )
  11. def commit: Unit
    Definition Classes
    SolverSolverTrait
  12. var commitFlag: Boolean
  13. def dump(fileName: String, format: String): Unit
    Definition Classes
    SolverAbstractSolver
  14. def encode: Boolean
  15. def encodeDelta: Unit
  16. var encoder: Encoder
  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  19. def find: Boolean

    Finds the first solution

    Finds the first solution

    Definition Classes
    SolverAbstractSolverSolverTrait
  20. def find(commitFlag: Boolean): Boolean
  21. def findBody: Boolean

    Body of the find method

    Body of the find method

    Definition Classes
    SolverAbstractSolver
  22. def findNext: Boolean

    Finds the next solution

    Finds the next solution

    Definition Classes
    SolverAbstractSolverSolverTrait
  23. def findNext(commitFlag: Boolean): Boolean
  24. def findNextBody: Boolean

    Body of the findNext method

    Body of the findNext method

    Definition Classes
    SolverAbstractSolver
  25. def findOpt: Boolean

    Finds the optimum solution

    Finds the optimum solution

    Definition Classes
    AbstractSolverSolverTrait
  26. def findOptBody: Boolean

    Body of the findOpt method

    Body of the findOpt method

    Definition Classes
    SolverAbstractSolver
  27. def findOptBound(lb: Int, ub: Int): Boolean

    Finds a solution within the given bounds

    Finds a solution within the given bounds

    Definition Classes
    AbstractSolver
  28. def findOptBoundBody(lb: Int, ub: Int): Boolean

    Body of the findOptBound method

    Body of the findOptBound method

    Definition Classes
    SolverAbstractSolver
  29. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  30. def getSolverStat(name: String): Map[String, Number]

    Gets the last status of ~name~ (experimental)

    Gets the last status of ~name~ (experimental)

    Definition Classes
    AbstractSolver
  31. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  32. def init: Unit

    Initializes the solver

    Initializes the solver

    Definition Classes
    SolverAbstractSolverSolverTrait
  33. var initial: Boolean
  34. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  35. def measureTime[T](name: String, key: String)(block: ⇒ T): T

    Measures the time spent for executing block (experimental)

    Measures the time spent for executing block (experimental)

    Definition Classes
    AbstractSolver
  36. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  37. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  38. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  39. var options: Map[String, String]

    Options of the solver

    Options of the solver

    Definition Classes
    AbstractSolver
  40. var outFileName: String
  41. def raiseTimeout: Nothing

    Raises the interrupted exception for timeout (experimental)

    Raises the interrupted exception for timeout (experimental)

    Definition Classes
    AbstractSolver
  42. def setTimeoutTask(task: ⇒ Unit): Unit

    Specifies the clean-up tasks of the timeout (experimental)

    Specifies the clean-up tasks of the timeout (experimental)

    Definition Classes
    AbstractSolver
  43. def shiftSolverStats: Unit

    Shifts the status (experimental)

    Shifts the status (experimental)

    Definition Classes
    AbstractSolver
  44. var smtFileName: String
  45. def smtSolve: Boolean
  46. var smtSolver: SmtSolver
  47. var solution: Solution

    Returns the current solution

    Returns the current solution

    Definition Classes
    SolverSolverTrait
  48. def solutions: Iterator[Solution]

    Returns the iterator of all solutions

    Returns the iterator of all solutions

    Definition Classes
    AbstractSolverSolverTrait
  49. var solverInfo: Map[String, String]

    Info of the solver (experimental)

    Info of the solver (experimental)

    Definition Classes
    AbstractSolver
  50. val solverName: String
  51. var solverStats: Seq[Map[String, Map[String, Number]]]

    Status of the solver (experimental)

    Status of the solver (experimental)

    Definition Classes
    AbstractSolver
  52. def startTimer(t: Long): Unit

    Starts the timer (experimental)

    Starts the timer (experimental)

    Definition Classes
    AbstractSolver
  53. def stopTimer: Unit

    Stops the timer (experimental)

    Stops the timer (experimental)

    Definition Classes
    AbstractSolver
  54. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  55. var timeout: Long

    Timeout value in miliseconds (experimental)

    Timeout value in miliseconds (experimental)

    Definition Classes
    AbstractSolver
  56. var timer: Timer

    Timer (experimental)

    Timer (experimental)

    Definition Classes
    AbstractSolver
  57. def toString(): String
    Definition Classes
    AnyRef → Any
  58. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  59. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  60. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def addDelta: Unit
    Annotations
    @deprecated
    Deprecated

    (Since version 2.2.0) use encodeDelta method of jp.kobe_u.copris.smt.Solver instead

  2. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

  3. def value(p: Bool): Boolean

    Returns the Boolean variable value of the current solution

    Returns the Boolean variable value of the current solution

    Definition Classes
    SolverTrait
    Annotations
    @deprecated
    Deprecated

    (Since version 1.0.1) use apply method of jp.kobe_u.copris.Solution instead

  4. def value(x: Var): Int

    Returns the integer variable value of the current solution

    Returns the integer variable value of the current solution

    Definition Classes
    SolverTrait
    Annotations
    @deprecated
    Deprecated

    (Since version 1.0.1) use apply method of jp.kobe_u.copris.Solution instead

  5. def values(p: Bool, ps: Bool*): Seq[Boolean]

    Returns the Boolean variable values of the current solution

    Returns the Boolean variable values of the current solution

    Definition Classes
    SolverTrait
    Annotations
    @deprecated
    Deprecated

    (Since version 1.0.1) use apply method of jp.kobe_u.copris.Solution instead

  6. def values(x: Var, xs: Var*): Seq[Int]

    Returns the integer variable values of the current solution

    Returns the integer variable values of the current solution

    Definition Classes
    SolverTrait
    Annotations
    @deprecated
    Deprecated

    (Since version 1.0.1) use apply method of jp.kobe_u.copris.Solution instead

Inherited from AbstractSolver

Inherited from SolverTrait

Inherited from AnyRef

Inherited from Any

Ungrouped