![]() |
SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Uses equations (or Boolean assertions) to eliminate variables from the remaining formula. Let the formula have the form , then we use knowledge gained from
to simplify
. If
is an arithmetic equation such that we can rewrite it to the form
(with
a variable) then we substitute
for
into
. Otherwise we simply replace
with
in
. This is done recursively in the formula.