You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

10 lines
586 B

\begin{itemize}
\item In eager encoding, all axioms of the theory are explicitly incorporated into the input formula. The resulting equisatisfiable propositional formula is then given to a SAT solver.
\item SMT solvers that use lazy encoding use specialized theory solvers in combination with SAT solvers to decide the satisfiability of formulas within a given theory.
In contrast to eager encoding, where a
sufficient set of constraints is computed at the beginning, lazy encoding starts
with no constraints at all, and lazily adds constraints only when required.
\end{itemize}