Merge branch 'wip-basic-smt'

.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

.travis.yml

@@ -1,10 +1,12 @@
 language: c
 env:
-  - OCAML_VERSION=4.00.1
+  - RUN_TEST=false OCAML_VERSION=4.00.1
-  - OCAML_VERSION=4.01.0
+  - RUN_TEST=false OCAML_VERSION=4.01.0
-  - OCAML_VERSION=4.02.3
+  - RUN_TEST=true OCAML_VERSION=4.02.3
-  - OCAML_VERSION=4.03.0
+  - RUN_TEST=true OCAML_VERSION=4.03.0
-  - OCAML_VERSION=4.03.0+flambda
+  - 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

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"
+)

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 remove $(NAME_OCAMLFIND) || true
-	ocamlfind install msat $(TO_INSTALL)
+	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

_tags

@@ -9,16 +9,22 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/core>: include
 <src/solver>: include
 <src/backend>: include
-<src/example>: include
 <src/util>: include
-<src/util/smtlib>: include
+<src/sat>: include
+<src/smt>: include
+<src/mcsat>: include
 
 # Pack options
 <src/core/*.cmx>: for-pack(Msat)
 <src/solver/*.cmx>: for-pack(Msat)
 <src/backend/*.cmx>: for-pack(Msat)
 <src/util/*.cmx>: for-pack(Msat)
-<src/example/*.cmx>: for-pack(Msat)
+
+# Testing dependencies
+<src/main.*>: package(dolmen)
+<src/util/type.*>: package(dolmen)
+<src/sat/type_sat.*>: package(dolmen)
+<src/smt/type_smt.*>: package(dolmen)
 
 # more warnings
 <src/**/*.ml>: warn_K, warn_Y, warn_X

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
+}

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}}}

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}

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
+  module Term : sig
-  (** Formula constants. A valid formula should never be physically equal to [dummy] *)
 
-  val fresh : unit -> Formula.t
+    type t
-  (** Returns a fresh litteral, distinct from any other literal (used in cnf conversion) *)
+    (** The type of terms *)
 
-  val neg : Formula.t -> Formula.t
+    val hash : t -> int
-  (** Formula negation *)
+    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
 

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
 

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: @[<hov>%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 *)
+          match th_eval first with
-          enqueue_bool first (decision_level ()) (Bcp c)
+          | 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 ->

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 =
+  let pp_reason fmt = function
-    match a.var.v_level, a.var.reason with
+    | n, _ when n < 0 ->
-    | n, _ when n < 0 -> sprintf "%%"
+      Format.fprintf fmt "%%"
-    | n, None   -> sprintf "%d" n
+    | n, None ->
-    | n, Some Decision   -> sprintf "@@%d" n
+      Format.fprintf fmt "%d" n
-    | n, Some Bcp c -> sprintf "->%d/%s" n c.name
+    | n, Some Decision ->
-    | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl
+      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 =
+  let pp_level fmt a =
-    if a.is_true then sprintf "[T%s]" (level a)
+    pp_reason fmt (a.var.v_level, a.var.reason)
-    else if a.neg.is_true then sprintf "[F%s]" (level a)
+
-    else "[]"
+  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 " ->@ @[<hov>%a@]" E.Term.print t
 
   let pp_lit out v =
-    Format.fprintf out "%d [lit:%a%a]"
+    Format.fprintf out "%d [lit:@[<hov>%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]@ "
+    Format.fprintf out "%s%d%a[atom:@[<hov>%a@]]@ "
-      (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
+      (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

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

src/example/cc.ml

@@ -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

src/example/cc.mli

@@ -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

src/example/expr.ml

@@ -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
-

src/example/expr.mli

@@ -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

src/example/mcsat.ml

@@ -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

src/example/sat.ml

@@ -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

src/example/sat.mli

@@ -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
-

src/example/sig.mli

@@ -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

src/example/smt.ml

@@ -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

src/example/smt.mli

@@ -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
-

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 *)
+let file = ref ""
-(* Types for input/output languages *)
+let p_cnf = ref false
-type sat_input =
+let p_check = ref false
-  | Auto
+let p_proof_print = ref false
-  | Dimacs
+let p_unsat_core = ref false
-  | Smtlib
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
 
-type sat_output =
+module P =
-  | Standard (* Only output problem status *)
+  Dolmen.Logic.Make(Dolmen.ParseLocation)
-  | Dedukti
+    (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement)
-  | Dot
 
-type solver =
+module type S = sig
-  | Smt
+  val do_task : Dolmen.Statement.t -> unit
-  | Mcsat
+end
 
-let input = ref Auto
+module Make
-let output = ref Standard
+    (S : External.S)
-let solver = ref Smt
+    (T : Type.S with type atom := S.atom)
+= struct
 
-let input_list = [
+  let hyps = ref []
-  "auto", Auto;
+
-  "dimacs", Dimacs;
+  let do_task s =
-  "smtlib", Smtlib;
+    match s.Dolmen.Statement.descr with
-]
+    | Dolmen.Statement.Def (id, t) -> T.def id t
-let output_list = [
+    | Dolmen.Statement.Decl (id, t) -> T.decl id t
-  "dot", Dot;
+    | Dolmen.Statement.Consequent t ->
-  "dk", Dedukti;
+      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;
+  "sat", (module Sat : S);
-  "mcsat", Mcsat;
+  "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),
     "<s>[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
+  let lang, input = P.parse_file !file in
-  if !p_cnf then
+  let module S = (val !solver : S) in
-    print_cnf cnf;
+  List.iter S.do_task input;
-  match !solver with
+  (* Small hack for dimacs, which do not output a "Prove" statement *)
-  | Smt ->
+  begin match lang with
-    Smt.assume cnf;
+    | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat ()
-    let res = Smt.solve () in
+    | _ -> ()
-    Gc.delete_alarm al;
+  end;
-    begin match res with
+  Gc.delete_alarm al;
-      | 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 () =
   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
 

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

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
+

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)
+

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
+

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
+

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
-

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
+# Auxiliary
-example/Sat
+util/Hashcons
-example/Smt
-

src/msat_sat.mlpack

@@ -0,0 +1 @@
+Sat

src/msat_sat.odocl

@@ -0,0 +1,3 @@
+
+smt/Sat
+

src/msat_smt.mlpack

@@ -0,0 +1,3 @@
+Smt
+Cc
+Explanation

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
+

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)
+

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 *)
+

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)
+

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

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
+

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
+

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

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

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 "}"

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

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 "@[<hov 0>%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 = "<dummy>"; id_type = Type; }
+
+  let ty =
+    { ty = TyVar id_ttype; ty_hash = -1; }
+
+  let id =
+    { index = -2; id_name = "<dummy>"; 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)
+

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
+

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)
+

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
+

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 "<tType>"
+  | 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))
+

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
+

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]

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

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

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

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

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

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 *)

src/util/.merlin

@@ -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/

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
+

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

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

src/util/parsedimacs.ml

@@ -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

src/util/smtlib/.merlin

@@ -1,9 +0,0 @@
-S ./
-S ../
-S ../../sat/
-
-B ../../_build/
-B ../../_build/util/
-B ../../_build/util/smtlib/
-B ../../_build/sat/
-B ../../_build/smt/

src/util/smtlib/lexsmtlib.mli

@@ -1,3 +0,0 @@
-(* Copyright 2014 INIA *)
-
-val token : Lexing.lexbuf -> Parsesmtlib.token

src/util/smtlib/lexsmtlib.mll

@@ -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))}{}

src/util/smtlib/parsesmtlib.mly

@@ -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 <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL
-
-                %type <Smtlib_syntax.commands option> main
-
-                                                      %type <Smtlib_syntax.an_option> an_option
-
-                                                                                      %type <Smtlib_syntax.attribute> attribute
-
-                                                                                                                      %type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5
-
-                                                                                                                                                                                    %type <Smtlib_syntax.attributevalue> attributevalue
-
-                                                                                                                                                                                                                         %type <Smtlib_syntax.command> command
-
-                                                                                                                                                                                                                                                       %type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13
-
-                                                                                                                                                                                                                                                                                                              %type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15
-
-                                                                                                                                                                                                                                                                                                                                                                         %type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                  %type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       %type <Smtlib_syntax.commands> commands
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      %type <Smtlib_syntax.commands_commands_command30> commands_commands_command30
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        %type <Smtlib_syntax.identifier> identifier
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         %type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       %type <Smtlib_syntax.infoflag> infoflag
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      %type <Smtlib_syntax.qualidentifier> qualidentifier
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           %type <Smtlib_syntax.sexpr> sexpr
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       %type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        %type <Smtlib_syntax.sort> sort
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   %type <Smtlib_syntax.sortedvar> sortedvar
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   %type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     %type <Smtlib_syntax.specconstant> specconstant
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        %type <Smtlib_syntax.symbol> symbol
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     %type <Smtlib_syntax.term> term
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                %type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         %type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               %type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     %type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         %type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          %type <Smtlib_syntax.varbinding> varbinding
-
-                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                           %type <Smtlib_util.pd> 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)) }

src/util/smtlib/smtlib.ml

@@ -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

src/util/smtlib/smtlib_syntax.ml

@@ -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;;

src/util/smtlib/smtlib_syntax.mli

@@ -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

src/util/smtlib/smtlib_util.ml

@@ -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;;

src/util/smtlib/smtlib_util.mli

@@ -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

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

tests/test_api.ml

@@ -6,18 +6,11 @@ Copyright 2014 Simon Cruanes
 
 (* Tests that require the API *)
 
-module F = Expr
+module F = Expr_sat
-module T = Cnf.S
+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),
     "<lvl> 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 (): (module BASIC_SOLVER) =
-
+  let module S = struct
-let mk_solver (s:solver): (module BASIC_SOLVER) =
+    include Sat.Make(struct end)
-  match s with
+    let solve ?assumptions ()= match solve ?assumptions() with
-    | Smt ->
+      | Sat _ ->
-      let module S = struct
+        R_sat
-        include Smt.Make(struct end)
+      | Unsat us ->
-        let solve ?assumptions ()= match solve ?assumptions() with
+        let p = us.Solver_intf.get_proof () in
-          | Sat _ ->
+        Proof.check p;
-            R_sat
+        R_unsat
-          | Unsat us ->
+  end
-            let p = us.Solver_intf.get_proof () in
+  in (module S)
-            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)
 
 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 ->
+    (fun test ->
-       List.iter
+       Printf.printf "%-10s... %!" test.Test.name;
-         (fun test ->
+       match Test.run test with
-            Printf.printf "(%-6s) %-10s... %!" (string_of_solver solver) test.Test.name;
+       | Test.Pass -> Printf.printf "ok\n%!"
-            match Test.run solver test with
+       | Test.Fail msg ->
-              | Test.Pass -> Printf.printf "ok\n%!"
+         failed := true;
-              | Test.Fail msg ->
+         Printf.printf "fail (%s)\n%!" msg)
-                failed := true;
+    Test.suite;
-                Printf.printf "fail (%s)\n%!" msg)
-         Test.suite)
-    [Smt; Mcsat];
   if !failed then exit 1
 
 let () = main()

tests/unsat/test-012.smt2

@@ -0,0 +1,2 @@
+(assert (and (= a b) (not (= (f a) (f b)))))
+(check-sat)

tests/unsat/test-013.smt2

@@ -0,0 +1,2 @@
+(assert (and (= a b) (not (p a)) (p b)))
+(check-sat)