From a theory procedure, determine in which state a given goal is.
Find constants that occur both in atoms constructed using predicates
from consideredPredicates
and in atoms constructed
using predicates not in theoryPredicates
.
Find constants that occur both in atoms constructed using predicates
from consideredPredicates
and in atoms constructed
using predicates not in theoryPredicates
. Arithmetic
facts (equations, disequations, inequalities) in a goal are not
considered, but arithmetic clauses are included.
Find constants that occur both in atoms constructed using theory predicates and in atoms constructed using non-theory predicates.
Find constants that occur both in atoms constructed using theory predicates and in atoms constructed using non-theory predicates. Arithmetic facts (equations, disequations, inequalities) in a goal are not considered, but arithmetic clauses are included.
An implicit function to simplify cascading of possible actions.
An implicit function to simplify cascading of possible actions.
(Since version ) see corresponding Javadoc for more information.
General interface for a theory-specific procedure that can be applied by a prover to reason about interpreted symbols.