Instantiate the outermost quantifiers with the given terms, starting with the innermost quantifier to be instantiated
Return whether this conjunction actually only is a single arithmetic literal (a single, unquantified (in)equation, inequality)
Return whether this
is a divisibility judgement
EX (n*_0 + t = 0)
Return whether this
is a divisibility judgement
EX (n*_0 + t = 0)
"Division quantifiers" of the form
EX ( n*_0 + t >= 0 & -n*_0 - t - m >= 0 & phi )
where 0 <= m < n
.
"Division quantifiers" of the form
EX ( n*_0 + t >= 0 & -n*_0 - t - m >= 0 & phi )
where 0 <= m < n
.
The result of this test is a triple
(n*_0 + t, -n*_0 - t - m, phi)
,
or None
if the formula is not of the guarded quantifier shape
"Exact division quantifiers" of the form
EX ( n*_0 + t = 0 & phi)
where 0 < n
.
"Exact division quantifiers" of the form
EX ( n*_0 + t = 0 & phi)
where 0 < n
.
The result of this test is a pair
(n*_0 + t, phi)
,
or None
if the formula is not of the guarded quantifier shape
The only allow case of false is when arithConj
is false and
everything else is empty.
The only allow case of false is when arithConj
is false and
everything else is empty.
Return whether this conjunction actually only is a single literal (a single, unquantified (in)equation, inequality or predicate literal)
Return whether this conjunction actually is the negation of a single conjunction
Return whether this
is a negated divisibility judgement
ALL (n*_0 + t != 0)
Return whether this
is a negated divisibility judgement
ALL (n*_0 + t != 0)
Assuming that this formula is a divisibility or non-divisibility statement,
check whether the divisibility is proper (i.e., not of the form
ALL (1*_0 + t != 0)
)
Assuming that this formula is a divisibility or non-divisibility statement,
check whether the divisibility is proper (i.e., not of the form
ALL (1*_0 + t != 0)
)
Return whether this conjunction only contains negated sub-conjunctions
Return whether this
is a divisibility judgement
EX (n*_0 + t = 0)
, possibly underneath quantifiers
Return whether this
is a divisibility judgement
EX (n*_0 + t = 0)
, possibly underneath quantifiers
Return whether this conjunction actually is the negation of a single conjunction
Return whether this
is a negated divisibility judgement
ALL (n*_0 + t != 0)
, possibly underneath quantifiers
Return whether this
is a negated divisibility judgement
ALL (n*_0 + t != 0)
, possibly underneath quantifiers
Return true
if this formula is obviously always true
Return true
if this formula is obviously always true
Re-sort an object with a new TermOrder
.
Re-sort an object with a new TermOrder
. It is guaranteed that
the result isSortedBy(order)
Remove the num
outermost quantifiers of this
Conjunction
, without changing the matrix of the formula
Remove the num
outermost quantifiers of this
Conjunction
, without changing the matrix of the formula
Update the arithmetic parts of this conjunction (without changing anything
else apart from the TermOrder
)
Update the arithmetic parts of this conjunction (without changing anything
else apart from the TermOrder
)
Update the inequalities of this conjunction (without changing anything
else apart from the TermOrder
)
Update the inequalities of this conjunction (without changing anything
else apart from the TermOrder
)
Update the inequalities of this conjunction (without changing anything
else apart from the TermOrder
)
Update the inequalities of this conjunction (without changing anything
else apart from the TermOrder
)
Update the negative equations of this conjunction (without changing anything
else apart from the TermOrder
)
Update the negative equations of this conjunction (without changing anything
else apart from the TermOrder
)
Update the positive equations of this conjunction (without changing anything
else apart from the TermOrder
)
Update the positive equations of this conjunction (without changing anything
else apart from the TermOrder
)
Update the predicate parts of this conjunction (without changing anything
else apart from the TermOrder
)
Update the predicate parts of this conjunction (without changing anything
else apart from the TermOrder
)
Class for representing (possibly quantified) conjunctions of arithmetic literal (equations, inequalities), predicate literals and negated
Conjunction
s.quans
describes how the lowestquans.size
variables are quantified in the conjunction (quans(0)
) is responsible forVariableTerm(0)
and is the innermost quantifier, etc).