Commit e49d88f4 authored by ehilin02's avatar ehilin02
Browse files

entailtment

parent 18ed5364
......@@ -7,12 +7,11 @@
\subsection{{\EPbA} summary of $\hls{}$ atoms}
\label{ssec:sat-hls-abs}
\noindent {\bf Lemma~\ref{lem-}}\begin{lemma}[Summary of $\hls{}$ atoms]
Let $ \hls{}(x, y; z)$ be an atom in \slah\
\noindent {\bf Lemma~\ref{lem-hls}}.
\emph{Let $ \hls{}(x, y; z)$ be an atom in \slah\
representing a non-empty heap, where $x, y, z$ are three distinct variables in $\cV$.
Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$, which summarizes $\hls{}(x, y; z)$, namely for every stack $s$ $s \models \abs^+(\hls{}(x,y; z))$ iff there exists a heap $h$ such that $s, h \models \hls{}(x, y, z)$.
Then there is an {\qfpa} formula, denoted by $\abs^+(\hls{}(x,y; z))$, which summarizes $\hls{}(x, y; z)$, namely for every stack $s$ $s \models \abs^+(\hls{}(x,y; z))$ iff there exists a heap $h$ such that $s, h \models \hls{}(x, y, z)$. }
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\end{lemma}
\begin{proof}
The constraint that the atom represents a non-empty heap means that
......@@ -30,7 +29,7 @@ $2 k \le y-x \le k z$. Then $\hls{}(x, y; z)$ is summarized by the formula $\exi
%and $v_i$ ($i\in\{1..n\}$) variables in $\cV$.
The formula $\exists k.\ k \ge 1 \wedge 2k \le y -x \le kz$ is actually equivalent to the disjunction of the two formulas corresponding to the following two cases:
\begin{itemize}
\item If $2 = z$, then $\abs^+(\hls{}(x, y; z))$ has the formula $\exists k.\ k \ge 1 \land y -x = 2k$ as a disjunct.
\item If $2 = z$, then $\abs^+(\hls{}(x, y; z))$ has the formula $\exists k.\ k \ge 1 \land y -x = 2k$, which is equivalent to the {\qfpa} formula $2 \le y -x \wedge y - x \equiv_2 0$, as a disjunct.
%
\item If $2 < z$, then we consider the following sub-cases:
\begin{itemize}
......@@ -66,10 +65,9 @@ To sum up, we obtain
which can be further simplified into
\begin{eqnarray*}
\abs^+(\hls{}(x, y; z)) & \triangleq
& \big(2 = z
~\land~ \exists k.\ k \ge 1 \land 2k = y-x \big) \\
& \big(2 = z \land 2 \le y -x \wedge y - x \equiv_2 0 \big) \\
& \lor & \big(2 < z
~\land~ 2 \le y - x
\land 2 \le y - x
\big).
\end{eqnarray*}
%
......@@ -216,9 +214,9 @@ From the definition of $h$, we know that $s, h \models \varphi$. Therefore, $\va
\begin{remark}
%The Boolean variables $\isemp_a$ in $\abs(\varphi)$ are introduced for improving the readability. They are redundant in the sense that they can be equivalently replaced by the formula $\atomhead(a) = \atomtail(a)$.
From the construction of $\abs(\varphi)$, we know that $\abs(\varphi)$ is in {\EPbA} and the size of $\abs(\varphi)$ is polynomial in that of $\varphi$. From the fact that the satisfiability of \EPbA\ is in NP, we conclude that the satisfiability of \slah\ is in NP.
From the construction of $\abs(\varphi)$, we know that $\abs(\varphi)$ is in {\qfpa} and the size of $\abs(\varphi)$ is polynomial in that of $\varphi$. From the fact that the satisfiability of {\qfpa} is in NP, we conclude that the satisfiability of \slah\ is in NP.
%
The formulas $\exists k.\ k \ge 1 \wedge 2k = y - x $ in $\abs^+(\hls{}(x, y; z))$ can be equivalently replaced by $y -x > 0 \wedge y -x \equiv 0 \bmod 2$. Therefore, $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints. The satisfiability of such formulas is still NP-complete.
%The formulas $\exists k.\ k \ge 1 \wedge 2k = y - x $ in $\abs^+(\hls{}(x, y; z))$ can be equivalently replaced by $y -x > 0 \wedge y -x \equiv 0 \bmod 2$. Therefore, $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints. The satisfiability of such formulas is still NP-complete.
%From now on, we shall assume that {\bf $\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}.
\end{remark}
......@@ -227,19 +225,19 @@ The formulas $\exists k.\ k \ge 1 \wedge 2k = y - x $ in $\abs^+(\hls{}(x, y; z)
\smallskip
\noindent {\bf Lemma~\ref{lem-eub}}.
\emph{For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, an {\EPbA} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \rightarrow \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
\emph{For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \rightarrow \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
}
\smallskip
\begin{proof}
From the construction of $\abs^+(\hls{}(t'_1, t'_2; t'_3))$ in Section~\ref{sec:sat-hls}, we know that for every store $s$, there is a heap $h$ such that $s, h \models \Pi: \hls{}(t'_1, t'_2; t'_3)$ iff $s \models \Pi \wedge \big((t'_3 = 2 \wedge \exists k.\ 2k = t'_2 - t'_1) \vee ( 2 < t'_3 \wedge 2 \le t'_2 - t'_1)\big)$. Then the fact that $z$ appears in some unfolding scheme of $\varphi$ w.r.t. some store $s$
From the construction of $\abs^+(\hls{}(t'_1, t'_2; t'_3))$ in Section~\ref{sec:sat-hls}, we know that for every store $s$, there is a heap $h$ such that $s, h \models \Pi: \hls{}(t'_1, t'_2; t'_3)$ iff $s \models \Pi \wedge \big((t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0) \vee ( 2 < t'_3 \wedge 2 \le t'_2 - t'_1)\big)$. Then the fact that $z$ appears in some unfolding scheme of $\varphi$ w.r.t. some store $s$
can be specified by the formula
\[
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge \exists k.\ 2k = t'_2 - t'_1 \wedge z = 2)\ \vee \\
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
(2 < t'_3 \wedge 2 \le z \le t'_3\ \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z))
\end{array}
\right),
......@@ -250,7 +248,7 @@ where $t'_2 - t'_1 - z$ denotes the remaining size of the heap after removing a
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge \exists k.\ 2k = t'_2 - t'_1 \wedge z = 2)\ \vee \\
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
\left(
\begin{array}{l}
2 < t'_3 \wedge 2 \le z \le t'_3 \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z) \ \wedge \\
......@@ -274,7 +272,7 @@ It follows that $\xi_{eub,\varphi}(z) $ can be simplified into
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge \exists k.\ 2k = t'_2 - t'_1 \wedge z = 2)\ \vee \\
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
\left(
\begin{array}{l}
2 < t'_3 \wedge 2 \le z \le t'_3 \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z) \ \wedge \\
......@@ -285,7 +283,7 @@ z+2 \le t'_3 \rightarrow t'_2 - t'_1 \neq z+2
\end{array}
\right),
\]
which is an \EPbA\ formula.
which is a {\qfpa} formula.
\qed
\end{proof}
......
......@@ -14,9 +14,9 @@ The satisfiability problem of {\slah} is NP-complete.
The NP lower bound follows from that of ASL in \cite{BrotherstonGK17}. The NP upper bound is achieved by encoding the satisfiability problem of {\slah} as that of an existentially quantified Presburger arithmetic formula. The rest of this section is devoted to the proof of the NP upper bound.
Presburger arithmetic (\PbA) is the first-order theory with equality
of the signature $\langle 0,1,+, <, (\bmod\ n)_{n \in \NN \setminus \{0\}}\rangle$ interpreted over the
of the signature $\langle 0,1,+, <, (\equiv_n)_{n \in \NN \setminus \{0\}}\rangle$ interpreted over the
domain of naturals $\NN$ with `$+$' interpreted as the addition,
`$<$' interpreted as the order relation, and $\bmod\ n$ interpreted as the modulo function.\footnote{%
`$<$' interpreted as the order relation, and $\equiv_n$ interpreted as the congruence relation modulo $n$.\footnote{%
Although `$<$' may be encoded using existential quantification in \PbA\ over naturals,
we prefer to keep it in the signature of \PbA\ to obtain quantifier free formulas.%
}
......@@ -51,7 +51,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 Also, the predicate atoms $\hls{}(t_1, t_2; t_3)$ are encoded by a formula in {\EPbA}, $\abs^+(\hls{}(t_1, t_2; t_3))$.
\item Also, the predicate atoms $\hls{}(t_1, t_2; t_3)$ are encoded by a formula in {\EPbA}, $t_1 = t_2 \vee \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.
......@@ -96,7 +96,7 @@ The following lemma states that
%In the sequel, we are going to show that
$\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned into an equivalent {\qfpa} formula.
\begin{lemma}[Summary of $\hls{}$ atoms]
\begin{lemma}[Summary of $\hls{}$ atoms]\label{lem-hls}
Let $ \hls{}(x, y; z)$ be an atom in \slah\
representing a non-empty heap, where $x, y, z$ are three distinct variables in $\cV$.
%Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$,
......
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