Packages

o

ap

PresburgerTools

object PresburgerTools

A collection of tools for analysing and transforming formulae in Presburger arithmetic

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. PresburgerTools
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def bounds(objective: LinearCombination, constraint: Conjunction): Option[(IdealInt, IdealInt)]

    Check whether the function objective has both a lower and an upper bound subject to constraint, and return such bounds.

  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  7. def containsBVNonlin(f: Formula): Boolean
  8. def containsTheories(f: Formula): Boolean
  9. def distinctInterpretation[T <: Term](terms: Set[T], order: TermOrder): Map[ConstantTerm, IdealInt]

    Find an interpretation of the constants in the given terms that will make all terms evaluate to pairwise distinct integers.

  10. def elimQuantifiersWithPreds(c: Conjunction): Conjunction

    Quantifier elimination procedure that can also handle uninterpreted predicates, provided that predicates never occur in the scope of quantifiers.

    Quantifier elimination procedure that can also handle uninterpreted predicates, provided that predicates never occur in the scope of quantifiers. Quantifiers above predicate occurrences are left in the formula. The method can also handle formulas with bit-vector arithmetic or non-linear multiplication, and is optimised for post-processing of interpolants.

  11. def eliminatePredicates(c: Conjunction, axioms: Conjunction, order: TermOrder): Conjunction

    Compute the most general quantifier-free formula without uninterpreted predicates that implies the given formula, modulo the given axioms.

    Compute the most general quantifier-free formula without uninterpreted predicates that implies the given formula, modulo the given axioms. If the input formula or the axioms contain quantifiers, this might not terminate.

  12. def enumDisjuncts(disjunction: Conjunction): Iterator[Conjunction]

    Enumerate the disjuncts of a formula that already is in DNF.

  13. def enumModels(formula: Conjunction): Iterator[Conjunction]

    Enumerate the models of a given formula.

    Enumerate the models of a given formula. Currently, we assume that the formula does not contain predicates and only existential quantifiers (this could be relaxed)

  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  16. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  17. def hasCountermodel(rawFormula: Conjunction): Option[Conjunction]
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  19. def isExistentialPresburger(f: Formula): Boolean
  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. def isPresburger(f: Formula): Boolean
  22. def isQFPresburger(f: Formula): Boolean
  23. def isQFPresburgerConjunction(f: Conjunction): Boolean
  24. def isSatisfiable(rawFormula: Conjunction): Boolean
  25. def isValid(rawFormula: Conjunction): Boolean
  26. def lowerBound(objective: LinearCombination, constraint: Conjunction): Option[IdealInt]

    Check whether the function objective has a lower bound subject to constraint, and return such a bound.

  27. def miniScope(c: Conjunction): Conjunction
  28. def minimiseFormula(c: Conjunction): Conjunction

    Minimise the given formula by eliminating unnecessary disjuncts.

    Minimise the given formula by eliminating unnecessary disjuncts. This is a stronger version of the simplification performed by ReduceWithConjunction, and also simplifies formulae a & (b | c) & (b | c') where c & c' is unsatisfiable.

  29. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  30. def nonDNFEnumDisjuncts(formula: Conjunction): Iterator[Conjunction]

    Enumerate the disjuncts of a formula (which might not be in DNF).

  31. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  32. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  33. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  34. def toDNF(formula: Conjunction): Conjunction

    Turn a formula into DNF.

    Turn a formula into DNF. The DNF might not be complete in the sense that a formula a & b | a & c might only be normalised to a & (b | c)

  35. def toPrenex(c: Conjunction): Conjunction

    Convert a given formula to prenex form.

    Convert a given formula to prenex form. TODO: do something special for divisibilities?

  36. def toString(): String
    Definition Classes
    AnyRef → Any
  37. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  38. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  39. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

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

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped