Commit b4741784 authored by ehilin02's avatar ehilin02
Browse files

satisfiability

parent c402552c
......@@ -52,7 +52,7 @@ that encodes its satisfiability:
\begin{compactitem}
\item At first, points-to atoms $t_1 \pto t_2$ are transformed into $\blk(t_1, t_1+1)$.
\item Then, the block atoms $\blk(t_1, t_2)$ are encoded by the constraint $t_1 < t_2$.
\item The predicate atoms $\hls{}(t_1, t_2; t_3)$, absent in ASL, are encoded by a formula in {\EPbA}, $t_1 = t_2 \vee \abs^+(\hls{}(t_1, t_2; t_3))$.
\item The predicate atoms $\hls{}(t_1, t_2; t_3)$, absent in ASL, are encoded by a formula in {\EPbA}, $t_1 = t_2 \vee (t_1 < t_2 \wedge \abs^+(\hls{}(t_1, t_2; t_3)))$.
\item Lastly, the separating conjunction is encoded by an {\EPbA} formula constraining the address terms of spatial atoms.
\end{compactitem}
The Appendix~\ref{app:sat-hls} provides more details.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment