Commit 2a1eb123 authored by Martin Jonáš's avatar Martin Jonáš
Browse files

Many-sorted logic + small changes

parent 44efecd9
......@@ -844,12 +844,12 @@
@techreport{BoolectorComp,
title = {{Boolector at the SMT competition 2016}},
year={2016},
series = {Technical Report 16/1},
date = {June 2016},
address = {{FMV Reports Series, Institute for Formal Models and
Verification, Johannes Kepler University, Altenbergerstr. 69, 4040
Linz, Austria}},
year={2016}
}
@inproceedings{CMR97,
......@@ -1098,4 +1098,27 @@ year = {2005},
Design, 1993},
pages = {42--47},
year = {1993}
}
@inproceedings{Min93,
author = {Shin{-}ichi Minato},
title = {Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems},
booktitle = {{DAC}},
pages = {272--277},
year = {1993}
}
@inproceedings{BFGHMPS,
author = {R. Iris Bahar and
Erica A. Frohm and
Charles M. Gaona and
Gary D. Hachtel and
Enrico Macii and
Abelardo Pardo and
Fabio Somenzi},
title = {Algebraic decision diagrams and their applications},
booktitle = {Proceedings of the 1993 {IEEE/ACM} International Conference on Computer-Aided
Design, 1993, Santa Clara, California, USA, November 7-11, 1993},
pages = {188--191},
year = {1993}
}
\ No newline at end of file
......@@ -63,8 +63,8 @@ if $\varphi$ is satisfiable precisely if $\psi$ is satisfiable.
\subsection{First-order logic and theories}
A \emph{signature} $\Sigma$ consists of a set of \emph{function
symbols} $\Sigma^f$ and a set of \emph{predicate symbols} $\Sigma^p$
and for each of the symbols a non-negative number called its
symbols} $\Sigma^f$, a set of \emph{predicate symbols} $\Sigma^p$
and for each of these symbols a non-negative number called its
\emph{arity}. Given a signature $\Sigma$, \emph{$\Sigma$-terms},
\emph{$\Sigma$-atoms}, \emph{$\Sigma$-literals},
\emph{$\Sigma$-clauses}, and \emph{$\Sigma$-formulas} are defined as
......@@ -178,12 +178,45 @@ $\mathcal{T}$-\emph{solver}.
% formula without existential quantifiers by introducing uninterpreted
% functions; this process is known as \emph{Skolemization}.
\subsection{Multi-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
by using a \emph{many-sorted logic}. In contrast with a single-sorted
signature, defined in the previous subsection, a many-sorted signature
$\Sigma$ further contains a set of \emph{sort symbols}
$\Sigma^S$. Arities in a many-sorted logic are also modified. Arity of
a symbol determines not only a number of its arguments, but also their
types -- each function symbol has assigned $(n+1)$-tuple of sort
symbols for a non-negative integer $n$ and each predicate symbols has
assigned a $n$-tuple of sort symbols for a non-negative integer
$n$. Simultaneous inductive definition of terms of a sort
$S \in \Sigma^S$ and definitions of atoms, literals, clauses and
formulas are straightforward and can be found for example in Enderton.
For a many-sorted signature $\Sigma$, a \emph{$\Sigma$-structure}
$\mathcal{A}$ consists of an assignment $(\_)^\mathcal{A}$, which to
each sort symbol $S \in \Sigma^S$ assigns a non-empty set
$S^\mathcal{A}$, caled the \emph{domain of S in $\mathcal{A}$}, to
each variable $x$ of sort $S$ assigns an element
$x^\mathcal{A} \in S^\mathcal{A}$, to each function symbol
$f \in \Sigma^f$ of arity $(S_1, \ldots, S_n, S_{n+1})$ assigns a
function
$f^\mathcal{A} \colon S_1^\mathcal{A} \times \ldots \times
S_n^\mathcal{A} \rightarrow S_{n+1}^\mathcal{A}$, and to each
predicate symbol $P \in \Sigma^p$ of arity $(S_1, \ldots, S_n)$
assigns a relation
$P^\mathcal{A} \subseteq S_1^\mathcal{A} \times \ldots \times
S_n^\mathcal{A}$. Definitions of many-sorted satisfiability, models,
entailment, and so on are also straightforward and can be found in
Enderton.
\section{Propositional satisfiability}
A \emph{propositional satisfiability problem} (\sat) is, for a given
formula $\varphi$ in \cnf, to decide whether it is satisfiable. The
restriction to formulas in \cnf is without a loss of generality, as
the Tseitin transformation can be used to transform every formula to
the Tseytin transformation can be used to transform every formula to
an equisatisfiable formula in \cnf with only linear increase of its
size~\cite{Tse68}.
......@@ -449,11 +482,11 @@ the search of the underlying \dpll solver has been named
further improvements, we refer the reader to survey on the
topic~\cite{Seb07}, or to the abstract description of the underlying
transition system~\cite{NOT06}. The \dpllt approach is used in the
majority of modern \smt solvers, including
majority of modern \smt solvers, including solvers
Barcelogic~\cite{Barcelogic}, CVC4~\cite{CVC4},
MathSAT~\cite{MathSAT}, OpenSMT~\cite{OpenSMT},
Simplify~\cite{Simplify}, Yices~\cite{Yices}, or
Z3~\cite{Z3}.\marginpar{TODO: Přetok}
Z3~\cite{Z3}.
\subsection{Natural domain \smt}
\label{ssec:natDomainSat}
......
......@@ -19,9 +19,10 @@ could benefit from better refinement of the approximation in the case
that the current approximation is too coarse.
Moreover, we want to implement other variants of decision diagrams
such as zero-suppressed decision diagrams introduced by ??? and
algebraic decision diagrams introduced by ??? and experimentally
evaluate their effect on the performance of the \smt solver.
such as zero-suppressed decision diagrams introduced by
Minato~\cite{Min93} and algebraic decision diagrams introduced by
Bahar et al.~\cite{BFGHMPS} and experimentally evaluate their effect
on the performance of the \smt solver.
\subsection{Hybrid approach to quantified bit-vectors}
Although our results with the symbolic \smt solver for quantified
......
Supports Markdown
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