# ReduceWithPredLits

### Related Docs: object ReduceWithPredLits | package preds

#### class ReduceWithPredLits extends AnyRef

Class for reducing a conjunction of predicate literals using a set of known literals (facts). This reduction can be done modulo the axiom of functionality (for predicates encoding functions or partial functions), and then potentially replaces predicate literals with simple equations.

Linear Supertypes
AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ReduceWithPredLits
2. AnyRef
3. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### 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

5. #### def apply(conj: PredConj): (PredConj, ArithConj)

Reduce a conjunction of predicate literals using known predicate literals.

Reduce a conjunction of predicate literals using known predicate literals. This function knows about functional predicates, and is able to apply the functionality axiom to replace predicate literals with equations.

6. #### def apply(conj: PredConj, logger: ComputationLogger): (PredConj, ArithConj)

Reduce a conjunction of predicate literals using known predicate literals.

Reduce a conjunction of predicate literals using known predicate literals. This function knows about functional predicates, and is able to apply the functionality axiom to replace predicate literals with equations.

7. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
8. #### def clone(): AnyRef

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

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

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

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

Definition Classes
AnyRef → Any
13. #### def hashCode(): Int

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

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

Definition Classes
AnyRef
16. #### final def notify(): Unit

Definition Classes
AnyRef
17. #### final def notifyAll(): Unit

Definition Classes
AnyRef
18. #### def passQuantifiers(num: Int): ReduceWithPredLits

Create a `ReduceWithPredLits` that can be used underneath `num` binders.

Create a `ReduceWithPredLits` that can be used underneath `num` binders. The conversion of de Brujin-variables is done on the fly, which should give a good performance when the resulting `ReduceWithEqs` is not applied too often (TODO: caching)

19. #### def reductionPossible(conj: PredConj): Boolean

Determine whether a formula that contains the given predicates might be reducible by this reducer

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

Definition Classes
AnyRef
21. #### def toString(): String

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )
25. #### lazy val withoutFacts: ReduceWithPredLits

A reducer corresponding to this one, but without assuming any facts known a priori.