diff --git a/.merlin b/.merlin index beb445b8..cfd63256 100644 --- a/.merlin +++ b/.merlin @@ -1,16 +1,20 @@ S src/core S src/solver -S src/example +S src/sat +S src/smt +S src/mcsat S src/backend S src/util -S src/util/smtlib S tests B _build/src/ B _build/src/core B _build/src/solver -B _build/src/example +B _build/src/sat +B _build/src/smt +B _build/src/mcsat B _build/src/util -B _build/src/util/smtlib B _build/src/backend B _build/tests + +PKG dolmen diff --git a/.travis.yml b/.travis.yml index c707458b..6256da54 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,10 +1,12 @@ language: c env: - - OCAML_VERSION=4.00.1 - - OCAML_VERSION=4.01.0 - - OCAML_VERSION=4.02.3 - - OCAML_VERSION=4.03.0 - - OCAML_VERSION=4.03.0+flambda + - RUN_TEST=false OCAML_VERSION=4.00.1 + - RUN_TEST=false OCAML_VERSION=4.01.0 + - RUN_TEST=true OCAML_VERSION=4.02.3 + - RUN_TEST=true OCAML_VERSION=4.03.0 + - RUN_TEST=true OCAML_VERSION=4.03.0+flambda + - RUN_TEST=true OCAML_VERSION=4.04.0 + - RUN_TEST=true OCAML_VERSION=4.04.0+flambda addons: apt: sources: @@ -18,8 +20,10 @@ before_install: - opam init - opam switch ${OCAML_VERSION} - eval `opam config env` -install: - opam install ocamlfind ocamlbuild - - make bin lib + - if ${RUN_TEST}; then opam pin add dolmen https://github.com/Gbury/dolmen.git; fi +install: + - make lib + - if ${RUN_TEST}; then make bin; fi script: - - make test + - if ${RUN_TEST}; then make test; fi diff --git a/META b/META index f2ed910c..993b7f01 100644 --- a/META +++ b/META @@ -1,3 +1,4 @@ +# meta name="msat" version="dev" description="MSAT is a modular SAT solver, plus extensions" @@ -6,3 +7,25 @@ archive(byte) = "msat.cma" archive(byte, plugin) = "msat.cma" archive(native) = "msat.cmxa" archive(native, plugin) = "msat.cmxs" + +package "sat" ( + version = "dev" + description = "SAT solver instance" + requires = "msat" + archive(byte) = "msat_sat.cma" + archive(byte, plugin) = "msat_sat.cma" + archive(native) = "msat_sat.cmxa" + archive(native, plugin) = "msat_sat.cmxs" + exists_if = "msat_sat.cma" +) + +package "smt" ( + version = "dev" + description = "SMT solver instance" + requires = "msat" + archive(byte) = "msat_smt.cma" + archive(byte, plugin) = "msat_smt.cma" + archive(native) = "msat_smt.cmxa" + archive(native, plugin) = "msat_smt.cmxs" + exists_if = "msat_smt.cma" +) diff --git a/Makefile b/Makefile index 406b5b38..8f9d6531 100644 --- a/Makefile +++ b/Makefile @@ -3,12 +3,22 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind FLAGS= -DOC=msat.docdir/index.html +DOC=msat.docdir/index.html msat_sat.docdir/index.html msat_smt.docdir/index.html BIN=main.native TEST_BIN=tests/test_api.native -NAME=msat -LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) +NAME_OCAMLFIND=msat +NAME_BIN=msat +NAME_CORE=msat +#NAME_SAT=msat_sat +#NAME_SMT=msat_smt +#NAME_MCSAT=msat_mcsat + +LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs) +#LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs) +#LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs) +#LIB_MCSAT=$(addprefix $(NAME_MCSAT), .cma .cmxa .cmxs) +LIB=$(LIB_CORE) # $(LIB_SAT) $(LIB_SMT) $(LIB_MCSAT) all: lib test @@ -20,7 +30,7 @@ doc: bin: $(COMP) $(FLAGS) $(BIN) - cp $(BIN) $(NAME) && rm $(BIN) + cp $(BIN) $(NAME_BIN) && rm $(BIN) test_bin: $(COMP) $(FLAGS) $(TEST_BIN) @@ -29,7 +39,7 @@ test: bin test_bin @echo "run API tests…" @./test_api.native @echo "run benchmarks…" - @/usr/bin/time -f "%e" ./tests/run smt + # @/usr/bin/time -f "%e" ./tests/run smt @/usr/bin/time -f "%e" ./tests/run mcsat enable_log: @@ -43,17 +53,28 @@ log: clean: $(COMP) -clean + rm -rf $(NAME_BIN) -TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(NAME).a $(NAME).cmi) +ALL_NAMES = $(NAME_CORE) # $(NAME_SAT) $(NAME_SMT) $(NAME_MCAT) +TO_INSTALL_LIB=$(addsuffix .a, $(ALL_NAMES)) \ + $(addsuffix .cmi, $(ALL_NAMES)) +TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB)) install: lib - ocamlfind install msat $(TO_INSTALL) + ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL) uninstall: - ocamlfind remove msat + ocamlfind remove $(NAME_OCAMLFIND) reinstall: all - ocamlfind remove msat || true - ocamlfind install msat $(TO_INSTALL) + ocamlfind remove $(NAME_OCAMLFIND) || true + ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL) + +watch: + while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + echo "============ at `date` ==========" ; \ + sleep 0.1; \ + make all; \ + done .PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test diff --git a/_tags b/_tags index c918133e..3714ec07 100644 --- a/_tags +++ b/_tags @@ -9,16 +9,22 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : include : include : include -: include : include -: include +: include +: include +: include # Pack options : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) -: for-pack(Msat) + +# Testing dependencies +: package(dolmen) +: package(dolmen) +: package(dolmen) +: package(dolmen) # more warnings : warn_K, warn_Y, warn_X diff --git a/docs/mcsat-vmcai2013.pdf b/docs/articles/mcsat-vmcai2013.pdf similarity index 100% rename from docs/mcsat-vmcai2013.pdf rename to docs/articles/mcsat-vmcai2013.pdf diff --git a/docs/mcsat_design.pdf b/docs/articles/mcsat_design.pdf similarity index 100% rename from docs/mcsat_design.pdf rename to docs/articles/mcsat_design.pdf diff --git a/docs/minisat.pdf b/docs/articles/minisat.pdf similarity index 100% rename from docs/minisat.pdf rename to docs/articles/minisat.pdf diff --git a/docs/biblio.bib b/docs/biblio.bib new file mode 100644 index 00000000..51f613a2 --- /dev/null +++ b/docs/biblio.bib @@ -0,0 +1,13 @@ +# $Id: fc4f8c6e8645238b51d6c5bc228b9c166291aa46 $ + +@inproceedings{FMCAD13, + author = "Jovanovic, Devan and Barrett, Clark and de Moura, Leonardo", + title = "The Design and Implementation of the Model Constructing Satisfiability Calculus", + year = 2013 +} + +@inproceedings{VMCAI13, + author = "Jovanovic, Devan and de Moura, Leonardo", + title = "A Model-Constructing Satisfiability Calculus", + year = 2013 +} diff --git a/docs/macros.tex b/docs/macros.tex new file mode 100644 index 00000000..a21ad2fb --- /dev/null +++ b/docs/macros.tex @@ -0,0 +1,17 @@ + +\def\ocaml{\textsf{OCaml}} + + +\def\sat{\textsf{Sat}} +\def\smt{\textsf{SMT}} +\def\mcsat{\textsf{McSat}} + +\def\dpll{\textsf{DPLL}} +\def\cdcl{\textsf{CDCL}} + +\def\msat{\textsf{mSAT}} + +\newcommand{\irule}[1]{{\small\textsc{#1}}} + +\EnableBpAbbreviations{} +\newcommand{\LLc}[1]{\LL{\irule{#1}}} diff --git a/docs/msat.pdf b/docs/msat.pdf new file mode 100644 index 00000000..99075567 Binary files /dev/null and b/docs/msat.pdf differ diff --git a/docs/msat.tex b/docs/msat.tex new file mode 100644 index 00000000..0043967c --- /dev/null +++ b/docs/msat.tex @@ -0,0 +1,610 @@ + +\documentclass{article} + +\usepackage[T1]{fontenc} +\usepackage{makeidx} +\usepackage{bussproofs} +\usepackage{amsmath,amssymb} +\usepackage{tabularx} +\usepackage{pgf, tikz} +% \usepackage[margin=4cm]{geometry} + +\usepackage{float} +\floatstyle{boxed} +\restylefloat{figure} + +\usepackage{listings} +\lstset{language=[Objective]caml} + +\input{macros} + +\usetikzlibrary{arrows, automata} + +\begin{document} + +\title{\msat{}: a \sat{}/\smt{}/\mcsat{} library} +\author{Guillaume~Bury} + +\maketitle + +\section{Introduction} + +The goal of the \msat{} library is to provide a way to easily +create automated theorem provers based on a \sat{} solver. More precisely, +the library, written in \ocaml{}, provides functors which, once instantiated, +provide a \sat{}, \smt{} or \mcsat{} solver. + +Given the current state of the art of \smt{} solvers, where most \sat{} solvers +are written in C and heavily optimised\footnote{Some solvers now have instructions +to manage a processor's cache}, the \msat{} library does not aim to provide solvers +competitive with the existing implementations, but rather an easy way to create +reasonably efficient solvers. + +\msat{} currently uses the following techniques: +\begin{itemize} + \item 2-watch literals scheme + \item Activity based decisions + \item Restarts +\end{itemize} + +Additionally, \msat{} has the following features: +\begin{itemize} + \item Local assumptions + \item Proof/Model output + \item Adding clauses during proof search +\end{itemize} + +\clearpage + +\tableofcontents{} + +\clearpage + +\section{\sat{} Solvers: principles and formalization}\label{sec:sat} + +\subsection{Idea} + +\subsection{Inference rules}\label{sec:trail} + +The SAT algorithm can be formalized as follows. During the search, the solver keeps +a set of clauses, containing the problem hypotheses and the learnt clauses, and +a trail, which is the current ordered list of assumptions and/or decisions made by +the solver. + +Each element in the trail (decision or propagation) has a level, which is the number of decision +appearing in the trail up to (and including) it. So for instance, propagations made before any +decisions have level $0$, and the first decision has level $1$. Propagations are written +$a \leadsto_C \top$, with $C$ the clause that caused the propagation, and decisions +$a \mapsto_n \top$, with $n$ the level of the decision. Trails are read +chronologically from left to right. + +In the following, given a trail $t$ and an atomic formula $a$, we will use the following notation: +$a \in t$ if $a \mapsto_n \top$ or $a \leadsto_C \top$ is in $t$, i.e.~$a \in t$ is $a$ is true +in the trail $t$. In this context, the negation $\neg$ is supposed to be involutive +(i.e.~$\neg \neg a = a$), so that, if $a \in t$ then $\neg \neg a = a \in t$. + +There exists two main \sat{} algorithms: \dpll{} and \cdcl{}. In both, there exists +two states: first, the starting state $\text{Solve}$, where propagations +and decisions are made, until a conflict is detected, at which point the algorithm +enters in the $\text{Analyse}$ state, where it analyzes the conflict, backtracks, +and re-enter the $\text{Solve}$ state. The difference between \dpll{} and \cdcl{} +is the treatment of conflicts during the $\text{Analyze}$ phase: \dpll{} will use +the conflict only to known where to backtrack/backjump, while in \cdcl{} the result +of the conflict analysis will be added to the set of hypotheses, so that the same +conflict does not occur again. +The $\text{Solve}$ state take as argument the set of hypotheses and the trail, while +the $\text{Analyze}$ state also take as argument the current conflict clause. + +We can now formalize the \cdcl{} algorithm using the inference rules +in Figure~\ref{fig:smt_rules}. In order to completely recover the \sat{} algorithm, +one must apply the rules with the following precedence and termination conditions, +depending on the current state: +\begin{itemize} + \item If the empty clause is in $\mathbb{S}$, then the problem is unsat. + If there is no more rule to apply, the problem is sat. + \item If we are in $\text{Solve}$ mode: + \begin{enumerate} + \item First is the rule \irule{Conflict}; + \item Then the try and use \irule{Propagate}; + \item Finally, is there is nothing left to be propagated, the \irule{Decide} + rule is used. + \end{enumerate} + \item If we are in $\text{Analyze}$ mode, we have a choice concerning + the order of application. First we can observe that the rules + \irule{Analyze-Propagate}, \irule{Analyze-Decision} and \irule{Analyze-Resolution} + can not apply simultaneously, and we will thus group them in a super-rule + \irule{Analyze}. We now have the choice of when to apply the \irule{Backjump} rule + compared to the \irule{Analyze} rule: + using \irule{Backjump} eagerly will result in the first UIP strategy, while delaying it + until later will yield other strategies, both of which are valid. +\end{itemize} + +\begin{figure} + \center{\underline{\sat{}}} + \begin{center} + \begin{tabular}{c@{\hspace{1cm}}l} + % Propagation (boolean) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Propagate} + \UIC{$\text{Sove}(\mathbb{S}, t :: a \leadsto_C \top)$} + \DP{} & + \begin{tabular}{l} + $a \in C, C \in \mathbb{S}, \neg a \notin t$ \\ + $\forall b \in C. b \neq a \rightarrow \neg b \in t$ \\ + \end{tabular} + \\ \\ + % Decide (boolean) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Decide} + \UIC{$\text{Solve}(\mathbb{S}, t :: a \mapsto_n \top)$} + \DP{} & + \begin{tabular}{l} + $a \notin t, \neg a \notin t, a \in \mathbb{S}$ \\ + $n = \text{max\_level}(t) + 1$ \\ + \end{tabular} + \\ \\ + % Conflict (boolean) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Conflict} + \UIC{$\text{Analyze}(\mathbb{S}, t, C)$} + \DP{} & + $C \in \mathbb{S}, \forall a \in C. \neg a \in t$ + \\ \\ + \end{tabular} + \end{center} + \begin{center} + \begin{tabular}{c@{\hspace{.5cm}}l} + % Analyze (propagation) + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \leadsto_C \top, D)$} + \LLc{Analyze-propagation} + \UIC{$\text{Analyze}(\mathbb{S}, t, D)$} + \DP{} & + $\neg a \notin D$ + \\ \\ + % Analyze (decision) + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \mapsto_n \top, D)$} + \LLc{Analyze-decision} + \UIC{$\text{Analyze}(\mathbb{S}, t, D)$} + \DP{} & + $\neg a \notin D$ + \\ \\ + % Resolution + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \leadsto_C \top, D)$} + \LLc{Analyze-Resolution} + \UIC{$\text{Analyze}(\mathbb{S}, t, (C - \{a\}) \cup (D - \{ \neg a\}))$} + \DP{} & + $\neg a \in D$ + \\ \\ + \end{tabular} + \end{center} + \begin{center} + \begin{tabular}{c@{\hspace{1cm}}l} + % BackJump + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \mapsto_d \top :: t', C)$} + \LLc{Backjump} + \UIC{$\text{Solve}(\mathbb{S} \cup \{ C \}, t)$} + \DP{} & + \begin{tabular}{l} + $\text{is\_uip}(C)$ \\ + $d \leq \text{uip\_level}(C)$ \\ + \end{tabular} + \\ \\ + \end{tabular} + \end{center} + + \center{\underline{\smt{}}} + \begin{center} + \begin{tabular}{c@{\hspace{1cm}}l} + % Conflict (theory) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Conflict-Smt} + \UIC{$\text{Analyze}(\mathbb{S}, t, C)$} + \DP{} & + \begin{tabular}{l} + $\mathcal{T} \vdash C$ \\ + $\forall a \in C. \neg a \in t$ \\ + \end{tabular} + \\ \\ + \end{tabular} + \end{center} + \caption{Inference rules for \sat{} and \smt{}}\label{fig:smt_rules} +\end{figure} + +\begin{figure} + \center{\underline{\mcsat{}}} + \begin{center} + \begin{tabular}{c@{\hspace{.2cm}}l} + % Decide (assignment) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Theory-Decide} + \UIC{$\text{Solve}(\mathbb{S}, t :: a \mapsto_n v)$} + \DP{} & + \begin{tabular}{l} + $a \mapsto_k \_ \notin t$ \\ + $n = \text{max\_level}(t) + 1$ \\ + $\sigma_{t :: a \mapsto_n v} \text{ compatible with } t$ + \end{tabular} + \\ \\ + % Propagation (semantic) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Propagate-Theory} + \UIC{$\text{Solve}(\mathbb{S}, t :: a \leadsto_n \top)$} + \DP{} & + $\sigma_t(a) = \top$ + \\ \\ + % Conflict (semantic) + \AXC{$\text{Solve}(\mathbb{S}, t)$} + \LLc{Conflict-Mcsat} + \UIC{$\text{Analyze}(\mathbb{S}, t, C)$} + \DP{} & + \begin{tabular}{l} + $\mathcal{T} \vdash C$ \\ + $\forall a \in C, \neg a \in t \lor \sigma_t(a) = \bot$ + \end{tabular} + \\ \\ + \end{tabular} + \end{center} + \begin{center} + \begin{tabular}{c@{\hspace{.2cm}}l} + % Analyze (assign) + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \mapsto_n v, C)$} + \LLc{Analyze-Assign} + \UIC{$\text{Analyze}(\mathbb{S}, t, C)$} + \DP{} & + \\ \\ + % Analyze (semantic) + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \leadsto_n \top, C)$} + \LLc{Analyze-Semantic} + \UIC{$\text{Analyze}(\mathbb{S}, t, C)$} + \DP{} & + \\ \\ + \end{tabular} + \end{center} + \begin{center} + \begin{tabular}{c@{\hspace{.2cm}}l} + % Backjump (semantic) + \AXC{$\text{Analyze}(\mathbb{S}, t :: a \mapsto_n \_ :: \_, C)$} + \LLc{Backjump-Semantic} + \UIC{$\text{Solve}(\mathbb{S}, t)$} + \DP{} & + \begin{tabular}{l} + $\text{is\_semantic}(C)$ \\ + $n = \text{slevel}(C)$ \\ + \end{tabular} + \\ \\ + \end{tabular} + \end{center} + \caption{\mcsat{} specific inference rules}\label{fig:mcsat_rules} +\end{figure} + +\subsection{Invariants, correctness and completeness} + +The following invariants are maintained by the inference rules in Figure~\ref{fig:smt_rules}: +\begin{description} + \item[Trail Soundness] In $\text{Solve}(\mathbb{S}, t)$, if $a \in t$ then $\neg a \notin t$ + \item[Conflict Analysis] In $\text{Analyze}(\mathbb{S}, t, C)$, $C$ is a clause implied by the + clauses in $\mathbb{S}$, and $\forall a \in C. \neg a \in t$ (i.e.~$C$ is entailed by the + hypotheses, yet false in the partial model formed by the trail $t$). + \item[Equivalence] In any rule \AXC{$s_1$}\UIC{$s_2$}\DP{}, the set of hypotheses + (usually written $\mathbb{S}$) in $s_1$ is equivalent to that of $s_2$. +\end{description} + +These invariants are relatively easy to prove, and provide an easy proof of correctness for +the \cdcl{} algorithm. Termination can be proved by observing that the same trail appears +at most twice during proof search (once during propagation, and eventually a second time +right after backjumping\footnote{This could be avoided by making the \irule{Backjump} rule +directly propagate the relevant literal of the conflict clause, but it needlessly +complicates the rule.}). Correctness and termination implies completeness of the \sat{} +algorithm. + + +\section{\smt{} solver architecture}\label{sec:smt} + +\subsection{Idea}\label{sec:smt_flow} + +In a \smt{} solver, after each propagation and decision, the solver sends the newly +assigned literals to the theory. The theory then has the possibility to declare the +current set of literals incoherent, and give the solver a tautology in which all +literals are currently assigned to $\bot$\footnote{or rather for each literal, its negation +is assigned to $\top$}, thus prompting the solver to backtrack. +We can represent a simplified version of the information flow (not taking into +account backtracking) of usual \smt{} Solvers, using the graph in fig~\ref{fig:smt_flow}. + +Contrary to what the Figure~\ref{fig:smt_flow} could suggest, it is not impossible +for the theory to propagate information back to the \sat{} solver. Indeed, +some \smt{} solvers already allow the theory to propagate entailed literals back to the +\sat{} solver. However, these propagations are in practice limited by the complexity +of deciding entailment. Moreover, procedures in a \smt{} solver should be incremental +in order to get decent performances, and deciding entailment in an incremental manner +is not easy (TODO~: ref nécessaire). Doing efficient, incremental entailment is exactly +what \mcsat{} allows (see Section~\ref{sec:mcsat}). + +\subsection{Formalization and Theory requirements} + +An \smt{} solver is the combination of a \sat{} solver, and a theory $\mathcal{T}$. +The role of the theory $\mathcal{T}$ is to stop the proof search as soon as the trail +of the \sat{} solver is inconsistent. A trail is inconsistent iff there exists a clause +$C$, which is a tautology of $\mathcal{T}$ (thus $\mathcal{T} \vdash C$), but is not +satisfied in the current trail (each of its literals has either been decided or +propagated to false). Thus, we can add the \irule{Conflict-Smt} rule (see +Figure~\ref{fig:smt_rules}) to the \cdcl{} inference rules in order to get a \smt{} solver. +We give the \irule{Conflict-Smt} rule a slightly lower precedence than the +\irule{Conflict} rule for performance reason (detecting boolean conflict is +faster than theory specific conflicts). + +So, what is the minimum that a theory must implement in practice to be used in a +\smt{} solver~? The theory has to ensure that the current trail is consistent +(when seen as a conjunction of literals), that is to say, given a trail $t$, +it must ensure that there exists a model $\mathcal{M}$ of $\mathcal{T} $so that +$\forall a \in t. \mathcal{M} \vDash a$, or if it is impossible (i.e.~the trail +is inconsistent) produce a conflict. + +\begin{figure} + \begin{center} + \begin{tikzpicture}[ + ->, % Arrow style + > = stealth, % arrow head style + shorten > = 1pt, % don't touch arrow head to node + node distance = 2cm, % distance between nodes + semithick, % line style + auto + ] + + \tikzstyle{state}=[rectangle,draw=black!75] + + \node (sat) {SAT Core}; + \node (th) [right of=sat, node distance=6cm] {Theory}; + \node[state] (d) [below of=sat, node distance=1cm] {Decision (boolean)}; + \node[state] (bp) [below of=d, node distance=2cm] {Boolean propagation}; + \node[state] (tp) [right of=bp, node distance=6cm] {Theory propagation}; + + \draw (d) edge [bend left=30] (bp); + \draw (bp) edge [bend left=30] (d); + \draw (bp) edge (tp); + + \draw[black!50] (-2,1) rectangle (2,-4); + \draw[black!50] (4,1) rectangle (8,-4); + + \end{tikzpicture} + \end{center} + \caption{Simplified \smt{} Solver architecture}\label{fig:smt_flow} +\end{figure} + +\section{\mcsat{}: An extension of \smt{} Solvers}\label{sec:mcsat} + +\subsection{Motivation and idea} + +\mcsat{} is an extension of usual \smt{} solvers, introduced in~\cite{VMCAI13} and~\cite{FMCAD13}. +In usual \smt{} Solvers, interaction between the core SAT Solver and the Theory is pretty limited~: +the SAT Solver make boolean decisions and propagations, and sends them to the theory, +whose role is in return to stop the SAT Solver as soon as the current set of assumptions +is incoherent. This means that the information that theories can give the SAT Solver is +pretty limited, and furthermore it heavily restricts the ability of theories to guide +the proof search (see Section~\ref{sec:smt_flow}). + +While it appears to leave a reasonably simple job to the theory, since it completely +hides the propositional structure of the problem, this simple interaction between the +SAT Solver and the theory makes it harder to combine multiple theories into one. Usual +techniques for combining theories in \smt{} solvers typically require to keep track of +equivalence classes (with respect to the congruence closure) and for instance +in the Nelson-Oppen method for combining theories (TODO~: ref nécessaire) require of +theories to propagate any equality implied by the current assertions. + +\mcsat{} extends the SAT paradigm by allowing more exchange of information between the theory +and the SAT Solver. This is achieved by allowing the solver to not only decide on the truth value +of atomic propositions, but also to decide assignments for terms that appear in the problem. +For instance, if the SAT Solver assigns a variable $x$ to $0$, +an arithmetic theory could propagate to the SAT Solver that the formula $x < 1$ must also hold, +instead of waiting for the SAT Solver to guess the truth value of $x < 1$ and then +inform the SAT Solver that the conjunction~: $x = 0 \land \neg x < 1$ is incoherent. + +This exchange of information between the SAT Solver and the theories results in +the construction of a model throughout the proof search (which explains the name +Model Constructing SAT). + +The main addition of \mcsat{} is that when the solver makes a decision, instead of +being restricted to making boolean assignment of formulas, the solver now can +decide to assign a value to a term belonging to one of the literals. In order to do so, +the solver first chooses a term that has not yet been assigned, and then asks +the theory for a possible assignment. Like in usual SMT Solvers, a \mcsat{} solver +only exchange information with one theory, but, as we will see, combination +of theories into one becomes easier in this framework, because assignments are +actually a very good way to exchange information. + +Using the assignments on terms, the theory can then very easily do efficient +propagation of formulas implied by the current assignments: it is enough to +evaluate formulas using the current partial assignment. +The information flow then looks like fig~\ref{fig:mcsat_flow}. + +\begin{figure} + \begin{center} + \begin{tikzpicture}[ + ->, % Arrow style + > = stealth, % arrow head style + shorten > = 1pt, % don't touch arrow head to node + node distance = 2cm, % distance between nodes + semithick, % line style + auto + ] + + \tikzstyle{state}=[rectangle,draw=black!75] + + \node (sat) {SAT Core}; + \node (th) [right of=sat, node distance=6cm] {Theory}; + \node[state] (d) [below of=sat, node distance=1cm] {Decision}; + \node[state] (ass) [right of=d, node distance=6cm] {Assignment}; + \node[state] (bp) [below of=d, node distance=2cm] {Boolean propagation}; + \node[state] (tp) [right of=bp, node distance=6cm] {Theory propagation}; + + \draw (bp)[right] edge [bend left=5] (tp); + \draw (tp) edge [bend left=5] (bp); + \draw (bp) edge [bend left=30] (d); + \draw (ass) edge [bend left=5] (d); + \draw (d) edge [bend left=5] (ass); + \draw (d) edge [bend left=30] (bp); + \draw[<->] (ass) edge (tp); + + \draw[black!50] (-2,1) rectangle (2,-4); + \draw[black!50] (4,1) rectangle (8,-4); + + \end{tikzpicture} + \end{center} + \caption{Simplified \mcsat{} Solver architecture}\label{fig:mcsat_flow} +\end{figure} + +\subsection{Decisions and propagations} + +In \mcsat{}, semantic propagations are a bit different from the propagations +used in traditional \smt{} Solvers. In the case of \mcsat{} (or at least the version presented here), +semantic propagations strictly correspond to the evaluation of formulas in the +current assignment. Moreover, in order to be able to correctly handle these semantic +propagations during backtrack, they are assigned a level: each decision is given a level +(using the same process as in a \sat{} solvers: a decision level is the number of decision +previous to it, plus one), and a formula is propagated at the maximum level of the decisions +used to evaluate it. + +We can thus extend the notations introduced in Section~\ref{sec:trail}: $t \mapsto_n v$ is +a semantic decision which assign $t$ to a concrete value $v$, $a \leadsto_n \top$ is a +semantic propagation at level $n$. + +For instance, if the current trail is $\{x \mapsto_1 0, x + y + z = 0 \mapsto_2 \top, y\mapsto_3 0\}$, +then $x + y = 0$ can be propagated at level $3$, but $z = 0$ can not be propagated, because +$z$ is not assigned yet, even if there is only one remaining valid value for $z$. +The problem with assignments as propagations is that it is not clear what to do with +them during the $\text{Analyze}$ phase of the solver, see later. + +\subsection{First order terms \& Models} + +A model traditionally is a triplet which comprises a domain, a signature and an interpretation +function. Since most problems define their signature using type definitions at the beginning, and +built-in theories such as arithmetic usually have canonic domain and signature, +we will consider in the following that the domain $\mathbb{D}$ and signature are given (and constant). +Additionally, we consider a fixed interpretation of the theory-defined symbols (which +usually does along with the domain). + +In the following, we use the following notations: +\begin{itemize} + \item $\mathbb{V}$ is an infinite set of variables; + \item $\mathbb{C}$ is the possibly infinite set of constants defined + by the input problem's theories\footnote{For instance, the theory of arithmetic + defines the usual operators $+, -, *, /$ as well as $0, -5, \frac{1}{2}, -2.3, \ldots$}; + \item $\mathbb{S}$ is the finite set of constants defined by the input problem's type + definitions; + \item $\mathbb{T}$ is the (infinite) set of first-order terms over $\mathbb{V}$, $\mathbb{C}$ + and $\mathbb{S}$ (for instance $a, f(0), x + y, \ldots$); + \item $\mathbb{F}$ is the (infinite) set of first order quantified formulas + over the terms in $\mathbb{T}$. +\end{itemize} + +We are therefore interested in finding an interpretation of a problem, and more +specifically an interpretation of the symbols in $\mathbb{S}$ not defined by +the theory, i.e.~non-interpreted functions. An interpretation +$\mathcal{I}$ can easily be extended to a function from ground terms and formulas +to model value by recursively applying it: +\[ + \mathcal{I}( f ( e_1, \ldots, e_n ) ) = + \mathcal{I}_f ( \mathcal{I}(e_1), \ldots, \mathcal{I}(e_n) ) +\] + +\paragraph{Partial Interpretation} +The goal of \mcsat{} is to construct a first-order model of the input formulas. To do so, +it has to build what we will call partial interpretations: intuitively, a partial +interpretation is a partial function from the constants symbols to the model values. +It is, however, not so simple: during proof search, the \mcsat{} algorithm maintains +a partial mapping from expressions to model values (and not from constant symbols +to model values). The intention of this mapping is to represent a set of constraints +on the partial interpretation that the algorithm is building. +For instance, given a function symbol $f$ of type $(\text{int} \rightarrow \text{int})$ and an +integer constant $a$, one such constraint that we would like to be able to express in +our mapping is the following: $f(a) \mapsto 0$, regardless of the values that $f$ takes on +other argument, and also regardless of the value mapped to $a$. To that end we introduce +the notion of abstract partial interpretation. + +An abstract partial interpretation $\sigma$ is a mapping from ground expressions to model values. +To each abstract partial interpretation correspond a set of complete models that realize it. +More precisely, any mapping $\sigma$ can be completed in various ways, leading to a set of +potential interpretations: +\[ + \text{Complete}(\sigma) = + \left\{ + \mathcal{I} + \; | \; + \forall t \mapsto v \in \sigma , \mathcal{I} ( t ) = v + \right\} +\] + +\paragraph{Coherence} +An abstract partial interpretation $\sigma$ is said to be coherent iff +there exists at least one model that completes it, +i.e.~$\text{Complete}(\sigma) \neq \emptyset$. One example +of incoherent abstract partial interpretation is the following +mapping: +\[ + \sigma = \left\{ + \begin{matrix} + a \mapsto 0 \\ + b \mapsto 0 \\ + f(a) \mapsto 0 \\ + f(b) \mapsto 1 \\ + \end{matrix} + \right. +\] + +\paragraph{Compatibility} +In order to do semantic propagations, we want to have some kind of notion +of evaluation for abstract partial interpretations, and we thus define the +partial interpretation function in the following way: +\[ + \forall t \in \mathbb{T} \cup \mathbb{F}. \forall v \in \mathbb{D}. + \left( + \forall \mathcal{I} \in \text{Complete}(\sigma). + \mathcal{I}(t) = v + \right) \rightarrow + \sigma(t) = v +\] + +The partial interpretation function is the intersection of the interpretation +functions of all the completions of $\sigma$, i.e.~it is the interpretation +where all completions agree. We can now say that a mapping $\sigma$ is compatible +with a trail $t$ iff $\sigma$ is coherent, and +$\forall a \in t. \not (\sigma(a) = \bot)$, or in other words, for every literal $a$ +true in the trail, there exists at least one model that completes $\sigma$ and where +$a$ is satisfied. + +\paragraph{Completeness} +We need one last property on abstract partial interpretations, which is to +specify the relation between the terms in a mapping, and the terms it can evaluate, +according to its partial interpretation function defined above. Indeed, at the end +of proof search, we want all terms (and sub-terms) of the initial problem to be +evaluated using the final mapping returned by the algorithm when it finds that the +problem is satisfiable: that is what we will call completeness of a mapping. +To that end we will here enumerate some sufficient conditions on the mapping domain +$\text{Dom}(\sigma)$ compared to the finite set of terms (and sub-terms) $T$ that +appear in the problem. + +A first way, is to have $\text{Dom}(\sigma) = T$, i.e.~all terms (and sub-terms) of the +initial problem are present in the mapping. While this is the simplest way to ensure that +the mapping is complete, it might be a bit heavy: for instance, we might have to assign +both $x$ and $2x$, which is redundant. The problem in that case is that we try and assign +a term for which we could actually compute the value from its arguments: indeed, +since the multiplication is interpreted, we do not need to interpret it in our mapping. +This leads to another way to have a complete mapping: if $\text{Dom}(\sigma)$ is the +set of terms of $T$ whose head symbol is uninterpreted (i.e.~not defined by the theory), +it is enough to ensure that the mapping is complete, because the theory will automatically +constrain the value of terms whose head symbol is interpreted. + +\subsection{Inference rules} + +In \mcsat{}, a trail $t$ contains boolean decision and propagations as well as semantic +decisions (assignments) and propagations. We can thus define $\sigma_t$ as the mapping +formed by all assignments in $t$. This lets us define the last rules in Figure~\ref{fig:mcsat_rules}, +that, together with the other rules, define the \mcsat{} algorithm. + + +\bibliographystyle{plain} +\bibliography{biblio} + +\clearpage +\appendix + +\end{document} diff --git a/src/core/expr_intf.ml b/src/core/expr_intf.ml index a718e935..84fe946f 100644 --- a/src/core/expr_intf.ml +++ b/src/core/expr_intf.ml @@ -11,39 +11,44 @@ type negated = Formula_intf.negated = module type S = sig (** Signature of formulas that parametrises the Mcsat Solver Module. *) - module Term : sig - (** The type of terms *) - type t - val hash : t -> int - val equal : t -> t -> bool - val print : Format.formatter -> t -> unit - end - - module Formula : sig - (** The type of atomic formulas over terms. *) - type t - val hash : t -> int - val equal : t -> t -> bool - val print : Format.formatter -> t -> unit - end - type proof (** An abstract type for proofs *) - val dummy : Formula.t - (** Formula constants. A valid formula should never be physically equal to [dummy] *) + module Term : sig - val fresh : unit -> Formula.t - (** Returns a fresh litteral, distinct from any other literal (used in cnf conversion) *) + type t + (** The type of terms *) - val neg : Formula.t -> Formula.t - (** Formula negation *) + val hash : t -> int + val equal : t -> t -> bool + val print : Format.formatter -> t -> unit + (** Common functions *) + + end + + module Formula : sig + + type t + (** The type of atomic formulas over terms. *) + + val hash : t -> int + val equal : t -> t -> bool + val print : Format.formatter -> t -> unit + (** Common functions *) + + val dummy : t + (** Formula constants. A valid formula should never be physically equal to [dummy] *) + + val neg : t -> t + (** Formula negation *) + + val norm : t -> t * negated + (** Returns a 'normalized' form of the formula, possibly negated + (in which case return [Negated]). + [norm] must be so that [a] and [neg a] normalise to the same formula, + but one returns [Negated] and the other [Same_sign]. *) + end - val norm : Formula.t -> Formula.t * negated - (** Returns a 'normalized' form of the formula, possibly negated - (in which case return [Negated]). - [norm] must be so that [a] and [neg a] normalise to the same formula, - but one returns [Negated] and the other [Same_sign]. *) end diff --git a/src/core/formula_intf.ml b/src/core/formula_intf.ml index 360fde32..366b2f46 100644 --- a/src/core/formula_intf.ml +++ b/src/core/formula_intf.ml @@ -17,12 +17,14 @@ module type S = sig type proof (** An abstract type for proofs *) + val hash : t -> int + val equal : t -> t -> bool + val print : Format.formatter -> t -> unit + (** Common functions *) + val dummy : t (** Formula constants. A valid formula should never be physically equal to [dummy] *) - val fresh : unit -> t - (** Returns a fresh literal, distinct from any other literal (used in cnf conversion) *) - val neg : t -> t (** Formula negation *) @@ -32,11 +34,5 @@ module type S = sig [norm] must be so that [a] and [neg a] normalise to the same formula, but one returns [Same_sign] and one returns [Negated] *) - val hash : t -> int - val equal : t -> t -> bool - (** Usual hash and comparison functions. Given to Hashtbl functors. *) - - val print : Format.formatter -> t -> unit - (** Printing function used for debugging. *) end diff --git a/src/core/internal.ml b/src/core/internal.ml index ac6acb47..44ad3744 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -221,7 +221,8 @@ module Make its subterms. *) let rec insert_var_order = function - | E_lit l -> Iheap.insert f_weight env.order l.lid + | E_lit l -> + Iheap.insert f_weight env.order l.lid | E_var v -> Iheap.insert f_weight env.order v.vid; iter_sub (fun t -> insert_var_order (elt_of_lit t)) v @@ -362,7 +363,6 @@ module Make let attach_clause c = assert (not c.attached); Log.debugf 60 "Attaching %a" (fun k -> k St.pp_clause c); - Array.iter (fun x -> insert_var_order (elt_of_var x.var)) c.atoms; Vec.push c.atoms.(0).neg.watched c; Vec.push c.atoms.(1).neg.watched c; c.attached <- true; @@ -464,6 +464,8 @@ module Make (* Boolean propagation. Wrapper function for adding a new propagated formula. *) let enqueue_bool a ~level:lvl reason : unit = + Log.debugf 99 "Trying to enqueue: @[%a@\n%a@]" + (fun k -> k St.pp_atom a St.pp_reason (lvl, Some reason)); if a.neg.is_true then begin Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a); assert false @@ -493,7 +495,8 @@ module Make l.assigned <- Some value; l.l_level <- lvl; Vec.push env.elt_queue (of_lit l); - () + Log.debugf 20 "Enqueue (%d): %a" + (fun k -> k (Vec.size env.elt_queue) pp_lit l) (* evaluate an atom for MCsat, if it's not assigned by boolean propagation/decision *) @@ -764,6 +767,7 @@ module Make else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history)) in Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause); + Array.iter (fun x -> insert_var_order (elt_of_var x.var)) clause.atoms; Vec.push vec clause; match atoms with | [] -> @@ -862,13 +866,18 @@ module Make end done; (* no watch lit found *) - if first.neg.is_true || (th_eval first = Some false) then begin + if first.neg.is_true then begin (* clause is false *) env.elt_head <- Vec.size env.elt_queue; raise (Conflict c) end else begin - (* clause is unit, keep the same watches, but propagate *) - enqueue_bool first (decision_level ()) (Bcp c) + match th_eval first with + | None -> (* clause is unit, keep the same watches, but propagate *) + enqueue_bool first (decision_level ()) (Bcp c) + | Some true -> () + | Some false -> + env.elt_head <- Vec.size env.elt_queue; + raise (Conflict c) end; Watch_kept with Exit -> diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index fbc3ec87..4ec1f9a8 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -81,7 +81,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct | E_var of var (* Dummy values *) - let dummy_lit = E.dummy + let dummy_lit = E.Formula.dummy let rec dummy_var = { vid = -101; @@ -145,7 +145,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let make_boolean_var : formula -> var * Expr_intf.negated = fun t -> - let lit, negated = E.norm t in + let lit, negated = E.Formula.norm t in try MF.find f_map lit, negated with Not_found -> @@ -169,7 +169,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct aid = cpt_fois_2 (* aid = vid*2 *) } and na = { var = var; - lit = E.neg lit; + lit = E.Formula.neg lit; watched = Vec.make 10 dummy_clause; neg = pa; is_true = false; @@ -263,18 +263,28 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct (* Complete debug printing *) let sign a = if a == a.var.pa then "+" else "-" - let level a = - match a.var.v_level, a.var.reason with - | n, _ when n < 0 -> sprintf "%%" - | n, None -> sprintf "%d" n - | n, Some Decision -> sprintf "@@%d" n - | n, Some Bcp c -> sprintf "->%d/%s" n c.name - | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl + let pp_reason fmt = function + | n, _ when n < 0 -> + Format.fprintf fmt "%%" + | n, None -> + Format.fprintf fmt "%d" n + | n, Some Decision -> + Format.fprintf fmt "@@%d" n + | n, Some Bcp c -> + Format.fprintf fmt "->%d/%s" n c.name + | n, Some Semantic lvl -> + Format.fprintf fmt "::%d/%d" n lvl - let value a = - if a.is_true then sprintf "[T%s]" (level a) - else if a.neg.is_true then sprintf "[F%s]" (level a) - else "[]" + let pp_level fmt a = + pp_reason fmt (a.var.v_level, a.var.reason) + + let pp_value fmt a = + if a.is_true then + Format.fprintf fmt "[T%a]" pp_level a + else if a.neg.is_true then + Format.fprintf fmt "[F%a]" pp_level a + else + Format.fprintf fmt "[]" let pp_premise out = function | Hyp -> Format.fprintf out "hyp" @@ -284,15 +294,15 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct let pp_assign out = function | None -> () - | Some t -> Format.fprintf out " ->@ %a" E.Term.print t + | Some t -> Format.fprintf out " ->@ @[%a@]" E.Term.print t let pp_lit out v = - Format.fprintf out "%d [lit:%a%a]" + Format.fprintf out "%d [lit:@[%a%a@]]" (v.lid+1) E.Term.print v.term pp_assign v.assigned let pp_atom out a = - Format.fprintf out "%s%d%s[atom:%a]@ " - (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit + Format.fprintf out "%s%d%a[atom:@[%a@]]@ " + (sign a) (a.var.vid+1) pp_value a E.Formula.print a.lit let pp_atoms_vec out vec = Array.iter (fun a -> pp_atom out a) vec diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 6b1dcdcf..2d790533 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -144,6 +144,7 @@ module type S = sig val pp_atom : Format.formatter -> atom -> unit val pp_clause : Format.formatter -> clause -> unit val pp_dimacs : Format.formatter -> clause -> unit + val pp_reason : Format.formatter -> (int * reason option) -> unit (** Debug function for atoms and clauses (very verbose) *) end diff --git a/src/example/cc.ml b/src/example/cc.ml deleted file mode 100644 index cbfa7d97..00000000 --- a/src/example/cc.ml +++ /dev/null @@ -1,99 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Make(T : Sig.OrderedType) = struct - - module M = Map.Make(T) - module U = Unionfind.Make(T) - - exception Unsat of (T.t * T.t * (T.t list)) - - type t = { - repr : U.t; - expl : T.t M.t; - size : int M.t; - } - - let empty = { - repr = U.empty; - expl = M.empty; - size = M.empty; - } - - let repr t a = U.find t.repr a - - let map_find m v default = try M.find v m with Not_found -> default - let find_parent v m = map_find m v v - - let rev_root m root = - let rec aux m curr next = - if T.compare curr next = 0 then - m, curr - else - let parent = find_parent next m in - let m' = M.add next curr (M.remove curr m) in - aux m' next parent - in - aux m root (find_parent root m) - - let rec root m acc curr = - let parent = find_parent curr m in - if T.compare curr parent = 0 then - curr :: acc - else - root m (curr :: acc) parent - - let expl t a b = - let rec aux last = function - | x :: r, y :: r' when T.compare x y = 0 -> - aux (Some x) (r, r') - | l, l' -> begin match last with - | Some z -> List.rev_append (z :: l) l' - | None -> List.rev_append l l' - end - in - aux None (root t.expl [] a, root t.expl [] b) - - let add_eq_aux t i j = - if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then - t - else - let m, old_root_i = rev_root t.expl i in - let m, old_root_j = rev_root m j in - let nb_i = map_find t.size old_root_i 0 in - let nb_j = map_find t.size old_root_j 0 in - if nb_i < nb_j then { - repr = t.repr; - expl = M.add i j m; - size = M.add j (nb_i + nb_j + 1) t.size; } - else { - repr = t.repr; - expl = M.add j i m; - size = M.add i (nb_i + nb_j + 1) t.size; } - - let add_eq t i j = - let t' = add_eq_aux t i j in - try - let u' = U.union t.repr i j in - { t' with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t' a b)) - - let add_neq t i j = - try - let u' = U.forbid t.repr i j in - { t with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t a b)) - - let are_neq t a b = - try - ignore (U.union t.repr a b); - false - with U.Unsat _ -> - true - -end diff --git a/src/example/cc.mli b/src/example/cc.mli deleted file mode 100644 index 005264d8..00000000 --- a/src/example/cc.mli +++ /dev/null @@ -1,18 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Make(T : Sig.OrderedType) : sig - type t - - exception Unsat of (T.t * T.t * (T.t list)) - - val empty : t - val add_eq : t -> T.t -> T.t -> t - val add_neq : t -> T.t -> T.t -> t - - val repr : t -> T.t -> T.t - val are_neq : t -> T.t -> T.t -> bool -end diff --git a/src/example/expr.ml b/src/example/expr.ml deleted file mode 100644 index 72eef2e1..00000000 --- a/src/example/expr.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module I = Formula_intf - -exception Invalid_var - -type var = string -type formula = - | Prop of int - | Equal of var * var - | Distinct of var * var -type t = formula -type proof = unit - -let dummy = Prop 0 - -let max_fresh = ref 0 -let fresh () = - incr max_fresh; - Prop (2 * !max_fresh + 1) - -let mk_prop i = - if i <> 0 && i < max_int / 2 then Prop (2 * i) - else raise Invalid_var - -let mk_var i = - if i <> "" then i - else raise Invalid_var - -let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) -let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) - -let neg = function - | Prop i -> Prop (-i) - | Equal (a, b) -> Distinct (a, b) - | Distinct (a, b) -> Equal (a, b) - -let norm = function - | Prop i -> Prop (abs i), if i < 0 then I.Negated else I.Same_sign - | Equal (a, b) -> Equal (a, b), I.Same_sign - | Distinct (a, b) -> Equal (a, b), I.Negated - -(* Only used after normalisation, so usual functions should work *) -let hash = Hashtbl.hash -let equal = (=) -let compare = Pervasives.compare - -let print fmt = function - | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) - | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b - | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b - -module Term = struct - type t = var - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare - let print fmt t = Format.fprintf fmt "%s" t -end - -module Formula = struct - type t = formula - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare - let print = print -end - diff --git a/src/example/expr.mli b/src/example/expr.mli deleted file mode 100644 index 8a9f7591..00000000 --- a/src/example/expr.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -type var = string -type formula = private - | Prop of int - | Equal of var * var - | Distinct of var * var - -type t = formula -type proof = unit - -include Formula_intf.S with type t := formula and type proof := proof - -val dummy : t - -val fresh : unit -> t - -val mk_prop : int -> t -val mk_eq : var -> var -> t -val mk_neq : var -> var -> t - -module Term : sig - type t = var - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end -module Formula : sig - type t = formula - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end diff --git a/src/example/mcsat.ml b/src/example/mcsat.ml deleted file mode 100644 index d5c42683..00000000 --- a/src/example/mcsat.ml +++ /dev/null @@ -1,115 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Fsmt = Expr - -module Tsmt = struct - - module M = Map.Make(Fsmt.Term) - module CC = Cc.Make(String) - - (* Type definitions *) - type term = Fsmt.Term.t - type formula = Fsmt.t - type proof = unit - - type level = { - cc : CC.t; - assign : (term * int) M.t; - } - - (* Functions *) - let dummy = { cc = CC.empty; assign = M.empty; } - - let env = ref dummy - - let current_level () = !env - - let to_clause (a, b, l) = - Log.debugf 10 "@[<2>Expl : %s; %s@ %a@]" - (fun k->k a b - (fun out () -> List.iter (Format.fprintf out " |- %s@ ") l) ()); - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) - - let assume s = - let open Plugin_intf in - try - for i = s.start to s.start + s.length - 1 do - match s.get i with - | Assign (x, v, lvl) -> - env := { !env with assign = M.add x (v, lvl) !env.assign } - | Lit f -> - Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print f); - match f with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> - env := { !env with cc = CC.add_eq !env.cc i j } - | Fsmt.Distinct (i, j) -> - env := { !env with cc = CC.add_neq !env.cc i j } - done; - Sat - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) - - let backtrack l = env := l - - let assign t = CC.repr !env.cc t - - let iter_assignable f = function - | Fsmt.Prop _ -> () - | Fsmt.Equal(a, b) - | Fsmt.Distinct (a, b) -> f a; f b - - let max (a: int) (b: int) = if a < b then b else a - - let eval = function - | Fsmt.Prop _ -> Plugin_intf.Unknown - | Fsmt.Equal (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Plugin_intf.Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) - with Not_found -> - Plugin_intf.Unknown - end - | Fsmt.Distinct (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Plugin_intf.Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b) - with Not_found -> - Plugin_intf.Unknown - end - - let if_sat _ = - Plugin_intf.Sat - -end - -module Make(Dummy:sig end) = struct - - include Mcsolver.Make(Fsmt)(Tsmt)(struct end) - module Dot = Dot.Make(Proof)(struct - let print_atom = St.print_atom - let lemma_info () = "Proof", Some "PURPLE", [] - end) - module Dedukti = Dedukti.Make(Proof)(struct - let print _ _ = () - let prove _ _ = () - let context _ _ = () - end) - - let print_clause = St.print_clause - let print_dot = Dot.print - let print_dedukti = Dedukti.print - -end diff --git a/src/example/sat.ml b/src/example/sat.ml deleted file mode 100644 index fcf4ed34..00000000 --- a/src/example/sat.ml +++ /dev/null @@ -1,93 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module FI = Formula_intf - -module Fsat = struct - - exception Bad_atom - - type t = int - type proof = unit - - let max_lit = max_int - let max_fresh = ref (-1) - let max_index = ref 0 - - let _make i = - if i <> 0 && (abs i) < max_lit then begin - max_index := max !max_index (abs i); - i - end else - raise Bad_atom - - let dummy = 0 - - let neg a = - a - let norm a = abs a, if a < 0 then FI.Negated else FI.Same_sign - let abs = abs - let sign i = i > 0 - let apply_sign b i = if b then i else neg i - let set_sign b i = if b then abs i else neg (abs i) - - let hash (a:int) = a land max_int - let equal (a:int) b = a=b - let compare (a:int) b = Pervasives.compare a b - - let make i = _make (2 * i) - - let fresh, iter = - let create () = - incr max_fresh; - _make (2 * !max_fresh + 1) - in - let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f j - done - in - create, iter - - let print fmt a = - Format.fprintf fmt "%s%s%d" - (if a < 0 then "~" else "") - (if a mod 2 = 0 then "v" else "f") - ((abs a) / 2) - -end - -module Tseitin = Tseitin.Make(Fsat) - -module Make(Dummy : sig end) = struct - - module Tsat = Solver.DummyTheory(Fsat) - include Solver.Make(Fsat)(Tsat)(struct end) - - let print_atom = Fsat.print - let print_clause = St.print_clause - let print_proof out p = - let module Dot = Dot.Make(Proof)(struct - let clause_name c = St.(c.name) - let print_atom = St.print_atom - let lemma_info () = "()", None, [] - end) - in - Dot.print out p - - let print_dimacs_clause fmt l = - Format.fprintf fmt "%a0" (fun fmt l -> - List.iter (fun i -> Format.fprintf fmt "%d " i) l) l - - let print_dimacs fmt l = - let l = List.map (fun c -> - List.map (fun a -> a.St.lit) (Proof.to_list c)) l in - let n, m = List.fold_left (fun (n, m) c -> - let m' = List.fold_left (fun i j -> max i (abs j)) m c in - (n + 1, m')) (0, 0) l in - Format.fprintf fmt "p cnf %d %d@\n" n m; - List.iter (fun c -> Format.fprintf fmt "%a@\n" print_dimacs_clause c) l - -end diff --git a/src/example/sat.mli b/src/example/sat.mli deleted file mode 100644 index bcc87f68..00000000 --- a/src/example/sat.mli +++ /dev/null @@ -1,62 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Fsat : sig - - include Formula_intf.S with type t = private int - - exception Bad_atom - (** Exception raised when a problem with atomic formula encoding is detected. *) - - val make : int -> t - (** Returns the literal corresponding to the integer. - @raise Bad_atom if given [0] as argument.*) - - val fresh : unit -> t - (** [new_atom ()] returns a fresh literal. - @raise Bad_atom if there are no more integer available to represent new atoms. *) - - val neg : t -> t - (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) - - val abs : t -> t - val sign : t -> bool - val apply_sign : bool -> t -> t - val set_sign : bool -> t -> t - (** Convenienc functions for manipulating literals. *) - - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - (** Usual hash and comparison functions. For now, directly uses - [Pervasives] and [Hashtbl] builtins. *) - - val iter : (t -> unit) -> unit - (** Allows iteration over all atoms created (even if unused). *) - -end - -module Tseitin : Tseitin.S with type atom = Fsat.t - -module Make(Dummy : sig end) : sig - (** Fonctor to make a pure SAT Solver module with built-in literals. *) - - include Solver.S with type St.formula = Fsat.t - - val print_atom : Format.formatter -> atom -> unit - (** Print the atom on the given formatter. *) - - val print_clause : Format.formatter -> St.clause -> unit - (** Print the clause on the given formatter. *) - - val print_proof : Format.formatter -> Proof.proof -> unit - (** Print the given proof in dot format. *) - - val print_dimacs : Format.formatter -> St.clause list -> unit - (** Prints a cnf in dimacs format on the given formatter *) - -end - diff --git a/src/example/sig.mli b/src/example/sig.mli deleted file mode 100644 index 1441de22..00000000 --- a/src/example/sig.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - - -module type OrderedType = sig - (** Signature for ordered types (mainly for use in Map.Make) *) - - type t - val compare : t -> t -> int -end diff --git a/src/example/smt.ml b/src/example/smt.ml deleted file mode 100644 index 0f25bcba..00000000 --- a/src/example/smt.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Fsmt = Expr - -module Tsmt = struct - - module CC = Cc.Make(String) - - type formula = Fsmt.t - type proof = unit - type level = CC.t - - let dummy = CC.empty - - let env = ref dummy - - let current_level () = !env - - let to_clause (a, b, l) = - Log.debugf 10 "@[Expl : %s; %s@ %a@]" - (fun k->k a b - (fun out () -> List.iter (Format.fprintf out "|- %s@ ") l) ()); - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) - - let assume s = - let open Theory_intf in - try - for i = s.start to s.start + s.length - 1 do - Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i)); - match s.get i with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j - | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j - done; - Sat - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) - - let if_sat _ = Theory_intf.Sat - - let backtrack l = env := l - -end - -module Make(Dummy:sig end) = struct - - include Solver.Make(Fsmt)(Tsmt)(struct end) - module Dot = Dot.Make(Proof)(struct - let print_atom = St.print_atom - let lemma_info () = "Proof", Some "PURPLE", [] - end) - module Dedukti = Dedukti.Make(Proof)(struct - let print _ _ = () - let prove _ _ = () - let context _ _ = () - end) - - let print_clause = St.print_clause - let print_dot = Dot.print - let print_dedukti = Dedukti.print - -end diff --git a/src/example/smt.mli b/src/example/smt.mli deleted file mode 100644 index f703efe4..00000000 --- a/src/example/smt.mli +++ /dev/null @@ -1,22 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Make(Dummy: sig end) : sig - (** Fonctor to make a SMT Solver module with built-in literals. *) - - include Solver.S with type St.formula = Expr.t - - val print_clause : Format.formatter -> St.clause -> unit - (** Print the clause on the given formatter. *) - - val print_dot : Format.formatter -> Proof.proof -> unit - (** Print the given proof in dot format. *) - - val print_dedukti : Format.formatter -> Proof.proof -> unit - (** Print the given proof in dot format. *) - -end - diff --git a/src/main.ml b/src/main.ml index 49fb2686..bc40bb32 100644 --- a/src/main.ml +++ b/src/main.ml @@ -4,47 +4,77 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module F = Expr -module T = Cnf.S -module Smt = Smt.Make(struct end) -module Mcsat = Mcsat.Make(struct end) - exception Incorrect_model exception Out_of_time exception Out_of_space -(* IO wrappers *) -(* Types for input/output languages *) -type sat_input = - | Auto - | Dimacs - | Smtlib +let file = ref "" +let p_cnf = ref false +let p_check = ref false +let p_proof_print = ref false +let p_unsat_core = ref false +let time_limit = ref 300. +let size_limit = ref 1000_000_000. -type sat_output = - | Standard (* Only output problem status *) - | Dedukti - | Dot +module P = + Dolmen.Logic.Make(Dolmen.ParseLocation) + (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement) -type solver = - | Smt - | Mcsat +module type S = sig + val do_task : Dolmen.Statement.t -> unit +end -let input = ref Auto -let output = ref Standard -let solver = ref Smt +module Make + (S : External.S) + (T : Type.S with type atom := S.atom) += struct -let input_list = [ - "auto", Auto; - "dimacs", Dimacs; - "smtlib", Smtlib; -] -let output_list = [ - "dot", Dot; - "dk", Dedukti; -] + let hyps = ref [] + + let do_task s = + match s.Dolmen.Statement.descr with + | Dolmen.Statement.Def (id, t) -> T.def id t + | Dolmen.Statement.Decl (id, t) -> T.decl id t + | Dolmen.Statement.Consequent t -> + let cnf = T.consequent t in + hyps := cnf @ !hyps; + S.assume cnf + | Dolmen.Statement.Antecedent t -> + let cnf = T.antecedent t in + hyps := cnf @ !hyps; + S.assume cnf + | Dolmen.Statement.Prove -> + let res = S.solve () in + let t = Sys.time () in + begin match res with + | S.Sat state -> + if !p_check then + if not (List.for_all (List.exists state.Solver_intf.eval) !hyps) then + raise Incorrect_model; + let t' = Sys.time () -. t in + Format.printf "Sat (%f/%f)@." t t' + | S.Unsat state -> + if !p_check then begin + let p = state.Solver_intf.get_proof () in + S.Proof.check p; + end; + let t' = Sys.time () -. t in + Format.printf "Unsat (%f/%f)@." t t' + end + | _ -> + Format.printf "Command not supported:@\n%a@." + Dolmen.Statement.print s +end + +module Sat = Make(Sat.Make(struct end))(Type_sat) +module Smt = Make(Smt.Make(struct end))(Type_smt) +module Mcsat = Make(Mcsat.Make(struct end))(Type_smt) + +let solver = ref (module Sat : S) let solver_list = [ - "smt", Smt; - "mcsat", Mcsat; + "sat", (module Sat : S); + "smt", (module Smt : S); + "mcsat", (module Mcsat : S); ] let error_msg opt arg l = @@ -58,95 +88,9 @@ let set_flag opt arg flag l = with Not_found -> invalid_arg (error_msg opt arg l) -let set_input s = set_flag "Input" s input input_list -let set_output s = set_flag "Output" s output output_list let set_solver s = set_flag "Solver" s solver solver_list -(* Input Parsing *) -let rec rev_flat_map f acc = function - | [] -> acc - | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r - -let format_of_filename s = - let last n = - try String.sub s (String.length s - n) n - with Invalid_argument _ -> "" - in - if last 4 = ".cnf" then - Dimacs - else if last 5 = ".smt2" then - Smtlib - else (* Default choice *) - Dimacs - -let parse_with_input file = function - | Auto -> assert false - | Dimacs -> List.rev_map (List.rev_map F.mk_prop) (Parsedimacs.parse file) - | Smtlib -> rev_flat_map T.make_cnf [] (Smtlib.parse file) - -let parse_input file = - parse_with_input file (match !input with - | Auto -> format_of_filename file - | f -> f) - -(* Printing wrappers *) -let std = Format.std_formatter - -let print format = match !output with - | Standard -> - Format.kfprintf (fun fmt -> Format.fprintf fmt "@.") std format - | Dot -> - Format.fprintf std "/* "; - Format.kfprintf (fun fmt -> Format.fprintf fmt " */@.") std format - | Dedukti -> - Format.fprintf std "(; "; - Format.kfprintf (fun fmt -> Format.fprintf fmt " ;)@.") std format - -let print_proof proof = match !output with - | Standard -> () - | Dot -> Smt.print_dot std proof - | Dedukti -> Smt.print_dedukti std proof - -let print_mcproof proof = match !output with - | Standard -> () - | Dot -> Mcsat.print_dot std proof - | Dedukti -> Mcsat.print_dedukti std proof - -let rec print_cl fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> F.print fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" F.print a print_cl r - -let print_lcl l = - List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l - -let print_lclause l = - List.iter (fun c -> Format.fprintf std "%a@\n" Smt.print_clause c) l - -let print_mclause l = - List.iter (fun c -> Format.fprintf std "%a@\n" Mcsat.print_clause c) l - -let print_cnf cnf = match !output with - | Standard -> print_lcl cnf - | Dot | Dedukti -> () - -let print_unsat_core u = match !output with - | Standard -> print_lclause u - | Dot | Dedukti -> () - -let print_mc_unsat_core u = match !output with - | Standard -> print_mclause u - | Dot | Dedukti -> () - (* Arguments parsing *) -let file = ref "" -let p_cnf = ref false -let p_check = ref false -let p_proof_print = ref false -let p_unsat_core = ref false -let time_limit = ref 300. -let size_limit = ref 1000_000_000. - let int_arg r arg = let l = String.length arg in let multiplier m = @@ -167,7 +111,7 @@ let int_arg r arg = | 'd' -> multiplier 86400. | '0'..'9' -> r := float_of_string arg | _ -> raise (Arg.Bad "bad numeric argument") - with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument") + with Failure _ -> raise (Arg.Bad "bad numeric argument") let setup_gc_stat () = at_exit (fun () -> @@ -186,12 +130,8 @@ let argspec = Arg.align [ " Build, check and print the proof (if output is set), if unsat"; "-gc", Arg.Unit setup_gc_stat, " Outputs statistics about the GC"; - "-i", Arg.String set_input, - " Sets the input format (default auto)"; - "-o", Arg.String set_output, - " Sets the output format (default none)"; "-s", Arg.String set_solver, - "{smt,mcsat} Sets the solver to use (default smt)"; + "{sat,smt,mcsat} Sets the solver to use (default smt)"; "-size", Arg.String (int_arg size_limit), "[kMGT] Sets the size limit for the sat solver"; "-time", Arg.String (int_arg time_limit), @@ -212,8 +152,6 @@ let check () = else if s > !size_limit then raise Out_of_space -(* Entry file parsing *) -let get_cnf () = parse_input !file let main () = (* Administrative duties *) @@ -225,66 +163,38 @@ let main () = let al = Gc.create_alarm check in (* Interesting stuff happening *) - let cnf = get_cnf () in - if !p_cnf then - print_cnf cnf; - match !solver with - | Smt -> - Smt.assume cnf; - let res = Smt.solve () in - Gc.delete_alarm al; - begin match res with - | Smt.Sat sat -> - let t = Sys.time () in - if !p_check then - if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then - raise Incorrect_model; - print "Sat (%f/%f)" t (Sys.time () -. t) - | Smt.Unsat us -> - let t = Sys.time () in - if !p_check then begin - let p = us.Solver_intf.get_proof () in - Smt.Proof.check p; - print_proof p; - if !p_unsat_core then - print_unsat_core (Smt.unsat_core p) - end; - print "Unsat (%f/%f)" t (Sys.time () -. t) - end - | Mcsat -> - Mcsat.assume cnf; - let res = Mcsat.solve () in - Gc.delete_alarm al; - begin match res with - | Mcsat.Sat sat -> - let t = Sys.time () in - if !p_check then - if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then - raise Incorrect_model; - print "Sat (%f/%f)" t (Sys.time () -. t) - | Mcsat.Unsat us -> - let t = Sys.time () in - if !p_check then begin - let p = us.Solver_intf.get_proof () in - Mcsat.Proof.check p; - print_mcproof p; - if !p_unsat_core then - print_mc_unsat_core (Mcsat.unsat_core p) - end; - print "Unsat (%f/%f)" t (Sys.time () -. t) - end + let lang, input = P.parse_file !file in + let module S = (val !solver : S) in + List.iter S.do_task input; + (* Small hack for dimacs, which do not output a "Prove" statement *) + begin match lang with + | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat () + | _ -> () + end; + Gc.delete_alarm al; + () let () = try main () with - | Incorrect_model -> - print "Internal error : incorrect *sat* model"; - exit 4 | Out_of_time -> - print "Timeout"; + Format.printf "Timeout@."; exit 2 | Out_of_space -> - print "Spaceout"; + Format.printf "Spaceout@."; exit 3 + | Incorrect_model -> + Format.printf "Internal error : incorrect *sat* model@."; + exit 4 + | Type_sat.Typing_error (msg, t) + | Type_smt.Typing_error (msg, t) -> + let b = Printexc.get_backtrace () in + let loc = match t.Dolmen.Term.loc with + | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0 + in + Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@." + Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg; + if Printexc.backtrace_status () then + Format.fprintf Format.std_formatter "%s@." b diff --git a/src/mcsat/eclosure.ml b/src/mcsat/eclosure.ml new file mode 100644 index 00000000..2fbbedb4 --- /dev/null +++ b/src/mcsat/eclosure.ml @@ -0,0 +1,231 @@ + +module type Key = sig + type t + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit +end + +module type S = sig + type t + type var + + exception Unsat of var * var * var list + + val create : Backtrack.Stack.t -> t + + val find : t -> var -> var + + val add_eq : t -> var -> var -> unit + val add_neq : t -> var -> var -> unit + val add_tag : t -> var -> var -> unit + + val find_tag : t -> var -> var * (var * var) option + +end + +module Make(T : Key) = struct + + module M = Map.Make(T) + module H = Backtrack.Hashtbl(T) + + type var = T.t + + exception Equal of var * var + exception Same_tag of var * var + exception Unsat of var * var * var list + + type repr_info = { + rank : int; + tag : (T.t * T.t) option; + forbidden : (var * var) M.t; + } + + type node = + | Follow of var + | Repr of repr_info + + type t = { + size : int H.t; + expl : var H.t; + repr : node H.t; + } + + let create s = { + size = H.create s; + expl = H.create s; + repr = H.create s; + } + + (* Union-find algorithm with path compression *) + let self_repr = Repr { rank = 0; tag = None; forbidden = M.empty } + + let find_hash m i default = + try H.find m i + with Not_found -> default + + let rec find_aux m i = + match find_hash m i self_repr with + | Repr r -> r, i + | Follow j -> + let r, k = find_aux m j in + H.add m i (Follow k); + r, k + + let get_repr h x = + let r, y = find_aux h.repr x in + y, r + + let tag h x v = + let r, y = find_aux h.repr x in + let new_m = + { r with + tag = match r.tag with + | Some (_, v') when not (T.equal v v') -> raise (Equal (x, y)) + | (Some _) as t -> t + | None -> Some (x, v) } + in + H.add h.repr y (Repr new_m) + + let find h x = fst (get_repr h x) + + let find_tag h x = + let r, y = find_aux h.repr x in + y, r.tag + + let forbid_aux m x = + try + let a, b = M.find x m in + raise (Equal (a, b)) + with Not_found -> () + + let link h x mx y my = + let new_m = { + rank = if mx.rank = my.rank then mx.rank + 1 else mx.rank; + tag = (match mx.tag, my.tag with + | Some (z, t1), Some (w, t2) -> + if not (T.equal t1 t2) then begin + Log.debugf 3 "Tag shenanigan : %a (%a) <> %a (%a)" (fun k -> + k T.print t1 T.print z T.print t2 T.print w); + raise (Equal (z, w)) + end else Some (z, t1) + | Some t, None | None, Some t -> Some t + | None, None -> None); + forbidden = M.merge (fun _ b1 b2 -> match b1, b2 with + | Some r, _ | None, Some r -> Some r | _ -> assert false) + mx.forbidden my.forbidden;} + in + let aux m z eq = + match H.find m z with + | Repr r -> + let r' = { r with + forbidden = M.add x eq (M.remove y r.forbidden) } + in + H.add m z (Repr r') + | _ -> assert false + in + M.iter (aux h.repr) my.forbidden; + H.add h.repr y (Follow x); + H.add h.repr x (Repr new_m) + + let union h x y = + let rx, mx = get_repr h x in + let ry, my = get_repr h y in + if T.compare rx ry <> 0 then begin + forbid_aux mx.forbidden ry; + forbid_aux my.forbidden rx; + if mx.rank > my.rank then begin + link h rx mx ry my + end else begin + link h ry my rx mx + end + end + + let forbid h x y = + let rx, mx = get_repr h x in + let ry, my = get_repr h y in + if T.compare rx ry = 0 then + raise (Equal (x, y)) + else match mx.tag, my.tag with + | Some (a, v), Some (b, v') when T.compare v v' = 0 -> + raise (Same_tag(a, b)) + | _ -> + H.add h.repr ry (Repr { my with forbidden = M.add rx (x, y) my.forbidden }); + H.add h.repr rx (Repr { mx with forbidden = M.add ry (x, y) mx.forbidden }) + + (* Equivalence closure with explanation output *) + let find_parent v m = find_hash m v v + + let rec root m acc curr = + let parent = find_parent curr m in + if T.compare curr parent = 0 then + curr :: acc + else + root m (curr :: acc) parent + + let rec rev_root m curr = + let next = find_parent curr m in + if T.compare curr next = 0 then + curr + else begin + H.remove m curr; + let res = rev_root m next in + H.add m next curr; + res + end + + let expl t a b = + let rec aux last = function + | x :: r, y :: r' when T.compare x y = 0 -> + aux (Some x) (r, r') + | l, l' -> begin match last with + | Some z -> List.rev_append (z :: l) l' + | None -> List.rev_append l l' + end + in + aux None (root t.expl [] a, root t.expl [] b) + + let add_eq_aux t i j = + if T.compare (find t i) (find t j) = 0 then + () + else begin + let old_root_i = rev_root t.expl i in + let old_root_j = rev_root t.expl j in + let nb_i = find_hash t.size old_root_i 0 in + let nb_j = find_hash t.size old_root_j 0 in + if nb_i < nb_j then begin + H.add t.expl i j; + H.add t.size j (nb_i + nb_j + 1) + end else begin + H.add t.expl j i; + H.add t.size i (nb_i + nb_j + 1) + end + end + + (* Functions wrapped to produce explanation in case + * something went wrong *) + let add_tag t x v = + match tag t x v with + | () -> () + | exception Equal (a, b) -> + raise (Unsat (a, b, expl t a b)) + + let add_eq t i j = + add_eq_aux t i j; + match union t i j with + | () -> () + | exception Equal (a, b) -> + raise (Unsat (a, b, expl t a b)) + + let add_neq t i j = + match forbid t i j with + | () -> () + | exception Equal (a, b) -> + raise (Unsat (a, b, expl t a b)) + | exception Same_tag (x, y) -> + add_eq_aux t i j; + let res = expl t i j in + raise (Unsat (i, j, res)) + +end diff --git a/src/mcsat/eclosure.mli b/src/mcsat/eclosure.mli new file mode 100644 index 00000000..d4d5f32c --- /dev/null +++ b/src/mcsat/eclosure.mli @@ -0,0 +1,60 @@ + +(** Equality closure using an union-find structure. + This module implements a equality closure algorithm using an union-find structure. + It supports adding of equality as well as inequalities, and raises exceptions + when trying to build an incoherent closure. + Please note that this does not implement congruence closure, as we do not + look inside the terms we are given. *) + +module type Key = sig + (** The type of keys used by the equality closure algorithm *) + + type t + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit +end + +module type S = sig + (** Type signature for the equality closure algorithm *) + + type t + (** Mutable state of the equality closure algorithm. *) + + type var + (** The type of expressions on which equality closure is built *) + + exception Unsat of var * var * var list + (** Raise when trying to build an incoherent equality closure, with an explanation + of the incoherence. + [Unsat (a, b, l)] is such that: + - [a <> b] has been previously added to the closure. + - [l] start with [a] and ends with [b] + - for each consecutive terms [p] and [q] in [l], + an equality [p = q] has been added to the closure. + *) + + val create : Backtrack.Stack.t -> t + (** Creates an empty state which uses the given backtrack stack *) + + val find : t -> var -> var + (** Returns the representative of the given expression in the current closure state *) + + val add_eq : t -> var -> var -> unit + val add_neq : t -> var -> var -> unit + (** Add an equality of inequality to the closure. *) + + val add_tag : t -> var -> var -> unit + (** Add a tag to an expression. The algorithm ensures that each equality class + only has one tag. If incoherent tags are added, an exception is raised. *) + + val find_tag : t -> var -> var * (var * var) option + (** Returns the tag associated with the equality class of the given term, if any. + More specifically, [find_tag e] returns a pair [(repr, o)] where [repr] is the representant of the equality + class of [e]. If the class has a tag, then [o = Some (e', t)] such that [e'] has been tagged with [t] previously. *) + +end + +module Make(T : Key) : S with type var = T.t + diff --git a/src/mcsat/mcsat.ml b/src/mcsat/mcsat.ml new file mode 100644 index 00000000..40d35e49 --- /dev/null +++ b/src/mcsat/mcsat.ml @@ -0,0 +1,13 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Make(Dummy:sig end) = + Mcsolver.Make(struct + type proof = unit + module Term = Expr_smt.Term + module Formula = Expr_smt.Atom + end)(Plugin_mcsat)(struct end) + diff --git a/src/util/smtlib/smtlib.mli b/src/mcsat/mcsat.mli similarity index 63% rename from src/util/smtlib/smtlib.mli rename to src/mcsat/mcsat.mli index c5c5bfed..edb13401 100644 --- a/src/util/smtlib/smtlib.mli +++ b/src/mcsat/mcsat.mli @@ -4,4 +4,5 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -val parse : string -> Cnf.S.t list +module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom + diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml new file mode 100644 index 00000000..eee5e1f0 --- /dev/null +++ b/src/mcsat/plugin_mcsat.ml @@ -0,0 +1,198 @@ + +(* Module initialization *) + +module E = Eclosure.Make(Expr_smt.Term) +module H = Backtrack.Hashtbl(Expr_smt.Term) +module M = Hashtbl.Make(Expr_smt.Term) + +(* Type definitions *) + +type proof = unit +type term = Expr_smt.Term.t +type formula = Expr_smt.Atom.t +type level = Backtrack.Stack.level + +exception Absurd of Expr_smt.Atom.t list + +(* Backtracking *) + +let stack = Backtrack.Stack.create () + +let dummy = Backtrack.Stack.dummy_level + +let current_level () = Backtrack.Stack.level stack + +let backtrack = Backtrack.Stack.backtrack stack + +(* Equality closure *) + +let uf = E.create stack + +let assign t = + match E.find_tag uf t with + | _, None -> t + | _, Some (_, v) -> v + +(* Propositional constants *) + +let true_ = Expr_smt.(Term.of_id (Id.ty "true" Ty.prop)) +let false_ = Expr_smt.(Term.of_id (Id.ty "false" Ty.prop)) + +(* Uninterpreted functions and predicates *) + +let map = H.create stack +let watch = M.create 4096 +let interpretation = H.create stack + +let pop_watches t = + try + let l = M.find watch t in + M.remove watch t; + l + with Not_found -> + [] + +let add_job j x = + let l = try M.find watch x with Not_found -> [] in + M.add watch x (j :: l) + +let update_job x ((t, watchees) as job) = + try + let y = List.find (fun y -> not (H.mem map y)) watchees in + add_job job y + with Not_found -> + add_job job x; + begin match t with + | { Expr_smt.term = Expr_smt.App (f, tys, l) } -> + let is_prop = Expr_smt.(Ty.equal t.t_type Ty.prop) in + let t_v, _ = H.find map t in + let l' = List.map (fun x -> fst (H.find map x)) l in + let u = Expr_smt.Term.apply f tys l' in + begin try + let t', u_v = H.find interpretation u in + if not (Expr_smt.Term.equal t_v u_v) then begin + match t' with + | { Expr_smt.term = Expr_smt.App (_, _, r) } when is_prop -> + let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in + if Expr_smt.(Term.equal u_v true_) then begin + let res = Expr_smt.Atom.pred t :: + Expr_smt.Atom.neg (Expr_smt.Atom.pred t') :: eqs in + raise (Absurd res) + end else begin + let res = Expr_smt.Atom.pred t' :: + Expr_smt.Atom.neg (Expr_smt.Atom.pred t) :: eqs in + raise (Absurd res) + end + | { Expr_smt.term = Expr_smt.App (_, _, r) } -> + let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in + let res = Expr_smt.Atom.eq t t' :: eqs in + raise (Absurd res) + | _ -> assert false + end + with Not_found -> + H.add interpretation u (t, t_v); + end + | _ -> assert false + end + +let rec update_watches x = function + | [] -> () + | job :: r -> + begin + try + update_job x job; + with exn -> + List.iter (fun j -> add_job j x) r; + raise exn + end; + update_watches x r + +let add_watch t l = + update_job t (t, l) + +let add_assign t v lvl = + H.add map t (v, lvl); + update_watches t (pop_watches t) + +(* Assignemnts *) + +let rec iter_aux f = function + | { Expr_smt.term = Expr_smt.Var _ } as t -> + Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t); + f t + | { Expr_smt.term = Expr_smt.App (_, _, l) } as t -> + if l <> [] then add_watch t (t :: l); + List.iter (iter_aux f) l; + Log.debugf 10 "Adding %a as assignable" (fun k -> k Expr_smt.Term.print t); + f t + +let iter_assignable f = function + | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _ } } -> () + | { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l) } as t) } -> + if l <> [] then add_watch t (t :: l); + List.iter (iter_aux f) l; + | { Expr_smt.atom = Expr_smt.Equal (a, b) } -> + iter_aux f a; iter_aux f b + +let eval = function + | { Expr_smt.atom = Expr_smt.Pred t } -> + begin try + let v, lvl = H.find map t in + if Expr_smt.Term.equal v true_ then + Plugin_intf.Valued (true, lvl) + else if Expr_smt.Term.equal v false_ then + Plugin_intf.Valued (false, lvl) + else + Plugin_intf.Unknown + with Not_found -> + Plugin_intf.Unknown + end + | { Expr_smt.atom = Expr_smt.Equal (a, b); sign } -> + begin try + let v_a, a_lvl = H.find map a in + let v_b, b_lvl = H.find map a in + if Expr_smt.Term.equal v_a v_b then + Plugin_intf.Valued(sign, max a_lvl b_lvl) + else + Plugin_intf.Valued(not sign, max a_lvl b_lvl) + with Not_found -> + Plugin_intf.Unknown + end + + +(* Theory propagation *) + +let rec chain_eq = function + | [] | [_] -> [] + | a :: ((b :: r) as l) -> (Expr_smt.Atom.eq a b) :: chain_eq l + +let assume s = + let open Plugin_intf in + try + for i = s.start to s.start + s.length - 1 do + match s.get i with + | Assign (t, v, lvl) -> + add_assign t v lvl; + E.add_tag uf t v + | Lit f -> + begin match f with + | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = true } -> + E.add_eq uf u v + | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = false } -> + E.add_neq uf u v + | { Expr_smt.atom = Expr_smt.Pred p; sign } -> + let v = if sign then true_ else false_ in + add_assign p v ~-1 + end + done; + Plugin_intf.Sat + with + | Absurd l -> + Plugin_intf.Unsat (l, ()) + | E.Unsat (a, b, l) -> + let c = Expr_smt.Atom.eq a b :: List.map Expr_smt.Atom.neg (chain_eq l) in + Plugin_intf.Unsat (c, ()) + +let if_sat _ = + Plugin_intf.Sat + diff --git a/src/msat.mlpack b/src/msat.mlpack index bf7c053c..eb1182bc 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -18,21 +18,11 @@ Solver Mcsolver Solver_types -# Backends +# Proofs & Backends +Res +Backend_intf Dot Dedukti # Auxiliary modules -Res Tseitin - -# Sat/Smt modules -Expr -Cnf -Sat -Mcsat -Cc -Sig -Smt -Unionfind - diff --git a/src/msat.odocl b/src/msat.odocl index 09f5e4ce..ff4f7d94 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -13,6 +13,7 @@ solver/Tseitin_intf # Main modules core/Res +core/Res_intf core/Internal core/External core/Solver_types @@ -20,13 +21,12 @@ core/Solver_types solver/Solver solver/Mcsolver solver/Tseitin +solver/Tseitin_intf # Backends backend/Dot backend/Dedukti backend/Backend_intf -# Examples -example/Sat -example/Smt - +# Auxiliary +util/Hashcons diff --git a/src/msat_sat.mlpack b/src/msat_sat.mlpack new file mode 100644 index 00000000..dc169686 --- /dev/null +++ b/src/msat_sat.mlpack @@ -0,0 +1 @@ +Sat diff --git a/src/msat_sat.odocl b/src/msat_sat.odocl new file mode 100644 index 00000000..1fb3c3bf --- /dev/null +++ b/src/msat_sat.odocl @@ -0,0 +1,3 @@ + +smt/Sat + diff --git a/src/msat_smt.mlpack b/src/msat_smt.mlpack new file mode 100644 index 00000000..1bba977f --- /dev/null +++ b/src/msat_smt.mlpack @@ -0,0 +1,3 @@ +Smt +Cc +Explanation diff --git a/src/msat_smt.odocl b/src/msat_smt.odocl new file mode 100644 index 00000000..ab9aa609 --- /dev/null +++ b/src/msat_smt.odocl @@ -0,0 +1,17 @@ + +smt/Smt + +# support +smt/Cc +smt/Cnf +smt/Explanation +smt/Expr +smt/ID +smt/Sat +smt/Literal +smt/Mcsat +smt/Symbols +smt/Term +smt/Ty +smt/Unionfind + diff --git a/src/sat/expr_sat.ml b/src/sat/expr_sat.ml new file mode 100644 index 00000000..23c0498d --- /dev/null +++ b/src/sat/expr_sat.ml @@ -0,0 +1,64 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +exception Bad_atom + +type t = int +type proof = unit + +let max_lit = max_int +let max_fresh = ref (-1) +let max_index = ref 0 + +let _make i = + if i <> 0 && (abs i) < max_lit then begin + max_index := max !max_index (abs i); + i + end else + raise Bad_atom + +let dummy = 0 + +let neg a = - a + +let norm a = + abs a, if a < 0 then + Formula_intf.Negated + else + Formula_intf.Same_sign + +let abs = abs + +let sign i = i > 0 + +let apply_sign b i = if b then i else neg i + +let set_sign b i = if b then abs i else neg (abs i) + +let hash (a:int) = a land max_int +let equal (a:int) b = a=b +let compare (a:int) b = Pervasives.compare a b + +let make i = _make (2 * i) + +let fresh, iter = + let create () = + incr max_fresh; + _make (2 * !max_fresh + 1) + in + let iter: (t -> unit) -> unit = fun f -> + for j = 1 to !max_index do + f j + done + in + create, iter + +let print fmt a = + Format.fprintf fmt "%s%s%d" + (if a < 0 then "~" else "") + (if a mod 2 = 0 then "v" else "f") + ((abs a) / 2) + diff --git a/src/sat/expr_sat.mli b/src/sat/expr_sat.mli new file mode 100644 index 00000000..7026d8e4 --- /dev/null +++ b/src/sat/expr_sat.mli @@ -0,0 +1,14 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +include Formula_intf.S + +val make : int -> t +(** Make a proposition from an integer. *) + +val fresh : unit -> t +(** Make a fresh atom *) + diff --git a/src/example/cnf.mli b/src/sat/sat.ml similarity index 57% rename from src/example/cnf.mli rename to src/sat/sat.ml index b0eae539..9e0442f3 100644 --- a/src/example/cnf.mli +++ b/src/sat/sat.ml @@ -4,4 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module S : Tseitin.S with type atom = Expr.Formula.t +module Make(Dummy : sig end) = + Solver.Make(Expr_sat)(Solver.DummyTheory(Expr_sat))(struct end) + diff --git a/src/util/parsedimacs.mli b/src/sat/sat.mli similarity index 63% rename from src/util/parsedimacs.mli rename to src/sat/sat.mli index 84a7b222..dc20113a 100644 --- a/src/util/parsedimacs.mli +++ b/src/sat/sat.mli @@ -4,6 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -exception Syntax_error of int +module Make(Dummy : sig end) : Solver.S with type St.formula = Expr_sat.t + -val parse : string -> int list list diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml new file mode 100644 index 00000000..6689f7f6 --- /dev/null +++ b/src/sat/type_sat.ml @@ -0,0 +1,73 @@ + +(* Log&Module Init *) +(* ************************************************************************ *) + +module Id = Dolmen.Id +module Ast = Dolmen.Term +module H = Hashtbl.Make(Id) +module Formula = Tseitin.Make(Expr_sat) + +(* Exceptions *) +(* ************************************************************************ *) + +exception Typing_error of string * Dolmen.Term.t + +(* Identifiers *) +(* ************************************************************************ *) + +let symbols = H.create 42 + +let find_id id = + try + H.find symbols id + with Not_found -> + let res = Expr_sat.fresh () in + H.add symbols id res; + res + +(* Actual parsing *) +(* ************************************************************************ *) + +let rec parse = function + | { Ast.term = Ast.Builtin Ast.True } -> + Formula.f_true + | { Ast.term = Ast.Builtin Ast.False } -> + Formula.f_false + | { Ast.term = Ast.Symbol id } -> + let s = find_id id in + Formula.make_atom s + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) } + | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } -> + Formula.make_not (parse p) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) } + | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } -> + Formula.make_and (List.map parse l) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) } + | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } -> + Formula.make_or (List.map parse l) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } -> + Formula.make_imply (parse p) (parse q) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } -> + Formula.make_equiv (parse p) (parse q) + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } -> + Formula.make_xor (parse p) (parse q) + | t -> + raise (Typing_error ("Term is not a pure proposition", t)) + +(* Exported functions *) +(* ************************************************************************ *) + +let decl _ t = + raise (Typing_error ("Declarations are not allowed in pure sat", t)) + +let def _ t = + raise (Typing_error ("Definitions are not allowed in pure sat", t)) + +let antecedent t = + let f = parse t in + Formula.make_cnf f + +let consequent t = + let f = parse t in + Formula.make_cnf @@ Formula.make_not f + diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli new file mode 100644 index 00000000..6d295a52 --- /dev/null +++ b/src/sat/type_sat.mli @@ -0,0 +1,7 @@ + +(** Typechecking of terms from Dolmen.Term.t + This module provides functions to parse terms from the untyped syntax tree + defined in Dolmen, and generate formulas as defined in the Expr_sat module. *) + +include Type.S with type atom := Expr_sat.t + diff --git a/src/smt/cc.ml b/src/smt/cc.ml new file mode 100644 index 00000000..b0b3f19a --- /dev/null +++ b/src/smt/cc.ml @@ -0,0 +1,515 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +let max_split = 1000000 + +let cc_active = ref true + +type answer = Yes of Explanation.t | No + +module type S = sig + type t + + val empty : unit -> t + val assume : cs:bool -> + Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int + val query : Literal.LT.t -> t -> answer + val class_of : t -> Term.t -> Term.t list +end + +module Make (Dummy : sig end) = struct + + module Ex = Explanation + module Uf = Uf.Make(Term) + module T = Term + module A = Literal + module LR = A.Make(struct type t = X.r include X end) + module SetT = Term.Set + module S = Symbols + + module SetX = Set.Make(struct type t = X.r let compare = X.compare end) + + (* module Uf = Pptarjan.Uf *) + + type env = { + uf : Uf.t ; + relation : X.Rel.t + } + + type choice_sign = + | CPos of int (* The explication of this choice *) + | CNeg (* The choice has been already negated *) + + type t = { + gamma : env; + gamma_finite : env ; + choices : (X.r A.view * Num.num * choice_sign * Ex.t) list; + (** the choice, the size, choice_sign, the explication set, + the explication for this choice. *) + } + + module Print = struct + + let begin_case_split () = () + + let end_case_split () = () + + let cc r1 r2 = () + + let make_cst t ctx = () + + let add_to_use t = () + + let lrepr fmt = List.iter (Format.fprintf fmt "%a " X.print) + + let leaves t lvs = () + + let contra_congruence a ex = () + + let split_size sz = () + + let split_backtrack neg_c ex_c = () + + let split_assume c ex_c = () + + let split_backjump c dep = () + + let assume_literal sa = () + + let congruent a ex = () + + let query a = () + + end + + let bottom = Hstring.make "@bottom" + let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint) + + let concat_leaves uf l = + let rec concat_rec acc t = + match X.leaves (fst (Uf.find uf t)) , acc with + [] , _ -> one::acc + | res, [] -> res + | res , _ -> List.rev_append res acc + in + match List.fold_left concat_rec [] l with + [] -> [one] + | res -> res + + let are_equal env ex t1 t2 = + if T.equal t1 t2 then ex + else match Uf.are_equal env.uf t1 t2 with + | Yes dep -> Ex.union ex dep + | No -> raise Exit + + let equal_only_by_congruence env ex t1 t2 acc = + if T.equal t1 t2 then acc + else + let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in + if X.fully_interpreted f1 then acc + else + let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in + if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then + try + let ex = List.fold_left2 (are_equal env) ex xs1 xs2 in + let a = A.LT.make (A.Eq(t1, t2)) in + Print.congruent a ex; + (LTerm a, ex) :: acc + with Exit -> acc + else acc + + let congruents env t1 s acc ex = + SetT.fold (equal_only_by_congruence env ex t1) s acc + + let fold_find_with_explanation find ex l = + List.fold_left + (fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex) + ([], ex) l + + let view find va ex_a = + match va with + | A.Eq (t1, t2) -> + let r1, ex1 = find t1 in + let r2, ex2 = find t2 in + let ex = Ex.union (Ex.union ex1 ex2) ex_a in + A.Eq(r1, r2), ex + | A.Distinct (b, lt) -> + let lr, ex = fold_find_with_explanation find ex_a lt in + A.Distinct (b, lr), ex + | A.Builtin(b, s, l) -> + let lr, ex = fold_find_with_explanation find ex_a l in + A.Builtin(b, s, List.rev lr), ex + + let term_canonical_view env a ex_a = + view (Uf.find env.uf) (A.LT.view a) ex_a + + let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a + + let new_facts_by_contra_congruence env r bol ex = + match X.term_extract r with + | None -> [] + | Some t1 -> + match T.view t1 with + | {T.f=f1 ; xs=[x]} -> + List.fold_left + (fun acc t2 -> + match T.view t2 with + | {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> + let a = A.LT.make (A.Distinct (false, [x; y])) in + let dist = LTerm a in + begin match Uf.are_distinct env.uf t1 t2 with + | Yes ex' -> + let ex_r = Ex.union ex ex' in + Print.contra_congruence a ex_r; + (dist, ex_r) :: acc + | No -> assert false + end + | _ -> acc + ) [] (Uf.class_of env.uf bol) + | _ -> [] + + let contra_congruence = + let true_,_ = X.make T.true_ in + let false_, _ = X.make T.false_ in + fun env r ex -> + if X.equal (fst (Uf.find_r env.uf r)) true_ then + new_facts_by_contra_congruence env r T.false_ ex + else if X.equal (fst (Uf.find_r env.uf r)) false_ then + new_facts_by_contra_congruence env r T.true_ ex + else [] + + let clean_use = + List.fold_left + (fun env (a, ex) -> + match a with + | LSem _ -> assert false + | LTerm t -> + begin + match A.LT.view t with + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let lvs = concat_leaves env.uf lt in + List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + let sa = SetA.remove (t, ex) sa in + { env with use = Use.add rx (st,sa) env.use } + ) env lvs + | _ -> assert false + end) + + let rec congruence_closure env r1 r2 ex = + Print.cc r1 r2; + let uf, res = Uf.union env.uf r1 r2 ex in + List.fold_left + (fun (env, l) (p, touched, v) -> + (* we look for use(p) *) + let p_t, p_a = Use.find p env.use in + + (* we compute terms and atoms to consider for congruence *) + let repr_touched = List.map (fun (_,a,_) -> a) touched in + let st_others, sa_others = Use.congr_close_up env.use p repr_touched in + + (* we update use *) + let nuse = Use.up_close_up env.use p v in + Use.print nuse; + + (* we check the congruence of the terms. *) + let env = {env with use=nuse} in + let new_eqs = + SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in + let touched_atoms = + List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched + in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) p_a touched_atoms in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) sa_others touched_atoms in + env, new_eqs @ touched_atoms + + ) ({env with uf=uf}, []) res + + let replay_atom env sa = + let relation, result = X.Rel.assume env.relation sa in + let env = { env with relation = relation } in + let env = clean_use env result.remove in + env, result.assume + + let rec add_term env choices t ex = + (* nothing to do if the term already exists *) + if Uf.mem env.uf t then env, choices + else begin + Print.add_to_use t; + (* we add t's arguments in env *) + let {T.f = f; xs = xs} = T.view t in + let env, choices = + List.fold_left (fun (env, ch) t -> add_term env ch t ex) + (env, choices) xs + in + (* we update uf and use *) + let nuf, ctx = Uf.add env.uf t in + Print.make_cst t ctx; + let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *) + + if !cc_active then + let lvs = concat_leaves nuf xs in + let nuse = Use.up_add env.use t rt lvs in + + (* If finitetest is used we add the term to the relation *) + let rel = X.Rel.add env.relation rt in + Use.print nuse; + + (* we compute terms to consider for congruence *) + (* we do this only for non-atomic terms with uninterpreted head-symbol *) + let st_uset = Use.congr_add nuse lvs in + + (* we check the congruence of each term *) + let env = {uf = nuf; use = nuse; relation = rel} in + let ct = congruents env t st_uset [] ex in + let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in + assume_literal env choices ct + else + let rel = X.Rel.add env.relation rt in + let env = {env with uf = nuf; relation = rel} in + env, choices + end + + and add env choices a ex = + match A.LT.view a with + | A.Eq (t1, t2) -> + let env, choices = add_term env choices t1 ex in + add_term env choices t2 ex + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let env, choices = List.fold_left + (fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in + let lvs = concat_leaves env.uf lt in (* A verifier *) + let env = List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + { env with + use = Use.add rx (st,SetA.add (a, ex) sa) env.use } + ) env lvs + in + env, choices + + and semantic_view env choices la = + List.fold_left + (fun (env, choices, lsa) (a, ex) -> + match a with + | LTerm a -> + let env, choices = add env choices a ex in + let sa, ex = term_canonical_view env a ex in + env, choices, (sa, Some a, ex)::lsa + + (* XXX si on fait canonical_view pour + A.Distinct, la theorie des tableaux + part dans les choux *) + | LSem (A.Builtin _ (*| A.Distinct _*) as sa) -> + let sa, ex = canonical_view env sa ex in + env, choices, (sa, None, ex)::lsa + | LSem sa -> + env, choices, (sa, None, ex)::lsa) + (env, choices, []) la + + and assume_literal env choices la = + if la = [] then env, choices + else + let env, choices, lsa = semantic_view env choices la in + let env, choices = + List.fold_left + (fun (env, choices) (sa, _, ex) -> + Print.assume_literal sa; + match sa with + | A.Eq(r1, r2) -> + if !cc_active then + let env, l = congruence_closure env r1 r2 ex in + let env, choices = assume_literal env choices l in + let env, choices = + assume_literal env choices (contra_congruence env r1 ex) + in + assume_literal env choices (contra_congruence env r2 ex) + else + {env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices + | A.Distinct (false, lr) -> + if Uf.already_distinct env.uf lr then env, choices + else + {env with uf = Uf.distinct env.uf lr ex}, choices + | A.Distinct (true, _) -> assert false + | A.Builtin _ -> env, choices) + (env, choices) lsa + in + let env, l = replay_atom env lsa in + assume_literal env (choices@l) l + + let look_for_sat ?(bad_last=No) ch t base_env l = + let rec aux ch bad_last dl base_env li = + match li, bad_last with + | [], _ -> + begin + match X.Rel.case_split base_env.relation with + | [] -> + { t with gamma_finite = base_env; choices = List.rev dl }, ch + | l -> + let l = + List.map + (fun (c, ex_c, size) -> + let exp = Ex.fresh_exp () in + let ex_c_exp = Ex.add_fresh exp ex_c in + (* A new explanation in order to track the choice *) + (c, size, CPos exp, ex_c_exp)) l in + let sz = + List.fold_left + (fun acc (a,s,_,_) -> + Num.mult_num acc s) (Num.Int 1) (l@dl) in + Print.split_size sz; + if Num.le_num sz max_split then aux ch No dl base_env l + else + { t with gamma_finite = base_env; choices = List.rev dl }, ch + end + | ((c, size, CNeg, ex_c) as a)::l, _ -> + let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in + aux ch bad_last (a::dl) base_env l + + (** This optimisation is not correct with the current explanation *) + (* | [(c, size, CPos exp, ex_c)], Yes dep -> *) + (* let neg_c = LR.neg (LR.make c) in *) + (* let ex_c = Ex.union ex_c dep in *) + (* Print.split_backtrack neg_c ex_c; *) + (* aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, ex_c] *) + + | ((c, size, CPos exp, ex_c_exp) as a)::l, _ -> + try + Print.split_assume (LR.make c) ex_c_exp; + let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in + aux ch bad_last (a::dl) base_env l + with Exception.Inconsistent dep -> + match Ex.remove_fresh exp dep with + | None -> + (* The choice doesn't participate to the inconsistency *) + Print.split_backjump (LR.make c) dep; + raise (Exception.Inconsistent dep) + | Some dep -> + (* The choice participates to the inconsistency *) + let neg_c = LR.neg (LR.make c) in + Print.split_backtrack neg_c dep; + aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep] + in + aux ch bad_last (List.rev t.choices) base_env l + + let try_it f t = + Print.begin_case_split (); + let r = + try + if t.choices = [] then look_for_sat [] t t.gamma [] + else + try + let env, lt = f t.gamma_finite in + look_for_sat lt t env [] + with Exception.Inconsistent dep -> + look_for_sat ~bad_last:(Yes dep) + [] { t with choices = []} t.gamma t.choices + with Exception.Inconsistent d -> + Print.end_case_split (); + raise (Exception.Inconsistent d) + in + Print.end_case_split (); r + + let extract_from_semvalues = + List.fold_left + (fun acc r -> + match X.term_extract r with Some t -> SetT.add t acc | _ -> acc) + + let extract_terms_from_choices = + List.fold_left + (fun acc (a, _, _, _) -> + match a with + | A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2] + | A.Distinct (_, l) -> extract_from_semvalues acc l + | _ -> acc) + + let extract_terms_from_assumed = + List.fold_left + (fun acc (a, _) -> + match a with + | LTerm r -> begin + match Literal.LT.view r with + | Literal.Eq (t1, t2) -> + SetT.add t1 (SetT.add t2 acc) + | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> + List.fold_right SetT.add l acc + end + | _ -> acc) + + let assume ~cs a ex t = + let a = LTerm a in + let gamma, ch = assume_literal t.gamma [] [a, ex] in + let t = { t with gamma = gamma } in + let t, ch = + if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t + else t, ch + in + let choices = extract_terms_from_choices SetT.empty t.choices in + let all_terms = extract_terms_from_assumed choices ch in + t, all_terms, 1 + + let class_of t term = Uf.class_of t.gamma.uf term + + let add_and_process a t = + let aux a ex env = + let gamma, l = add env [] a ex in assume_literal gamma [] l + in + let gamma, _ = aux a Ex.empty t.gamma in + let t = { t with gamma = gamma } in + let t, _ = try_it (aux a Ex.empty) t in + Use.print t.gamma.use; t + + let query a t = + Print.query a; + try + match A.LT.view a with + | A.Eq (t1, t2) -> + let t = add_and_process a t in + Uf.are_equal t.gamma.uf t1 t2 + + | A.Distinct (false, [t1; t2]) -> + let na = A.LT.neg a in + let t = add_and_process na t in (* na ? *) + Uf.are_distinct t.gamma.uf t1 t2 + + | A.Distinct _ -> + assert false (* devrait etre capture par une analyse statique *) + + | _ -> + let na = A.LT.neg a in + let t = add_and_process na t in + let env = t.gamma in + let rna, ex_rna = term_canonical_view env na Ex.empty in + X.Rel.query env.relation (rna, Some na, ex_rna) + with Exception.Inconsistent d -> Yes d + + let empty () = + let env = { + use = Use.empty ; + uf = Uf.empty ; + relation = X.Rel.empty (); + } + in + let t = { gamma = env; gamma_finite = env; choices = [] } in + let t, _, _ = + assume ~cs:false + (A.LT.make (A.Distinct (false, [T.true_; T.false_]))) Ex.empty t + in t + +end diff --git a/src/smt/cc.mli b/src/smt/cc.mli new file mode 100644 index 00000000..935ed2ea --- /dev/null +++ b/src/smt/cc.mli @@ -0,0 +1,37 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +val cc_active : bool ref + +type answer = Yes of Explanation.t | No + +module type S = sig + type t + + val empty : unit -> t + + val assume : + cs:bool -> + Literal.LT.t -> + Explanation.t -> + t -> t * Term.Set.t * int + + val query : Literal.LT.t -> t -> answer + + val class_of : t -> Term.t -> Term.t list +end + +module Make (Dummy : sig end) : S diff --git a/src/smt/explanation.ml b/src/smt/explanation.ml new file mode 100644 index 00000000..3646c112 --- /dev/null +++ b/src/smt/explanation.ml @@ -0,0 +1,68 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type atom = Literal.LT.t + +type exp = Atom of atom | Fresh of int + +module S = + Set.Make + (struct + type t = exp + let compare a b = match a,b with + | Atom _, Fresh _ -> -1 + | Fresh _, Atom _ -> 1 + | Fresh i1, Fresh i2 -> i1 - i2 + | Atom a, Atom b -> a.aid - b.aid + end) + +type t = S.t + +let singleton e = S.singleton (Atom e) + +let empty = S.empty + +let union s1 s2 = S.union s1 s2 + +let iter_atoms f s = + S.iter (fun e -> match e with + | Fresh _ -> () + | Atom a -> f a) s + +let fold_atoms f s acc = + S.fold (fun e acc -> match e with + | Fresh _ -> acc + | Atom a -> f a acc) s acc + +let merge e1 e2 = e1 + + +let fresh_exp = + let r = ref (-1) in + fun () -> incr r; !r + +let remove_fresh i s = + let fi = Fresh i in + if S.mem fi s then Some (S.remove fi s) + else None + +let add_fresh i = S.add (Fresh i) + + +let print fmt ex = + fprintf fmt "{"; + S.iter (function + | Atom a -> fprintf fmt "%a, " Debug.atom a + | Fresh i -> fprintf fmt "Fresh%d " i) ex; + fprintf fmt "}" diff --git a/src/smt/explanation.mli b/src/smt/explanation.mli new file mode 100644 index 00000000..b362b0c3 --- /dev/null +++ b/src/smt/explanation.mli @@ -0,0 +1,39 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type t + +type exp + +type atom = Literal.LT.t + +val empty : t + +val singleton : atom-> t + +val union : t -> t -> t + +val merge : t -> t -> t + +val iter_atoms : (atom -> unit) -> t -> unit + +val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a + +val fresh_exp : unit -> int + +val remove_fresh : int -> t -> t option + +val add_fresh : int -> t -> t + +val print : Format.formatter -> t -> unit diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml new file mode 100644 index 00000000..5fb8acfe --- /dev/null +++ b/src/smt/expr_smt.ml @@ -0,0 +1,525 @@ +(* + Base modules that defines the terms used in the prover. +*) + +(* Type definitions *) +(* ************************************************************************ *) + +(* Private aliases *) +type hash = int +type index = int + +(* Identifiers, parametrized by the kind of the type of the variable *) +type 'ty id = { + id_type : 'ty; + id_name : string; + index : index; (** unique *) +} + +(* Type for first order types *) +type ttype = Type + +(* The type of functions *) +type 'ty function_descr = { + fun_vars : ttype id list; (* prenex forall *) + fun_args : 'ty list; + fun_ret : 'ty; +} + +(* Types *) +type ty_descr = + | TyVar of ttype id (** Bound variables *) + | TyApp of ttype function_descr id * ty list + +and ty = { + ty : ty_descr; + mutable ty_hash : hash; (** lazy hash *) +} + +(* Terms & formulas *) +type term_descr = + | Var of ty id + | App of ty function_descr id * ty list * term list + +and term = { + term : term_descr; + t_type : ty; + mutable t_hash : hash; (* lazy hash *) +} + +type atom_descr = + | Pred of term + | Equal of term * term + +and atom = { + sign : bool; + atom : atom_descr; + mutable f_hash : hash; (* lazy hash *) +} + +(* Utilities *) +(* ************************************************************************ *) + +let rec list_cmp ord l1 l2 = + match l1, l2 with + | [], [] -> 0 + | [], _ -> -1 + | _, [] -> 1 + | x1::l1', x2::l2' -> + let c = ord x1 x2 in + if c = 0 + then list_cmp ord l1' l2' + else c + +(* Exceptions *) +(* ************************************************************************ *) + +exception Type_mismatch of term * ty * ty +exception Bad_arity of ty function_descr id * ty list * term list +exception Bad_ty_arity of ttype function_descr id * ty list + +(* Printing functions *) +(* ************************************************************************ *) + +module Print = struct + let rec list f sep fmt = function + | [] -> () + | [x] -> f fmt x + | x :: ((y :: _) as r) -> + Format.fprintf fmt "%a%s" f x sep; + list f sep fmt r + + let id fmt v = Format.fprintf fmt "%s" v.id_name + let ttype fmt = function Type -> Format.fprintf fmt "Type" + + let rec ty fmt t = match t.ty with + | TyVar v -> id fmt v + | TyApp (f, []) -> + Format.fprintf fmt "%a" id f + | TyApp (f, l) -> + Format.fprintf fmt "%a(%a)" id f (list ty ", ") l + + let params fmt = function + | [] -> () + | l -> Format.fprintf fmt "∀ %a. " (list id ", ") l + + let signature print fmt f = + match f.fun_args with + | [] -> Format.fprintf fmt "%a%a" params f.fun_vars print f.fun_ret + | l -> Format.fprintf fmt "%a%a -> %a" params f.fun_vars + (list print " -> ") l print f.fun_ret + + let fun_ty = signature ty + let fun_ttype = signature ttype + + let id_type print fmt v = Format.fprintf fmt "%a : %a" id v print v.id_type + + let id_ty = id_type ty + let id_ttype = id_type ttype + let const_ty = id_type fun_ty + let const_ttype = id_type fun_ttype + + let rec term fmt t = match t.term with + | Var v -> id fmt v + | App (f, [], []) -> + Format.fprintf fmt "%a" id f + | App (f, [], args) -> + Format.fprintf fmt "%a(%a)" id f + (list term ", ") args + | App (f, tys, args) -> + Format.fprintf fmt "%a(%a; %a)" id f + (list ty ", ") tys + (list term ", ") args + + let atom_aux fmt f = + match f.atom with + | Equal (a, b) -> + Format.fprintf fmt "%a %s %a" + term a (if f.sign then "=" else "<>") term b + | Pred t -> + Format.fprintf fmt "%s%a" (if f.sign then "" else "¬ ") term t + + let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f + +end + +(* Substitutions *) +(* ************************************************************************ *) + +module Subst = struct + module Mi = Map.Make(struct + type t = int * int + let compare (a, b) (c, d) = match compare a c with 0 -> compare b d | x -> x + end) + + type ('a, 'b) t = ('a * 'b) Mi.t + + (* Usual functions *) + let empty = Mi.empty + + let is_empty = Mi.is_empty + + let iter f = Mi.iter (fun _ (key, value) -> f key value) + + let fold f = Mi.fold (fun _ (key, value) acc -> f key value acc) + + let bindings s = Mi.fold (fun _ (key, value) acc -> (key, value) :: acc) s [] + + (* Comparisons *) + let equal f = Mi.equal (fun (_, value1) (_, value2) -> f value1 value2) + let compare f = Mi.compare (fun (_, value1) (_, value2) -> f value1 value2) + let hash h s = Mi.fold (fun i (_, value) acc -> Hashtbl.hash (acc, i, h value)) s 1 + + let choose m = snd (Mi.choose m) + + (* Iterators *) + let exists pred s = + try + iter (fun m s -> if pred m s then raise Exit) s; + false + with Exit -> + true + + let for_all pred s = + try + iter (fun m s -> if not (pred m s) then raise Exit) s; + true + with Exit -> + false + + let print print_key print_value fmt map = + let aux _ (key, value) = + Format.fprintf fmt "%a -> %a@ " print_key key print_value value + in + Format.fprintf fmt "@[%a@]" (fun _ -> Mi.iter aux) map + + module type S = sig + type 'a key + val get : 'a key -> ('a key, 'b) t -> 'b + val mem : 'a key -> ('a key, 'b) t -> bool + val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t + val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t + end + + (* Variable substitutions *) + module Id = struct + type 'a key = 'a id + let tok v = (v.index, 0) + let get v s = snd (Mi.find (tok v) s) + let mem v s = Mi.mem (tok v) s + let bind v t s = Mi.add (tok v) (v, t) s + let remove v s = Mi.remove (tok v) s + end + +end + +(* Dummies *) +(* ************************************************************************ *) + +module Dummy = struct + + let id_ttype = + { index = -1; id_name = ""; id_type = Type; } + + let ty = + { ty = TyVar id_ttype; ty_hash = -1; } + + let id = + { index = -2; id_name = ""; id_type = ty; } + + let term = + { term = Var id; t_type = ty; t_hash = -1; } + + let atom = + { atom = Pred term; sign = true; f_hash = -1; } + +end + +(* Variables *) +(* ************************************************************************ *) + +module Id = struct + type 'a t = 'a id + + (* Hash & comparisons *) + let hash v = v.index + + let compare: 'a. 'a id -> 'a id -> int = + fun v1 v2 -> compare v1.index v2.index + + let equal v1 v2 = compare v1 v2 = 0 + + (* Printing functions *) + let print = Print.id + + (* Id count *) + let _count = ref 0 + + (* Constructors *) + let mk_new id_name id_type = + incr _count; + let index = !_count in + { index; id_name; id_type } + + let ttype name = mk_new name Type + let ty name ty = mk_new name ty + + let const name fun_vars fun_args fun_ret = + mk_new name { fun_vars; fun_args; fun_ret; } + + let ty_fun name n = + let rec replicate acc n = + if n <= 0 then acc + else replicate (Type :: acc) (n - 1) + in + const name [] (replicate [] n) Type + + let term_fun = const + + (* Builtin Types *) + let prop = ty_fun "Prop" 0 + let base = ty_fun "$i" 0 + +end + +(* Types *) +(* ************************************************************************ *) + +module Ty = struct + type t = ty + type subst = (ttype id, ty) Subst.t + + (* Hash & Comparisons *) + let rec hash_aux t = match t.ty with + | TyVar v -> Id.hash v + | TyApp (f, args) -> + Hashtbl.hash (Id.hash f, List.map hash args) + + and hash t = + if t.ty_hash = -1 then + t.ty_hash <- hash_aux t; + t.ty_hash + + let discr ty = match ty.ty with + | TyVar _ -> 1 + | TyApp _ -> 2 + + let rec compare u v = + let hu = hash u and hv = hash v in + if hu <> hv then Pervasives.compare hu hv + else match u.ty, v.ty with + | TyVar v1, TyVar v2 -> Id.compare v1 v2 + | TyApp (f1, args1), TyApp (f2, args2) -> + begin match Id.compare f1 f2 with + | 0 -> list_cmp compare args1 args2 + | x -> x + end + | _, _ -> Pervasives.compare (discr u) (discr v) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.ty + + (* Constructors *) + let mk_ty ty = { ty; ty_hash = -1; } + + let of_id v = mk_ty (TyVar v) + + let apply f args = + assert (f.id_type.fun_vars = []); + if List.length args <> List.length f.id_type.fun_args then + raise (Bad_ty_arity (f, args)) + else + mk_ty (TyApp (f, args)) + + (* Builtin types *) + let prop = apply Id.prop [] + let base = apply Id.base [] + + (* Substitutions *) + let rec subst_aux map t = match t.ty with + | TyVar v -> begin try Subst.Id.get v map with Not_found -> t end + | TyApp (f, args) -> + let new_args = List.map (subst_aux map) args in + if List.for_all2 (==) args new_args then t + else apply f new_args + + let subst map t = if Subst.is_empty map then t else subst_aux map t + + (* Typechecking *) + let instantiate f tys args = + if List.length f.id_type.fun_vars <> List.length tys || + List.length f.id_type.fun_args <> List.length args then + raise (Bad_arity (f, tys, args)) + else + let map = List.fold_left2 (fun acc v ty -> Subst.Id.bind v ty acc) Subst.empty f.id_type.fun_vars tys in + let fun_args = List.map (subst map) f.id_type.fun_args in + List.iter2 (fun t ty -> + if not (equal t.t_type ty) then raise (Type_mismatch (t, t.t_type, ty))) + args fun_args; + subst map f.id_type.fun_ret + +end + +(* Terms *) +(* ************************************************************************ *) + +module Term = struct + type t = term + type subst = (ty id, term) Subst.t + + (* Hash & Comparisons *) + let rec hash_aux t = match t.term with + | Var v -> Id.hash v + | App (f, tys, args) -> + let l = List.map Ty.hash tys in + let l' = List.map hash args in + Hashtbl.hash (Id.hash f, l, l') + + and hash t = + if t.t_hash = -1 then + t.t_hash <- hash_aux t; + t.t_hash + + let discr t = match t.term with + | Var _ -> 1 + | App _ -> 2 + + let rec compare u v = + let hu = hash u and hv = hash v in + if hu <> hv then Pervasives.compare hu hv + else match u.term, v.term with + | Var v1, Var v2 -> Id.compare v1 v2 + | App (f1, tys1, args1), App (f2, tys2, args2) -> + begin match Id.compare f1 f2 with + | 0 -> + begin match list_cmp Ty.compare tys1 tys2 with + | 0 -> list_cmp compare args1 args2 + | x -> x + end + | x -> x + end + | _, _ -> Pervasives.compare (discr u) (discr v) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.term + + (* Constructors *) + let mk_term term t_type = + { term; t_type; t_hash = -1; } + + let of_id v = + mk_term (Var v) v.id_type + + let apply f ty_args t_args = + mk_term (App (f, ty_args, t_args)) (Ty.instantiate f ty_args t_args) + + (* Substitutions *) + let rec subst_aux ty_map t_map t = match t.term with + | Var v -> begin try Subst.Id.get v t_map with Not_found -> t end + | App (f, tys, args) -> + let new_tys = List.map (Ty.subst ty_map) tys in + let new_args = List.map (subst_aux ty_map t_map) args in + if List.for_all2 (==) new_tys tys && List.for_all2 (==) new_args args then t + else apply f new_tys new_args + + let subst ty_map t_map t = + if Subst.is_empty ty_map && Subst.is_empty t_map then + t + else + subst_aux ty_map t_map t + + let rec replace (t, t') t'' = match t''.term with + | _ when equal t t'' -> t' + | App (f, ty_args, t_args) -> + apply f ty_args (List.map (replace (t, t')) t_args) + | _ -> t'' + +end + +(* Formulas *) +(* ************************************************************************ *) + +module Atom = struct + type t = atom + + type proof = unit + + (* Hash & Comparisons *) + let h_eq = 2 + let h_pred = 3 + + let rec hash_aux f = match f.atom with + | Equal (t1, t2) -> + Hashtbl.hash (h_eq, Term.hash t1, Term.hash t2) + | Pred t -> + Hashtbl.hash (h_pred, Term.hash t) + + and hash f = + if f.f_hash = -1 then + f.f_hash <- hash_aux f; + f.f_hash + + let discr f = match f.atom with + | Equal _ -> 1 + | Pred _ -> 2 + + let compare f g = + let hf = hash f and hg = hash g in + if hf <> hg then Pervasives.compare hf hg + else match f.atom, g.atom with + | Equal (u1, v1), Equal(u2, v2) -> + list_cmp Term.compare [u1; v1] [u2; v2] + | Pred t1, Pred t2 -> Term.compare t1 t2 + | _, _ -> Pervasives.compare (discr f) (discr g) + + let equal u v = + u == v || (hash u = hash v && compare u v = 0) + + (* Printing functions *) + let print = Print.atom + + (* Constructors *) + let mk_formula f = { + sign = true; + atom = f; + f_hash = -1; + } + + let dummy = Dummy.atom + + let pred t = + if not (Ty.equal Ty.prop t.t_type) then + raise (Type_mismatch (t, t.t_type, Ty.prop)) + else + mk_formula (Pred t) + + let fresh () = + let id = Id.ty "fresh" Ty.prop in + pred (Term.of_id id) + + let neg f = + { f with sign = not f.sign } + + let eq a b = + if not (Ty.equal a.t_type b.t_type) then + raise (Type_mismatch (b, b.t_type, a.t_type)) + else if Term.compare a b < 0 then + mk_formula (Equal (a, b)) + else + mk_formula (Equal (b, a)) + + let norm f = + { f with sign = true }, + if f.sign then Formula_intf.Same_sign + else Formula_intf.Negated + +end + +module Formula = Tseitin.Make(Atom) + diff --git a/src/smt/expr_smt.mli b/src/smt/expr_smt.mli new file mode 100644 index 00000000..229cf51b --- /dev/null +++ b/src/smt/expr_smt.mli @@ -0,0 +1,326 @@ + +(** Expressions for TabSat *) + +(** {2 Type definitions} *) + +(** These are custom types used in functions later. *) + +(** {3 Identifiers} *) + +(** Identifiers are the basic building blocks used to build types terms and expressions. *) + +type hash +type index = private int + +(** Private aliases to provide access. You should not have any need + to use these, instead use the functions provided by this module. *) + +type 'ty id = private { + id_type : 'ty; + id_name : string; + index : index; (** unique *) +} + +(** The type of identifiers. An ['a id] is an identifier whose solver-type + is represented by an inhabitant of type ['a]. + All identifier have an unique [index] which is used for comparison, + so that the name of a variable is only there for tracability + and/or pretty-printing. *) + +(** {3 Types} *) + +type ttype = Type + +(** The caml type of solver-types. *) + +type 'ty function_descr = private { + fun_vars : ttype id list; (* prenex forall *) + fun_args : 'ty list; + fun_ret : 'ty; +} + +(** This represents the solver-type of a function. + Functions can be polymorphic in the variables described in the + [fun_vars] field. *) + +type ty_descr = private + | TyVar of ttype id + (** bound variables (i.e should only appear under a quantifier) *) + | TyApp of ttype function_descr id * ty list + (** application of a constant to some arguments *) + +and ty = private { + ty : ty_descr; + mutable ty_hash : hash; (** Use Ty.hash instead *) +} + +(** These types defines solver-types, i.e the representation of the types + of terms in the solver. Record definition for [type ty] is shown in order + to be able to use the [ty.ty] field in patter matches. Other fields shoud not + be accessed directly, but throught the functions provided by the [Ty] module. *) + +(** {3 Terms} *) + +type term_descr = private + | Var of ty id + (** bound variables (i.e should only appear under a quantifier) *) + | App of ty function_descr id * ty list * term list + (** application of a constant to some arguments *) + +and term = private { + term : term_descr; + t_type : ty; + mutable t_hash : hash; (** Do not use this filed, call Term.hash instead *) +} + +(** Types defining terms in the solver. The definition is vary similar to that + of solver-types, except for type arguments of polymorphic functions which + are explicit. This has the advantage that there is a clear and typed distinction + between solver-types and terms, but may lead to some duplication of code + in some places. *) + +(** {3 Formulas} *) + +type atom_descr = private + (** Atoms *) + | Pred of term + | Equal of term * term + +and atom = private { + sign : bool; + atom : atom_descr; + mutable f_hash : hash; (** Use Formula.hash instead *) +} + +(** The type of atoms in the solver. The list of free arguments in quantifiers + is a bit tricky, so you should not touch it (see full doc for further + explanations). *) + +(** {3 Exceptions} *) + +exception Type_mismatch of term * ty * ty +(* Raised when as Type_mismatch(term, actual_type, expected_type) *) + +exception Bad_arity of ty function_descr id * ty list * term list +exception Bad_ty_arity of ttype function_descr id * ty list +(** Raised when trying to build an application with wrong arity *) + +(** {2 Printing} *) + +module Print : sig + (** Pretty printing functions *) + + val id : Format.formatter -> 'a id -> unit + val id_ty : Format.formatter -> ty id -> unit + val id_ttype : Format.formatter -> ttype id -> unit + + val const_ty : Format.formatter -> ty function_descr id -> unit + val const_ttype : Format.formatter -> ttype function_descr id -> unit + + val ty : Format.formatter -> ty -> unit + val fun_ty : Format.formatter -> ty function_descr -> unit + + val ttype : Format.formatter -> ttype -> unit + val fun_ttype : Format.formatter -> ttype function_descr -> unit + + val term : Format.formatter -> term -> unit + val atom : Format.formatter -> atom -> unit +end + +(** {2 Identifiers & Metas} *) + +module Id : sig + type 'a t = 'a id + (* Type alias *) + + val hash : 'a t -> int + val equal : 'a t -> 'a t -> bool + val compare : 'a t -> 'a t -> int + (** Usual functions for hash/comparison *) + + val print : Format.formatter -> 'a t -> unit + (** Printing for variables *) + + val prop : ttype function_descr id + val base : ttype function_descr id + (** Constants representing the type for propositions and a default type + for term, respectively. *) + + val ttype : string -> ttype id + (** Create a fresh type variable with the given name. *) + + val ty : string -> ty -> ty id + (** Create a fresh variable with given name and type *) + + val ty_fun : string -> int -> ttype function_descr id + (** Create a fresh type constructor with given name and arity *) + + val term_fun : string -> ttype id list -> ty list -> ty -> ty function_descr id + (** [ty_fun name type_vars arg_types return_type] returns a fresh constant symbol, + possibly polymorphic with respect to the variables in [type_vars] (which may appear in the + types in [arg_types] and in [return_type]). *) + +end + +(** {2 Substitutions} *) + +module Subst : sig + (** Module to handle substitutions *) + + type ('a, 'b) t + (** The type of substitutions from values of type ['a] to values of type ['b]. *) + + val empty : ('a, 'b) t + (** The empty substitution *) + + val is_empty : ('a, 'b) t -> bool + (** Test wether a substitution is empty *) + + val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit + (** Iterates over the bindings of the substitution. *) + + val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c + (** Fold over the elements *) + + val bindings : ('a, 'b) t -> ('a * 'b) list + (** Returns the list of bindings ofa substitution. *) + + val exists : ('a -> 'b -> bool) -> ('a, 'b) t -> bool + (** Tests wether the predicate holds for at least one binding. *) + + val for_all : ('a -> 'b -> bool) -> ('a, 'b) t -> bool + (** Tests wether the predicate holds for all bindings. *) + + val hash : ('b -> int) -> ('a, 'b) t -> int + val compare : ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int + val equal : ('b -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t -> bool + (** Comparison and hash functions, with a comparison/hash function on values as parameter *) + + val print : + (Format.formatter -> 'a -> unit) -> + (Format.formatter -> 'b -> unit) -> + Format.formatter -> ('a, 'b) t -> unit + (** Prints the substitution, using the given functions to print keys and values. *) + + val choose : ('a, 'b) t -> 'a * 'b + (** Return one binding of the given substitution, or raise Not_found if the substitution is empty.*) + + (** {5 Concrete subtitutions } *) + module type S = sig + type 'a key + val get : 'a key -> ('a key, 'b) t -> 'b + (** [get v subst] returns the value associated with [v] in [subst], if it exists. + @raise Not_found if there is no binding for [v]. *) + val mem : 'a key -> ('a key, 'b) t -> bool + (** [get v subst] returns wether there is a value associated with [v] in [subst]. *) + val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t + (** [bind v t subst] returns the same substitution as [subst] with the additional binding from [v] to [t]. + Erases the previous binding of [v] if it exists. *) + val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t + (** [remove v subst] returns the same substitution as [subst] except for [v] which is unbound in the returned substitution. *) + end + + module Id : S with type 'a key = 'a id +end + +(** {2 Types} *) + +module Ty : sig + type t = ty + (** Type alias *) + + type subst = (ttype id, ty) Subst.t + (** The type of substitutions over types. *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + + val prop : ty + val base : ty + (** The type of propositions and individuals *) + + val of_id : ttype id -> ty + (** Creates a type from a variable *) + + val apply : ttype function_descr id -> ty list -> ty + (** Applies a constant to a list of types *) + + val subst : subst -> ty -> ty + (** Substitution over types. *) + +end + +(** {2 Terms} *) + +module Term : sig + type t = term + (** Type alias *) + + type subst = (ty id, term) Subst.t + (** The type of substitutions in types. *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + (** Printing functions *) + + val of_id : ty id -> term + (** Create a term from a variable *) + + val apply : ty function_descr id -> ty list -> term list -> term + (** Applies a constant function to type arguments, then term arguments *) + + val subst : Ty.subst -> subst -> term -> term + (** Substitution over types. *) + + val replace : term * term -> term -> term + (** [replace (t, t') t''] returns the term [t''] where every occurence of [t] + has been replace by [t']. *) + +end + +(** {2 Formulas} *) + +module Atom : sig + type t = atom + type proof = unit + (** Type alias *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash/compare functions *) + + val print : Format.formatter -> t -> unit + (** Printing functions *) + + val dummy : atom + (** A dummy atom, different from any other atom. *) + + val fresh : unit -> atom + (** Create a fresh propositional atom. *) + + val eq : term -> term -> atom + (** Create an equality over two terms. The two given terms + must have the same type [t], which must be different from {!Ty.prop} *) + + val pred : term -> atom + (** Create a atom from a term. The given term must have type {!Ty.prop} *) + + val neg : atom -> atom + (** Returns the negation of the given atom *) + + val norm : atom -> atom * Formula_intf.negated + (** Normalization functions as required by msat. *) + +end + +module Formula : Tseitin.S with type atom = atom + diff --git a/src/smt/smt.ml b/src/smt/smt.ml new file mode 100644 index 00000000..5acf092d --- /dev/null +++ b/src/smt/smt.ml @@ -0,0 +1,11 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Th = Solver.DummyTheory(Expr_smt.Atom) + +module Make(Dummy:sig end) = + Solver.Make(Expr_smt.Atom)(Th)(struct end) + diff --git a/src/example/cnf.ml b/src/smt/smt.mli similarity index 63% rename from src/example/cnf.ml rename to src/smt/smt.mli index f778231a..edb13401 100644 --- a/src/example/cnf.ml +++ b/src/smt/smt.mli @@ -4,4 +4,5 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module S = Tseitin.Make(Expr) +module Make(Dummy: sig end) : Solver.S with type St.formula = Expr_smt.atom + diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml new file mode 100644 index 00000000..fd95c77f --- /dev/null +++ b/src/smt/type_smt.ml @@ -0,0 +1,624 @@ + +(* Log&Module Init *) +(* ************************************************************************ *) + +module Ast = Dolmen.Term +module Id = Dolmen.Id +module M = Map.Make(Id) +module H = Hashtbl.Make(Id) +module Expr = Expr_smt + +(* Types *) +(* ************************************************************************ *) + +(* The type of potentially expected result type for parsing an expression *) +type expect = + | Nothing + | Type + | Typed of Expr.ty + +(* The type returned after parsing an expression. *) +type res = + | Ttype + | Ty of Expr.ty + | Term of Expr.term + | Formula of Expr.Formula.t + + +(* The local environments used for type-checking. *) +type env = { + + (* local variables (mostly quantified variables) *) + type_vars : (Expr.ttype Expr.id) M.t; + term_vars : (Expr.ty Expr.id) M.t; + + (* Bound variables (through let constructions) *) + term_lets : Expr.term M.t; + prop_lets : Expr.Formula.t M.t; + + (* Typing options *) + expect : expect; +} + +(* Exceptions *) +(* ************************************************************************ *) + +(* Internal exception *) +exception Found of Ast.t + +(* Exception for typing errors *) +exception Typing_error of string * Ast.t + +(* Convenience functions *) +let _expected s t = raise (Typing_error ( + Format.asprintf "Expected a %s" s, t)) +let _bad_arity s n t = raise (Typing_error ( + Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t)) +let _type_mismatch t ty ty' ast = raise (Typing_error ( + Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected" + Expr.Print.term t Expr.Print.ty ty Expr.Print.ty ty', ast)) +let _fo_term s t = raise (Typing_error ( + Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t)) + +(* Global Environment *) +(* ************************************************************************ *) + +(* Global identifier table; stores declared types and aliases. *) +let global_env = H.create 42 + +let find_global name = + try H.find global_env name + with Not_found -> `Not_found + +(* Symbol declarations *) +let decl_ty_cstr id c = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Ty c); + Log.debugf 1 "New type constructor : %a" (fun k -> k Expr.Print.const_ttype c) + +let decl_term id c = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Term c); + Log.debugf 1 "New constant : %a" (fun k -> k Expr.Print.const_ty c) + +(* Symbol definitions *) +let def_ty id args body = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Ty_alias (args, body)) + +let def_term id ty_args args body = + if H.mem global_env id then + Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + (fun k -> k Id.print id); + H.add global_env id (`Term_alias (ty_args, args, body)) + +(* Local Environment *) +(* ************************************************************************ *) + +(* Make a new empty environment *) +let empty_env ?(expect=Nothing) () = { + type_vars = M.empty; + term_vars = M.empty; + term_lets = M.empty; + prop_lets = M.empty; + expect; +} + +(* Generate new fresh names for shadowed variables *) +let new_name pre = + let i = ref 0 in + (fun () -> incr i; pre ^ (string_of_int !i)) + +let new_ty_name = new_name "ty#" +let new_term_name = new_name "term#" + +(* Add local variables to environment *) +let add_type_var env id v = + let v' = + if M.mem id env.type_vars then + Expr.Id.ttype (new_ty_name ()) + else + v + in + Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Expr.Print.id_ttype v'); + v', { env with type_vars = M.add id v' env.type_vars } + +let add_type_vars env l = + let l', env' = List.fold_left (fun (l, acc) (id, v) -> + let v', acc' = add_type_var acc id v in + v' :: l, acc') ([], env) l in + List.rev l', env' + +let add_term_var env id v = + let v' = + if M.mem id env.type_vars then + Expr.Id.ty (new_term_name ()) Expr.(v.id_type) + else + v + in + Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Expr.Print.id_ty v'); + v', { env with term_vars = M.add id v' env.term_vars } + +let find_var env name = + try `Ty (M.find name env.type_vars) + with Not_found -> + begin + try + `Term (M.find name env.term_vars) + with Not_found -> + `Not_found + end + +(* Add local bound variables to env *) +let add_let_term env id t = + Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Expr.Print.term t); + { env with term_lets = M.add id t env.term_lets } + +let add_let_prop env id t = + Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Expr.Formula.print t); + { env with prop_lets = M.add id t env.prop_lets } + +let find_let env name = + try `Term (M.find name env.term_lets) + with Not_found -> + begin + try + `Prop (M.find name env.prop_lets) + with Not_found -> + `Not_found + end + +let pp_expect fmt = function + | Nothing -> Format.fprintf fmt "<>" + | Type -> Format.fprintf fmt "" + | Typed ty -> Expr.Print.ty fmt ty + +let pp_map pp fmt map = + M.iter (fun k v -> + Format.fprintf fmt "%s->%a;" k.Id.name pp v) map + +(* Some helper functions *) +(* ************************************************************************ *) + +let flat_map f l = List.flatten (List.map f l) + +let take_drop n l = + let rec aux acc = function + | 0, res | _, ([] as res) -> List.rev acc, res + | m, x :: r -> aux (x :: acc) (m - 1, r) + in + aux [] (n, l) + +let diagonal l = + let rec single x acc = function + | [] -> acc + | y :: r -> single x ((x, y) :: acc) r + and aux acc = function + | [] -> acc + | x :: r -> aux (single x acc r) r + in + aux [] l + +(* Wrappers for expression building *) +(* ************************************************************************ *) + +let arity f = + List.length Expr.(f.id_type.fun_vars) + + List.length Expr.(f.id_type.fun_args) + +let ty_apply env ast f args = + try + Expr.Ty.apply f args + with Expr.Bad_ty_arity _ -> + _bad_arity Expr.(f.id_name) (arity f) ast + +let term_apply env ast f ty_args t_args = + try + Expr.Term.apply f ty_args t_args + with + | Expr.Bad_arity _ -> + _bad_arity Expr.(f.id_name) (arity f) ast + | Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast + +let ty_subst ast_term id args f_args body = + let aux s v ty = Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Expr.Subst.empty f_args args with + | subst -> + Expr.Ty.subst subst body + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_args) ast_term + +let term_subst ast_term id ty_args t_args f_ty_args f_t_args body = + let aux s v ty = Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with + | ty_subst -> + begin + let aux s v t = Expr.Subst.Id.bind v t s in + match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with + | t_subst -> + Expr.Term.subst ty_subst t_subst body + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term + end + | exception Invalid_argument _ -> + _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term + +let make_eq ast_term a b = + try + Expr.Formula.make_atom @@ Expr.Atom.eq a b + with Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast_term + +let make_pred ast_term p = + try + Expr.Formula.make_atom @@ Expr.Atom.pred p + with Expr.Type_mismatch (t, ty, ty') -> + _type_mismatch t ty ty' ast_term + +let infer env s args = + match env.expect with + | Nothing -> `Nothing + | Type -> + let n = List.length args in + let res = Expr.Id.ty_fun s.Id.name n in + decl_ty_cstr s res; + `Ty res + | Typed ty -> + let n = List.length args in + let rec replicate acc n = + if n <= 0 then acc else replicate (Expr.Ty.base :: acc) (n - 1) + in + let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in + decl_term s res; + `Term res + +(* Expression parsing *) +(* ************************************************************************ *) + +let rec parse_expr (env : env) t = + match t with + (* Base Type *) + | { Ast.term = Ast.Symbol { Id.name = "Bool" } } -> + Ty (Expr_smt.Ty.prop) + + (* Basic formulas *) + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) } + | { Ast.term = Ast.Builtin Ast.True } -> + Formula Expr.Formula.f_true + + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) } + | { Ast.term = Ast.Builtin Ast.False } -> + Formula Expr.Formula.f_false + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } + | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" }}, l) } -> + Formula (Expr.Formula.make_and (List.map (parse_formula env) l)) + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } + | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" }}, l) } -> + Formula (Expr.Formula.make_or (List.map (parse_formula env) l)) + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_not (Expr.Formula.make_equiv f g)) + | _ -> _bad_arity "xor" 2 t + end + + | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t) + | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=>" }}, l) } as t) -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_imply f g) + | _ -> _bad_arity "=>" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, l) } as t -> + begin match l with + | [p; q] -> + let f = parse_formula env p in + let g = parse_formula env q in + Formula (Expr.Formula.make_equiv f g) + | _ -> _bad_arity "<=>" 2 t + end + + | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t) + | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" }}, l) } as t) -> + begin match l with + | [p] -> + Formula (Expr.Formula.make_not (parse_formula env p)) + | _ -> _bad_arity "not" 1 t + end + + (* (Dis)Equality *) + | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t) + | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=" }}, l) } as t) -> + begin match l with + | [a; b] -> + Formula ( + make_eq t + (parse_term env a) + (parse_term env b) + ) + | _ -> _bad_arity "=" 2 t + end + + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t -> + let l' = List.map (parse_term env) args in + let l'' = diagonal l' in + Formula ( + Expr.Formula.make_and + (List.map (fun (a, b) -> + Expr.Formula.make_not + (make_eq t a b)) l'') + ) + + (* General case: application *) + | { Ast.term = Ast.Symbol s } as ast -> + parse_app env ast s [] + | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast -> + parse_app env ast s l + + (* Local bindings *) + | { Ast.term = Ast.Binder (Ast.Let, vars, f) } -> + parse_let env f vars + + (* Other cases *) + | ast -> raise (Typing_error ("Couldn't parse the expression", ast)) + +and parse_var env = function + | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> + begin match parse_expr env e with + | Ttype -> `Ty (s, Expr.Id.ttype s.Id.name) + | Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty) + | _ -> _expected "type (or Ttype)" e + end + | { Ast.term = Ast.Symbol s } -> + begin match env.expect with + | Nothing -> assert false + | Type -> `Ty (s, Expr.Id.ttype s.Id.name) + | Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty) + end + | t -> _expected "(typed) variable" t + +and parse_quant_vars env l = + let ttype_vars, typed_vars, env' = List.fold_left ( + fun (l1, l2, acc) v -> + match parse_var acc v with + | `Ty (id, v') -> + let v'', acc' = add_type_var acc id v' in + (v'' :: l1, l2, acc') + | `Term (id, v') -> + let v'', acc' = add_term_var acc id v' in + (l1, v'' :: l2, acc') + ) ([], [], env) l in + List.rev ttype_vars, List.rev typed_vars, env' + +and parse_let env f = function + | [] -> parse_expr env f + | x :: r -> + begin match x with + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [ + { Ast.term = Ast.Symbol s }; e]) } -> + let t = parse_term env e in + let env' = add_let_term env s t in + parse_let env' f r + | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [ + { Ast.term = Ast.Symbol s }; e]) } -> + let t = parse_formula env e in + let env' = add_let_prop env s t in + parse_let env' f r + | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> + begin match parse_expr env e with + | Term t -> + let env' = add_let_term env s t in + parse_let env' f r + | Formula t -> + let env' = add_let_prop env s t in + parse_let env' f r + | _ -> _expected "term of formula" e + end + | t -> _expected "let-binding" t + end + +and parse_app env ast s args = + match find_let env s with + | `Term t -> + if args = [] then Term t + else _fo_term s ast + | `Prop p -> + if args = [] then Formula p + else _fo_term s ast + | `Not_found -> + begin match find_var env s with + | `Ty f -> + if args = [] then Ty (Expr.Ty.of_id f) + else _fo_term s ast + | `Term f -> + if args = [] then Term (Expr.Term.of_id f) + else _fo_term s ast + | `Not_found -> + begin match find_global s with + | `Ty f -> + parse_app_ty env ast f args + | `Term f -> + parse_app_term env ast f args + | `Ty_alias (f_args, body) -> + parse_app_subst_ty env ast s args f_args body + | `Term_alias (f_ty_args, f_t_args, body) -> + parse_app_subst_term env ast s args f_ty_args f_t_args body + | `Not_found -> + begin match infer env s args with + | `Ty f -> parse_app_ty env ast f args + | `Term f -> parse_app_term env ast f args + | `Nothing -> + raise (Typing_error ( + Format.asprintf "Scoping error: '%a' not found" Id.print s, ast)) + end + end + end + +and parse_app_ty env ast f args = + let l = List.map (parse_ty env) args in + Ty (ty_apply env ast f l) + +and parse_app_term env ast f args = + let n = List.length Expr.(f.id_type.fun_vars) in + let ty_l, t_l = take_drop n args in + let ty_args = List.map (parse_ty env) ty_l in + let t_args = List.map (parse_term env) t_l in + Term (term_apply env ast f ty_args t_args) + +and parse_app_subst_ty env ast id args f_args body = + let l = List.map (parse_ty env) args in + Ty (ty_subst ast id l f_args body) + +and parse_app_subst_term env ast id args f_ty_args f_t_args body = + let n = List.length f_ty_args in + let ty_l, t_l = take_drop n args in + let ty_args = List.map (parse_ty env) ty_l in + let t_args = List.map (parse_term env) t_l in + Term (term_subst ast id ty_args t_args f_ty_args f_t_args body) + +and parse_ty env ast = + match parse_expr { env with expect = Type } ast with + | Ty ty -> ty + | _ -> _expected "type" ast + +and parse_term env ast = + match parse_expr { env with expect = Typed Expr.Ty.base } ast with + | Term t -> t + | _ -> _expected "term" ast + +and parse_formula env ast = + match parse_expr { env with expect = Typed Expr.Ty.prop } ast with + | Term t when Expr.(Ty.equal Ty.prop t.t_type) -> + make_pred ast t + | Formula p -> p + | _ -> _expected "formula" ast + +let parse_ttype_var env t = + match parse_var env t with + | `Ty (id, v) -> (id, v) + | `Term _ -> _expected "type variable" t + +let rec parse_sig_quant env = function + | { Ast.term = Ast.Binder (Ast.Pi, vars, t) } -> + let ttype_vars = List.map (parse_ttype_var env) vars in + let ttype_vars', env' = add_type_vars env ttype_vars in + let l = List.combine vars ttype_vars' in + parse_sig_arrow l [] env' t + | t -> + parse_sig_arrow [] [] env t + +and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function + | { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } -> + let t_args = parse_sig_args env args in + parse_sig_arrow ttype_vars (ty_args @ t_args) env ret + | t -> + begin match parse_expr env t with + | Ttype -> + begin match ttype_vars with + | (h, _) :: _ -> + raise (Typing_error ( + "Type constructor signatures cannot have quantified type variables", h)) + | [] -> + let aux n = function + | (_, Ttype) -> n + 1 + | (ast, _) -> raise (Found ast) + in + begin + match List.fold_left aux 0 ty_args with + | n -> `Ty_cstr n + | exception Found err -> + raise (Typing_error ( + Format.asprintf + "Type constructor signatures cannot have non-ttype arguments,", err)) + end + end + | Ty ret -> + let aux acc = function + | (_, Ty t) -> t :: acc + | (ast, _) -> raise (Found ast) + in + begin + match List.fold_left aux [] ty_args with + | exception Found err -> _expected "type" err + | l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret) + end + | _ -> _expected "Ttype of type" t + end + +and parse_sig_args env l = + flat_map (parse_sig_arg env) l + +and parse_sig_arg env = function + | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } -> + List.map (fun x -> x, parse_expr env x) l + | t -> + [t, parse_expr env t] + +let parse_sig = parse_sig_quant + +let rec parse_fun ty_args t_args env = function + | { Ast.term = Ast.Binder (Ast.Fun, l, ret) } -> + let ty_args', t_args', env' = parse_quant_vars env l in + parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret + | ast -> + begin match parse_expr env ast with + | Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast)) + | Ty body -> + if t_args = [] then `Ty (ty_args, body) + else _expected "term" ast + | Term body -> `Term (ty_args, t_args, body) + | Formula _ -> _expected "type or term" ast + end + +(* High-level parsing functions *) +(* ************************************************************************ *) + +let decl id t = + let env = empty_env () in + Log.debugf 5 "Typing declaration: %s : %a" + (fun k -> k id.Id.name Ast.print t); + begin match parse_sig env t with + | `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n) + | `Fun_ty (vars, args, ret) -> + decl_term id (Expr.Id.term_fun id.Id.name vars args ret) + end + +let def id t = + let env = empty_env () in + Log.debugf 5 "Typing definition: %s = %a" + (fun k -> k id.Id.name Ast.print t); + begin match parse_fun [] [] env t with + | `Ty (ty_args, body) -> def_ty id ty_args body + | `Term (ty_args, t_args, body) -> def_term id ty_args t_args body + end + +let formula t = + let env = empty_env () in + Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t); + parse_formula env t + +let antecedent t = + Expr.Formula.make_cnf (formula t) + +let consequent t = + Expr.Formula.make_cnf (Expr.Formula.make_not (formula t)) + diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli new file mode 100644 index 00000000..51957bc8 --- /dev/null +++ b/src/smt/type_smt.mli @@ -0,0 +1,7 @@ + +(** Typechecking of terms from Dolmen.Term.t + This module provides functions to parse terms from the untyped syntax tree + defined in Dolmen, and generate formulas as defined in the Expr_smt module. *) + +include Type.S with type atom := Expr_smt.Atom.t + diff --git a/src/smt/uf.ml b/src/smt/uf.ml new file mode 100644 index 00000000..9ee4e98f --- /dev/null +++ b/src/smt/uf.ml @@ -0,0 +1,310 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type answer = Yes of Explanation.t | No + +type 'a literal = + | LSem of 'a Literal.view + | LTerm of Literal.LT.t + +exception Inconsistent of Explanation.t +exception Unsolvable + +module Ex = Explanation +module Sy = Symbols +module T = Term +module MapT = Term.Map +module SetT = Term.Set + +module Lit = Literal.Make(T) +module MapL = Lit.Map + +module MapR = MapT +module SetR = SetT + +module R = struct + include T + type r = t + + let leaves t : r list = match T.head t with + | T.Ite (a, _, _) -> [a] + | T.App (_, l) -> l +end + +type r = R.r + +module SetRR = Set.Make(struct + type t = r * r + let compare (r1, r1') (r2, r2') = + let c = T.compare r1 r2 in + if c <> 0 then c + else T.compare r1' r2' + end) + + +type t = { + (* term -> [t] *) + make : r MapT.t; + + (* representative table *) + repr : (r * Ex.t) MapR.t; + + (* r -> class (of terms) *) + classes : SetT.t MapR.t; + + (*associates each value r with the set of semantical values whose + representatives contains r *) + gamma : SetR.t MapR.t; + + (* the disequations map *) + neqs: Ex.t MapL.t MapR.t; + +} + +let empty = { + make = MapT.empty; + repr = MapR.empty; + classes = MapR.empty; + gamma = MapR.empty; + neqs = MapR.empty; +} + +module Env = struct + let mem env t = MapT.mem t env.make + + let lookup_by_t t env = + try MapR.find (MapT.find t env.make) env.repr + with Not_found -> + assert false (*R.make t, Ex.empty*) (* XXXX *) + + let lookup_by_r r env = + try MapR.find r env.repr with Not_found -> r, Ex.empty + + let lookup_for_neqs env r = + try MapR.find r env.neqs with Not_found -> MapL.empty + + let add_to_classes t r classes = + MapR.add r + (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) + classes + + let update_classes c nc classes = + let s1 = try MapR.find c classes with Not_found -> SetT.empty in + let s2 = try MapR.find nc classes with Not_found -> SetT.empty in + MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) + + let add_to_gamma r c gamma = + List.fold_left + (fun gamma x -> + let s = try MapR.find x gamma with Not_found -> SetR.empty in + MapR.add x (SetR.add r s) gamma) + gamma + (R.leaves c) + + (* r1 = r2 => neqs(r1) \uplus neqs(r2) *) + let update_neqs r1 r2 dep env = + let nq_r1 = lookup_for_neqs env r1 in + let nq_r2 = lookup_for_neqs env r2 in + let mapl = + MapL.fold + (fun l1 ex1 mapl -> + try + let ex2 = MapL.find l1 mapl in + let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) + raise (Inconsistent ex) + with Not_found -> + MapL.add l1 (Ex.union ex1 dep) mapl) + nq_r1 nq_r2 + in + MapR.add r2 mapl (MapR.add r1 mapl env.neqs) + + let filter_leaves r = + List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) + + let find_or_normal_form env r = + try MapR.find r env.repr with Not_found -> r, Ex.empty + + let init_leaf env p = + let in_repr = MapR.mem p env.repr in + let in_neqs = MapR.mem p env.neqs in + { env with + repr = + if in_repr then env.repr + else MapR.add p (p, Ex.empty) env.repr; + classes = + if in_repr then env.classes + else update_classes p p env.classes; + gamma = + if in_repr then env.gamma + else add_to_gamma p p env.gamma ; + neqs = + if in_neqs then env.neqs + else update_neqs p p Ex.empty env } + + let init_term env t = + let mkr, ctx = R.make t in + let rp, ex = normal_form env mkr in + { make = MapT.add t mkr env.make; + repr = MapR.add mkr (rp,ex) env.repr; + classes = add_to_classes t rp env.classes; + gamma = add_to_gamma mkr rp env.gamma; + neqs = + if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) + else MapR.add rp MapL.empty env.neqs}, ctx + + + let update_aux dep set env= + SetRR.fold + (fun (rr, nrr) env -> + { env with + neqs = update_neqs rr nrr dep env ; + classes = update_classes rr nrr env.classes}) + set env + + let apply_sigma_uf env (p, v, dep) = + assert (MapR.mem p env.gamma); + let use_p = MapR.find p env.gamma in + try + let env, tch, neqs_to_up = SetR.fold + (fun r (env, touched, neqs_to_up) -> + let rr, ex = MapR.find r env.repr in + let nrr = R.subst p v rr in + if R.equal rr nrr then env, touched, neqs_to_up + else + let ex = Ex.union ex dep in + let env = + {env with + repr = MapR.add r (nrr, ex) env.repr; + gamma = add_to_gamma r nrr env.gamma } + in + env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up + ) use_p (env, [], SetRR.empty) in + (* Correction : Do not update neqs twice for the same r *) + update_aux dep neqs_to_up env, tch + + with Not_found -> assert false + + let apply_sigma eqs env tch ((p, v, dep) as sigma) = + let env = init_leaf env p in + let env, touched = apply_sigma_uf env sigma in + env, ((p, touched, v) :: tch) +end + +let add env t = + if MapT.mem t env.make then env, [] else Env.init_term env t + +let ac_solve eqs dep (env, tch) (p, v) = + (* pourquoi recuperer le representant de rv? r = rv d'apres testopt *) + (* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *) + let rv, ex_rv = Env.find_or_normal_form env v in + (* let rv = v in *) + (* assert ( let rv, _ = Env.find_or_normal_form env v in R.equal v rv); *) + let dep = Ex.union ex_rv dep in + Env.apply_sigma eqs env tch (p, rv, dep) + +let check_consistent env r1 r2 dep : unit = + let rr1, ex_r1 = Env.find_or_normal_form env r1 in + let rr2, ex_r2 = Env.find_or_normal_form env r2 in + if R.equal rr1 rr2 + then () (* Remove rule *) + else + let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in + begin + ignore (Env.update_neqs rr1 rr2 dep env); + if R.can_be_equal rr1 rr2 + then () + else raise (Inconsistent dep) + end + +let union env r1 r2 dep = + check_consistent env r1 r2 dep; + () + +let rec distinct env rl dep = + let d = Lit.make (Literal.Distinct (false,rl)) in + let env, _, newds = + List.fold_left + (fun (env, mapr, newds) r -> + let rr, ex = Env.find_or_normal_form env r in + try + let exr = MapR.find rr mapr in + raise (Inconsistent (Ex.union ex exr)) + with Not_found -> + let uex = Ex.union ex dep in + let mdis = + try MapR.find rr env.neqs with Not_found -> MapL.empty in + let mdis = + try + MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis + with Not_found -> + MapL.add d uex mdis + in + let env = Env.init_leaf env rr in + let env = {env with neqs = MapR.add rr mdis env.neqs} in + env, MapR.add rr uex mapr, (rr, ex, mapr)::newds + ) + (env, MapR.empty, []) + rl + in + List.fold_left + (fun env (r1, ex1, mapr) -> + MapR.fold (fun r2 ex2 env -> + let ex = Ex.union ex1 (Ex.union ex2 dep) in + try match R.solve r1 r2 with + | [a, b] -> + if (R.equal a r1 && R.equal b r2) || + (R.equal a r2 && R.equal b r1) then env + else + distinct env [a; b] ex + | [] -> + raise (Inconsistent ex) + | _ -> env + with Unsolvable -> env) mapr env) + env newds + +let are_equal env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 env in + let r2, ex_r2 = Env.lookup_by_t t2 env in + if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No + +let are_distinct env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 env in + let r2, ex_r2 = Env.lookup_by_t t2 env in + try + ignore (union env r1 r2 (Ex.union ex_r1 ex_r2)); + No + with Inconsistent ex -> Yes(ex) + +let already_distinct env lr = + let d = Lit.make (Literal.Distinct (false,lr)) in + try + List.iter (fun r -> + let mdis = MapR.find r env.neqs in + ignore (MapL.find d mdis) + ) lr; + true + with Not_found -> false + +let find env t = + Env.lookup_by_t t env + +let find_r = Env.find_or_normal_form + +let mem = Env.mem + +let class_of env t = + try + let rt, _ = MapR.find (MapT.find t env.make) env.repr in + SetT.elements (MapR.find rt env.classes) + with Not_found -> [t] diff --git a/src/smt/uf.mli b/src/smt/uf.mli new file mode 100644 index 00000000..8205e3ee --- /dev/null +++ b/src/smt/uf.mli @@ -0,0 +1,45 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type answer = Yes of Explanation.t | No + +type 'a literal = + | LSem of 'a Literal.view + | LTerm of Literal.LT.t + +type t + +type r +(** representative *) + +val empty : t +val add : t -> Term.t -> t * Literal.LT.t list + +val mem : t -> Term.t -> bool + +val find : t -> Term.t -> r * Explanation.t + +val find_r : t -> r -> r * Explanation.t + +val union : + t -> r -> r -> Explanation.t -> + t * (r * (r * r * Explanation.t) list * r) list + +val distinct : t -> r list -> Explanation.t -> t + +val are_equal : t -> Term.t -> Term.t -> Sig.answer +val are_distinct : t -> Term.t -> Term.t -> Sig.answer +val already_distinct : t -> r list -> bool + +val class_of : t -> Term.t -> Term.t list diff --git a/src/example/unionfind.ml b/src/smt/unionfind.ml similarity index 88% rename from src/example/unionfind.ml rename to src/smt/unionfind.ml index 7211fbe0..ab81a1ad 100644 --- a/src/example/unionfind.ml +++ b/src/smt/unionfind.ml @@ -4,13 +4,20 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +module type OrderedType = sig + type t + val compare : t -> t -> int +end + (* Union-find Module *) -module Make(T : Sig.OrderedType) = struct +module Make(T : OrderedType) = struct exception Unsat of T.t * T.t type var = T.t module M = Map.Make(T) + (* TODO: better treatment of inequalities *) + type t = { rank : int M.t; forbid : ((var * var) list); @@ -43,7 +50,7 @@ module Make(T : Sig.OrderedType) = struct h.parent <- f; cx - (* Highly ineficient treatment of inequalities *) + (* Highly inefficient treatment of inequalities *) let possible h = let aux (a, b) = let ca = find h a in diff --git a/src/example/unionfind.mli b/src/smt/unionfind.mli similarity index 72% rename from src/example/unionfind.mli rename to src/smt/unionfind.mli index 4d559ced..adf2cd25 100644 --- a/src/example/unionfind.mli +++ b/src/smt/unionfind.mli @@ -4,7 +4,12 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make(T : Sig.OrderedType) : sig +module type OrderedType = sig + type t + val compare : t -> t -> int +end + +module Make(T : OrderedType) : sig type t exception Unsat of T.t * T.t val empty : t diff --git a/src/solver/tseitin.ml b/src/solver/tseitin.ml index b4ea0dbb..fa124f83 100644 --- a/src/solver/tseitin.ml +++ b/src/solver/tseitin.ml @@ -12,7 +12,7 @@ module type S = Tseitin_intf.S -module Make (F : Formula_intf.S) = struct +module Make (F : Tseitin_intf.Arg) = struct exception Empty_Or type combinator = And | Or | Imp | Not diff --git a/src/solver/tseitin.mli b/src/solver/tseitin.mli index 1eb9dc6c..bd52ffeb 100644 --- a/src/solver/tseitin.mli +++ b/src/solver/tseitin.mli @@ -6,4 +6,5 @@ Copyright 2014 Simon Cruanes module type S = Tseitin_intf.S -module Make : functor (F : Formula_intf.S) -> S with type atom = F.t +module Make : functor + (F : Tseitin_intf.Arg) -> S with type atom = F.t diff --git a/src/solver/tseitin_intf.ml b/src/solver/tseitin_intf.ml index 22f7cac9..3f02b4f8 100644 --- a/src/solver/tseitin_intf.ml +++ b/src/solver/tseitin_intf.ml @@ -10,6 +10,22 @@ (* *) (**************************************************************************) +module type Arg = sig + + type t + (** Type of atomic formulas *) + + val neg : t -> t + (** Negation of atomic formulas *) + + val fresh : unit -> t + (** Generate fresh formulas *) + + val print : Format.formatter -> t -> unit + (** Print the given formula *) + +end + module type S = sig (** The type of ground formulas *) diff --git a/src/util/.merlin b/src/util/.merlin deleted file mode 100644 index 962d669c..00000000 --- a/src/util/.merlin +++ /dev/null @@ -1,11 +0,0 @@ -S ./ -S ./smtlib/ -S ../sat/ -S ../common/ - -B ../_build/ -B ../_build/util/ -B ../_build/util/smtlib/ -B ../_build/sat/ -B ../_build/smt/ -B ../_build/common/ diff --git a/src/util/backtrack.ml b/src/util/backtrack.ml new file mode 100644 index 00000000..aff629cc --- /dev/null +++ b/src/util/backtrack.ml @@ -0,0 +1,99 @@ + +module Stack = struct + + type op = + (* Stack structure *) + | Nil : op + | Level : op * int -> op + (* Undo operations *) + | Set : 'a ref * 'a * op -> op + | Call1 : ('a -> unit) * 'a * op -> op + | Call2 : ('a -> 'b -> unit) * 'a * 'b * op -> op + | Call3 : ('a -> 'b -> 'c -> unit) * 'a * 'b * 'c * op -> op + | CallUnit : (unit -> unit) * op -> op + + type t = { + mutable stack : op; + mutable last : int; + } + + type level = int + + let dummy_level = -1 + + let create () = { + stack = Nil; + last = dummy_level; + } + + let register_set t ref value = t.stack <- Set(ref, value, t.stack) + let register_undo t f = t.stack <- CallUnit (f, t.stack) + let register1 t f x = t.stack <- Call1 (f, x, t.stack) + let register2 t f x y = t.stack <- Call2 (f, x, y, t.stack) + let register3 t f x y z = t.stack <- Call3 (f, x, y, z, t.stack) + + let curr = ref 0 + + let push t = + let level = !curr in + t.stack <- Level (t.stack, level); + t.last <- level; + incr curr + + let rec level t = + match t.stack with + | Level (_, lvl) -> lvl + | _ -> push t; level t + + let backtrack t lvl = + let rec pop = function + | Nil -> assert false + | Level (op, level) as current -> + if level = lvl then begin + t.stack <- current; + t.last <- level + end else + pop op + | Set (ref, x, op) -> ref := x; pop op + | CallUnit (f, op) -> f (); pop op + | Call1 (f, x, op) -> f x; pop op + | Call2 (f, x, y, op) -> f x y; pop op + | Call3 (f, x, y, z, op) -> f x y z; pop op + in + pop t.stack + + let pop t = backtrack t (t.last) + +end + +module Hashtbl(K : Hashtbl.HashedType) = struct + + module H = Hashtbl.Make(K) + + type key = K.t + type 'a t = { + tbl : 'a H.t; + stack : Stack.t; + } + + let create ?(size=256) stack = {tbl = H.create size; stack; } + + let mem {tbl; _} x = H.mem tbl x + let find {tbl; _} k = H.find tbl k + + let add t k v = + Stack.register2 t.stack H.remove t.tbl k; + H.add t.tbl k v + + let remove t k = + try + let v = find t k in + Stack.register3 t.stack H.add t.tbl k v; + H.remove t.tbl k + with Not_found -> () + + let fold t f acc = H.fold f t.tbl acc + + let iter f t = H.iter f t.tbl +end + diff --git a/src/util/backtrack.mli b/src/util/backtrack.mli new file mode 100644 index 00000000..6480cf63 --- /dev/null +++ b/src/util/backtrack.mli @@ -0,0 +1,77 @@ + +(** Provides helpers for backtracking. + This module defines backtracking stacks, i.e stacks of undo actions + to perform when backtracking to a certain point. This allows for + side-effect backtracking, and so to have backtracking automatically + handled by extensions without the need for explicit synchronisation + between the dispatcher and the extensions. +*) + +module Stack : sig + (** A backtracking stack is a stack of undo actions to perform + in order to revert back to a (mutable) state. *) + + type t + (** The type for a stack. *) + + type level + (** The type of backtracking point. *) + + val create : unit -> t + (** Creates an empty stack. *) + + val dummy_level : level + (** A dummy level. *) + + val push : t -> unit + (** Creates a backtracking point at the top of the stack. *) + + val pop : t -> unit + (** Pop all actions in the undo stack until the first backtracking point. *) + + val level : t -> level + (** Insert a named backtracking point at the top of the stack. *) + + val backtrack : t -> level -> unit + (** Backtrack to the given named backtracking point. *) + + val register_undo : t -> (unit -> unit) -> unit + (** Adds a callback at the top of the stack. *) + + val register1 : t -> ('a -> unit) -> 'a -> unit + val register2 : t -> ('a -> 'b -> unit) -> 'a -> 'b -> unit + val register3 : t -> ('a -> 'b -> 'c -> unit) -> 'a -> 'b -> 'c -> unit + (** Register functions to be called on the given arguments at the top of the stack. + Allows to save some space by not creating too much closure as would be the case if + only [unit -> unit] callbacks were stored. *) + + val register_set : t -> 'a ref -> 'a -> unit + (** Registers a ref to be set to the given value upon backtracking. *) + +end + +module Hashtbl : + functor (K : Hashtbl.HashedType) -> + sig + (** Provides wrappers around hastables in order to have + very simple integration with backtraking stacks. + All actions performed on this table register the corresponding + undo operations so that backtracking is automatic. *) + + type key = K.t + (** The type of keys of the Hashtbl. *) + + type 'a t + (** The type of hastable from keys to values of type ['a]. *) + + val create : ?size:int -> Stack.t -> 'a t + (** Creates an empty hashtable, that registers undo operations on the given stack. *) + + val add : 'a t -> key -> 'a -> unit + val mem : 'a t -> key -> bool + val find : 'a t -> key -> 'a + val remove : 'a t -> key -> unit + val iter : (key -> 'a -> unit) -> 'a t -> unit + val fold : 'a t -> (key -> 'a -> 'b -> 'b) -> 'b -> 'b + (** Usual operations on the hashtabl. For more information see the Hashtbl module of the stdlib. *) + end diff --git a/src/util/hashcons.ml b/src/util/hashcons.ml new file mode 100644 index 00000000..2f2fa7e7 --- /dev/null +++ b/src/util/hashcons.ml @@ -0,0 +1,28 @@ + +module type ARG = sig + type t + val equal : t -> t -> bool + val hash : t -> int + val set_id : t -> int -> unit +end + +module Make(A : ARG): sig + val hashcons : A.t -> A.t + val iter : (A.t -> unit) -> unit +end = struct + module W = Weak.Make(A) + + let tbl_ = W.create 1024 + let n_ = ref 0 + + (* hashcons terms *) + let hashcons t = + let t' = W.merge tbl_ t in + if t == t' then ( + incr n_; + A.set_id t' !n_; + ); + t' + + let iter yield = W.iter yield tbl_ +end diff --git a/src/util/parsedimacs.ml b/src/util/parsedimacs.ml deleted file mode 100644 index df5c3c8c..00000000 --- a/src/util/parsedimacs.ml +++ /dev/null @@ -1,75 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Syntax_error of int - -type line = - | Empty - | Comment - | Pcnf of int * int - | Clause of int list - -let rec _read_word s acc i len = - assert (len>0); - if i+len=String.length s - then String.sub s i len :: acc - else match s.[i+len] with - | ' ' | '\t' -> - let acc = String.sub s i len :: acc in - _skip_space s acc (i+len+1) - | _ -> _read_word s acc i (len+1) - -and _skip_space s acc i = - if i=String.length s - then acc - else match s.[i] with - | ' ' | '\t' -> _skip_space s acc (i+1) - | _ -> _read_word s acc i 1 - -let ssplit s = List.rev (_skip_space s [] 0) - -let of_input f = - match ssplit (input_line f) with - | [] -> Empty - | "c" :: _ -> Comment - | "p" :: "cnf" :: i :: j :: [] -> - begin try - Pcnf (int_of_string i, int_of_string j) - with Failure _ -> - raise (Syntax_error (-1)) - end - | l -> - begin try - begin match List.rev_map int_of_string l with - | 0 :: r -> Clause r - | _ -> raise (Syntax_error (-1)) - end - with Failure _ -> raise (Syntax_error (-1)) - end - -let parse_with todo file = - let f = open_in file in - let line = ref 0 in - try - while true do - incr line; - todo (of_input f) - done - with - | Syntax_error _ -> - raise (Syntax_error !line) - | End_of_file -> - close_in f - -let cnf = ref [] -let parse_line = function - | Empty | Comment | Pcnf _ -> () - | Clause l -> cnf := l :: !cnf - -let parse f = - cnf := []; - parse_with parse_line f; - !cnf diff --git a/src/util/smtlib/.merlin b/src/util/smtlib/.merlin deleted file mode 100644 index 23ddf6ef..00000000 --- a/src/util/smtlib/.merlin +++ /dev/null @@ -1,9 +0,0 @@ -S ./ -S ../ -S ../../sat/ - -B ../../_build/ -B ../../_build/util/ -B ../../_build/util/smtlib/ -B ../../_build/sat/ -B ../../_build/smt/ diff --git a/src/util/smtlib/lexsmtlib.mli b/src/util/smtlib/lexsmtlib.mli deleted file mode 100644 index a53450a7..00000000 --- a/src/util/smtlib/lexsmtlib.mli +++ /dev/null @@ -1,3 +0,0 @@ -(* Copyright 2014 INIA *) - -val token : Lexing.lexbuf -> Parsesmtlib.token diff --git a/src/util/smtlib/lexsmtlib.mll b/src/util/smtlib/lexsmtlib.mll deleted file mode 100644 index b192c3f3..00000000 --- a/src/util/smtlib/lexsmtlib.mll +++ /dev/null @@ -1,48 +0,0 @@ -{ - (* auto-generated by gt *) - -open Parsesmtlib;; -} - -rule token = parse -| ['\t' ' ' ]+ { token lexbuf } -| ';' (_ # '\n')* { token lexbuf } -| ['\n']+ as str { Smtlib_util.line := (!Smtlib_util.line + (String.length str)); token lexbuf } -| "_" { UNDERSCORE } -| "(" { LPAREN } -| ")" { RPAREN } -| "as" { AS } -| "let" { LET } -| "forall" { FORALL } -| "exists" { EXISTS } -| "!" { EXCLIMATIONPT } -| "set-logic" { SETLOGIC } -| "set-option" { SETOPTION } -| "set-info" { SETINFO } -| "declare-sort" { DECLARESORT } -| "define-sort" { DEFINESORT } -| "declare-fun" { DECLAREFUN } -| "define-fun" { DEFINEFUN } -| "push" { PUSH } -| "pop" { POP } -| "assert" { ASSERT } -| "check-sat" { CHECKSAT } -| "get-assertions" { GETASSERT } -| "get-proof" { GETPROOF } -| "get-unsat-core" { GETUNSATCORE } -| "get-value" { GETVALUE } -| "get-assignment" { GETASSIGN } -| "get-option" { GETOPTION } -| "get-info" { GETINFO } -| "exit" { EXIT } -| '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+ as str { HEXADECIMAL(str) } -| '#' 'b' ['0'-'1']+ as str { BINARY(str) } -| '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|' as str { ASCIIWOR(str) } -| ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+ as str { KEYWORD(str) } -| ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']* as str { SYMBOL(str) } -| '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str { STRINGLIT(str) } -| ( '0' | ['1'-'9'] ['0'-'9']* ) as str { NUMERAL(str) } -| ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) } -| eof { EOF } -| _ {failwith((Lexing.lexeme lexbuf) ^ - ": lexing error on line "^(string_of_int !Smtlib_util.line))}{} diff --git a/src/util/smtlib/parsesmtlib.mly b/src/util/smtlib/parsesmtlib.mly deleted file mode 100644 index 65a14660..00000000 --- a/src/util/smtlib/parsesmtlib.mly +++ /dev/null @@ -1,330 +0,0 @@ -%{ - (* auto-generated by gt *) - -open Smtlib_syntax;; -let parse_error s = - print_string s; - print_string " on line "; - print_int !Smtlib_util.line; - print_string "\n";; - -%} - -%start main - -%token EOF AS ASSERT CHECKSAT DECLAREFUN DECLARESORT DEFINEFUN DEFINESORT EXCLIMATIONPT EXISTS EXIT FORALL GETASSERT GETASSIGN GETINFO GETOPTION GETPROOF GETUNSATCORE GETVALUE LET LPAREN POP PUSH RPAREN SETINFO SETLOGIC SETOPTION UNDERSCORE -%token ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL - - %type main - - %type an_option - - %type attribute - - %type attributevalsexpr_attributevalue_sexpr5 - - %type attributevalue - - %type command - - %type commanddeclarefun_command_sort13 - - %type commanddefinefun_command_sortedvar15 - - %type commanddefinesort_command_symbol11 - - %type commandgetvalue_command_term24 - - %type commands - - %type commands_commands_command30 - - %type identifier - - %type idunderscoresymnum_identifier_numeral33 - - %type infoflag - - %type qualidentifier - - %type sexpr - - %type sexprinparen_sexpr_sexpr41 - - %type sort - - %type sortedvar - - %type sortidsortmulti_sort_sort44 - - %type specconstant - - %type symbol - - %type term - - %type termexclimationpt_term_attribute64 - - %type termexiststerm_term_sortedvar62 - - %type termforallterm_term_sortedvar60 - - %type termletterm_term_varbinding58 - - %type termqualidterm_term_term56 - - %type varbinding - - %type cur_position - - %% - - main: - | commands { Some($1) } - | EOF { None } - - cur_position: - | { Smtlib_util.cur_pd() } - - an_option: - | attribute { AnOptionAttribute(pd_attribute $1, $1) } - - attribute: - | cur_position KEYWORD { AttributeKeyword($1, $2) } - - attribute: - | cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) } - - attributevalue: - | specconstant { AttributeValSpecConst(pd_specconstant $1, $1) } - - attributevalue: - | symbol { AttributeValSymbol(pd_symbol $1, $1) } - - attributevalue: - | cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) } - - command: - | cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) } - - command: - | cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) } - - command: - | cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) } - - command: - | cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) } - - command: - | cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) } - - command: - | cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) } - - command: - | cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) } - - command: - | cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) } - - command: - | cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) } - - command: - | cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) } - - command: - | cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) } - - command: - | cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) } - - command: - | cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) } - - command: - | cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) } - - command: - | cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) } - - command: - | cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) } - - command: - | cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) } - - command: - | cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) } - - command: - | cur_position LPAREN EXIT RPAREN { CommandExit($1) } - - commands: - | commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) } - - identifier: - | symbol { IdSymbol(pd_symbol $1, $1) } - - identifier: - | cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) } - - infoflag: - | cur_position KEYWORD { InfoFlagKeyword($1, $2) } - - qualidentifier: - | identifier { QualIdentifierId(pd_identifier $1, $1) } - - qualidentifier: - | cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) } - - sexpr: - | specconstant { SexprSpecConst(pd_specconstant $1, $1) } - - sexpr: - | symbol { SexprSymbol(pd_symbol $1, $1) } - - sexpr: - | cur_position KEYWORD { SexprKeyword($1, $2) } - - sexpr: - | cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) } - - sort: - | identifier { SortIdentifier(pd_identifier $1, $1) } - - sort: - | cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) } - - sortedvar: - | cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) } - - specconstant: - | cur_position DECIMAL { SpecConstsDec($1, $2) } - - specconstant: - | cur_position NUMERAL { SpecConstNum($1, $2) } - - specconstant: - | cur_position STRINGLIT { SpecConstString($1, $2) } - - specconstant: - | cur_position HEXADECIMAL { SpecConstsHex($1, $2) } - - specconstant: - | cur_position BINARY { SpecConstsBinary($1, $2) } - - symbol: - | cur_position SYMBOL { Symbol($1, $2) } - - symbol: - | cur_position ASCIIWOR { SymbolWithOr($1, $2) } - - term: - | specconstant { TermSpecConst(pd_specconstant $1, $1) } - - term: - | qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) } - - term: - | cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) } - - term: - | cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) } - - term: - | cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) } - - term: - | cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) } - - term: - | cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) } - - varbinding: - | cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) } - - termexclimationpt_term_attribute64: - | attribute { (pd_attribute $1, ($1)::[]) } - - termexclimationpt_term_attribute64: - | attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) } - - termexiststerm_term_sortedvar62: - | sortedvar { (pd_sortedvar $1, ($1)::[]) } - - termexiststerm_term_sortedvar62: - | sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - termforallterm_term_sortedvar60: - | sortedvar { (pd_sortedvar $1, ($1)::[]) } - - termforallterm_term_sortedvar60: - | sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - termletterm_term_varbinding58: - | varbinding { (pd_varbinding $1, ($1)::[]) } - - termletterm_term_varbinding58: - | varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) } - - termqualidterm_term_term56: - | term { (pd_term $1, ($1)::[]) } - - termqualidterm_term_term56: - | term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } - - sortidsortmulti_sort_sort44: - | sort { (pd_sort $1, ($1)::[]) } - - sortidsortmulti_sort_sort44: - | sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } - - sexprinparen_sexpr_sexpr41: - | cur_position { ($1, []) } - - sexprinparen_sexpr_sexpr41: - | sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } - - idunderscoresymnum_identifier_numeral33: - | cur_position NUMERAL { ($1, ($2)::[]) } - - idunderscoresymnum_identifier_numeral33: - | cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) } - - commands_commands_command30: - | cur_position { ($1, []) } - - commands_commands_command30: - | command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) } - - commandgetvalue_command_term24: - | term { (pd_term $1, ($1)::[]) } - - commandgetvalue_command_term24: - | term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } - - commanddefinefun_command_sortedvar15: - | cur_position { ($1, []) } - - commanddefinefun_command_sortedvar15: - | sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } - - commanddeclarefun_command_sort13: - | cur_position { ($1, []) } - - commanddeclarefun_command_sort13: - | sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } - - commanddefinesort_command_symbol11: - | cur_position { ($1, []) } - - commanddefinesort_command_symbol11: - | symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) } - - attributevalsexpr_attributevalue_sexpr5: - | cur_position { ($1, []) } - - attributevalsexpr_attributevalue_sexpr5: - | sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } diff --git a/src/util/smtlib/smtlib.ml b/src/util/smtlib/smtlib.ml deleted file mode 100644 index 49057058..00000000 --- a/src/util/smtlib/smtlib.ml +++ /dev/null @@ -1,112 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -open Smtlib_syntax - -module F = Expr -module T = Cnf.S - -exception Bad_arity of string -exception Unknown_command -exception Incomplete_translation - -(* Environment *) -let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; -Hashtbl.add env "true" T.f_true;; -Hashtbl.add env "false" T.f_false;; - -let get_atom s = - try - Hashtbl.find env s - with Not_found -> - let f = T.make_atom (F.fresh ()) in - Hashtbl.add env s f; - f - -(* Term translation *) -let translate_const = function - | SpecConstsDec(_, s) - | SpecConstNum(_, s) - | SpecConstString(_, s) - | SpecConstsHex(_, s) - | SpecConstsBinary(_, s) -> s - -let translate_symbol = function - | Symbol(_, s) - | SymbolWithOr(_, s) -> s - -let translate_id = function - | IdSymbol(_, s) -> translate_symbol s - | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation - -let translate_qualid = function - | QualIdentifierId(_, id) -> translate_id id - | QualIdentifierAs(_, id, s) -> raise Incomplete_translation - -let left_assoc s f = function - | x :: r -> List.fold_left f x r - | _ -> raise (Bad_arity s) - -let rec right_assoc s f = function - | [] -> raise (Bad_arity s) - | [x] -> x - | x :: r -> f x (right_assoc s f r) - -let translate_atom = function - | TermSpecConst(_, const) -> translate_const const - | TermQualIdentifier(_, id) -> translate_qualid id - | _ -> raise Incomplete_translation - -let rec translate_term = function - | TermQualIdTerm(_, f, (_, l)) -> - begin match (translate_qualid f) with - | "=" -> - begin match (List.map translate_atom l) with - | [a; b] -> T.make_atom (F.mk_eq a b) - | _ -> assert false - end - | s -> - begin match s, (List.map translate_term l) with - (* CORE theory translation - 'distinct','ite' not yet implemented *) - | "not", [e] -> T.make_not e - | "not", _ -> raise (Bad_arity "not") - | "and", l -> T.make_and l - | "or", l -> T.make_or l - | "xor" as s, l -> left_assoc s T.make_xor l - | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> - Format.printf "unknown : %s@." s; - raise Unknown_command - end - end - | e -> (get_atom (translate_atom e)) - -(* Command Translation *) -let translate_command = function - | CommandDeclareFun(_, s, (_, []), _) -> - None - | CommandAssert(_, t) -> - Some (translate_term t) - | _ -> None - -let rec translate_command_list acc = function - | [] -> acc - | c :: r -> - begin match translate_command c with - | None -> translate_command_list acc r - | Some t -> translate_command_list (t :: acc) r - end - -let translate = function - | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) - | None -> [] - -let parse file = - let f = open_in file in - let lexbuf = Lexing.from_channel f in - let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in - close_in f; - translate commands diff --git a/src/util/smtlib/smtlib_syntax.ml b/src/util/smtlib/smtlib_syntax.ml deleted file mode 100644 index 6f33e693..00000000 --- a/src/util/smtlib/smtlib_syntax.ml +++ /dev/null @@ -1,229 +0,0 @@ -(* auto-generated by gt *) - -open Smtlib_util;; - -type dummy = Dummy -and an_option = | AnOptionAttribute of pd * attribute -and attribute = | AttributeKeyword of pd * string | AttributeKeywordValue of pd * string * attributevalue -and attributevalue = | AttributeValSpecConst of pd * specconstant | AttributeValSymbol of pd * symbol | AttributeValSexpr of pd * attributevalsexpr_attributevalue_sexpr5 -and command = | CommandSetLogic of pd * symbol | CommandSetOption of pd * an_option | CommandSetInfo of pd * attribute | CommandDeclareSort of pd * symbol * string | CommandDefineSort of pd * symbol * commanddefinesort_command_symbol11 * sort | CommandDeclareFun of pd * symbol * commanddeclarefun_command_sort13 * sort | CommandDefineFun of pd * symbol * commanddefinefun_command_sortedvar15 * sort * term | CommandPush of pd * string | CommandPop of pd * string | CommandAssert of pd * term | CommandCheckSat of pd | CommandGetAssert of pd | CommandGetProof of pd | CommandGetUnsatCore of pd | CommandGetValue of pd * commandgetvalue_command_term24 | CommandGetAssign of pd | CommandGetOption of pd * string | CommandGetInfo of pd * infoflag | CommandExit of pd -and commands = | Commands of pd * commands_commands_command30 -and identifier = | IdSymbol of pd * symbol | IdUnderscoreSymNum of pd * symbol * idunderscoresymnum_identifier_numeral33 -and infoflag = | InfoFlagKeyword of pd * string -and qualidentifier = | QualIdentifierId of pd * identifier | QualIdentifierAs of pd * identifier * sort -and sexpr = | SexprSpecConst of pd * specconstant | SexprSymbol of pd * symbol | SexprKeyword of pd * string | SexprInParen of pd * sexprinparen_sexpr_sexpr41 -and sort = | SortIdentifier of pd * identifier | SortIdSortMulti of pd * identifier * sortidsortmulti_sort_sort44 -and sortedvar = | SortedVarSymSort of pd * symbol * sort -and specconstant = | SpecConstsDec of pd * string | SpecConstNum of pd * string | SpecConstString of pd * string | SpecConstsHex of pd * string | SpecConstsBinary of pd * string -and symbol = | Symbol of pd * string | SymbolWithOr of pd * string -and term = | TermSpecConst of pd * specconstant | TermQualIdentifier of pd * qualidentifier | TermQualIdTerm of pd * qualidentifier * termqualidterm_term_term56 | TermLetTerm of pd * termletterm_term_varbinding58 * term | TermForAllTerm of pd * termforallterm_term_sortedvar60 * term | TermExistsTerm of pd * termexiststerm_term_sortedvar62 * term | TermExclimationPt of pd * term * termexclimationpt_term_attribute64 -and varbinding = | VarBindingSymTerm of pd * symbol * term -and termexclimationpt_term_attribute64 = pd * ( attribute) list -and termexiststerm_term_sortedvar62 = pd * ( sortedvar) list -and termforallterm_term_sortedvar60 = pd * ( sortedvar) list -and termletterm_term_varbinding58 = pd * ( varbinding) list -and termqualidterm_term_term56 = pd * ( term) list -and sortidsortmulti_sort_sort44 = pd * ( sort) list -and sexprinparen_sexpr_sexpr41 = pd * ( sexpr) list -and idunderscoresymnum_identifier_numeral33 = pd * ( string) list -and commands_commands_command30 = pd * ( command) list -and commandgetvalue_command_term24 = pd * ( term) list -and commanddefinefun_command_sortedvar15 = pd * ( sortedvar) list -and commanddeclarefun_command_sort13 = pd * ( sort) list -and commanddefinesort_command_symbol11 = pd * ( symbol) list -and attributevalsexpr_attributevalue_sexpr5 = pd * ( sexpr) list;; - -(* pd stands for pos (position) and extradata *) -let dummy () = () -and pd_an_option = function - | AnOptionAttribute(d,_) -> d - -and pd_attribute = function - | AttributeKeyword(d,_) -> d - - | AttributeKeywordValue(d,_,_) -> d - -and pd_attributevalue = function - | AttributeValSpecConst(d,_) -> d - - | AttributeValSymbol(d,_) -> d - - | AttributeValSexpr(d,_) -> d - -and pd_command = function - | CommandSetLogic(d,_) -> d - - | CommandSetOption(d,_) -> d - - | CommandSetInfo(d,_) -> d - - | CommandDeclareSort(d,_,_) -> d - - | CommandDefineSort(d,_,_,_) -> d - - | CommandDeclareFun(d,_,_,_) -> d - - | CommandDefineFun(d,_,_,_,_) -> d - - | CommandPush(d,_) -> d - - | CommandPop(d,_) -> d - - | CommandAssert(d,_) -> d - - | CommandCheckSat(d) -> d - - | CommandGetAssert(d) -> d - - | CommandGetProof(d) -> d - - | CommandGetUnsatCore(d) -> d - - | CommandGetValue(d,_) -> d - - | CommandGetAssign(d) -> d - - | CommandGetOption(d,_) -> d - - | CommandGetInfo(d,_) -> d - - | CommandExit(d) -> d - -and pd_commands = function - | Commands(d,_) -> d - -and pd_identifier = function - | IdSymbol(d,_) -> d - - | IdUnderscoreSymNum(d,_,_) -> d - -and pd_infoflag = function - | InfoFlagKeyword(d,_) -> d - -and pd_qualidentifier = function - | QualIdentifierId(d,_) -> d - - | QualIdentifierAs(d,_,_) -> d - -and pd_sexpr = function - | SexprSpecConst(d,_) -> d - - | SexprSymbol(d,_) -> d - - | SexprKeyword(d,_) -> d - - | SexprInParen(d,_) -> d - -and pd_sort = function - | SortIdentifier(d,_) -> d - - | SortIdSortMulti(d,_,_) -> d - -and pd_sortedvar = function - | SortedVarSymSort(d,_,_) -> d - -and pd_specconstant = function - | SpecConstsDec(d,_) -> d - - | SpecConstNum(d,_) -> d - - | SpecConstString(d,_) -> d - - | SpecConstsHex(d,_) -> d - - | SpecConstsBinary(d,_) -> d - -and pd_symbol = function - | Symbol(d,_) -> d - - | SymbolWithOr(d,_) -> d - -and pd_term = function - | TermSpecConst(d,_) -> d - - | TermQualIdentifier(d,_) -> d - - | TermQualIdTerm(d,_,_) -> d - - | TermLetTerm(d,_,_) -> d - - | TermForAllTerm(d,_,_) -> d - - | TermExistsTerm(d,_,_) -> d - - | TermExclimationPt(d,_,_) -> d - -and pd_varbinding = function - | VarBindingSymTerm(d,_,_) -> d - -and pd_termexclimationpt_term_attribute64 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termexiststerm_term_sortedvar62 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termforallterm_term_sortedvar60 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termletterm_term_varbinding58 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_termqualidterm_term_term56 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_sortidsortmulti_sort_sort44 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_sexprinparen_sexpr_sexpr41 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_idunderscoresymnum_identifier_numeral33 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commands_commands_command30 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commandgetvalue_command_term24 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddefinefun_command_sortedvar15 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddeclarefun_command_sort13 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_commanddefinesort_command_symbol11 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d - -and pd_attributevalsexpr_attributevalue_sexpr5 = function - | (d,[]) -> d - - | (d,( _ )::f1239o2) -> d -;; -let pd e = pd_commands e;; diff --git a/src/util/smtlib/smtlib_syntax.mli b/src/util/smtlib/smtlib_syntax.mli deleted file mode 100644 index 05ad8cc7..00000000 --- a/src/util/smtlib/smtlib_syntax.mli +++ /dev/null @@ -1,123 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -type dummy = Dummy -and an_option = AnOptionAttribute of Smtlib_util.pd * attribute -and attribute = - AttributeKeyword of Smtlib_util.pd * string - | AttributeKeywordValue of Smtlib_util.pd * string * attributevalue -and attributevalue = - AttributeValSpecConst of Smtlib_util.pd * specconstant - | AttributeValSymbol of Smtlib_util.pd * symbol - | AttributeValSexpr of Smtlib_util.pd * - attributevalsexpr_attributevalue_sexpr5 -and command = - CommandSetLogic of Smtlib_util.pd * symbol - | CommandSetOption of Smtlib_util.pd * an_option - | CommandSetInfo of Smtlib_util.pd * attribute - | CommandDeclareSort of Smtlib_util.pd * symbol * string - | CommandDefineSort of Smtlib_util.pd * symbol * - commanddefinesort_command_symbol11 * sort - | CommandDeclareFun of Smtlib_util.pd * symbol * - commanddeclarefun_command_sort13 * sort - | CommandDefineFun of Smtlib_util.pd * symbol * - commanddefinefun_command_sortedvar15 * sort * term - | CommandPush of Smtlib_util.pd * string - | CommandPop of Smtlib_util.pd * string - | CommandAssert of Smtlib_util.pd * term - | CommandCheckSat of Smtlib_util.pd - | CommandGetAssert of Smtlib_util.pd - | CommandGetProof of Smtlib_util.pd - | CommandGetUnsatCore of Smtlib_util.pd - | CommandGetValue of Smtlib_util.pd * commandgetvalue_command_term24 - | CommandGetAssign of Smtlib_util.pd - | CommandGetOption of Smtlib_util.pd * string - | CommandGetInfo of Smtlib_util.pd * infoflag - | CommandExit of Smtlib_util.pd -and commands = Commands of Smtlib_util.pd * commands_commands_command30 -and identifier = - IdSymbol of Smtlib_util.pd * symbol - | IdUnderscoreSymNum of Smtlib_util.pd * symbol * - idunderscoresymnum_identifier_numeral33 -and infoflag = InfoFlagKeyword of Smtlib_util.pd * string -and qualidentifier = - QualIdentifierId of Smtlib_util.pd * identifier - | QualIdentifierAs of Smtlib_util.pd * identifier * sort -and sexpr = - SexprSpecConst of Smtlib_util.pd * specconstant - | SexprSymbol of Smtlib_util.pd * symbol - | SexprKeyword of Smtlib_util.pd * string - | SexprInParen of Smtlib_util.pd * sexprinparen_sexpr_sexpr41 -and sort = - SortIdentifier of Smtlib_util.pd * identifier - | SortIdSortMulti of Smtlib_util.pd * identifier * - sortidsortmulti_sort_sort44 -and sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort -and specconstant = - SpecConstsDec of Smtlib_util.pd * string - | SpecConstNum of Smtlib_util.pd * string - | SpecConstString of Smtlib_util.pd * string - | SpecConstsHex of Smtlib_util.pd * string - | SpecConstsBinary of Smtlib_util.pd * string -and symbol = - Symbol of Smtlib_util.pd * string - | SymbolWithOr of Smtlib_util.pd * string -and term = - TermSpecConst of Smtlib_util.pd * specconstant - | TermQualIdentifier of Smtlib_util.pd * qualidentifier - | TermQualIdTerm of Smtlib_util.pd * qualidentifier * - termqualidterm_term_term56 - | TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term - | TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term - | TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term - | TermExclimationPt of Smtlib_util.pd * term * - termexclimationpt_term_attribute64 -and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term -and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list -and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list -and termforallterm_term_sortedvar60 = Smtlib_util.pd * sortedvar list -and termletterm_term_varbinding58 = Smtlib_util.pd * varbinding list -and termqualidterm_term_term56 = Smtlib_util.pd * term list -and sortidsortmulti_sort_sort44 = Smtlib_util.pd * sort list -and sexprinparen_sexpr_sexpr41 = Smtlib_util.pd * sexpr list -and idunderscoresymnum_identifier_numeral33 = Smtlib_util.pd * string list -and commands_commands_command30 = Smtlib_util.pd * command list -and commandgetvalue_command_term24 = Smtlib_util.pd * term list -and commanddefinefun_command_sortedvar15 = Smtlib_util.pd * sortedvar list -and commanddeclarefun_command_sort13 = Smtlib_util.pd * sort list -and commanddefinesort_command_symbol11 = Smtlib_util.pd * symbol list -and attributevalsexpr_attributevalue_sexpr5 = Smtlib_util.pd * sexpr list -val dummy : unit -> unit -val pd_an_option : an_option -> Smtlib_util.pd -val pd_attribute : attribute -> Smtlib_util.pd -val pd_attributevalue : attributevalue -> Smtlib_util.pd -val pd_command : command -> Smtlib_util.pd -val pd_commands : commands -> Smtlib_util.pd -val pd_identifier : identifier -> Smtlib_util.pd -val pd_infoflag : infoflag -> Smtlib_util.pd -val pd_qualidentifier : qualidentifier -> Smtlib_util.pd -val pd_sexpr : sexpr -> Smtlib_util.pd -val pd_sort : sort -> Smtlib_util.pd -val pd_sortedvar : sortedvar -> Smtlib_util.pd -val pd_specconstant : specconstant -> Smtlib_util.pd -val pd_symbol : symbol -> Smtlib_util.pd -val pd_term : term -> Smtlib_util.pd -val pd_varbinding : varbinding -> Smtlib_util.pd -val pd_termexclimationpt_term_attribute64 : 'a * 'b list -> 'a -val pd_termexiststerm_term_sortedvar62 : 'a * 'b list -> 'a -val pd_termforallterm_term_sortedvar60 : 'a * 'b list -> 'a -val pd_termletterm_term_varbinding58 : 'a * 'b list -> 'a -val pd_termqualidterm_term_term56 : 'a * 'b list -> 'a -val pd_sortidsortmulti_sort_sort44 : 'a * 'b list -> 'a -val pd_sexprinparen_sexpr_sexpr41 : 'a * 'b list -> 'a -val pd_idunderscoresymnum_identifier_numeral33 : 'a * 'b list -> 'a -val pd_commands_commands_command30 : 'a * 'b list -> 'a -val pd_commandgetvalue_command_term24 : 'a * 'b list -> 'a -val pd_commanddefinefun_command_sortedvar15 : 'a * 'b list -> 'a -val pd_commanddeclarefun_command_sort13 : 'a * 'b list -> 'a -val pd_commanddefinesort_command_symbol11 : 'a * 'b list -> 'a -val pd_attributevalsexpr_attributevalue_sexpr5 : 'a * 'b list -> 'a -val pd : commands -> Smtlib_util.pd diff --git a/src/util/smtlib/smtlib_util.ml b/src/util/smtlib/smtlib_util.ml deleted file mode 100644 index 8e1da4d5..00000000 --- a/src/util/smtlib/smtlib_util.ml +++ /dev/null @@ -1,12 +0,0 @@ -(* auto-generated by gt *) - -(* no extra data from grammar file. *) -type extradata = unit;; -let initial_data() = ();; - -let file = ref "stdin";; -let line = ref 1;; -type pos = int;; -let string_of_pos p = "line "^(string_of_int p);; -let cur_pd() = (!line, initial_data());; (* "pd": pos + extradata *) -type pd = pos * extradata;; diff --git a/src/util/smtlib/smtlib_util.mli b/src/util/smtlib/smtlib_util.mli deleted file mode 100644 index 24ff66b8..00000000 --- a/src/util/smtlib/smtlib_util.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -type extradata = unit -val initial_data : unit -> unit -val file : string ref -val line : int ref -type pos = int -val string_of_pos : int -> string -val cur_pd : unit -> int * unit -type pd = pos * extradata diff --git a/src/util/type.ml b/src/util/type.ml new file mode 100644 index 00000000..788328a3 --- /dev/null +++ b/src/util/type.ml @@ -0,0 +1,25 @@ + +(** Typechecking of terms from Dolmen.Term.t + This module defines the requirements for typing expre'ssions from dolmen. *) + +module type S = sig + + type atom + (** The type of atoms that will be fed to tha sovler. *) + + exception Typing_error of string * Dolmen.Term.t + (** Exception raised during typechecking. *) + + val decl : Dolmen.Id.t -> Dolmen.Term.t -> unit + (** New declaration, i.e an identifier and its type. *) + + val def : Dolmen.Id.t -> Dolmen.Term.t -> unit + (** New definition, i.e an identifier and the term it is equal to. *) + + val consequent : Dolmen.Term.t -> atom list list + val antecedent : Dolmen.Term.t -> atom list list + (** Parse a formula, and return a cnf ready to be given to the solver. + Consequent is for hypotheses (left of the sequent), while antecedent + is for goals (i.e formulas on the right of a sequent). *) + +end diff --git a/tests/test_api.ml b/tests/test_api.ml index 74f36e37..75ae7fd2 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -6,18 +6,11 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) -module F = Expr -module T = Cnf.S +module F = Expr_sat +module T = Tseitin.Make(F) let (|>) x f = f x -type solver = Smt | Mcsat -let solver_list = [ - "smt", Smt; - "mcsat", Mcsat; -] - -let solver = ref Smt let p_check = ref false let time_limit = ref 300. let size_limit = ref 1000_000_000. @@ -32,59 +25,38 @@ let set_flag opt arg flag l = flag := List.assoc arg l with Not_found -> invalid_arg (error_msg opt arg l) -let set_solver s = set_flag "Solver" s solver solver_list let usage = "Usage : test_api [options]" let argspec = Arg.align [ "-check", Arg.Set p_check, " Build, check and print the proof (if output is set), if unsat"; - "-s", Arg.String set_solver, - "{smt,mcsat} Sets the solver to use (default smt)"; "-v", Arg.Int (fun i -> Log.set_debug i), " Sets the debug verbose level"; ] -let string_of_solver = function - | Mcsat -> "mcsat" - | Smt -> "smt" - type solver_res = | R_sat | R_unsat +exception Incorrect_model + module type BASIC_SOLVER = sig val solve : ?assumptions:F.t list -> unit -> solver_res val assume : ?tag:int -> F.t list list -> unit end -exception Incorrect_model - -let mk_solver (s:solver): (module BASIC_SOLVER) = - match s with - | Smt -> - let module S = struct - include Smt.Make(struct end) - let solve ?assumptions ()= match solve ?assumptions() with - | Sat _ -> - R_sat - | Unsat us -> - let p = us.Solver_intf.get_proof () in - Proof.check p; - R_unsat - end - in (module S) - | Mcsat -> - let module S = struct - include Mcsat.Make(struct end) - let solve ?assumptions ()= match solve ?assumptions() with - | Sat _ -> - R_sat - | Unsat us -> - let p = us.Solver_intf.get_proof () in - Proof.check p; - R_unsat - end - in (module S) +let mk_solver (): (module BASIC_SOLVER) = + let module S = struct + include Sat.Make(struct end) + let solve ?assumptions ()= match solve ?assumptions() with + | Sat _ -> + R_sat + | Unsat us -> + let p = us.Solver_intf.get_proof () in + Proof.check p; + R_unsat + end + in (module S) exception Error of string @@ -102,19 +74,19 @@ module Test = struct } let mk_test name l = {name; actions=l} - let assume l = A_assume (List.map (List.map F.mk_prop) l) + let assume l = A_assume (List.map (List.map F.make) l) let assume1 c = assume [c] let solve ?(assumptions=[]) e = - let assumptions = List.map F.mk_prop assumptions in + let assumptions = List.map F.make assumptions in A_solve (assumptions, e) type result = | Pass | Fail of string - let run (solver:solver) (t:t): result = + let run (t:t): result = (* Interesting stuff happening *) - let (module S: BASIC_SOLVER) = mk_solver solver in + let (module S: BASIC_SOLVER) = mk_solver () in try List.iter (function @@ -190,17 +162,14 @@ let main () = Arg.parse argspec (fun _ -> ()) usage; let failed = ref false in List.iter - (fun solver -> - List.iter - (fun test -> - Printf.printf "(%-6s) %-10s... %!" (string_of_solver solver) test.Test.name; - match Test.run solver test with - | Test.Pass -> Printf.printf "ok\n%!" - | Test.Fail msg -> - failed := true; - Printf.printf "fail (%s)\n%!" msg) - Test.suite) - [Smt; Mcsat]; + (fun test -> + Printf.printf "%-10s... %!" test.Test.name; + match Test.run test with + | Test.Pass -> Printf.printf "ok\n%!" + | Test.Fail msg -> + failed := true; + Printf.printf "fail (%s)\n%!" msg) + Test.suite; if !failed then exit 1 let () = main() diff --git a/tests/unsat/test-012.smt2 b/tests/unsat/test-012.smt2 new file mode 100644 index 00000000..1a2946b1 --- /dev/null +++ b/tests/unsat/test-012.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (not (= (f a) (f b))))) +(check-sat) diff --git a/tests/unsat/test-013.smt2 b/tests/unsat/test-013.smt2 new file mode 100644 index 00000000..d67c8f07 --- /dev/null +++ b/tests/unsat/test-013.smt2 @@ -0,0 +1,2 @@ +(assert (and (= a b) (not (p a)) (p b))) +(check-sat)