Apply this procedure to the given goal in model-generation mode.
Apply this procedure to the given goal in model-generation mode. In this mode, we have already established that a problem is satisfiable, but still need to compute a full/concrete model.
From a theory procedure, determine in which state a given goal is.
From a theory procedure, determine in which state a given goal is.
Apply this plugin to the given goal.
Apply this plugin to the given goal.
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.
Execution of a sequence of plugins.