Nelson-Oppen

Bibliography.bib

@@ -1121,4 +1121,15 @@ year = {2005},
                Design, 1993, Santa Clara, California, USA, November 7-11, 1993},
   pages     = {188--191},
   year      = {1993}
-}
\ No newline at end of file
+}
+
+@article{NO79,
+  author    = {Greg Nelson and
+               Derek C. Oppen},
+  title     = {Simplification by Cooperating Decision Procedures},
+  journal   = {{ACM} Trans. Program. Lang. Syst.},
+  volume    = {1},
+  number    = {2},
+  pages     = {245--257},
+  year      = {1979}
+}

Chapters/Chapter02.tex

@@ -178,7 +178,7 @@ $\mathcal{T}$-\emph{solver}.
 % formula without existential quantifiers by introducing uninterpreted
 % functions; this process is known as \emph{Skolemization}.
 
-\subsection{Multi-sorted logic}
+\subsection{Many-sorted logic}
 
 For some theories, it can be convinient to distinguish several types
 of objects instead of having only one universe. This can be achieved
@@ -412,12 +412,14 @@ Nelson and Oppen have shown that satisfiability of combination of
 stably infinite theories with disjoint signatures can be solved by
 using separate satisfiability solvers for the respective theories,
 which interchange implied equalities and disequalities between shared
-variables. A theory $\mathcal{T}$ is \emph{stably infinite} for every
-$\mathcal{T}$-satisfiable formula exists a $\mathcal{T}$ model, whose
-universe is infinite. For a theory over a multi-sorted logic, the
-theory is \emph{stably infinite} for every $\mathcal{T}$-satisfiable
-formula exists a $\mathcal{T}$ model, whose every sort is interpreted
-as infinite. This is not a strong restriction, almost all
+variables~\cite{NO79}. A theory $\mathcal{T}$ is \emph{stably
+  infinite} if every $\mathcal{T}$-satisfiable formula has a
+$\mathcal{T}$ model whose universe is infinite. For a theory over in a
+many-sorted logic, the theory is \emph{stably infinite} if every
+$\mathcal{T}$-satisfiable formula has a model model, whose every sort
+has an infinite domain. Although almost all practically used theories
+are stably infinite, this is not true for inherently finite theories
+like the theory of bit-vectors.
 
 \subsection{DPLL modulo theories}
 
@@ -597,7 +599,7 @@ and uninterpreted functions~\cite{McM11}.
 
 \section{Satisfiability of quantifier-free bit-vector formulas}
 
-The \emph{theory of fixed sized bit-vectors (\BV)} is a multi-sorted
+The \emph{theory of fixed sized bit-vectors (\BV)} is a many-sorted
 first-order theory with infinitely many sorts $\sort{n}$ corresponding
 to bit-vectors of length $n$. The only predicate symbols in the \BV
 theory are $=$, $\leq_u$, and $\leq_s$, interpreted as equality,

Chapters/Chapter04.tex

@@ -4,15 +4,38 @@
 
 \section{Objectives and Expected Results}
 
+\subsection{Unconstrained variable propagation for quantified
+  bit-vectors}
+Simplifications using unconstrained variables can be extended to
+quantified formulas. However, in the quantified setting, constraints
+can be induced also by the order of the quantified variables. We have
+hypothesis of the necessary condition for the quantified variable to
+be unconstrained and we have implemented an proof-of-concept
+simplification procedure using unconstrained variables for the
+quantified bit-vector formulas. Although the initial experimental
+results, conducted on the formulas from the semi-symbolic model
+checker \SymDivine look promissing, the formal proof of the correctnes
+is not yet complete.
+
+Furthermore, we suggest simplifications even for term in the form
+$k \times x$ with odd values of $x$. If $x$ has bit-width $n$, $i$ is
+the largest number such that $2^i$ which divides the constant $k$ and
+the value $x$ is unconstrained, the term $k \times x$ can be rewritten
+to $extract_0^{n-i}(x) \cdot 0^i$. This approach can possibly be
+extended to the multiplication of two variables from one is
+unconstrained and further generalized. We plan to prove the
+correctness of these rules and develop a formal framework to classify
+such rewrite rules.
+
 \subsection{Symbolic solver for quantified bit-vectors}
-I plan to further develop the implemented symbolic \smt solver for
+I plan to continue developing the implemented symbolic \smt solver for
 quantified bit-vecors Q3B. Besides implementing the proposed
-simplifiactions using unconstrained variables, I plan to add support
-of uninterpreted functions and theory of arrays, which are highly
-desirable for the usage in program verification. I also want to
-implement a support for extracting unsatisfiable cores from the
-intermediate \bdds, which were produced during the computation of the
-solver.
+simplifiactions for quantified formulas containing unconstrained
+variables, I plan to add support of uninterpreted functions and theory
+of arrays, which are highly desirable for the usage in program
+verification. I also want to implement a support for extracting
+unsatisfiable cores from the intermediate \bdds, which were produced
+during the computation of the solver.
 
 Additionally, approximations implemented are right now very simple and
 could benefit from better refinement of the approximation in the case
@@ -42,29 +65,6 @@ As the part of my PhD study, also an implementation of a proposed
 hybrid approach and its evaluation on the representative set of
 benchmark is expected.
 
-\subsection{Unconstrained variable propagation for quantified
-  bit-vectors}
-Simplifications using unconstrained variables can be extended to
-quantified formulas. However, in the quantified setting, constraints
-can be induced also by the order of the quantified variables. We have
-hypothesis of the necessary condition for the quantified variable to
-be unconstrained and we have implemented an proof-of-concept
-simplification procedure using unconstrained variables for the
-quantified bit-vector formulas. Although the initial experimental
-results, conducted on the formula from the semi-symbolic model checker
-\SymDivine look promissing, the formal proof of the correctnes is not
-yet complete.
-
-Furthermore, we suggest simplifications even for term in the form
-$k \times x$ with odd values of $x$. If $x$ has bit-width $n$, $i$ is
-the largest number such that $2^i$ which divides the constant $k$ and
-the value $x$ is unconstrained, the term $k \times x$ can be rewritten
-to $extract_0^{n-i}(x) \cdot 0^i$. This approach can possibly be
-extended to the multiplication of two variables from one is
-unconstrained and further generalized. We plan to prove the
-correctness of these rules and develop a formal framework to classify
-such rewrite rules.
-
 \subsection{Complexity of BV2}
 As was explained in section ???, the precise complexity of quantified
 bit-vector formulas with binary-encoded bit-widths and without