sbt.logic

Logic

object Logic

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Logic
  2. AnyRef
  3. Any
  1. Hide All
  2. Show all
Learn more about member selection
Visibility
  1. Public
  2. All

Type Members

  1. final case class Atoms(inHead: Set[Atom], inFormula: Set[Atom]) extends Product with Serializable

    Represents the set of atoms in the heads of clauses and in the bodies (formulas) of clauses.

  2. final class CyclicNegation extends LogicException

  3. final class InitialContradictions extends LogicException

  4. final class InitialOverlap extends LogicException

  5. sealed abstract class LogicException extends AnyRef

  6. final class Matched extends AnyRef

    Tracks proven atoms in the reverse order they were proved.

Value Members

  1. final def !=(arg0: AnyRef): Boolean

    Definition Classes
    AnyRef
  2. final def !=(arg0: Any): Boolean

    Definition Classes
    Any
  3. final def ##(): Int

    Definition Classes
    AnyRef → Any
  4. final def ==(arg0: AnyRef): Boolean

    Definition Classes
    AnyRef
  5. final def ==(arg0: Any): Boolean

    Definition Classes
    Any
  6. object Matched

  7. def applyAll(c: Clause, facts: Set[Literal]): Option[Clause]

  8. def applyAll(cs: Clauses, facts: Set[Literal]): Option[Clauses]

    Applies known facts to clauses, deriving a new, possibly empty list of clauses.

    Applies known facts to clauses, deriving a new, possibly empty list of clauses. 1. If a fact is in the body of a clause, the derived clause has that fact removed from the body. 2. If the negation of a fact is in a body of a clause, that clause fails and is removed. 3. If a fact or its negation is in the head of a clause, the derived clause has that fact (or its negation) removed from the head. 4. If a head is empty, the clause proves nothing and is removed.

    NOTE: empty bodies do not cause a clause to succeed yet. All known facts must be applied before this can be done in order to avoid inconsistencies. Precondition: no contradictions in facts Postcondition: no atom in facts is present in the result Postcondition: No clauses have an empty head

  9. final def asInstanceOf[T0]: T0

    Definition Classes
    Any
  10. def atoms(formula: Formula): Set[Atom]

    Computes the set of all atoms in formula.

  11. def atoms(cs: Clauses): Atoms

    Computes the atoms in the heads and bodies of the clauses in clause.

  12. def clone(): AnyRef

    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  13. final def eq(arg0: AnyRef): Boolean

    Definition Classes
    AnyRef
  14. def equals(arg0: Any): Boolean

    Definition Classes
    AnyRef → Any
  15. def finalize(): Unit

    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. final def getClass(): Class[_]

    Definition Classes
    AnyRef → Any
  17. def hasNegatedDependency(clauses: Seq[Clause], posDeps: Relation[Atom, Atom], negDeps: Relation[Atom, Atom]): List[Atom]

    Computes the set of atoms in clauses that directly or transitively take a negated atom as input.

    Computes the set of atoms in clauses that directly or transitively take a negated atom as input. For example, for the following clauses, this method would return List(a, d) : a :- b, not c d :- a

    Annotations
    @tailrec()
  18. def hashCode(): Int

    Definition Classes
    AnyRef → Any
  19. final def isInstanceOf[T0]: Boolean

    Definition Classes
    Any
  20. final def ne(arg0: AnyRef): Boolean

    Definition Classes
    AnyRef
  21. final def notify(): Unit

    Definition Classes
    AnyRef
  22. final def notifyAll(): Unit

    Definition Classes
    AnyRef
  23. def reduce(clauses: Clauses, initialFacts: Set[Literal]): Either[LogicException, Matched]

    Computes the variables in the unique stable model for the program represented by clauses and initialFacts.

    Computes the variables in the unique stable model for the program represented by clauses and initialFacts. clause may not have any negative feedback (that is, negation is acyclic) and initialFacts cannot be in the head of any clauses in clause. These restrictions ensure that the logic program has a unique minimal model.

  24. def reduceAll(clauses: List[Clause], initialFacts: Set[Literal]): Either[LogicException, Matched]

  25. def substitute(formula: Formula, facts: Set[Literal]): Option[Formula]

    Derives the formula that results from substituting facts into formula.

    Derives the formula that results from substituting facts into formula.

    Annotations
    @tailrec()
  26. final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes
    AnyRef
  27. def toString(): String

    Definition Classes
    AnyRef → Any
  28. final def wait(): Unit

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long): Unit

    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped