Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
Martin Jonáš
DTEDI
Commits
7b2c36cd
Commit
7b2c36cd
authored
Sep 04, 2016
by
Martin Jonáš
Browse files
Fix todos
parent
bc0a4271
Changes
2
Hide whitespace changes
Inline
Side-by-side
Bibliography.bib
View file @
7b2c36cd
...
...
@@ -150,13 +150,10 @@
year
=
{2015}
}
@
inproceedings
{
BF15restarts
,
@
misc
{
BF15restarts
,
author
=
{Armin Biere and
Andreas Fr{\"{o}}hlich}
,
title
=
{Evaluating {CDCL} Restart Schemes}
,
booktitle
=
{Workshop on Pragmatics of SAT -- {POS'15}, Austin, TX,
USA, September 24-27, 2015, Proceedings}
,
pages
=
{405--422}
,
year
=
{2015}
}
...
...
@@ -1140,4 +1137,38 @@ year = {2005},
journal
=
{CoRR}
,
volume
=
{abs/1602.03050}
,
year
=
{2016}
}
@article
{
TZ05
,
author
=
{Cesare Tinelli and
Calogero G. Zarba}
,
title
=
{Combining Nonstably Infinite Theories}
,
journal
=
{J. Autom. Reasoning}
,
volume
=
{34}
,
number
=
{3}
,
pages
=
{209--238}
,
year
=
{2005}
}
@inproceedings
{
JB10
,
author
=
{Dejan Jovanovic and
Clark Barrett}
,
title
=
{Polite Theories Revisited}
,
booktitle
=
{Logic for Programming, Artificial Intelligence, and Reasoning - 17th
International Conference, LPAR-17, Yogyakarta, Indonesia, October
10-15, 2010. Proceedings}
,
pages
=
{402--416}
,
year
=
{2010}
}
@inproceedings
{
RRZ05
,
author
=
{Silvio Ranise and
Christophe Ringeissen and
Calogero G. Zarba}
,
title
=
{Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted
Logic}
,
booktitle
=
{Frontiers of Combining Systems, 5th International Workshop, FroCoS
2005, Vienna, Austria, September 19-21, 2005, Proceedings}
,
pages
=
{48--64}
,
year
=
{2005}
}
\ No newline at end of file
Chapters/Chapter02.tex
View file @
7b2c36cd
...
...
@@ -122,10 +122,11 @@ For two signatures $\Sigma$ and $\Omega$, we call $\Omega$ a
$
\Omega
^
p
\subseteq
\Sigma
^
p
$
. Given a
$
\Sigma
$
-structure
$
\mathcal
{
A
}$
and a signature
$
\Omega
$
that is a sub-signature of
$
\Sigma
$
, the
\emph
{
reduct
}
of
$
\mathcal
{
A
}$
to a sub-signature
$
\Omega
$
is an
$
\Omega
$
-structure
$
\mathcal
{
A
}
'
$
that coincides with
$
\mathcal
{
A
}$
on all symbols from
$
\Omega
$
. For a
$
\Sigma
_
1
$
-theory
$
\mathcal
{
T
}_
1
$
and a
$
\Sigma
_
2
$
-theory
$
\mathcal
{
T
}_
2
$
, their
\emph
{
combination
}
$
\mathcal
{
T
}_
1
+
\mathcal
{
T
}_
2
$
is the largest
$
\Omega
$
is an
$
\Omega
$
-structure
$
\mathcal
{
A
}
'
$
that has the same
universe as
$
\mathcal
{
A
}$
and coincides with
$
\mathcal
{
A
}$
on all
symbols from
$
\Omega
$
. For a
$
\Sigma
_
1
$
-theory
$
\mathcal
{
T
}_
1
$
and a
$
\Sigma
_
2
$
-theory
$
\mathcal
{
T
}_
2
$
, their
\emph
{
combination
}
$
\mathcal
{
T
}_
1
+
\mathcal
{
T
}_
2
$
is the largest
$
(
\Sigma
_
1
\cup
\Sigma
_
2
)
$
-theory that contains all
$
(
\Sigma
_
1
\cup
\Sigma
_
2
)
$
-structures
$
\mathcal
{
A
}$
for which the
reduct of
$
\mathcal
{
A
}$
to
$
\Sigma
_
1
$
is in
$
\mathcal
{
T
}_
1
$
and the
...
...
@@ -317,8 +318,7 @@ solutions~\cite{GSK98}. Although most commonly used heuristic to
decide when to restart the solver is based on the
\emph
{
Luby
sequence
}
~
\cite
{
LSZ93
}
, the recent survey has shown that it is
outperformed by a heuristic based on the concept of exponential moving
averages~
\cite
{
BF15restarts
}
.
\marginpar
{
spravit citaci, BF15a nevyšlo
v proceedings
}
averages~
\cite
{
BF15restarts
}
.
In addition to the mentioned heuristics, an efficient implementation
of
\cdcl
based
\sat
solver relies on lazy data structures used in the
...
...
@@ -409,7 +409,12 @@ Notable examples of decidable first-order theories include
interpreted as a value on the index
$
i
$
of the array
$
a
$
, and a
ternary function
$
\arwrite
(
a, i, v
)
$
interpreted as an array
$
a
$
modified to contain the value
$
v
$
on the index
$
i
$
;
\item
the theory of
\emph
{
fixed-size bit-vectors
}
.
\marginpar
{
TODO: describe
}
\item
the theory of
\emph
{
fixed-size bit-vectors
}
, in which the
structure contains all bit-vectors as an universe, ordering
relations according to the corresponding integers, and interpreted
functions are bit-wise operations on the bit-vectors and modular
arithmetic operations on the corresponding integers. This theory is
in detail described in section
\ref
{
sec:qfbv
}
.
\end{itemize}
For a detailed description of these theories and implementation of the
respective
$
\mathcal
{
T
}$
-solvers, we refer the reader for example to the book of
...
...
@@ -426,10 +431,12 @@ 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 a
many-sorted logic, the theory is
\emph
{
stably infinite
}
if every
$
\mathcal
{
T
}$
-satisfiable formula has a 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.
$
\mathcal
{
T
}$
-satisfiable formula has a 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. Therefore, variants of the theory
combinations in which one of the theories does not have to be stably
infinite have been proposed~
\cite
{
TZ05, RRZ05, JB10
}
.
\subsection
{
DPLL modulo theories
}
...
...
@@ -608,6 +615,7 @@ arithmetic~\cite{CHN12}, linear integer arithmetic~\cite{KLR10, GLS11,
and uninterpreted functions~
\cite
{
McM11
}
.
\section
{
Satisfiability of quantifier-free bit-vector formulas
}
\label
{
sec:qfbv
}
The
\emph
{
theory of fixed sized bit-vectors (
\BV
)
}
is a many-sorted
first-order theory with infinitely many sorts
$
\sort
{
n
}$
corresponding
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment