Object

ap

PresburgerTools

Related Doc: package ap

Permalink

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. All

Value Members

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

    Permalink
    Definition Classes
    AnyRef → Any

  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any

  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  4. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  5. def bounds(objective: LinearCombination, constraint: Conjunction): Option[(IdealInt, IdealInt)]

    Permalink

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

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

  6. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

  7. def containsBVNonlin(f: Formula): Boolean

    Permalink

  8. def containsTheories(f: Formula): Boolean

    Permalink

  9. def distinctInterpretation[T <: Term](terms: Set[T], order: TermOrder): Map[ConstantTerm, IdealInt]

    Permalink

    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

    Permalink

    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

    Permalink

    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]

    Permalink

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

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

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  15. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  16. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  17. def hasCountermodel(rawFormula: Conjunction): Option[Conjunction]

    Permalink

  18. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  19. def isExistentialPresburger(f: Formula): Boolean

    Permalink

  20. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  21. def isPresburger(f: Formula): Boolean

    Permalink

  22. def isQFPresburger(f: Formula): Boolean

    Permalink

  23. def isQFPresburgerConjunction(f: Conjunction): Boolean

    Permalink

  24. def isSatisfiable(rawFormula: Conjunction): Boolean

    Permalink

  25. def isValid(rawFormula: Conjunction): Boolean

    Permalink

  26. def lowerBound(objective: LinearCombination, constraint: Conjunction): Option[IdealInt]

    Permalink

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

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

  27. def miniScope(c: Conjunction): Conjunction

    Permalink

  28. def minimiseFormula(c: Conjunction): Conjunction

    Permalink

    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

    Permalink
    Definition Classes
    AnyRef

  30. def nonDNFEnumDisjuncts(formula: Conjunction): Iterator[Conjunction]

    Permalink

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

  31. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  32. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  33. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef

  34. def toDNF(formula: Conjunction): Conjunction

    Permalink

    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

    Permalink

    Convert a given formula to prenex form.

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

  36. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  37. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  38. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  39. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Ungrouped