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
    @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. def finalize(): Unit

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

    Permalink
    Definition Classes
    AnyRef → Any
  18. def hasCountermodel(rawFormula: Conjunction): Option[Conjunction]

    Permalink
  19. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  20. def isExistentialPresburger(f: Formula): Boolean

    Permalink
  21. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  22. def isPresburger(f: Formula): Boolean

    Permalink
  23. def isQFPresburger(f: Formula): Boolean

    Permalink
  24. def isQFPresburgerConjunction(f: Conjunction): Boolean

    Permalink
  25. def isSatisfiable(rawFormula: Conjunction): Boolean

    Permalink
  26. def isValid(rawFormula: Conjunction): Boolean

    Permalink
  27. 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.

  28. def miniScope(c: Conjunction): Conjunction

    Permalink
  29. 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.

  30. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  31. def nonDNFEnumDisjuncts(formula: Conjunction): Iterator[Conjunction]

    Permalink

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

  32. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  33. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  34. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  35. 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)

  36. 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?

  37. def toString(): String

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

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped