wip: have a proper smtlib parser

Makefile

@@ -1,36 +1,22 @@
 # copyright (c) 2014, guillaume bury
 # copyright (c) 2017, simon cruanes
 
-BIN=main.native
-TEST_BIN=tests/test_api.native
+.PHONY: clean build build-dev
 
 NAME=msat
 J?=3
 TIMEOUT?=30
-TARGETS=src/bin/main.exe
+TARGETS=src/main/main.exe
 OPTS= -j $(J)
 
-LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
-
-all: build test
-all-dev: build-dev test
-
 build:
-	jbuilder build $(OPTS) @install
+	jbuilder build $(TARGETS) $(OPTS)
+
+build-install:
+	jbuilder build @install
 
 build-dev:
-	jbuilder build $(OPTS) @install --dev
-
-build-test: build
-	jbuilder build $(OPTS) src/main_test/main_test.exe
-
-test: build-test
-	@echo "run API tests…"
-	jbuilder runtest
-	@echo "run benchmarks…"
-	@/usr/bin/time -f "%e" ./tests/run sat
-	#@/usr/bin/time -f "%e" ./tests/run smt
-	# @/usr/bin/time -f "%e" ./tests/run mcsat
+	jbuilder build $(TARGETS) $(OPTS) --dev
 
 enable_log:
 	cd src/core; ln -sf log_real.ml log.ml
@@ -63,9 +49,9 @@ reindent: ocp-indent
 	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: "
 	@find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i
 
-WATCH=all
+WATCH=build
 watch:
-	while find src/ tests/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
+	while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
 		echo "============ at `date` ==========" ; \
 		make $(WATCH); \
 	done

README.md

@@ -1,6 +1,6 @@
-# CDCL [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL)
+# dagon [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL)
 
-CDCL is an OCaml library with a functor to create SMT solvers following
+Dagon is an OCaml library with a functor to create SMT solvers following
 the CDCL(T) approach (so called "lazy SMT").
 
 It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero)
@@ -9,16 +9,16 @@ and its fork [mSAT](https://github.com/gbury/msat).
 
 ## Documentation
 
-See https://c-cube.github.io/cdcl/
+See https://c-cube.github.io/dagon/
 
 ## Installation
 
 ### Via opam
 
-Once the package is on [opam](http://opam.ocaml.org), just `opam install cdcl`.
+Once the package is on [opam](http://opam.ocaml.org), just `opam install dagon`.
 For the development version, use:
 
-    opam pin add msat https://github.com/c-cube/cdcl.git
+    opam pin add dagon https://github.com/c-cube/dagon.git
 
 ### Manual installation
 
@@ -26,13 +26,6 @@ You will need jbuilder. The command is:
 
     make install
 
-## Usage
-
-The main module is `CDCL`.
-
-A modular implementation of the SMT algorithm can be found in the `CDCL.Make` functor,
-as a functor which takes a `Theory_intf.S` module
-
 ## Copyright
 
 This program is distributed under the Apache Software License version

TODO.md

@@ -2,7 +2,7 @@
 
 ## TODO
 
-- typing and translation Ast -> Term
+- typing and translation Ast -> Term (from mc2?)
 - main executable for SMT solver
 - theory of boolean constructs (on the fly Tseitin using local clauses)
 - make CC work on QF_UF
@@ -10,6 +10,8 @@
   * basic notion of activity for `ite`?
 - have `CDCL.push_local` work properly
 
+- remove tseitin lib
+
 - write Shostak theory of datatypes (without acyclicity) with local case splits
 - design evaluation system (guards + `eval_bool:(term -> bool) option` in custom TC)
 - compilation of rec functions to defined constants

cdcl.opam

@@ -1,25 +0,0 @@
-opam-version: "1.2"
-name: "cdcl"
-license: "Apache"
-version: "dev"
-author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
-maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
-build: ["jbuilder" "build" "@install" "-p" name]
-build-doc: ["jbuilder" "build" "@doc" "-p" name]
-install: ["jbuilder" "install" name]
-remove: ["jbuilder" "uninstall" name]
-depends: [
-  "ocamlfind" {build}
-  "jbuilder" {build}
-]
-depopts: [
-  "dolmen"
-]
-available: [
-  ocaml-version >= "4.03.0"
-]
-tags: [ "sat" "smt" ]
-homepage: "https://github.com/c-cube/cdcl"
-dev-repo: "https://github.com/c-cube/cdcl.git"
-bug-reports: "https://github.com/c-cube/cdcl/issues/"
-

dagon.opam

@@ -0,0 +1,25 @@
+opam-version: "1.2"
+name: "dagon"
+license: "Apache"
+version: "dev"
+author: ["Simon Cruanes" "Guillaume Bury" "Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer"]
+maintainer: ["simon.cruanes.2007@m4x.org"]
+build: ["jbuilder" "build" "@install" "-p" name]
+build-doc: ["jbuilder" "build" "@doc" "-p" name]
+depends: [
+  "ocamlfind" {build}
+  "jbuilder" {build}
+  "containers"
+  "sequence"
+]
+depopts: [
+  "dolmen"
+]
+available: [
+  ocaml-version >= "4.03.0"
+]
+tags: [ "sat" "smt" ]
+homepage: "https://github.com/c-cube/dagon"
+dev-repo: "https://github.com/c-cube/dagon.git"
+bug-reports: "https://github.com/c-cube/dagon/issues/"
+

main.exe

@@ -1 +1 @@
-_build/default/src/main_test/main_test.exe
+_build/default/src/main/main.exe

src/backend/jbuild

@@ -2,11 +2,11 @@
 
 ; main binary
 (library
-  ((name CDCL_backend)
-   (public_name cdcl.backend)
-   (synopsis "proof backends for cdcl")
-   (libraries (cdcl))
-   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL))
+  ((name Dagon_backend)
+   (public_name dagon.backend)
+   (synopsis "proof backends for Dagon")
+   (libraries (dagon.sat))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Dagon_sat))
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))
   ))

src/main/jbuild

@@ -0,0 +1,17 @@
+; vim:ft=lisp:
+
+(jbuild_version 1)
+
+; main binary
+(executable
+  ((name main)
+   (public_name dagon)
+   (package dagon)
+   (libraries (containers sequence result
+               dagon.sat dagon.smt dagon.smtlib dagon.backend))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8
+           -safe-string -color always -open Dagon_util))
+   (ocamlopt_flags (:standard -O3 -color always
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+

src/main/main.ml

@@ -0,0 +1,183 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+open CCResult.Infix
+
+module E = CCResult
+module Fmt = CCFormat
+module Term = Dagon_smt.Term
+module Ast = Dagon_smt.Ast
+
+type 'a or_error = ('a, string) E.t
+
+exception Out_of_time
+exception Out_of_space
+
+let file = ref ""
+let p_cnf = ref false
+let p_dot_proof = ref ""
+let p_proof_print = ref false
+let p_model = ref false
+let check = ref true
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
+let restarts = ref true
+let gc = ref true
+let p_stat = ref false
+let p_gc_stat = ref false
+let p_progress = ref false
+
+(* FIXME
+module Dot = CDCL_backend.Dot.Make(CDCL_backend.Dot.Default(Sat))
+   *)
+
+let hyps : Ast.term list ref = ref []
+
+let check_model _state =
+  let check_clause _c =
+    true
+    (* FIXME
+    let l =
+      List.map
+        (fun a ->
+           Dagon_sat.Log.debugf 99
+             (fun k -> k "Checking value of %a" Term.pp (Sat.Atom.term a));
+           Sat_solver.Sat_state.eval state a)
+        c
+    in
+    List.exists (fun x -> x) l
+       *)
+  in
+  let l = List.map check_clause !hyps in
+  List.for_all (fun x -> x) l
+
+(* Arguments parsing *)
+let int_arg r arg =
+  let l = String.length arg in
+  let multiplier m =
+    let arg1 = String.sub arg 0 (l-1) in
+    r := m *. (float_of_string arg1)
+  in
+  if l = 0 then raise (Arg.Bad "bad numeric argument")
+  else
+    try
+      match arg.[l-1] with
+        | 'k' -> multiplier 1e3
+        | 'M' -> multiplier 1e6
+        | 'G' -> multiplier 1e9
+        | 'T' -> multiplier 1e12
+        | 's' -> multiplier 1.
+        | 'm' -> multiplier 60.
+        | 'h' -> multiplier 3600.
+        | 'd' -> multiplier 86400.
+        | '0'..'9' -> r := float_of_string arg
+        | _ -> raise (Arg.Bad "bad numeric argument")
+    with Failure _ -> raise (Arg.Bad "bad numeric argument")
+
+let input_file = fun s -> file := s
+
+let usage = "Usage : main [options] <file>"
+let argspec = Arg.align [
+    "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces";
+    "-cnf", Arg.Set p_cnf, " prints the cnf used.";
+    "-check", Arg.Set check, " build, check and print the proof (if output is set), if unsat";
+    "-no-check", Arg.Clear check, " inverse of -check";
+    "-gc", Arg.Set gc, " enable garbage collection";
+    "-no-gc", Arg.Clear gc, " disable garbage collection";
+    "-restarts", Arg.Set restarts, " enable restarts";
+    "-no-restarts", Arg.Clear restarts, " disable restarts";
+    "-dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file";
+    "-stat", Arg.Set p_stat, " print statistics";
+    "-model", Arg.Set p_model, " print model";
+    "-no-model", Arg.Clear p_model, " do not print model";
+    "-gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
+    "-p", Arg.Set p_progress, " print progress bar";
+    "-no-p", Arg.Clear p_progress, " no progress bar";
+    "-size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
+    "-time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
+    "-v", Arg.Int Dagon_sat.Log.set_debug, "<lvl> sets the debug verbose level";
+  ]
+
+type syntax =
+  | Dimacs
+  | Smtlib
+
+let syntax_of_file file =
+  if CCString.suffix ~suf:".cnf" file then Dimacs
+  else Smtlib
+
+let main () =
+  CCFormat.set_color_default true;
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then (
+    Arg.usage argspec usage;
+    exit 2
+  );
+  let syn = syntax_of_file !file in
+  Util.setup_gc();
+  let solver =
+    let theories = match syn with
+      | Dimacs -> []
+      | Smtlib ->
+        [] (* TODO: more theories *)
+    in
+    Dagon_smt.Solver.create ~theories ()
+  in
+  let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
+  let res = match syn with
+    | Smtlib ->
+      (* parse pb *)
+      Dagon_smtlib.parse !file >>= fun input ->
+      (* TODO: parse list of plugins on CLI *)
+      (* process statements *)
+      begin
+        try
+          E.fold_l
+            (fun () ->
+               Dagon_smtlib.process_stmt
+                 ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
+                 ~time:!time_limit ~memory:!size_limit
+                 ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress
+                 solver)
+            () input
+        with Exit ->
+          E.return()
+      end
+    | Dimacs ->
+      assert false (* TODO *)
+  in
+  if !p_stat then (
+    Format.printf "%a@." Dagon_smt.Solver.pp_stats solver;
+  );
+  if !p_gc_stat then (
+    Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;
+  );
+  res
+
+let () = match main() with
+  | E.Ok () -> ()
+  | E.Error msg ->
+    print_endline msg;
+    exit 1
+  | exception e ->
+    let b = Printexc.get_backtrace () in
+    begin match e with
+      | Util.Error msg ->
+        print_endline msg;
+        ignore @@ exit 1
+      | Out_of_time ->
+        Format.printf "Timeout@.";
+        exit 2
+      | Out_of_space ->
+        Format.printf "Spaceout@.";
+        exit 3
+      | _ -> raise e
+    end;
+    if Printexc.backtrace_status () then (
+      Format.fprintf Format.std_formatter "%s@." b
+    )
+

src/main_test/jbuild

@@ -2,8 +2,8 @@
 
 (executable
   ((name main_test)
-   (libraries (cdcl cdcl.backend cdcl.tseitin cdcl.sat dolmen))
-   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL))
+   (libraries (dagon_sat dagon.backend dagon.th_sat dolmen))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Dagon_sat))
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))
   ))

src/sat/jbuild

@@ -1,13 +1,12 @@
 ; vim:ft=lisp:
 
 (library
-  ((name CDCL_sat)
-   (public_name cdcl.sat)
-   (libraries (cdcl cdcl.tseitin))
-   (synopsis "sat interface")
-   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL))
+  ((name Dagon_sat)
+   (public_name dagon.sat)
+   (synopsis "core SAT solver for Dagon")
+   (libraries (dagon.util))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8
+           -color always -safe-string -open Dagon_util))
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))
   ))
-
-

src/smt/Ast.ml

@@ -4,22 +4,9 @@
 (** {1 Preprocessing AST} *)
 
 module Fmt = CCFormat
-module S = CCSexp
 
 type 'a or_error = ('a, string) CCResult.t
 
-exception Error of string
-exception Ill_typed of string
-
-let () = Printexc.register_printer
-    (function
-      | Error msg -> Some ("ast error: " ^ msg)
-      | Ill_typed msg -> Some ("ill-typed: " ^ msg)
-      | _ -> None)
-
-let errorf msg =
-  CCFormat.ksprintf ~f:(fun e -> raise (Error e)) msg
-
 (** {2 Types} *)
 
 module Var = struct
@@ -43,28 +30,33 @@ end
 module Ty = struct
   type t =
     | Prop
-    | Const of ID.t
+    | App of ID.t * t list
     | Arrow of t * t
 
   let prop = Prop
-  let const id = Const id
+  let app id l = App (id,l)
+  let const id = app id []
   let arrow a b = Arrow (a,b)
   let arrow_l = List.fold_right arrow
 
+  let int = const ID.B.int
+  let rat = const ID.B.rat
+
   let to_int_ = function
     | Prop -> 0
-    | Const _ -> 1
+    | App _ -> 1
     | Arrow _ -> 2
 
   let (<?>) = CCOrd.(<?>)
 
   let rec compare a b = match a, b with
     | Prop, Prop -> 0
-    | Const a, Const b -> ID.compare a b
+    | App (a,la), App (b,lb) ->
+      CCOrd.(ID.compare a b <?> (list compare, la, lb))
     | Arrow (a1,a2), Arrow (b1,b2) ->
       compare a1 b1 <?> (compare, a2,b2)
     | Prop, _
-    | Const _, _
+    | App _, _
     | Arrow _, _ -> CCInt.compare (to_int_ a) (to_int_ b)
 
   let equal a b = compare a b = 0
@@ -80,7 +72,8 @@ module Ty = struct
 
   let rec pp out = function
     | Prop -> Fmt.string out "prop"
-    | Const id -> ID.pp out id
+    | App (id,[]) -> ID.pp out id
+    | App (id,l) -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp) l
     | Arrow _ as ty ->
       let args, ret = unfold ty in
       Fmt.fprintf out "(@[-> %a@ %a@])"
@@ -93,22 +86,6 @@ module Ty = struct
     data_cstors: t ID.Map.t;
   }
 
-  (* FIXME
-  let data_to_sexp d =
-    let cstors =
-      ID.Map.fold
-        (fun c ty acc ->
-           let ty_args, _ = unfold ty in
-           let c_sexp = match ty_args with
-             | [] -> ID.to_sexp c
-             | _::_ -> S.of_list (ID.to_sexp c :: List.map to_sexp ty_args)
-           in
-           c_sexp :: acc)
-        d.data_cstors []
-    in
-    S.of_list (ID.to_sexp d.data_id :: cstors)
-     *)
-
   module Map = CCMap.Make(struct
       type _t = t
       type t = _t
@@ -116,18 +93,27 @@ module Ty = struct
     end)
 
   let ill_typed fmt =
-    CCFormat.ksprintf
-      ~f:(fun s -> raise (Ill_typed s))
-      fmt
+    Util.errorf ("ill-typed: " ^^ fmt)
 end
 
 type var = Ty.t Var.t
 
-type binop =
+type op =
   | And
   | Or
   | Imply
   | Eq
+  | Distinct
+
+type arith_op =
+  | Leq
+  | Lt
+  | Geq
+  | Gt
+  | Add
+  | Minus
+  | Mult
+  | Div
 
 type binder =
   | Fun
@@ -142,16 +128,17 @@ type term = {
 and term_cell =
   | Var of var
   | Const of ID.t
-  | Unknown of var (* meta var *)
+  | Num_z of Z.t
+  | Num_q of Q.t
   | App of term * term list
   | If of term * term * term
-  | Select of select * term
   | Match of term * (var list * term) ID.Map.t
-  | Switch of term * term ID.Map.t (* switch on constants *)
+  | Select of select * term
   | Bind of binder * var * term
-  | Let of var * term * term
+  | Arith of arith_op * term list
+  | Let of (var * term) list * term
   | Not of term
-  | Binop of binop * term * term
+  | Op of op * term list
   | Asserting of term * term
   | Undefined_value
   | Bool of bool
@@ -162,32 +149,98 @@ and select = {
   select_i: int;
 }
 
+
 type definition = ID.t * Ty.t * term
 
 type statement =
+  | SetLogic of string
+  | SetOption of string list
+  | SetInfo of string list
   | Data of Ty.data list
-  | TyDecl of ID.t (* new atomic cstor *)
+  | TyDecl of ID.t * int (* new atomic cstor *)
   | Decl of ID.t * Ty.t
   | Define of definition list
   | Assert of term
   | Goal of var list * term
+  | CheckSat
+  | Exit
 
-(** {2 Helper} *)
+(** {2 Helpers} *)
 
-let unfold_fun t =
+let is_true = function {term=Bool true;_} -> true | _ -> false
+let is_false = function {term=Bool false;_} -> true | _ -> false
+
+let unfold_binder b t =
   let rec aux acc t = match t.term with
-    | Bind (Fun, v, t') -> aux (v::acc) t'
+    | Bind (b', v, t') when b=b' -> aux (v::acc) t'
     | _ -> List.rev acc, t
   in
   aux [] t
 
-(* TODO *)
+let unfold_fun = unfold_binder Fun
 
-let pp_term out _ = Fmt.string out "todo:term"
+let pp_binder out = function
+  | Forall -> Fmt.string out "forall"
+  | Exists -> Fmt.string out "exists"
+  | Fun -> Fmt.string out "lambda"
+  | Mu -> Fmt.string out "mu"
 
-let pp_ty out _ = Fmt.string out "todo:ty"
+let pp_op out = function
+  | And -> Fmt.string out "and"
+  | Or -> Fmt.string out "or"
+  | Imply -> Fmt.string out "=>"
+  | Eq -> Fmt.string out "="
+  | Distinct -> Fmt.string out "distinct"
 
-let pp_statement out _ = Fmt.string out "todo:stmt"
+let pp_arith out = function
+  | Leq -> Fmt.string out "<="
+  | Lt -> Fmt.string out "<"
+  | Geq -> Fmt.string out ">="
+  | Gt -> Fmt.string out ">"
+  | Add -> Fmt.string out "+"
+  | Minus -> Fmt.string out "-"
+  | Mult -> Fmt.string out "*"
+  | Div -> Fmt.string out "/"
+
+let pp_term =
+  let rec pp out t = match t.term with
+    | Var v -> Var.pp out v
+    | Const id -> ID.pp out id
+    | App (f, l) -> Fmt.fprintf out "(@[<hv1>%a@ %a@])" pp f (Util.pp_list pp) l
+    | If (a,b,c) -> Fmt.fprintf out "(@[<hv>ite@ %a@ %a@ %a@])" pp a pp b pp c
+    | Match (u, m) ->
+      let pp_case out (id,(vars,rhs)) =
+        if vars=[] then Fmt.fprintf out "(@[<2>case %a@ %a@])" ID.pp id pp rhs
+        else Fmt.fprintf out "(@[<2>case (@[%a@ %a@])@ %a@])"
+            ID.pp id (Util.pp_list Var.pp) vars pp rhs
+      in
+      Fmt.fprintf out "(@[<hv2>match %a@ %a@])"
+        pp u (Util.pp_list pp_case) (ID.Map.to_list m)
+    | Select (s, t) ->
+      Fmt.fprintf out "(@[select_%a_%d@ %a@])"
+        ID.pp s.select_cstor s.select_i pp t
+    | Bool b -> Fmt.fprintf out "%B" b
+    | Not t -> Fmt.fprintf out "(@[<1>not@ %a@])" pp t
+    | Op (o,l) -> Fmt.fprintf out "(@[<hv1>%a@ %a@])" pp_op o (Util.pp_list pp) l
+    | Bind (b,v,u) ->
+      Fmt.fprintf out "(@[<1>%a ((@[%a@ %a@]))@ %a@])"
+        pp_binder b Var.pp v Ty.pp (Var.ty v) pp u
+    | Let (vbs,u) ->
+      Fmt.fprintf out "(@[<1>let (@[%a@])@ %a@])" pp_vbs vbs pp u
+    | Num_z z -> Z.pp_print out z
+    | Num_q z -> Q.pp_print out z
+    | Arith (op, l) ->
+      Fmt.fprintf out "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp) l
+    | Undefined_value -> Fmt.string out "<undefined>"
+    | Asserting (t, g) ->
+      Fmt.fprintf out "(@[asserting@ %a@ %a@])" pp t pp g
+
+  and pp_vbs out l =
+    let pp_vb out (v,t) = Fmt.fprintf out "(@[%a@ %a@])" Var.pp v pp t in
+    Util.pp_list pp_vb out l
+  in pp
+
+let pp_ty = Ty.pp
 
 (** {2 Constructors} *)
 
@@ -200,7 +253,7 @@ let rec app_ty_ ty l : Ty.t = match ty, l with
     then app_ty_ ty_rest tail
     else Ty.ill_typed "expected `@[%a@]`,@ got `@[%a : %a@]`"
         Ty.pp ty_a pp_term a Ty.pp a.ty
-  | (Ty.Prop | Ty.Const _), a::_ ->
+  | (Ty.Prop | Ty.App _), a::_ ->
     Ty.ill_typed "cannot apply ty `@[%a@]`@ to `@[%a@]`" Ty.pp ty pp_term a
 
 let mk_ term ty = {term; ty}
@@ -217,12 +270,8 @@ let asserting t g =
   mk_ (Asserting (t,g)) t.ty
 
 let var v = mk_ (Var v) (Var.ty v)
-let unknown v = mk_ (Unknown v) (Var.ty v)
-
 let const id ty = mk_ (Const id) ty
 
-let select (s:select) (t:term) ty = mk_ (Select (s,t)) ty
-
 let app f l = match f.term, l with
   | _, [] -> f
   | App (f1, l1), _ ->
@@ -255,22 +304,25 @@ let match_ t m =
     m;
   mk_ (Match (t,m)) rhs1.ty
 
-let switch u m =
-  try
-    let _, t1 = ID.Map.choose m in
-    mk_ (Switch (u,m)) t1.ty
-  with Not_found ->
-    invalid_arg "Ast.switch: empty list of cases"
+let let_l vbs t = match vbs with
+  | [] -> t
+  | _::_ ->
+    List.iter
+      (fun (v,t) ->
+        if not (Ty.equal (Var.ty v) t.ty) then (
+          Ty.ill_typed
+            "let: variable %a : @[%a@]@ and bounded term : %a@ should have same type"
+            Var.pp v Ty.pp (Var.ty v) Ty.pp t.ty;
+        );)
+      vbs;
+    mk_ (Let (vbs,t)) t.ty
 
-let let_ v t u =
-  if not (Ty.equal (Var.ty v) t.ty)
-  then Ty.ill_typed
-      "let: variable %a : @[%a@]@ and bounded term : %a@ should have same type"
-      Var.pp v Ty.pp (Var.ty v) Ty.pp t.ty;
-  mk_ (Let (v,t,u)) u.ty
+let let_ v t u = let_l [v,t] u
 
 let bind ~ty b v t = mk_ (Bind(b,v,t)) ty
 
+let select ~ty (s:select) (t:term) = mk_ (Select (s,t)) ty
+
 let fun_ v t =
   let ty = Ty.arrow (Var.ty v) t.ty in
   mk_ (Bind (Fun,v,t)) ty
@@ -303,16 +355,17 @@ let eq a b =
   if not (Ty.equal a.ty b.ty)
   then Ty.ill_typed "eq: `@[%a@]` and `@[%a@]` do not have the same type"
       pp_term a pp_term b;
-  mk_ (Binop (Eq,a,b)) Ty.prop
+  mk_ (Op (Eq,[a;b])) Ty.prop
 
 let check_prop_ t =
-  if not (Ty.equal t.ty Ty.prop)
-  then Ty.ill_typed "expected prop, got `@[%a : %a@]`" pp_term t Ty.pp t.ty
+  if not (Ty.equal t.ty Ty.prop) then (
+    Ty.ill_typed "expected prop, got `@[%a : %a@]`" pp_term t Ty.pp t.ty
+  )
 
-let binop op a b = mk_ (Binop (op, a, b)) Ty.prop
-let binop_prop op a b =
+let op op l = mk_ (Op (op, l)) Ty.prop
+let binop_prop o a b =
   check_prop_ a; check_prop_ b;
-  binop op a b
+  op o [a;b]
 
 let and_ = binop_prop And
 let or_ = binop_prop Or
@@ -321,17 +374,75 @@ let imply = binop_prop Imply
 let and_l = function
   | [] -> true_
   | [f] -> f
-  | a :: l -> List.fold_left and_ a l
+  | l -> op And l
 
 let or_l = function
   | [] -> false_
   | [f] -> f
-  | a :: l -> List.fold_left or_ a l
+  | l -> op Or l
 
 let not_ t =
   check_prop_ t;
   mk_ (Not t) Ty.prop
 
+let arith ty op l = mk_ (Arith (op,l)) ty
+
+let num_q ty z = mk_ (Num_q z) ty
+let num_z ty z = mk_ (Num_z z) ty
+
+let parse_num ~where (s:string) : [`Q of Q.t | `Z of Z.t] =
+  let fail() =
+    Util.errorf "%sexpected number, got `%s`" (Lazy.force where) s
+  in
+  begin match Z.of_string s with
+    | n -> `Z n
+    | exception _ ->
+      begin match Q.of_string s with
+        | n -> `Q n
+        | exception _ ->
+          if String.contains s '.' then (
+            let p1, p2 = CCString.Split.left_exn ~by:"." s in
+            let n1, n2 =
+              try Z.of_string p1, Z.of_string p2
+              with _ -> fail()
+            in
+            let factor_10 = Z.pow (Z.of_int 10) (String.length p2) in
+            (* [(p1·10^{length p2}+p2) / 10^{length p2}] *)
+            let n =
+              Q.div
+                (Q.of_bigint (Z.add n2 (Z.mul n1 factor_10)))
+                (Q.of_bigint factor_10)
+            in
+            `Q n
+          ) else fail()
+      end
+  end
+
+let num_str ty s =
+  begin match parse_num ~where:(Lazy.from_val "") s with
+    | `Q x -> num_q ty x
+    | `Z x -> num_z ty x
+  end
+
+(** {2 More IO} *)
+
+let pp_statement out = function
+  | SetLogic s -> Fmt.fprintf out "(set-logic %s)" s
+  | SetOption l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l
+  | SetInfo l -> Fmt.fprintf out "(@[set-info@ %a@])" (Util.pp_list Fmt.string) l
+  | CheckSat -> Fmt.string out "(check-sat)"
+  | TyDecl (s,n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n
+  | Decl (id,ty) ->
+    let args, ret = Ty.unfold ty in
+    Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])"
+      ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret
+  | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t
+  | Goal (vars,g) ->
+    Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g))
+  | Exit -> Fmt.string out "(exit)"
+  | Data _ -> assert false (* TODO *)
+  | Define _ -> assert false (* TODO *)
+
 (** {2 Environment} *)
 
 type env_entry =
@@ -363,14 +474,15 @@ let env_add_statement env st =
              (fun c_id c_ty map -> add_def c_id (E_cstor c_ty) map)
              data_cstors map)
         env l
-    | TyDecl id -> add_def id E_uninterpreted_ty env
+    | TyDecl (id,_) -> add_def id E_uninterpreted_ty env
     | Decl (id,ty) -> add_def id (E_const ty) env
     | Define l ->
       List.fold_left
         (fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map)
         env l
-    | Goal _
-    | Assert _ -> env
+    | Goal _ | Assert _ | CheckSat | Exit
+    | SetLogic _ | SetOption _ | SetInfo _
+      -> env
 
 let env_of_statements seq =
   Sequence.fold env_add_statement env_empty seq

src/smt/Ast.mli

@@ -7,9 +7,6 @@ type 'a or_error = ('a, string) CCResult.t
 
 (** {2 Types} *)
 
-exception Error of string
-exception Ill_typed of string
-
 module Var : sig
   type 'ty t = private {
     id: ID.t;
@@ -17,6 +14,7 @@ module Var : sig
   }
 
   val make : ID.t -> 'ty -> 'ty t
+  val makef : ty:'a -> ('b, Format.formatter, unit, 'a t) format4 -> 'b
   val copy : 'a t -> 'a t
   val id : _ t -> ID.t
   val ty : 'a t -> 'a
@@ -29,14 +27,18 @@ end
 module Ty : sig
   type t =
     | Prop
-    | Const of ID.t
+    | App of ID.t * t list
     | Arrow of t * t
 
   val prop : t
   val const : ID.t -> t
+  val app : ID.t -> t list -> t
   val arrow : t -> t -> t
   val arrow_l : t list -> t -> t
 
+  val rat : t
+  val int : t
+
   include Intf.EQ with type t := t
   include Intf.ORD with type t := t
   include Intf.HASH with type t := t
@@ -63,11 +65,22 @@ end
 
 type var = Ty.t Var.t
 
-type binop =
+type op =
   | And
   | Or
   | Imply
   | Eq
+  | Distinct
+
+type arith_op =
+  | Leq
+  | Lt
+  | Geq
+  | Gt
+  | Add
+  | Minus
+  | Mult
+  | Div
 
 type binder =
   | Fun
@@ -82,16 +95,17 @@ type term = private {
 and term_cell =
   | Var of var
   | Const of ID.t
-  | Unknown of var
+  | Num_z of Z.t
+  | Num_q of Q.t
   | App of term * term list
   | If of term * term * term
-  | Select of select * term
   | Match of term * (var list * term) ID.Map.t
-  | Switch of term * term ID.Map.t (* switch on constants *)
+  | Select of select * term
   | Bind of binder * var * term
-  | Let of var * term * term
+  | Arith of arith_op * term list
+  | Let of (var * term) list * term
   | Not of term
-  | Binop of binop * term * term
+  | Op of op * term list
   | Asserting of term * term
   | Undefined_value
   | Bool of bool
@@ -107,12 +121,17 @@ and select = {
 type definition = ID.t * Ty.t * term
 
 type statement =
+  | SetLogic of string
+  | SetOption of string list
+  | SetInfo of string list
   | Data of Ty.data list
-  | TyDecl of ID.t (* new atomic cstor *)
+  | TyDecl of ID.t * int (* new atomic cstor *)
   | Decl of ID.t * Ty.t
   | Define of definition list
   | Assert of term
   | Goal of var list * term
+  | CheckSat
+  | Exit
 
 (** {2 Constructors} *)
 
@@ -121,15 +140,14 @@ val ty : term -> Ty.t
 
 val var : var -> term
 val const : ID.t -> Ty.t -> term
-val unknown : var -> term
 val app : term -> term list -> term
 val app_a : term -> term array -> term
-val select : select -> term -> Ty.t -> term
 val if_ : term -> term -> term -> term
 val match_ : term -> (var list * term) ID.Map.t -> term
-val switch : term -> term ID.Map.t -> term
 val let_ : var -> term -> term -> term
+val let_l : (var * term) list -> term -> term
 val bind : ty:Ty.t -> binder -> var -> term -> term
+val select : ty:Ty.t -> select -> term -> term
 val fun_ : var -> term -> term
 val fun_l : var list -> term -> term
 val fun_a : var array -> term -> term
@@ -140,7 +158,7 @@ val exists_l : var list -> term -> term
 val mu : var -> term -> term
 val eq : term -> term -> term
 val not_ : term -> term
-val binop : binop -> term -> term -> term
+val op : op -> term list -> term
 val and_ : term -> term -> term
 val and_l : term list -> term
 val or_ : term -> term -> term
@@ -150,7 +168,17 @@ val true_ : term
 val false_ : term
 val undefined_value : Ty.t -> term
 val asserting : term -> term -> term
+val num_z : Ty.t -> Z.t -> term
+val num_q : Ty.t -> Q.t -> term
+val num_str : Ty.t -> string -> term (** parses int + {!num} *)
+val arith : Ty.t -> arith_op -> term list -> term
 
+(** {2 helpers} *)
+
+val is_true : term -> bool
+val is_false : term -> bool
+
+val unfold_binder : binder -> term -> var list * term
 val unfold_fun : term -> var list * term
 
 (** {2 Printing} *)

src/smt/Congruence_closure.ml

@@ -1,5 +1,6 @@
 
-open CDCL
+module Vec = Dagon_sat.Vec
+module Log = Dagon_sat.Log
 open Solver_types
 
 type node = Equiv_class.t

src/smt/Explanation.ml

@@ -1,5 +1,4 @@
 
-open CDCL
 open Solver_types
 
 type t = explanation

src/smt/Lit.ml

@@ -47,7 +47,7 @@ let pp = pp_lit
 let print = pp
 
 let norm l =
-  if l.lit_sign then l, CDCL.Same_sign else neg l, CDCL.Negated
+  if l.lit_sign then l, Dagon_sat.Same_sign else neg l, Dagon_sat.Negated
 
 module Set = CCSet.Make(struct type t = lit let compare=compare end)
 module Tbl = CCHashtbl.Make(struct type t = lit let equal=equal let hash=hash end)

src/smt/Lit.mli

@@ -12,7 +12,6 @@ val fresh_with : ID.t -> t
 val fresh : unit -> t
 val dummy : t
 val atom : ?sign:bool -> term -> t
-val cstor_test : data_cstor -> term -> t
 val eq : Term.state -> term -> term -> t
 val neq : Term.state -> term -> term -> t
 val cstor_test : Term.state -> data_cstor -> term -> t
@@ -22,7 +21,7 @@ val compare : t -> t -> int
 val equal : t -> t -> bool
 val print : t Fmt.printer
 val pp : t Fmt.printer
-val norm : t -> t * CDCL.negated
+val norm : t -> t * Dagon_sat.negated
 module Set : CCSet.S with type elt = t
 module Tbl : CCHashtbl.S with type key = t
 

src/smt/Model.ml

@@ -3,8 +3,6 @@
 
 (** {1 Model} *)
 
-open CDCL
-
 module A = Ast
 
 type term = A.term
@@ -104,28 +102,21 @@ let rec as_cstor_app env t = match A.term_view t with
     CCOpt.map (fun (id,ty,l') -> id,ty,l'@l) (as_cstor_app env f)
   | _ -> None
 
-let as_domain_elt env t = match A.term_view t with
-  | A.Const id ->
-    begin match A.env_find_def env id with
-      | Some A.E_uninterpreted_cst -> Some id
-      | _ -> None
-    end
-  | _ -> None
-
 let pp_stack out (l:term list) : unit =
   let ppt out t = Format.fprintf out "(@[%a@ :ty %a@])" A.pp_term t A.Ty.pp t.A.ty in
   CCFormat.(within "[" "]" (hvbox (list ppt))) out l
 
 let apply_subst (subst:subst) t =
   let rec aux subst t = match A.term_view t with
+    | A.Num_z _ | A.Num_q _ -> t
     | A.Var v ->
       begin match VarMap.get v subst with
         | None -> t
         | Some (lazy t') -> t'
       end
     | A.Undefined_value
-    | A.Bool _ | A.Const _ | A.Unknown _ -> t
-    | A.Select (sel, t) -> A.select sel (aux subst t) t.A.ty
+    | A.Bool _ | A.Const _ -> t
+    | A.Select (sel, t) -> A.select ~ty:t.A.ty sel (aux subst t)
     | A.App (f,l) -> A.app (aux subst f) (List.map (aux subst) l)
     | A.If (a,b,c) -> A.if_ (aux subst a) (aux subst b) (aux subst c)
     | A.Match (u,m) ->
@@ -134,38 +125,56 @@ let apply_subst (subst:subst) t =
            (fun (vars,rhs) ->
               let subst, vars = rename_vars subst vars in
               vars, aux subst rhs) m)
-    | A.Switch (u,m) ->
-      A.switch (aux subst u) (ID.Map.map (aux subst) m)
-    | A.Let (x,t,u) ->
-      let subst', x' = rename_var subst x in
-      A.let_ x' (aux subst t) (aux subst' u)
+    | A.Let (vbs,u) ->
+      let subst', vbs' =
+        CCList.fold_map
+          (fun subst' (x,t) ->
+             let t = aux subst t in
+             let subst', x' = rename_var subst' x in
+             subst', (x',t))
+          subst vbs
+      in
+      A.let_l vbs' (aux subst' u)
     | A.Bind (A.Mu, _,_) -> assert false
     | A.Bind (b, x,body) ->
       let subst', x'  = rename_var subst x in
       A.bind ~ty:(A.ty t) b x' (aux subst' body)
     | A.Not f -> A.not_ (aux subst f)
-    | A.Binop (op,a,b) -> A.binop op (aux subst a)(aux subst b)
+    | A.Op (op,l) -> A.op op (List.map (aux subst) l)
     | A.Asserting (t,g) ->
       A.asserting (aux subst t)(aux subst g)
+    | A.Arith (op,l) ->
+      let ty = A.ty t in
+      A.arith ty op (List.map (aux subst) l)
   in
   if VarMap.is_empty subst then t else aux subst t
 
+type partial_eq =
+  | Eq
+  | Neq
+  | Unknown
+
+let equal_as_values (_:A.term) (_:A.term) : partial_eq =
+  Unknown (* TODO *)
+
 (* Weak Head Normal Form.
    @param m the model
    @param st the "stack trace" (terms around currently being evaluated)
    @param t the term to eval *)
 let rec eval_whnf (m:t) (st:term list) (subst:subst) (t:term): term =
-  Log.debugf 5
+  Dagon_sat.Log.debugf 5
     (fun k->k "%s@[<2>eval_whnf `@[%a@]`@ in @[%a@]@]"
         (String.make (List.length st) ' ') (* indent *)
         A.pp_term t pp_subst subst);
   let st = t :: st in
   try
     eval_whnf_rec m st subst t
-  with A.Ill_typed msg ->
+  with Util.Error msg ->
     errorf "@[<2>Model:@ internal type error `%s`@ in %a@]" msg pp_stack st
 and eval_whnf_rec m st subst t = match A.term_view t with
-  | A.Undefined_value | A.Bool _ | A.Unknown _ -> t
+  | A.Num_q _
+  | A.Num_z _ -> t
+  | A.Undefined_value | A.Bool _ -> t
   | A.Var v ->
     begin match VarMap.get v subst with
       | None -> t
@@ -196,10 +205,15 @@ and eval_whnf_rec m st subst t = match A.term_view t with
   | A.Bind (A.Mu,v,body) ->
     let subst' = VarMap.add v (lazy t) subst in
     eval_whnf m st subst' body
-  | A.Let (x,t,u) ->
-    let t = lazy (eval_whnf m st subst t) in
-    let subst' = VarMap.add x t subst in
-    eval_whnf m st subst' u
+  | A.Let (vbs,u) ->
+    let subst =
+      List.fold_left
+        (fun subst (x,t) ->
+             let t = lazy (eval_whnf m st subst t) in
+             VarMap.add x t subst)
+        subst vbs
+    in
+    eval_whnf m st subst u
   | A.Bind (A.Fun,_,_) -> apply_subst subst t
   | A.Bind ((A.Forall | A.Exists) as b,v,body) ->
     let ty = A.Var.ty v in
@@ -227,7 +241,7 @@ and eval_whnf_rec m st subst t = match A.term_view t with
     eval_whnf m st subst t'
   | A.Select (sel, u) ->
     let u = eval_whnf m st subst u in
-    let t' = A.select sel u t.A.ty in
+    let t' = A.select ~ty:t.A.ty sel u in
     begin match as_cstor_app m.env u with
       | None -> t'
       | Some (cstor, _, args) ->
@@ -266,20 +280,6 @@ and eval_whnf_rec m st subst t = match A.term_view t with
             in
             eval_whnf m st subst' rhs
     end
-  | A.Switch (u, map) ->
-    let u = eval_whnf m st subst u in
-    begin match as_domain_elt m.env u with
-      | None ->
-        let map = ID.Map.map (apply_subst subst) map in
-        A.switch u map
-      | Some cst ->
-        begin match ID.Map.get cst map with
-          | Some rhs -> eval_whnf m st subst rhs
-          | None ->
-            let map = ID.Map.map (apply_subst subst) map in
-            A.switch u map
-        end
-    end
   | A.Not f ->
     let f = eval_whnf m st subst f in
     begin match A.term_view f with
@@ -295,59 +295,41 @@ and eval_whnf_rec m st subst t = match A.term_view t with
         A.undefined_value u.A.ty (* assertion failed, uncharted territory! *)
       | _ -> A.asserting u g'
     end
-  | A.Binop (op, a, b) ->
-    let a = eval_whnf m st subst a in
-    let b = eval_whnf m st subst b in
+  | A.Op (op, l) ->
+    let l = List.map (eval_whnf m st subst) l in
     begin match op with
       | A.And ->
-        begin match A.term_view a, A.term_view b with
-          | A.Bool true, A.Bool true -> A.true_
-          | A.Bool false, _
-          | _, A.Bool false -> A.false_
-          | _ -> A.and_ a b
-        end
+        if List.exists A.is_false l then A.false_
+        else if List.for_all A.is_true l then A.true_
+        else A.and_l l
       | A.Or ->
-        begin match A.term_view a, A.term_view b with
-          | A.Bool true, _
-          | _, A.Bool true -> A.true_
-          | A.Bool false, A.Bool false -> A.false_
-          | _ -> A.or_ a b
-        end
+        if List.exists A.is_true l then A.true_
+        else if List.for_all A.is_false l then A.false_
+        else A.or_l l
       | A.Imply ->
-        begin match A.term_view a, A.term_view b with
-          | _, A.Bool true
-          | A.Bool false, _  -> A.true_
-          | A.Bool true, A.Bool false -> A.false_
-          | _ -> A.imply a b
-        end
+        assert false (* TODO *)
       | A.Eq ->
-        begin match A.term_view a, A.term_view b with
-          | A.Bool true, A.Bool true
-          | A.Bool false, A.Bool false -> A.true_
-          | A.Bool true, A.Bool false
-          | A.Bool false, A.Bool true -> A.false_
-          | A.Var v1, A.Var v2 when A.Var.equal v1 v2 -> A.true_
-          | A.Const id1, A.Const id2 when ID.equal id1 id2 -> A.true_
-          | _ ->
-            begin match as_cstor_app m.env a, as_cstor_app m.env b with
-              | Some (c1,_,l1), Some (c2,_,l2) ->
-                if ID.equal c1 c2 then (
-                  assert (List.length l1 = List.length l2);
-                  eval_whnf m st subst (A.and_l (List.map2 A.eq l1 l2))
-                ) else A.false_
-              | _ ->
-                begin match as_domain_elt m.env a, as_domain_elt m.env b with
-                  | Some c1, Some c2 ->
-                    (* domain elements: they are all distinct *)
-                    if ID.equal c1 c2
-                    then A.true_
-                    else A.false_
-                  | _ ->
-                    A.eq a b
-                end
-            end
+        begin match l with
+          | [] -> assert false
+          | x :: tail ->
+            if List.for_all (fun y -> equal_as_values x y = Eq) tail
+            then A.true_
+            else if List.exists (fun y -> equal_as_values x y = Neq) tail
+            then A.false_
+            else A.op A.Eq l
         end
+      | A.Distinct ->
+        if
+          Sequence.diagonal_l l
+          |> Sequence.exists (fun (t,u) -> equal_as_values t u = Eq)
+        then A.false_
+        else if
+          Sequence.diagonal_l l
+          |> Sequence.for_all (fun (t,u) -> equal_as_values t u = Neq)
+        then A.true_
+        else A.op A.Distinct l
     end
+  | A.Arith (_, _) -> assert false (* TODO *)
 (* beta-reduce [f l] while [f] is a function,constant or variable *)
 and eval_whnf_app m st subst_f subst_l f l = match A.term_view f, l with
   | A.Bind (A.Fun,v, body), arg :: tail ->

src/smt/Solver.ml

@@ -21,21 +21,23 @@ let get_time : unit -> float = Sys.time
 
 type level = int
 
-module Sat = CDCL.Make(Theory_combine)
+module Sat_solver = Dagon_sat.Make(Theory_combine)
 
 (* main solver state *)
 type t = {
-  solver: Sat.t;
+  solver: Sat_solver.t;
   stat: Stat.t;
   config: Config.t
 }
 
-let th_combine (self:t) : Theory_combine.t =
-  Sat.theory self.solver
+let solver self = self.solver
+let th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
+let add_theory self th = Theory_combine.add_theory (th_combine self) th
+let stats self = self.stat
 
 let create ?size ?(config=Config.empty) ~theories () : t =
   let self = {
-    solver=Sat.create ?size ();
+    solver=Sat_solver.create ?size ();
     stat=Stat.create ();
     config;
   } in
@@ -706,11 +708,11 @@ end
 
 (** {2 Main} *)
 
-let[@inline] clause_of_mclause (c:Sat.clause): Clause.t =
-  Sat.Clause.atoms_l c |> Clause.make
+let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t =
+  Sat_solver.Clause.atoms_l c |> Clause.make
 
 (* convert unsat-core *)
-let clauses_of_unsat_core (core:Sat.clause list): Clause.t Sequence.t =
+let clauses_of_unsat_core (core:Sat_solver.clause list): Clause.t Sequence.t =
   Sequence.of_list core
   |> Sequence.map clause_of_mclause
 
@@ -747,20 +749,20 @@ let add_statement_l (_:t) _ = ()
 (* TODO: move this into submodule *)
 let pp_proof out p =
   let pp_step_res out p =
-    let {Sat.Proof.conclusion; _ } = Sat.Proof.expand p in
+    let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
     let conclusion = clause_of_mclause conclusion in
     Clause.pp out conclusion
   in
   let pp_step out = function
-    | Sat.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
-    | Sat.Proof.Resolution (p1, p2, _) ->
+    | Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
+    | Sat_solver.Proof.Resolution (p1, p2, _) ->
       Format.fprintf out "(@[<1>resolution@ %a@ %a@])"
         pp_step_res p1 pp_step_res p2
     | _ -> Fmt.string out "<other>"
   in
   Format.fprintf out "(@[<v>";
-  Sat.Proof.fold
-    (fun () {Sat.Proof.conclusion; step } ->
+  Sat_solver.Proof.fold
+    (fun () {Sat_solver.Proof.conclusion; step } ->
        let conclusion = clause_of_mclause conclusion in
        Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
          Clause.pp conclusion pp_step step)

src/smt/Solver.mli

@@ -5,18 +5,6 @@
 
     The solving algorithm, based on MCSat *)
 
-open CDCL
-
-type term
-type cst
-type ty = Solver_types.ty (** types *)
-type ty_def = Solver_types.ty_def
-
-type ty_cell = Solver_types.ty_cell =
-  | Prop
-  | Atomic of ID.t * ty_def
-  | Arrow of ty * ty
-
 (** {2 Result} *)
 
 type model = Model.t
@@ -31,6 +19,11 @@ type res =
   | Unsat (* TODO: proof *)
   | Unknown of unknown
 
+module Sat_solver : Dagon_sat.S
+      with type formula = Lit.t
+       and type theory = Theory_combine.t
+       and type Proof.lemma = Theory_combine.proof
+
 (** {2 Main} *)
 
 type t
@@ -42,6 +35,11 @@ val create :
   theories:Theory.t list ->
   unit -> t
 
+val solver : t -> Sat_solver.t
+val th_combine : t -> Theory_combine.t
+val add_theory : t -> Theory.t -> unit
+val stats : t -> Stat.t
+
 val add_statement_l : t -> Ast.statement list -> unit
 
 val solve :

src/smt/Solver_types.ml

@@ -1,6 +1,4 @@
 
-open CDCL
-
 module Fmt = CCFormat
 module Node_bits = CCBitField.Make(struct end)
 

src/smt/Term.mli

@@ -1,5 +1,4 @@
 
-open CDCL
 open Solver_types
 
 type t = term

src/smt/Theory.ml

@@ -1,6 +1,4 @@
 
-open Solver_types
-
 (** Runtime state of a theory, with all the operations it provides *)
 type state = {
   on_merge: Equiv_class.t -> Equiv_class.t -> Explanation.t -> unit;

src/smt/Theory_combine.ml

@@ -3,6 +3,7 @@
 
 (** Combine the congruence closure with a number of plugins *)
 
+module Sat_solver = Dagon_sat
 open Solver_types
 
 module Proof = struct
@@ -21,7 +22,7 @@ type conflict = Explanation.t Bag.t
 exception Exn_conflict of conflict
 
 type t = {
-  cdcl_acts: (formula,proof) CDCL.actions;
+  cdcl_acts: (formula,proof) Sat_solver.actions;
   (** actions provided by the SAT solver *)
   tst: Term.state;
   (** state for managing terms *)
@@ -49,7 +50,7 @@ let[@inline] theories (self:t) : Theory.state Sequence.t =
 
 (* handle a literal assumed by the SAT solver *)
 let assume_lit (self:t) (lit:Lit.t) : unit =
-  CDCL.Log.debugf 2
+  Sat_solver.Log.debugf 2
     (fun k->k "(@[<1>@{<green>theory_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit);
   (* check consistency first *)
   begin match Lit.view lit with
@@ -65,26 +66,26 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
 
 (* push clauses from {!lemma_queue} into the slice *)
 let push_new_clauses_into_cdcl (self:t) : unit =
-  let CDCL.Actions r = self.cdcl_acts in
+  let Sat_solver.Actions r = self.cdcl_acts in
   (* persistent lemmas *)
   while not (Queue.is_empty self.lemma_q) do
     let c = Queue.pop self.lemma_q in
-    CDCL.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c);
+    Sat_solver.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c);
     r.push c Proof.default
   done;
   (* local splits *)
   while not (Queue.is_empty self.split_q) do
     let c = Queue.pop self.split_q in
-    CDCL.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c);
+    Sat_solver.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c);
     r.push_local c Proof.default
   done
 
 (* return result to the SAT solver *)
-let cdcl_return_res (self:t) : _ CDCL.res =
+let cdcl_return_res (self:t) : _ Sat_solver.res =
   begin match self.conflict with
     | None ->
       push_new_clauses_into_cdcl self;
-      CDCL.Sat
+      Sat_solver.Sat
     | Some c ->
       let lit_set =
         Bag.to_seq c
@@ -95,19 +96,19 @@ let cdcl_return_res (self:t) : _ CDCL.res =
         |> List.map Lit.neg
         |> Clause.make
       in
-      CDCL.Log.debugf 3
+      Sat_solver.Log.debugf 3
         (fun k->k "(@[<1>conflict@ clause: %a@])"
             Clause.pp conflict_clause);
-      CDCL.Unsat (Clause.lits conflict_clause, Proof.default)
+      Sat_solver.Unsat (Clause.lits conflict_clause, Proof.default)
   end
 
 let[@inline] check (self:t) : unit =
   Congruence_closure.check (cc self)
 
 (* propagation from the bool solver *)
-let assume_real (self:t) (slice:_ CDCL.slice_actions) =
+let assume_real (self:t) (slice:_ Sat_solver.slice_actions) =
   (* TODO if Config.progress then print_progress(); *)
-  let CDCL.Slice_acts slice = slice in
+  let Sat_solver.Slice_acts slice = slice in
   begin
     try
       slice.slice_iter (assume_lit self);
@@ -120,7 +121,7 @@ let assume_real (self:t) (slice:_ CDCL.slice_actions) =
   cdcl_return_res self
 
 (* propagation from the bool solver *)
-let assume (self:t) (slice:_ CDCL.slice_actions) =
+let assume (self:t) (slice:_ Sat_solver.slice_actions) =
   match self.conflict with
   | None -> assume_real self slice
   | Some _ ->
@@ -128,11 +129,11 @@ let assume (self:t) (slice:_ CDCL.slice_actions) =
     cdcl_return_res self
 
 (* perform final check of the model *)
-let if_sat (self:t) (slice:_) : _ CDCL.res =
+let if_sat (self:t) (slice:_) : _ Sat_solver.res =
   Congruence_closure.final_check (cc self);
   (* all formulas in the SAT solver's trail *)
   let forms =
-    let CDCL.Slice_acts r = slice in
+    let Sat_solver.Slice_acts r = slice in
     r.slice_iter
   in
   (* final check for each theory *)
@@ -144,13 +145,13 @@ let if_sat (self:t) (slice:_) : _ CDCL.res =
 
 (* forward propagations from CC or theories directly to the SMT core *)
 let act_propagate (self:t) f guard : unit =
-  let CDCL.Actions r = self.cdcl_acts in
+  let Sat_solver.Actions r = self.cdcl_acts in
   let guard =
     Bag.to_seq guard
     |> Congruence_closure.explain_unfold (cc self)
     |> Lit.Set.to_list
   in
-  CDCL.Log.debugf 2
+  Sat_solver.Log.debugf 2
     (fun k->k "(@[@{<green>propagate@}@ %a@ :guard %a@])"
         Lit.pp f Clause.pp guard);
   r.propagate f guard Proof.default
@@ -165,7 +166,7 @@ let on_merge_from_cc (self:t) r1 r2 e : unit =
     (fun th -> th.Theory.on_merge r1 r2 e)
 
 let mk_cc_actions (self:t) : Congruence_closure.actions =
-  let CDCL.Actions r = self.cdcl_acts in
+  let Sat_solver.Actions r = self.cdcl_acts in
   {
     Congruence_closure.
     on_backtrack = r.on_backtrack;
@@ -178,8 +179,8 @@ let mk_cc_actions (self:t) : Congruence_closure.actions =
 (** {2 Main} *)
 
 (* create a new theory combination *)
-let create (cdcl_acts:_ CDCL.actions) : t =
-  CDCL.Log.debug 5 "theory_combine.create";
+let create (cdcl_acts:_ Sat_solver.actions) : t =
+  Sat_solver.Log.debug 5 "theory_combine.create";
   let rec self = {
     cdcl_acts;
     tst=Term.create ~size:1024 ();
@@ -210,18 +211,18 @@ let act_find self t =
   |> Congruence_closure.find (cc self)
 
 let act_case_split self (c:Clause.t) =
-  CDCL.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c);
+  Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c);
   Queue.push c self.split_q
 
 (* push one clause into [M], in the current level (not a lemma but
    an axiom) *)
 let act_add_axiom self (c:Clause.t): unit =
-  CDCL.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c);
+  Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c);
   (* TODO incr stat_num_clause_push; *)
   Queue.push c self.lemma_q
 
 let mk_theory_actions (self:t) : Theory.actions =
-  let CDCL.Actions r = self.cdcl_acts in
+  let Sat_solver.Actions r = self.cdcl_acts in
   {
     Theory.
     on_backtrack = r.on_backtrack;
@@ -236,7 +237,7 @@ let mk_theory_actions (self:t) : Theory.actions =
   }
 
 let add_theory (self:t) (th:Theory.t) : unit =
-  CDCL.Log.debugf 2
+  Sat_solver.Log.debugf 2
     (fun k->k "(@[theory_combine.add_th@ :name %S@])" th.Theory.name);
   let th_s = th.Theory.make self.tst (mk_theory_actions self) in
   self.theories <- th_s :: self.theories

src/smt/Theory_combine.mli

@@ -7,7 +7,7 @@ module Proof : sig
   type t = Proof
 end
 
-include CDCL.Theory_intf.S
+include Dagon_sat.Theory_intf.S
   with type formula = Lit.t
    and type proof = Proof.t
 

src/smt/Ty.ml

@@ -1,5 +1,4 @@
 
-open CDCL
 open Solver_types
 
 type t = ty

src/smt/Ty.mli

@@ -1,8 +1,6 @@
 
 (** {1 Hashconsed Types} *)
 
-open CDCL
-
 type t = Solver_types.ty
 type cell = Solver_types.ty_cell
 type def = Solver_types.ty_def

src/smt/Ty_card.mli

@@ -1,8 +1,6 @@
 
 (** {1 Type Cardinality} *)
 
-open CDCL
-
 type t = Solver_types.ty_card
 
 val (+) : t -> t -> t

src/smt/jbuild

@@ -1,9 +1,10 @@
 ; vim:ft=lisp:
 
 (library
-  ((name CDCL_smt)
-   (public_name cdcl.smt)
-   (libraries (containers containers.data sequence cdcl))
-   (flags (:standard -w +a-4-44-48-58-60@8 -color always -safe-string -short-paths))
+  ((name Dagon_smt)
+   (public_name dagon.smt)
+   (libraries (containers containers.data sequence dagon.util dagon.sat zarith))
+   (flags (:standard -w +a-4-44-48-58-60@8
+           -color always -safe-string -short-paths -open Dagon_util))
    (ocamlopt_flags (:standard -O3 -color always
                     -unbox-closures -unbox-closures-factor 20))))

src/smtlib/Convert.ml

@@ -0,0 +1,455 @@
+
+(* This file is free software. See file "license" for more details. *)
+
+(** {1 Preprocessing AST} *)
+
+module Loc = Locations
+module Fmt = CCFormat
+
+module A = Dagon_smt.Ast
+module PA = Parse_ast
+
+type 'a or_error = ('a, string) CCResult.t
+
+let pp_loc_opt = Loc.pp_opt
+
+(** {2 Parsing} *)
+
+module StrTbl = CCHashtbl.Make(struct
+    type t = string
+    let equal = CCString.equal
+    let hash = CCString.hash
+  end)
+
+module Ctx = struct
+  type kind =
+    | K_ty of ty_kind
+    | K_fun of A.Ty.t
+    | K_var of A.var (* local *)
+    | K_cstor of A.Ty.t
+    | K_select of A.Ty.t * A.select
+
+  and ty_kind =
+    | K_uninterpreted (* uninterpreted type *)
+    | K_other
+    | K_bool
+    | K_data (* data type *)
+
+  type t = {
+    names: ID.t StrTbl.t;
+    kinds: kind ID.Tbl.t;
+    data: (ID.t * A.Ty.t) list ID.Tbl.t; (* data -> cstors *)
+    mutable loc: Loc.t option; (* current loc *)
+  }
+
+  let create () : t = {
+    names=StrTbl.create 64;
+    kinds=ID.Tbl.create 64;
+    data=ID.Tbl.create 64;
+    loc=None;
+  }
+
+  let loc t = t.loc
+  let set_loc ?loc t = t.loc <- loc
+
+  let add_id t (s:string) (k:kind): ID.t =
+    let id = ID.make s in
+    StrTbl.add t.names s id;
+    ID.Tbl.add t.kinds id k;
+    id
+
+  let add_data t (id:ID.t) cstors: unit =
+    ID.Tbl.add t.data id cstors
+
+  let with_var t (s:string) (ty:A.Ty.t) (f:A.var -> 'a): 'a =
+    let id = ID.make s in
+    StrTbl.add t.names s id;
+    let v = A.Var.make id ty in
+    ID.Tbl.add t.kinds id (K_var v);
+    CCFun.finally1 f v
+      ~h:(fun () -> StrTbl.remove t.names s)
+
+  let with_vars t (l:(string*A.Ty.t) list) (f:A.var list -> 'a): 'a =
+    let rec aux ids l f = match l with
+      | [] -> f (List.rev ids)
+      | (s,ty) :: l' -> with_var t s ty (fun id -> aux (id::ids) l' f)
+    in
+    aux [] l f
+
+  let find_kind t (id:ID.t) : kind =
+    try ID.Tbl.find t.kinds id
+    with Not_found -> Util.errorf "did not find kind of ID `%a`" ID.pp id
+
+  let as_data t (ty:A.Ty.t) : (ID.t * A.Ty.t) list = match ty with
+    | A.Ty.App (id,_) ->
+      begin match ID.Tbl.get t.data id with
+        | Some l -> l
+        | None -> Util.errorf "expected %a to be a datatype" A.Ty.pp ty
+      end
+    | _ -> Util.errorf "expected %a to be a constant type" A.Ty.pp ty
+
+  let pp_kind out = function
+    | K_ty _ -> Format.fprintf out "type"
+    | K_cstor ty ->
+      Format.fprintf out "(@[cstor : %a@])" A.Ty.pp ty
+    | K_select (ty,s) ->
+      Format.fprintf out "(@[select-%a-%d : %a@])"
+        ID.pp s.A.select_cstor s.A.select_i A.Ty.pp ty
+    | K_fun ty ->
+      Format.fprintf out "(@[fun : %a@])" A.Ty.pp ty
+    | K_var v ->
+      Format.fprintf out "(@[var : %a@])" A.Ty.pp (A.Var.ty v)
+
+  let pp out t =
+    Format.fprintf out "ctx {@[%a@]}"
+      Fmt.(seq ~sep:(return "@ ") @@ pair ID.pp pp_kind) (ID.Tbl.to_seq t.kinds)
+end
+
+let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx)
+let errorf_ctx ctx msg =
+  Util.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx)
+
+let check_bool_ t =
+  if not (A.Ty.equal (A.ty t) A.Ty.prop) then (
+    A.Ty.ill_typed "expected bool, got `@[%a : %a@]`" A.pp_term t A.Ty.pp (A.ty t)
+  )
+
+let find_id_ ctx (s:string): ID.t =
+  try StrTbl.find ctx.Ctx.names s
+  with Not_found -> errorf_ctx ctx "name `%s` not in scope" s
+
+(* parse a type *)
+let rec conv_ty ctx (t:PA.ty) : A.Ty.t * _ = match t with
+  | PA.Ty_bool -> A.Ty.prop, Ctx.K_ty Ctx.K_bool
+  | PA.Ty_app ("Rat",[]) -> A.Ty.rat, Ctx.K_ty Ctx.K_other
+  | PA.Ty_app ("Int",[]) -> A.Ty.int , Ctx.K_ty Ctx.K_other
+  | PA.Ty_app (f, l) ->
+    let id = find_id_ ctx f in
+    let l = List.map (conv_ty_fst ctx) l in
+    A.Ty.app id l, Ctx.find_kind ctx id
+  | PA.Ty_arrow (args, ret) ->
+    let args = List.map (conv_ty_fst ctx) args in
+    let ret, _ = conv_ty ctx ret in
+    A.Ty.arrow_l args ret, Ctx.K_ty Ctx.K_other
+
+and conv_ty_fst ctx t = fst (conv_ty ctx t)
+
+let conv_var ctx (v,ty) = v, conv_ty_fst ctx ty
+let conv_vars ctx l = List.map (fun (v,ty) -> v, conv_ty_fst ctx ty) l
+
+let is_num s =
+  let is_digit_or_dot = function '0' .. '9' | '.' -> true | _ -> false in
+  if s.[0] = '-'
+  then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1))
+  else CCString.for_all is_digit_or_dot s
+
+let rec conv_term ctx (t:PA.term) : A.term = match t with
+  | PA.True -> A.true_
+  | PA.False -> A.false_
+  | PA.Const s when is_num s -> A.num_str A.Ty.rat s (* numeral *)
+  | PA.Const f ->
+    let id = find_id_ ctx f in
+    begin match Ctx.find_kind ctx id with
+      | Ctx.K_var v -> A.var v
+      | Ctx.K_fun ty -> A.const id ty
+      | Ctx.K_ty _ ->
+        errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id
+      | Ctx.K_cstor ty -> A.const id ty
+      | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported"
+    end
+  | PA.If (a,b,c) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    let c = conv_term ctx c in
+    A.if_ a b c
+  | PA.Fun (v, body) ->
+    let v = conv_var ctx v in
+    Ctx.with_var ctx (fst v)(snd v)
+      (fun v ->
+         let body = conv_term ctx body in
+         A.fun_ v body)
+  | PA.Forall _ | PA.Exists _ ->
+    errorf_ctx ctx "cannot process quantifiers in %a" PA.pp_term t
+  | PA.Let (vbs, u) ->
+    let vars, terms =
+      List.map
+        (fun (v,t) ->
+           let t = conv_term ctx t in
+           (v,A.ty t), t)
+        vbs
+      |> List.split
+    in
+    Ctx.with_vars ctx vars
+      (fun vars ->
+         let vbs = List.combine vars terms in
+         let u = conv_term ctx u in
+         A.let_l vbs u)
+  | PA.Distinct l ->
+    let l = List.map (conv_term ctx) l in
+    A.op A.Distinct l
+  | PA.And l ->
+    let l = List.map (conv_term ctx) l in
+    A.and_l l
+  | PA.Or l ->
+    let l = List.map (conv_term ctx) l in
+    A.or_l l
+  | PA.Not a ->
+    let a = conv_term ctx a in
+    A.not_ a
+  | PA.Eq (a,b) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    A.eq a b
+  | PA.Imply (a,b) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    A.imply a b
+  | PA.Xor (a,b) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    A.or_ (A.and_ a (A.not_ b)) (A.and_ (A.not_ a) b)
+  | PA.Match (lhs, l) ->
+    (*
+    errorf_ctx ctx "TODO: support match in %a" PA.pp_term t
+    assert false
+       *)
+    (* convert a regular case *)
+    let conv_case c vars rhs =
+      let c_id = find_id_ ctx c in
+      (* obtain the type *)
+      let ty_args, _ty_ret = match Ctx.find_kind ctx c_id with
+       | Ctx.K_cstor ty -> A.Ty.unfold ty
+       | _ ->
+         errorf_ctx ctx "expected `@[%a@]`@ to be a constructor" ID.pp c_id
+      in
+      (* pair variables with their type *)
+      if List.length vars <> List.length ty_args then (
+       errorf_ctx ctx
+         "in @[%a@] for case %a,@ wrong number of arguments (expected %d)"
+         PA.pp_term t ID.pp c_id (List.length ty_args);
+      );
+      let vars = List.combine vars ty_args in
+      Ctx.with_vars ctx vars
+       (fun vars ->
+          let rhs = conv_term ctx rhs in
+          c_id, vars, rhs)
+     in
+     (* convert default case, where [m] contains the partial map. We have
+     to complete this map *)
+     let lhs = conv_term ctx lhs in
+     let default, cases =
+     List.fold_left
+      (fun (def,cases) branch -> match branch with
+         | PA.Match_case (c,vars,rhs) ->
+           let c, vars, rhs = conv_case c vars rhs in
+           (* no duplicate *)
+           if ID.Map.mem c cases
+           then errorf_ctx ctx "constructor %a occurs twice" ID.pp c;
+           def, ID.Map.add c (vars,rhs) cases
+        | PA.Match_default rhs ->
+          (* check there is only one "default" case *)
+          begin match def with
+            | Some _ -> errorf_ctx ctx "cannot have two `default` cases"
+            | None ->
+              let rhs = conv_term ctx rhs in
+              Some rhs, cases
+          end)
+      (None,ID.Map.empty) l
+     in
+     (* now fill the blanks, check exhaustiveness *)
+     let all_cstors = Ctx.as_data ctx lhs.A.ty in
+     let cases = match default with
+     | None ->
+      (* check exhaustiveness *)
+      let missing =
+        all_cstors
+        |> List.filter (fun (cstor,_) -> not (ID.Map.mem cstor cases))
+        |> List.map fst
+      in
+      if missing<>[] then (
+        errorf_ctx ctx
+          "missing cases in `@[%a@]`: @[%a@]"
+          PA.pp_term t (Util.pp_list ID.pp) missing;
+      );
+      cases
+     | Some def_rhs ->
+      List.fold_left
+        (fun cases (cstor,ty_cstor) ->
+           if ID.Map.mem cstor cases then cases
+           else (
+             let args, _ = A.Ty.unfold ty_cstor in
+             let vars = List.mapi (fun i ty -> A.Var.makef ~ty "_%d" i) args in
+             ID.Map.add cstor (vars, def_rhs) cases
+           ))
+        cases all_cstors
+     in
+     A.match_ lhs cases
+  | PA.Arith (op, l) ->
+    let l = List.map (conv_term ctx) l in
+    List.iter
+      (fun t ->
+         if not (A.Ty.equal A.Ty.rat (A.ty t)) then (
+           errorf_ctx ctx "expected rational term,@ got `%a`" A.pp_term t
+         ))
+      l;
+    let ty, op = match op with
+      | PA.Leq -> A.Ty.prop, A.Leq
+      | PA.Lt -> A.Ty.prop,A. Lt
+      | PA.Geq -> A.Ty.prop, A.Geq
+      | PA.Gt -> A.Ty.prop, A.Gt
+      | PA.Add -> A.Ty.rat, A.Add
+      | PA.Minus -> A.Ty.rat, A.Minus
+      | PA.Mult -> A.Ty.rat, A.Mult
+      | PA.Div -> A.Ty.rat, A.Div
+    in
+    A.arith ty op l
+  | PA.Cast (t, ty_expect) ->
+    let t = conv_term ctx t in
+    let ty_expect = conv_ty_fst ctx ty_expect in
+    if not (A.Ty.equal (A.ty t) ty_expect) then (
+      A.Ty.ill_typed "term `%a`@ should have type `%a`" A.pp_term t A.Ty.pp ty_expect
+    );
+    t
+  | _ ->
+    errorf_ctx ctx "unsupported term %a" PA.pp_term t
+
+let find_file_ name ~dir : string option =
+  Dagon_sat.Log.debugf 2 (fun k->k "search %s in %s" name dir);
+  let abs_path = Filename.concat dir name in
+  if Sys.file_exists abs_path
+  then Some abs_path
+  else None
+
+let conv_fun_decl ctx f : string * A.Ty.t =
+  if f.PA.fun_ty_vars <> [] then (
+    errorf_ctx ctx "cannot convert polymorphic function@ %a"
+      (PA.pp_fun_decl PA.pp_ty) f
+  );
+  let args = List.map (conv_ty_fst ctx) f.PA.fun_args in
+  let ty = A.Ty.arrow_l args (conv_ty_fst ctx f.PA.fun_ret) in
+  f.PA.fun_name, ty
+
+let conv_fun_def ctx f_decl body : string * A.Ty.t * (unit -> A.term) =
+  if f_decl.PA.fun_ty_vars <> [] then (
+    errorf_ctx ctx "cannot convert polymorphic function@ %a"
+      (PA.pp_fun_decl PA.pp_typed_var) f_decl;
+  );
+  let args = conv_vars ctx f_decl.PA.fun_args in
+  let ty =
+    A.Ty.arrow_l
+      (List.map snd args)
+      (conv_ty_fst ctx f_decl.PA.fun_ret)
+  in
+  (* delayed body, for we need to declare the functions in the recursive block first *)
+  let conv_body() =
+    Ctx.with_vars ctx args
+      (fun args ->
+         A.fun_l args (conv_term ctx body))
+  in
+  f_decl.PA.fun_name, ty, conv_body
+
+let conv_fun_defs ctx decls bodies : A.definition list =
+  let l = List.map2 (conv_fun_def ctx) decls bodies in
+  let ids = List.map (fun (f,ty,_) -> Ctx.add_id ctx f (Ctx.K_fun ty)) l in
+  let defs = List.map2 (fun id (_,ty,body) -> id, ty, body()) ids l in
+  (* parse id,ty and declare them before parsing the function bodies *)
+  defs
+
+let rec conv_statement ctx (s:PA.statement): A.statement list =
+  Log.debugf 4 (fun k->k "(@[<1>statement_of_ast@ %a@])" PA.pp_stmt s);
+  Ctx.set_loc ctx ?loc:(PA.loc s);
+  conv_statement_aux ctx s
+
+and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.view stmt with
+  | PA.Stmt_set_logic s -> [A.SetLogic s]
+  | PA.Stmt_set_option l -> [A.SetOption l]
+  | PA.Stmt_set_info l -> [A.SetInfo l]
+  | PA.Stmt_exit -> [A.Exit]
+  | PA.Stmt_decl_sort (s,n) ->
+    let id = Ctx.add_id ctx s (Ctx.K_ty Ctx.K_uninterpreted) in
+    [A.TyDecl (id,n)]
+  | PA.Stmt_decl fr ->
+    let f, ty = conv_fun_decl ctx fr in
+    let id = Ctx.add_id ctx f (Ctx.K_fun ty) in
+    [A.Decl (id, ty)]
+  | PA.Stmt_data ([],l) ->
+    (* first, read and declare each datatype (it can occur in the other
+    datatypes' construtors) *)
+    let pre_parse (data_name,cases) =
+      let data_id = Ctx.add_id ctx data_name (Ctx.K_ty Ctx.K_data) in
+      data_id, cases
+    in
+    let l = List.map pre_parse l in
+    (* now parse constructors *)
+    let l =
+     List.map
+       (fun (data_id, (cstors:PA.cstor list)) ->
+         let data_ty = A.Ty.const data_id in
+         let parse_case {PA.cstor_name=c; cstor_args} =
+           let selectors =
+             List.map (fun (n,ty) -> Some n, conv_ty_fst ctx ty) cstor_args
+           in
+           let ty_args = List.map snd selectors in
+           (* declare cstor *)
+           let ty_c = A.Ty.arrow_l ty_args data_ty in
+           let id_c = Ctx.add_id ctx c (Ctx.K_cstor ty_c) in
+           (* now declare selectors *)
+           List.iteri
+             (fun i (name_opt,ty) -> match name_opt with
+                | None -> ()
+                | Some select_str ->
+                  (* declare this selector *)
+                  let rec select_name = lazy
+                    (Ctx.add_id ctx select_str
+                       (Ctx.K_select (ty,
+                          {A.select_name; select_cstor=id_c; select_i=i})))
+                  in
+                  ignore (Lazy.force select_name))
+             selectors;
+           (* return cstor *)
+           id_c, ty_c
+         in
+         let cstors = List.map parse_case cstors in
+         (* update info on [data] *)
+         Ctx.add_data ctx data_id cstors;
+         {A.Ty.data_id; data_cstors=ID.Map.of_list cstors})
+      l
+    in
+    [A.Data l]
+  | PA.Stmt_data _ ->
+    errorf_ctx ctx "not implemented: parametric datatypes" PA.pp_stmt stmt
+  | PA.Stmt_funs_rec defs ->
+    (* errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt *)
+    let {PA.fsr_decls=decls; fsr_bodies=bodies} = defs in
+    if List.length decls <> List.length bodies then (
+      errorf_ctx ctx "declarations and bodies should have same length";
+    );
+    let defs = conv_fun_defs ctx decls bodies in
+    [A.Define defs]
+  | PA.Stmt_fun_def
+      {PA.fr_decl={PA.fun_ty_vars=[]; fun_args=[]; fun_name; fun_ret}; fr_body} ->
+    (* turn [def f : ret := body] into [decl f : ret; assert f=body] *)
+    let ret = conv_ty_fst ctx fun_ret in
+    let id = Ctx.add_id ctx fun_name (Ctx.K_fun ret) in
+    let rhs = conv_term ctx fr_body in
+    [ A.Decl (id,ret);
+      A.Assert (A.eq (A.const id ret) rhs);
+    ]
+  | PA.Stmt_fun_rec _
+  | PA.Stmt_fun_def _
+    -> errorf_ctx ctx "unsupported definition: %a" PA.pp_stmt stmt
+  | PA.Stmt_assert t ->
+    let t = conv_term ctx t in
+    check_bool_ t;
+    [A.Assert t]
+  | PA.Stmt_assert_not ([], t) ->
+    let vars, t = A.unfold_binder A.Forall (conv_term ctx t) in
+    let g = A.not_ t in (* negate *)
+    [A.Goal (vars, g)]
+  | PA.Stmt_assert_not (_::_, _) ->
+    errorf_ctx ctx "cannot convert polymorphic goal@ `@[%a@]`"
+      PA.pp_stmt stmt
+  | PA.Stmt_lemma _ ->
+    errorf_ctx ctx "smbc does not know how to handle `lemma` statements"
+  | PA.Stmt_check_sat -> [A.CheckSat]
+

src/smtlib/Convert.mli

@@ -0,0 +1,24 @@
+
+(* This file is free software. See file "license" for more details. *)
+
+(** {1 Preprocessing AST} *)
+
+module Loc = Locations
+
+type 'a or_error = ('a, string) CCResult.t
+
+(** {2 Parsing and Typing} *)
+
+module Ctx : sig
+  type t
+  val create: unit -> t
+  val pp : t CCFormat.printer
+end
+
+module PA = Parse_ast
+module A = Dagon_smt.Ast
+
+val conv_term : Ctx.t -> PA.term -> A.term
+
+val conv_statement : Ctx.t -> PA.statement -> A.statement list
+

src/smtlib/Dagon_smtlib.ml

@@ -0,0 +1,456 @@
+
+(** {1 Process Statements} *)
+
+open Dagon_smt
+
+module Fmt = CCFormat
+module A = Ast
+module PA = Parse_ast
+module E = CCResult
+module Loc = Locations
+
+type 'a or_error = ('a, string) CCResult.t
+
+module Parse = struct
+  let parse_chan_exn ?(filename="<no name>") ic =
+    let lexbuf = Lexing.from_channel ic in
+    Loc.set_file lexbuf filename;
+    Parser.parse_list Lexer.token lexbuf
+
+  let parse_chan ?filename ic =
+    try Result.Ok (parse_chan_exn ?filename ic)
+    with e -> Result.Error (Printexc.to_string e)
+
+  let parse_file_exn file : PA.statement list =
+    CCIO.with_in file (parse_chan_exn ~filename:file)
+
+  let parse_file file =
+    try Result.Ok (parse_file_exn file)
+    with e -> Result.Error (Printexc.to_string e)
+
+  let parse_file_exn ctx file : Ast.statement list =
+    (* delegate parsing to [Tip_parser] *)
+    parse_file_exn file
+    |> CCList.flat_map (Convert.conv_statement ctx)
+
+  let parse file =
+    let ctx = Convert.Ctx.create () in
+    try Result.Ok (parse_file_exn ctx file)
+    with e -> Result.Error (Printexc.to_string e)
+
+  let parse_stdin () =
+    let ctx = Convert.Ctx.create () in
+    try
+      parse_chan_exn ~filename:"<stdin>" stdin
+      |> CCList.flat_map (Convert.conv_statement ctx)
+      |> CCResult.return
+    with e -> Result.Error (Printexc.to_string e)
+end
+
+let parse = Parse.parse
+let parse_stdin = Parse.parse_stdin
+
+(** {2 Conversion into {!Term.t}} *)
+
+module Subst = struct
+  type 'a t = 'a ID.Map.t
+  let empty = ID.Map.empty
+  let mem subst v = ID.Map.mem (A.Var.id v) subst
+  let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out
+  let add subst v t =
+    if mem subst v then (
+      Util.errorf "%a already bound" A.Var.pp v;
+    );
+    ID.Map.add (A.Var.id v) t subst
+  let find subst v = ID.Map.get (A.Var.id v) subst
+  let find_exn subst v = ID.Map.find (A.Var.id v) subst
+end
+
+let mk_ite_id =
+  let n = ref 0 in
+  fun () -> ID.makef "ite_%d" (CCRef.incr_then_get n)
+
+let mk_sub_form =
+  let n = ref 0 in
+  fun () -> ID.makef "sub_form_%d" (CCRef.incr_then_get n)
+
+let mk_lra_id =
+  let n = ref 0 in
+  fun () -> ID.makef "lra_%d" (CCRef.incr_then_get n)
+
+type term_or_form =
+  | T of A.term
+  | Rat of RLE.t (* rational linear expression *)
+
+let[@inline] ret_t t = T t
+let[@inline] ret_f f = F f
+let[@inline] ret_rat t = Rat t
+let[@inline] ret_any t = if Term.is_bool t then F (F.atom (Term.Bool.pa t)) else T t
+
+let conv_ty (reg:Reg.t) (ty:A.Ty.t) : Type.t =
+  let mk_ty = Reg.find_exn reg Mc2_unin_sort.k_make in
+  (* convert a type *)
+  let rec aux_ty (ty:A.Ty.t) : Type.t = match ty with
+    | A.Ty.Ty_bool -> Type.bool
+    | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat
+    | A.Ty.Atomic (id, args) -> mk_ty id (List.map aux_ty args)
+    | A.Ty.Arrow _ ->
+      Util.errorf "cannot convert arrow type `%a`" A.Ty.pp ty
+  in
+  aux_ty ty
+
+let conv_bool_term (reg:Reg.t) (t:A.term): atom list list =
+  let decl = Reg.find_exn reg Mc2_uf.k_decl in
+  (* polymorphic equality *)
+  let[@inline] mk_eq_ t u = Term.mk_eq t u in
+  let mk_app = Reg.find_exn reg Mc2_uf.k_app in
+  let mk_const = Reg.find_exn reg Mc2_uf.k_const in
+  let fresh = Reg.find_exn reg Mc2_propositional.k_fresh in
+  let mk_eq t u = Term.Bool.pa (mk_eq_ t u) in
+  let mk_neq t u = Term.Bool.na (mk_eq_ t u) in
+  let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in
+  let mk_lra_eq t u = mk_lra_pred Mc2_lra.Eq0 (RLE.diff t u) |> Term.Bool.pa in
+  let side_clauses : atom list list ref = ref [] in
+  (* introduce intermediate variable for LRA sub-expression *)
+  let mk_lra_expr (e:RLE.t): term = match RLE.as_const e, RLE.as_singleton e with
+    | Some n, _ -> Reg.find_exn reg Mc2_lra.k_make_const n
+    | None, Some (n,t) when Q.equal n Q.one -> t
+    | _ ->
+      let id = mk_lra_id() in
+      Log.debugf 30
+        (fun k->k"(@[smtlib.name_lra@ %a@ :as %a@])" RLE.pp e ID.pp id);
+      decl id [] (Reg.find_exn reg Mc2_lra.k_rat);
+      let t = mk_const id in
+      side_clauses := [mk_lra_eq (RLE.singleton1 t) e] :: !side_clauses;
+      t
+  in
+  (* adaptative equality *)
+  let mk_eq_t_tf (t:term) (u:term_or_form) : F.t = match u with
+    | F u -> F.equiv (F.atom (Term.Bool.pa t)) u
+    | T u when Term.is_bool u ->
+      F.equiv (F.atom (Term.Bool.pa t)) (F.atom (Term.Bool.pa u))
+    | T u -> mk_eq t u |> F.atom
+    | Rat u -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
+  and mk_eq_tf_tf (t:term_or_form) (u:term_or_form) = match t, u with
+    | T t, T u -> mk_eq t u |> F.atom
+    | T t, Rat u | Rat u, T t -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
+    | Rat t, Rat u -> mk_lra_eq t u |> F.atom
+    | F t, F u -> F.equiv t u
+    | _ -> assert false
+  in
+  (* convert term *)
+  let rec aux (subst:term_or_form Subst.t) (t:A.term) : term_or_form =
+    begin match A.term_view t with
+      | A.Var v ->
+        begin match Subst.find subst v with
+          | None -> Util.errorf "variable %a not bound" A.Var.pp v
+          | Some t -> t
+        end
+      | A.Const id -> mk_const id |> ret_any
+      | A.App (f, l) ->
+        let l = List.map (aux_t subst) l in
+        begin match A.term_view f with
+          | A.Const id -> mk_app id l |> ret_any
+          | _ -> Util.errorf "cannot process HO application %a" A.pp_term t
+        end
+      | A.If (a,b,c) ->
+        let a = aux_form subst a in
+        let b = aux subst b in
+        let c = aux subst c in
+        let ty_b = match b with
+          | F _ -> Type.bool
+          | T t -> Term.ty t
+          | Rat _ -> Reg.find_exn reg Mc2_lra.k_rat
+        in
+        let placeholder_id = mk_ite_id () in
+        Log.debugf 30
+          (fun k->k"(@[smtlib.name_term@ %a@ :as %a@])" A.pp_term t ID.pp placeholder_id);
+        decl placeholder_id [] ty_b;
+        let placeholder = mk_const placeholder_id in
+        (* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *)
+        let form =
+          F.and_
+            [ F.imply a (mk_eq_t_tf placeholder b);
+              F.imply (F.not_ a) (mk_eq_t_tf placeholder c);
+            ]
+        in
+        side_clauses := List.rev_append (mk_cnf form) !side_clauses;
+        ret_t placeholder
+      | A.Let (v,t,u) ->
+        let subst = Subst.add subst v (aux subst t) in
+        aux subst u
+      | A.Op (A.And, l) -> F.and_ (List.map (aux_form subst) l) |> ret_f
+      | A.Op (A.Or, l) -> F.or_ (List.map (aux_form subst) l) |> ret_f
+      | A.Op (A.Imply, l) ->
+        let rec curry_imply_ = function
+          | [] -> assert false
+          | [a] -> aux_form subst a
+          | a :: b -> F.imply (aux_form subst a) (curry_imply_ b)
+        in
+        curry_imply_ l |> ret_f
+      | A.Op (A.Eq, l) ->
+        let l = List.map (aux subst) l in
+        let rec curry_eq = function
+          | [] | [_] -> assert false
+          | [a;b] -> [mk_eq_tf_tf a b]
+          | a :: b :: tail ->
+            mk_eq_tf_tf a b :: curry_eq (b::tail)
+        in
+        F.and_ (curry_eq l) |> ret_f
+      | A.Op (A.Distinct, l) ->
+        (* TODO: more efficient "distinct"? *)
+        List.map (aux_t subst) l
+        |> CCList.diagonal
+        |> List.map (fun (t,u) -> mk_neq t u |> F.atom)
+        |> F.and_ |> ret_f
+      | A.Not f -> F.not_ (aux_form subst f) |> ret_f
+      | A.Bool_term true -> ret_f F.true_
+      | A.Bool_term false -> ret_f F.false_
+      | A.Num_q n -> Mc2_lra.LE.const n |> ret_rat
+      | A.Num_z n -> Mc2_lra.LE.const (Q.of_bigint n) |> ret_rat
+      | A.Arith (op, l) ->
+        let l = List.map (aux_rat subst) l in
+        begin match op, l with
+          | A.Minus, [a] -> RLE.neg a |> ret_rat
+          | _, [] | _, [_] ->
+            Util.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t
+          | A.Leq, [a;b] ->
+            let e = RLE.diff a b in
+            mk_lra_pred Mc2_lra.Leq0 e |> ret_any
+          | A.Geq, [a;b] ->
+            let e = RLE.diff b a in
+            mk_lra_pred Mc2_lra.Leq0 e |> ret_any
+          | A.Lt, [a;b] ->
+            let e = RLE.diff a b in
+            mk_lra_pred Mc2_lra.Lt0 e |> ret_any
+          | A.Gt, [a;b] ->
+            let e = RLE.diff b a in
+            mk_lra_pred Mc2_lra.Lt0 e |> ret_any
+          | (A.Leq | A.Lt | A.Geq | A.Gt), _ ->
+            Util.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t
+          | A.Add, _ ->
+            let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in
+            mk_lra_expr e |> ret_t
+          | A.Minus, a::tail ->
+            let e =
+              List.fold_left
+                (fun n t -> RLE.diff n t)
+                a tail
+            in
+            mk_lra_expr e |> ret_t
+          | A.Mult, _::_::_ ->
+            let coeffs, terms =
+              CCList.partition_map
+                (fun t -> match RLE.as_const t with
+                   | None -> `Right t
+                   | Some c -> `Left c)
+                l
+            in
+            begin match coeffs, terms with
+              | c::c_tail, [] ->
+                List.fold_right RLE.mult c_tail (RLE.const c) |> ret_rat
+              | _, [t] ->
+                List.fold_right RLE.mult coeffs t |> ret_rat
+              | _ ->
+                Util.errorf "non-linear expr:@ `%a`" A.pp_term t
+            end
+          | A.Div, (first::l) ->
+            (* support t/a/b/c where only [t] is a rational *)
+            let coeffs =
+              List.map
+                (fun c -> match RLE.as_const c with
+                   | None ->
+                     Util.errorf "non-linear expr:@ `%a`" A.pp_term t
+                   | Some c -> Q.inv c)
+                l
+            in
+            List.fold_right RLE.mult coeffs first |> ret_rat
+        end
+      | A.Select _ -> assert false (* TODO *)
+      | A.Match _ -> assert false (* TODO *)
+      | A.Bind _ -> assert false (* TODO *)
+    end
+
+  (* expect a term *)
+  and aux_t subst (t:A.term) : term = match aux subst t with
+    | T t -> t
+    | Rat e -> mk_lra_expr e
+    | F (F.Lit a) when Atom.is_pos a -> Atom.term a
+    | F f ->
+      (* name the sub-formula and add CNF *)
+      let placeholder_id = mk_sub_form() in
+      decl placeholder_id [] Type.bool;
+      let placeholder = mk_const placeholder_id in
+      (* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *)
+      let form = F.equiv (F.atom (Term.Bool.pa placeholder)) f in
+      side_clauses := List.rev_append (mk_cnf form) !side_clauses;
+      placeholder
+
+  (* convert formula *)
+  and aux_form subst (t:A.term): F.t = match aux subst t with
+    | T t -> F.atom (Term.Bool.pa t)
+    | F f -> f
+    | Rat _ -> Util.errorf "expected proposition,@ got %a" A.pp_term t
+
+  (* expect a rational expr *)
+  and aux_rat subst (t:A.term) : RLE.t = match aux subst t with
+    | Rat e -> e
+    | T t -> RLE.singleton1 t
+    | F _ -> assert false
+
+  and mk_cnf (f:F.t) : atom list list =
+    F.cnf ~fresh f
+  in
+  let cs = aux_form Subst.empty t |> mk_cnf in
+  List.rev_append !side_clauses cs
+
+(** {2 Processing Statements} *)
+
+(* list of (local) hypothesis *)
+let hyps = ref []
+
+let check_model state : bool =
+  Log.debug 4 "checking model";
+  let check_clause c =
+    Log.debugf 15
+      (fun k -> k "(@[check.clause@ %a@])" Clause.debug_atoms c);
+    let ok =
+      List.exists (fun t -> Solver.Sat_state.eval_opt state t = Some true) c
+    in
+    if not ok then (
+      Log.debugf 0
+        (fun k->k "(@[check.fail:@ clause %a@ not satisfied in model@])" Clause.debug_atoms c);
+    );
+    ok
+  in
+  Solver.Sat_state.check_model state &&
+  List.for_all check_clause !hyps
+
+module Dot = Mc2_backend.Dot.Make(Mc2_backend.Dot.Default)
+
+(* call the solver to check-sat *)
+let solve
+    ?gc ?restarts ?dot_proof
+    ?(pp_model=false) ?(check=false) ?time ?memory ?progress
+    ~assumptions s : unit =
+  let t1 = Sys.time() in
+  let res = Solver.solve ?gc ?restarts ?time ?memory ?progress s ~assumptions in
+  let t2 = Sys.time () in
+  begin match res with
+    | Solver.Sat state ->
+      if pp_model then (
+        let pp_t out = function
+          | A_bool (t,b) -> Fmt.fprintf out "(@[%a@ %B@])" Term.pp t b
+          | A_semantic (t,v) -> Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Value.pp v
+        in
+        Format.printf "(@[<hv1>model@ %a@])@."
+          (Util.pp_list pp_t) (Solver.Sat_state.model state)
+      );
+      if check then (
+        if not (check_model state) then (
+          Util.error "invalid model"
+        )
+      );
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
+    | Solver.Unsat state ->
+      if check then (
+        let p = Solver.Unsat_state.get_proof state in
+        Proof.check p;
+        begin match dot_proof with
+          | None ->  ()
+          | Some file ->
+            CCIO.with_out file
+              (fun oc ->
+                 Log.debugf 1 (fun k->k "write proof into `%s`" file);
+                 let fmt = Format.formatter_of_out_channel oc in
+                 Dot.print fmt p;
+                 Format.pp_print_flush fmt (); flush oc)
+        end
+      );
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
+  end
+
+(* process a single statement *)
+let process_stmt
+    ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
+    ?time ?memory ?progress
+    (solver:Solver.t)
+    (stmt:Ast.statement) : unit or_error =
+  Log.debugf 5
+    (fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt);
+  let decl_sort = Solver.get_service_exn solver Mc2_unin_sort.k_decl_sort in
+  let decl = Solver.get_service_exn solver Mc2_uf.k_decl in
+  let conv_ty = conv_ty (Solver.services solver) in
+  begin match stmt with
+    | A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return ()
+    | A.SetLogic s ->
+      Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
+      E.return ()
+    | A.SetOption l ->
+      Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l);
+      E.return ()
+    | A.SetInfo _ -> E.return ()
+    | A.Exit ->
+      Log.debug 1 "exit";
+      raise Exit
+    | A.CheckSat ->
+      solve ?gc ?restarts ?dot_proof ?check ?pp_model ?time ?memory ?progress
+        solver ~assumptions:[];
+      E.return()
+    | A.TyDecl (id,n) ->
+      decl_sort id n;
+      E.return ()
+    | A.Decl (f,ty) ->
+      let ty_args, ty_ret = A.Ty.unfold ty in
+      let ty_args = List.map conv_ty ty_args in
+      let ty_ret = conv_ty ty_ret in
+      decl f ty_args ty_ret;
+      E.return ()
+    | A.Assert t ->
+      let clauses =
+        conv_bool_term (Solver.services solver) t
+      in
+      if pp_cnf then (
+        Format.printf "(@[<hv1>assert@ %a@])@."
+          (Util.pp_list Clause.pp_atoms) clauses;
+      );
+      hyps := clauses @ !hyps;
+      Solver.assume solver clauses;
+      E.return()
+    | A.Goal (_, _) ->
+      Util.errorf "cannot deal with goals yet"
+
+      (*
+    | Dolmen.Statement.Def (id, t) -> T.def id t
+    | Dolmen.Statement.Decl (id, t) -> T.decl id t
+    | Dolmen.Statement.Consequent t ->
+      let cnf = T.consequent t in
+      pp_cnf solver cnf;
+      hyps := cnf @ !hyps;
+      S.assume s cnf
+    | Dolmen.Statement.Antecedent t ->
+      let cnf = T.antecedent t in
+      pp_cnf cnf;
+      hyps := cnf @ !hyps;
+      S.assume cnf
+    | Dolmen.Statement.Pack [
+        { Dolmen.Statement.descr = Dolmen.Statement.Push 1; _ };
+        { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; _ };
+        { Dolmen.Statement.descr = Dolmen.Statement.Prove; _ };
+        { Dolmen.Statement.descr = Dolmen.Statement.Pop 1; _ };
+      ] ->
+      let assumptions = T.assumptions f in
+      prove solver ~assumptions
+    | Dolmen.Statement.Prove ->
+      prove solver ~assumptions:[]
+    | Dolmen.Statement.Set_info _
+    | Dolmen.Statement.Set_logic _ -> ()
+    | Dolmen.Statement.Exit -> exit 0
+    | _ ->
+      Format.printf "Command not supported:@\n%a@."
+        Dolmen.Statement.print s
+         *)
+  end
+

src/smtlib/Dagon_smtlib.mli

@@ -0,0 +1,34 @@
+
+(** {1 SMTLib-2 Interface} *)
+
+(** This library provides a parser, a type-checker, and a solver interface
+    for processing SMTLib-2 problems.
+*)
+
+type 'a or_error = ('a, string) CCResult.t
+
+module Ast = Ast
+
+val parse : string -> Dagon_smt.Ast.statement list or_error
+
+val parse_stdin : unit -> Dagon_smt.Ast.statement list or_error
+
+val conv_bool_term : Dagon_smt.Term.state -> Dagon_smt.Ast.term -> Dagon_smt.Lit.t list list
+(** Convert a boolean term into CNF *)
+
+val process_stmt :
+  ?gc:bool ->
+  ?restarts:bool ->
+  ?pp_cnf:bool ->
+  ?dot_proof:string ->
+  ?pp_model:bool ->
+  ?check:bool ->
+  ?time:float ->
+  ?memory:float ->
+  ?progress:bool ->
+  Dagon_smt.Solver.t ->
+  Dagon_smt.Ast.statement ->
+  unit or_error
+(** Process the given statement.
+    @raise Incorrect_model if model is not correct
+*)

src/smtlib/Lexer.mll

@@ -0,0 +1,95 @@
+
+(* This file is free software. See file "license" for more details. *)
+
+(** {1 Lexer for TIP} *)
+
+{
+  module A = Parse_ast
+  module Loc = Locations
+  open Parser (* for tokens *)
+
+}
+
+let printable_char = [^ '\n']
+let comment_line = ';' printable_char*
+
+let sym = [^ '"' '(' ')' '\\' ' ' '\t' '\r' '\n']
+
+let ident = sym+
+
+let quoted = '"' ([^ '"'] | '\\' '"')* '"'
+let escaped = '|' [^ '|']* '|'
+
+rule token = parse
+  | eof { EOI }
+  | '\n' { Lexing.new_line lexbuf; token lexbuf }
+  | [' ' '\t' '\r'] { token lexbuf }
+  | comment_line { token lexbuf }
+  | '(' { LEFT_PAREN }
+  | ')' { RIGHT_PAREN }
+  | "true" { TRUE }
+  | "false" { FALSE }
+  | "or" { OR }
+  | "and" { AND }
+  | "not" { NOT }
+  | "xor" { XOR }
+  | "distinct" { DISTINCT }
+  | "ite" { IF }
+  | "as" { AS }
+  | "match" { MATCH }
+  | "case" { CASE }
+  | "default" { DEFAULT }
+  | "lambda" { FUN }
+  | "let" { LET }
+  | "par" { PAR }
+  | "=>" { ARROW }
+  | "=" { EQ }
+  | "@" { AT }
+  | "+" { ADD }
+  | "-" { MINUS }
+  | "*" { PROD }
+  | "/" { DIV }
+  | "<=" { LEQ }
+  | "<" { LT }
+  | ">=" { GEQ }
+  | ">" { GT }
+  | "declare-datatypes" { DATA }
+  | "assert" { ASSERT }
+  | "lemma" { LEMMA }
+  | "assert-not" { ASSERT_NOT }
+  | "declare-sort" { DECLARE_SORT }
+  | "declare-fun" { DECLARE_FUN }
+  | "declare-const" { DECLARE_CONST }
+  | "define-fun" { DEFINE_FUN }
+  | "define-fun-rec" { DEFINE_FUN_REC }
+  | "define-funs-rec" { DEFINE_FUNS_REC }
+  | "forall" { FORALL }
+  | "exists" { EXISTS }
+  | "check-sat" { CHECK_SAT }
+  | "set-logic" { SET_LOGIC }
+  | "set-option" { SET_OPTION }
+  | "set-info" { SET_INFO }
+  | "exit" { EXIT }
+  | ident {
+    let s = Lexing.lexeme lexbuf in
+    IDENT(s)
+  }
+  | quoted {
+      (* TODO: unescape *)
+      let s = Lexing.lexeme lexbuf in
+      let s = String.sub s 1 (String.length s -2) in (* remove " " *)
+      QUOTED s }
+  | escaped {
+      let s = Lexing.lexeme lexbuf in
+      CCString.iter (function '\n' -> Lexing.new_line lexbuf | _ -> ()) s;
+      let s = String.sub s 1 (String.length s -2) in (* remove "|" *)
+      ESCAPED s }
+  | _ as c
+    {
+      let loc = Loc.of_lexbuf lexbuf in
+      A.parse_errorf ~loc "unexpected char '%c'" c
+    }
+
+{
+
+}

src/smtlib/Locations.ml

@@ -0,0 +1,71 @@
+
+(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *)
+
+(** {1 Locations} *)
+
+type t = {
+  file : string;
+  start_line : int;
+  start_column : int;
+  stop_line : int;
+  stop_column : int;
+}
+
+let mk file start_line start_column stop_line stop_column =
+  { file; start_line; start_column; stop_line; stop_column; }
+
+let mk_pair file (a,b)(c,d) = mk file a b c d
+
+let mk_pos start stop =
+  let open Lexing in
+  mk
+    start.pos_fname
+    start.pos_lnum (start.pos_cnum - start.pos_bol)
+    stop.pos_lnum (stop.pos_cnum - stop.pos_bol)
+
+let equal = (=)
+
+let pp out pos =
+  if pos.start_line = pos.stop_line
+  then
+    Format.fprintf out "file '%s': line %d, col %d to %d"
+      pos.file pos.start_line pos.start_column pos.stop_column
+  else
+    Format.fprintf out "file '%s': line %d, col %d to line %d, col %d"
+      pos.file
+      pos.start_line pos.start_column
+      pos.stop_line pos.stop_column
+
+let pp_opt out = function
+  | None -> Format.fprintf out "<no location>"
+  | Some pos -> pp out pos
+
+let pp_to_string pp x =
+  let buf = Buffer.create 64 in
+  let fmt = Format.formatter_of_buffer buf in
+  pp fmt x;
+  Format.pp_print_flush fmt ();
+  Buffer.contents buf
+
+let to_string_opt = pp_to_string pp_opt
+
+(** {2 Lexbuf} *)
+
+let set_file buf filename =
+  let open Lexing in
+  buf.lex_curr_p <- {buf.lex_curr_p with pos_fname=filename;};
+  ()
+
+let get_file buf =
+  let open Lexing in
+  buf.lex_curr_p.pos_fname
+
+let of_lexbuf lexbuf =
+  let start = Lexing.lexeme_start_p lexbuf in
+  let end_ = Lexing.lexeme_end_p lexbuf in
+  let s_l = start.Lexing.pos_lnum in
+  let s_c = start.Lexing.pos_cnum - start.Lexing.pos_bol in
+  let e_l = end_.Lexing.pos_lnum in
+  let e_c = end_.Lexing.pos_cnum - end_.Lexing.pos_bol in
+  let file = get_file lexbuf in
+  mk file s_l s_c e_l e_c

src/smtlib/Parse_ast.ml

@@ -0,0 +1,294 @@
+
+(* This file is free software. See file "license" for more details. *)
+
+(** {1 Simple AST for parsing} *)
+
+module Loc = Locations
+module Fmt = CCFormat
+
+let pp_str = Format.pp_print_string
+
+let pp_to_string pp x =
+  let buf = Buffer.create 64 in
+  let fmt = Format.formatter_of_buffer buf in
+  pp fmt x;
+  Format.pp_print_flush fmt ();
+  Buffer.contents buf
+
+type var = string
+type ty_var = string
+
+(** Polymorphic types *)
+type ty =
+  | Ty_bool
+  | Ty_app of ty_var * ty list
+  | Ty_arrow of ty list * ty
+
+type typed_var = var * ty
+
+type arith_op =
+  | Leq
+  | Lt
+  | Geq
+  | Gt
+  | Add
+  | Minus
+  | Mult
+  | Div
+
+(** {2 AST: S-expressions with locations} *)
+type term =
+  | True
+  | False
+  | Const of string
+  | Arith of arith_op * term list
+  | App of string * term list
+  | HO_app of term * term (* higher-order application *)
+  | Match of term * match_branch list
+  | If of term * term * term
+  | Let of (var * term) list * term
+  | Fun of typed_var * term
+  | Eq of term * term
+  | Imply of term * term
+  | And of term list
+  | Or of term list
+  | Not of term
+  | Xor of term * term
+  | Distinct of term list
+  | Cast of term * ty (* type cast *)
+  | Forall of (var * ty) list * term
+  | Exists of (var * ty) list * term
+
+and match_branch =
+  | Match_default of term
+  | Match_case of string * var list * term
+
+type cstor = {
+  cstor_name: string;
+  cstor_args: (string * ty) list; (* selector+type *)
+}
+
+type 'arg fun_decl = {
+  fun_ty_vars: ty_var list;
+  fun_name: string;
+  fun_args: 'arg list;
+  fun_ret: ty;
+}
+
+type fun_def = {
+  fr_decl: typed_var fun_decl;
+  fr_body: term;
+}
+
+type funs_rec_def = {
+  fsr_decls: typed_var fun_decl list;
+  fsr_bodies: term list;
+}
+
+type statement = {
+  stmt: stmt;
+  loc: Loc.t option;
+}
+
+and stmt =
+  | Stmt_decl_sort of string * int (* arity *)
+  | Stmt_decl of ty fun_decl
+  | Stmt_fun_def of fun_def
+  | Stmt_fun_rec of fun_def
+  | Stmt_funs_rec of funs_rec_def
+  | Stmt_data of ty_var list * (string * cstor list) list
+  | Stmt_assert of term
+  | Stmt_lemma of term
+  | Stmt_assert_not of ty_var list * term
+  | Stmt_set_logic of string
+  | Stmt_set_option of string list
+  | Stmt_set_info of string list
+  | Stmt_check_sat
+  | Stmt_exit
+
+let ty_bool = Ty_bool
+let ty_app s l = Ty_app (s,l)
+let ty_const s = ty_app s []
+let ty_arrow_l args ret = if args=[] then ret else Ty_arrow (args, ret)
+let ty_arrow a b = ty_arrow_l [a] b
+
+let true_ = True
+let false_ = False
+let const s = Const s
+let app f l = App (f,l)
+let ho_app a b = HO_app (a,b)
+let ho_app_l a l = List.fold_left ho_app a l
+let match_ u l = Match (u,l)
+let if_ a b c = If(a,b,c)
+let fun_ v t = Fun (v,t)
+let fun_l = List.fold_right fun_
+let let_ l t = Let (l,t)
+let eq a b = Eq (a,b)
+let imply a b = Imply(a,b)
+let xor a b = Xor (a,b)
+let and_ l = And l
+let or_ l = Or l
+let distinct l = Distinct l
+let cast t ~ty = Cast (t, ty)
+let forall vars f = match vars with [] -> f | _ -> Forall (vars, f)
+let exists vars f = match vars with [] -> f | _ -> Exists (vars, f)
+let rec not_ t = match t with
+  | Forall (vars,u) -> exists vars (not_ u)
+  | Exists (vars,u) -> forall vars (not_ u)
+  | _ -> Not t
+
+let arith op l = Arith (op,l)
+
+let _mk ?loc stmt = { loc; stmt }
+
+let mk_cstor name l : cstor = { cstor_name=name; cstor_args=l }
+let mk_fun_decl ~ty_vars f args ret =
+  { fun_ty_vars=ty_vars; fun_name=f;
+    fun_args=args; fun_ret=ret; }
+let mk_fun_rec ~ty_vars f args ret body =
+  { fr_decl=mk_fun_decl ~ty_vars f args ret; fr_body=body; }
+
+let decl_sort ?loc s ~arity = _mk ?loc (Stmt_decl_sort (s, arity))
+let decl_fun ?loc ~tyvars f ty_args ty_ret =
+  let d = {fun_ty_vars=tyvars; fun_name=f; fun_args=ty_args; fun_ret=ty_ret} in
+  _mk ?loc (Stmt_decl d)
+let fun_def ?loc fr = _mk ?loc (Stmt_fun_def fr)
+let fun_rec ?loc fr = _mk ?loc (Stmt_fun_rec fr)
+let funs_rec ?loc decls bodies = _mk ?loc (Stmt_funs_rec {fsr_decls=decls; fsr_bodies=bodies})
+let data ?loc tyvars l = _mk ?loc (Stmt_data (tyvars,l))
+let assert_ ?loc t = _mk ?loc (Stmt_assert t)
+let lemma ?loc t = _mk ?loc (Stmt_lemma t)
+let assert_not ?loc ~ty_vars t = _mk ?loc (Stmt_assert_not (ty_vars, t))
+let set_logic ?loc s = _mk ?loc (Stmt_set_logic s)
+let set_option ?loc l = _mk ?loc (Stmt_set_option l)
+let set_info ?loc l = _mk ?loc (Stmt_set_info l)
+let check_sat ?loc () = _mk ?loc Stmt_check_sat
+let exit ?loc () = _mk ?loc Stmt_exit
+
+let loc t = t.loc
+let view t = t.stmt
+
+let fpf = Format.fprintf
+
+
+let pp_tyvar = pp_str
+
+let rec pp_ty out (ty:ty) = match ty with
+  | Ty_bool -> pp_str out "Bool"
+  | Ty_app (s,[]) -> pp_str out s
+  | Ty_app (s,l) -> Format.fprintf out "(@[<hv1>%s@ %a@])" s (Util.pp_list pp_ty) l
+  | Ty_arrow (args,ret) ->
+    fpf out "(@[=>@ %a@ %a@])" (Util.pp_list pp_ty) args pp_ty ret
+
+let pp_arith out = function
+  | Leq -> Fmt.string out "<="
+  | Lt -> Fmt.string out "<"
+  | Geq -> Fmt.string out ">="
+  | Gt -> Fmt.string out ">"
+  | Add -> Fmt.string out "+"
+  | Minus -> Fmt.string out "-"
+  | Mult -> Fmt.string out "*"
+  | Div -> Fmt.string out "/"
+
+let rec pp_term out (t:term) = match t with
+  | True -> pp_str out "true"
+  | False -> pp_str out "false"
+  | Arith (op,l) ->
+    Fmt.fprintf out "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp_term) l
+  | Const s -> pp_str out s
+  | App (f,l) -> fpf out "(@[<1>%s@ %a@])" f (Util.pp_list pp_term) l
+  | HO_app (a,b) -> fpf out "(@[<1>@@@ %a@ %a@])" pp_term a pp_term b
+  | Match (lhs,cases) ->
+    let pp_case out = function
+      | Match_default rhs -> fpf out "(@[<1>case default@ %a@])" pp_term rhs
+      | Match_case (c,[],rhs) ->
+        fpf out "(@[<1>case %s@ %a@])" c pp_term rhs
+      | Match_case (c,vars,rhs) ->
+        fpf out "(@[<1>case@ (@[%s@ %a@])@ %a@])" c (Util.pp_list pp_str) vars pp_term rhs
+    in
+    fpf out "(@[<1>match@ %a@ @[<v>%a@]@])" pp_term lhs
+      (Util.pp_list pp_case) cases
+  | If (a,b,c) -> fpf out "(@[<hv1>ite %a@ %a@ %a@])" pp_term a pp_term b pp_term c
+  | Fun (v,body) -> fpf out "(@[<1>lambda @ (%a)@ %a@])" pp_typed_var v pp_term body
+  | Let (l,t) ->
+    let pp_binding out (v,t) = fpf out "(@[%s@ %a@])" v pp_term t in
+    fpf out "(@[let@ (@[%a@])@ %a@])" (Util.pp_list pp_binding) l pp_term t
+  | Eq (a,b) -> fpf out "(@[=@ %a@ %a@])" pp_term a pp_term b
+  | Imply (a,b) -> fpf out "(@[=>@ %a@ %a@])" pp_term a pp_term b
+  | Xor(a,b) -> fpf out "(@[xor@ %a@ %a@])" pp_term a pp_term b
+  | And l -> fpf out "(@[<hv>and@ %a@])" (Util.pp_list pp_term) l
+  | Or l -> fpf out "(@[<hv>or@ %a@])" (Util.pp_list pp_term) l
+  | Not t -> fpf out "(not %a)" pp_term t
+  | Distinct l -> fpf out "(@[distinct@ %a@])" (Util.pp_list pp_term) l
+  | Cast (t, ty) -> fpf out "(@[<hv1>as@ @[%a@]@ @[%a@]@])" pp_term t pp_ty ty
+  | Forall (vars,f) ->
+    fpf out "(@[<hv1>forall@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
+  | Exists (vars,f) ->
+    fpf out "(@[<hv1>exists@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
+and pp_typed_var out (v,ty) =
+  fpf out "(@[%s@ %a@])" v pp_ty ty
+
+let pp_par pp_x out (ty_vars,x) = match ty_vars with
+  | [] -> pp_x out x
+  | _ ->
+    fpf out "(@[<1>par (@[%a@])@ (%a)@])" (Util.pp_list pp_tyvar) ty_vars pp_x x
+
+let pp_fun_decl pp_arg out fd =
+  fpf out "%s@ (@[%a@])@ %a"
+    fd.fun_name (Util.pp_list pp_arg) fd.fun_args pp_ty fd.fun_ret
+
+let pp_fr out fr =
+  fpf out "@[<1>%a@ %a@]" (pp_fun_decl pp_typed_var) fr.fr_decl pp_term fr.fr_body
+
+let pp_stmt out (st:statement) = match view st with
+  | Stmt_set_logic s -> fpf out "(@[declare-logic@ %s@])" s
+  | Stmt_set_option l -> fpf out "(@[set-option@ %a@])" (Util.pp_list CCFormat.string) l
+  | Stmt_set_info l -> fpf out "(@[set-info@ %a@])" (Util.pp_list CCFormat.string) l
+  | Stmt_decl_sort (s,n) -> fpf out "(@[declare-sort@ %s %d@])" s n
+  | Stmt_assert t -> fpf out "(@[assert@ %a@])" pp_term t
+  | Stmt_lemma t -> fpf out "(@[lemma@ %a@])" pp_term t
+  | Stmt_assert_not (ty_vars,t) ->
+    fpf out "(@[assert-not@ %a@])" (pp_par pp_term) (ty_vars,t)
+  | Stmt_decl d ->
+    fpf out "(@[declare-fun@ %a@])"
+      (pp_par (pp_fun_decl pp_ty)) (d.fun_ty_vars,d)
+  | Stmt_fun_def fr ->
+    fpf out "(@[<1>define-fun@ %a@])"
+      (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
+  | Stmt_fun_rec fr ->
+    fpf out "(@[<1>define-fun-rec@ %a@])"
+      (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
+  | Stmt_funs_rec fsr ->
+    let pp_decl' out d = fpf out "(@[<1>%a@])" (pp_fun_decl pp_typed_var) d in
+    fpf out "(@[<hv1>define-funs-rec@ (@[<v>%a@])@ (@[<v>%a@])@])"
+      (Util.pp_list pp_decl') fsr.fsr_decls (Util.pp_list pp_term) fsr.fsr_bodies
+  | Stmt_data (tyvars,l) ->
+    let pp_cstor_arg out (sel,ty) = fpf out "(@[%s %a@])" sel pp_ty ty in
+    let pp_cstor out c =
+      if c.cstor_args = []
+      then fpf out "(%s)" c.cstor_name
+      else fpf out "(@[<1>%s@ %a@])" c.cstor_name (Util.pp_list pp_cstor_arg) c.cstor_args
+    in
+    let pp_data out (s,cstors) =
+      fpf out "(@[<1>%s@ @[<v>%a@]@])" s (Util.pp_list pp_cstor) cstors
+    in
+    fpf out "(@[<hv1>declare-datatypes@ (@[%a@])@ (@[<v>%a@])@])"
+      (Util.pp_list pp_tyvar) tyvars (Util.pp_list pp_data) l
+  | Stmt_check_sat -> pp_str out "(check-sat)"
+  | Stmt_exit -> pp_str out "(exit)"
+
+(** {2 Errors} *)
+
+exception Parse_error of Loc.t option * string
+
+let () = Printexc.register_printer
+    (function
+      | Parse_error (loc, msg) ->
+        let pp out () =
+          Format.fprintf out "parse error at %a:@ %s" Loc.pp_opt loc msg
+        in
+        Some (pp_to_string pp ())
+      | _ -> None)
+
+let parse_error ?loc msg = raise (Parse_error (loc, msg))
+let parse_errorf ?loc msg = Format.ksprintf (parse_error ?loc) msg

src/smtlib/Parser.mly

@@ -0,0 +1,377 @@
+
+
+(* This file is free software, part of tip-parser. See file "license" for more details. *)
+
+(** {1 Parser for TIP} *)
+
+(* vim:SyntasticToggleMode:
+   vim:set ft=yacc: *)
+
+%{
+  module A = Parse_ast
+  module Loc = Locations
+
+%}
+
+%token EOI
+
+%token LEFT_PAREN
+%token RIGHT_PAREN
+
+%token PAR
+%token ARROW
+
+%token TRUE
+%token FALSE
+%token OR
+%token AND
+%token XOR
+%token DISTINCT
+%token NOT
+%token EQ
+%token IF
+%token MATCH
+%token CASE
+%token DEFAULT
+%token FUN
+%token LET
+%token AS
+%token AT
+
+%token LEQ
+%token LT
+%token GEQ
+%token GT
+%token ADD
+%token MINUS
+%token PROD
+%token DIV
+
+%token SET_LOGIC
+%token SET_OPTION
+%token SET_INFO
+%token DATA
+%token ASSERT
+%token LEMMA
+%token ASSERT_NOT
+%token FORALL
+%token EXISTS
+%token DECLARE_SORT
+%token DECLARE_CONST
+%token DECLARE_FUN
+%token DEFINE_FUN
+%token DEFINE_FUN_REC
+%token DEFINE_FUNS_REC
+%token CHECK_SAT
+%token EXIT
+
+%token <string>IDENT
+%token <string>QUOTED
+%token <string>ESCAPED
+
+%start <Parse_ast.term> parse_term
+%start <Parse_ast.ty> parse_ty
+%start <Parse_ast.statement> parse
+%start <Parse_ast.statement list> parse_list
+
+%%
+
+parse_list: l=stmt* EOI {l}
+parse: t=stmt EOI { t }
+parse_term: t=term EOI { t }
+parse_ty: t=ty EOI { t }
+
+cstor_arg:
+  | LEFT_PAREN name=id ty=ty RIGHT_PAREN { name, ty }
+
+cstor:
+  | LEFT_PAREN c=id RIGHT_PAREN { A.mk_cstor c [] }
+  | LEFT_PAREN c=id l=cstor_arg+ RIGHT_PAREN
+    { A.mk_cstor c l }
+
+data:
+  | LEFT_PAREN s=id l=cstor+ RIGHT_PAREN { s,l }
+
+fun_def_mono:
+  | f=id
+    LEFT_PAREN args=typed_var* RIGHT_PAREN
+    ret=ty
+    { f, args, ret }
+
+fun_decl_mono:
+  | f=id
+    LEFT_PAREN args=ty* RIGHT_PAREN
+    ret=ty
+    { f, args, ret }
+
+fun_decl:
+  | tup=fun_decl_mono { let f, args, ret = tup in [], f, args, ret }
+  | LEFT_PAREN
+      PAR
+      LEFT_PAREN tyvars=tyvar* RIGHT_PAREN
+      LEFT_PAREN tup=fun_decl_mono RIGHT_PAREN
+    RIGHT_PAREN
+    { let f, args, ret = tup in tyvars, f, args, ret }
+
+fun_rec:
+  | tup=fun_def_mono body=term
+    {
+      let f, args, ret = tup in
+      A.mk_fun_rec ~ty_vars:[] f args ret body
+    }
+  | LEFT_PAREN
+      PAR
+      LEFT_PAREN l=tyvar* RIGHT_PAREN
+      LEFT_PAREN tup=fun_def_mono body=term RIGHT_PAREN
+    RIGHT_PAREN
+    {
+      let f, args, ret = tup in
+      A.mk_fun_rec ~ty_vars:l f args ret body
+    }
+
+funs_rec_decl:
+  | LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
+    {
+      let f, args, ret = tup in
+      A.mk_fun_decl ~ty_vars:[] f args ret
+    }
+  | LEFT_PAREN
+      PAR
+      LEFT_PAREN l=tyvar* RIGHT_PAREN
+      LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
+    RIGHT_PAREN
+    {
+      let f, args, ret = tup in
+      A.mk_fun_decl ~ty_vars:l f args ret
+    }
+
+assert_not:
+  | LEFT_PAREN
+      PAR LEFT_PAREN tyvars=tyvar+ RIGHT_PAREN t=term
+    RIGHT_PAREN
+  { tyvars, t }
+  | t=term
+  { [], t }
+
+id:
+  | s=IDENT { s }
+  | s=QUOTED { s }
+  | s=ESCAPED { s }
+
+stmt:
+  | LEFT_PAREN SET_LOGIC s=id RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.set_logic ~loc s
+    }
+  | LEFT_PAREN SET_OPTION l=id+ RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.set_option ~loc l
+    }
+  | LEFT_PAREN SET_INFO l=id+ RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.set_info ~loc l
+    }
+  | LEFT_PAREN ASSERT t=term RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.assert_ ~loc t
+    }
+  | LEFT_PAREN LEMMA t=term RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.lemma ~loc t
+    }
+  | LEFT_PAREN DECLARE_SORT s=id n=id RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      try
+        let n = int_of_string n in
+        A.decl_sort ~loc s ~arity:n
+      with Failure _ ->
+        A.parse_errorf ~loc "expected arity to be an integer, not `%s`" n
+    }
+  | LEFT_PAREN DATA
+      LEFT_PAREN vars=tyvar* RIGHT_PAREN
+      LEFT_PAREN l=data+ RIGHT_PAREN
+    RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.data ~loc vars l
+    }
+  | LEFT_PAREN DECLARE_FUN tup=fun_decl RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      let tyvars, f, args, ret = tup in
+      A.decl_fun ~loc ~tyvars f args ret
+    }
+  | LEFT_PAREN DECLARE_CONST f=id ty=ty RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.decl_fun ~loc ~tyvars:[] f [] ty
+    }
+  | LEFT_PAREN DEFINE_FUN f=fun_rec RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.fun_def ~loc f
+    }
+  | LEFT_PAREN
+    DEFINE_FUN_REC
+    f=fun_rec
+    RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.fun_rec ~loc f
+    }
+  | LEFT_PAREN
+    DEFINE_FUNS_REC
+      LEFT_PAREN decls=funs_rec_decl+ RIGHT_PAREN
+      LEFT_PAREN bodies=term+ RIGHT_PAREN
+    RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.funs_rec ~loc decls bodies
+    }
+  | LEFT_PAREN
+    ASSERT_NOT
+    tup=assert_not
+    RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      let ty_vars, f = tup in
+      A.assert_not ~loc ~ty_vars f
+    }
+  | LEFT_PAREN CHECK_SAT RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.check_sat ~loc ()
+    }
+  | LEFT_PAREN EXIT RIGHT_PAREN
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.exit ~loc ()
+    }
+  | error
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.parse_errorf ~loc "expected statement"
+    }
+
+var:
+  | s=id { s }
+tyvar:
+  | s=id { s }
+
+ty:
+  | s=id {
+    begin match s with
+      | "Bool" -> A.ty_bool
+      | _ -> A.ty_const s
+    end
+    }
+  | LEFT_PAREN s=id args=ty+ RIGHT_PAREN
+    { A.ty_app s args }
+  | LEFT_PAREN ARROW tup=ty_arrow_args RIGHT_PAREN
+    {
+      let args, ret = tup in
+      A.ty_arrow_l args ret }
+  | error
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.parse_errorf ~loc "expected type"
+    }
+
+ty_arrow_args:
+  | a=ty ret=ty { [a], ret }
+  | a=ty tup=ty_arrow_args { a :: fst tup, snd tup }
+
+typed_var:
+  | LEFT_PAREN s=id ty=ty RIGHT_PAREN { s, ty }
+
+case:
+  | LEFT_PAREN
+      CASE
+      c=id
+      rhs=term
+    RIGHT_PAREN
+    { A.Match_case (c, [], rhs) }
+  | LEFT_PAREN
+      CASE
+      LEFT_PAREN c=id vars=var+ RIGHT_PAREN
+      rhs=term
+    RIGHT_PAREN
+    { A.Match_case (c, vars, rhs) }
+  | LEFT_PAREN
+     CASE DEFAULT rhs=term
+    RIGHT_PAREN
+    { A.Match_default rhs }
+
+binding:
+  | LEFT_PAREN v=var t=term RIGHT_PAREN { v, t }
+
+term:
+  | TRUE { A.true_ }
+  | FALSE { A.false_ }
+  | s=id { A.const s }
+  | t=composite_term { t }
+  | error
+    {
+      let loc = Loc.mk_pos $startpos $endpos in
+      A.parse_errorf ~loc "expected term"
+    }
+
+%inline arith_op:
+  | ADD { A.Add }
+  | MINUS { A.Minus }
+  | PROD { A.Mult }
+  | DIV { A.Div }
+  | LEQ { A.Leq }
+  | LT { A.Lt }
+  | GEQ { A.Geq }
+  | GT { A.Gt }
+
+composite_term:
+  | LEFT_PAREN IF a=term b=term c=term RIGHT_PAREN { A.if_ a b c }
+  | LEFT_PAREN OR l=term+ RIGHT_PAREN { A.or_ l }
+  | LEFT_PAREN AND l=term+ RIGHT_PAREN { A.and_ l }
+  | LEFT_PAREN NOT t=term RIGHT_PAREN { A.not_ t }
+  | LEFT_PAREN DISTINCT l=term+ RIGHT_PAREN { A.distinct l }
+  | LEFT_PAREN EQ a=term b=term RIGHT_PAREN { A.eq a b }
+  | LEFT_PAREN ARROW a=term b=term RIGHT_PAREN { A.imply a b }
+  | LEFT_PAREN XOR a=term b=term RIGHT_PAREN { A.xor a b }
+  | LEFT_PAREN f=id args=term+ RIGHT_PAREN { A.app f args }
+  | LEFT_PAREN o=arith_op args=term+ RIGHT_PAREN { A.arith o args }
+  | LEFT_PAREN f=composite_term args=term+ RIGHT_PAREN { A.ho_app_l f args }
+  | LEFT_PAREN AT f=term arg=term RIGHT_PAREN { A.ho_app f arg }
+  | LEFT_PAREN
+      MATCH
+      lhs=term
+      l=case+
+    RIGHT_PAREN
+    { A.match_ lhs l }
+  | LEFT_PAREN
+      FUN
+      LEFT_PAREN vars=typed_var+ RIGHT_PAREN
+      body=term
+    RIGHT_PAREN
+    { A.fun_l vars body }
+  | LEFT_PAREN
+      LET
+      LEFT_PAREN l=binding+ RIGHT_PAREN
+      r=term
+    RIGHT_PAREN
+    { A.let_ l r }
+  | LEFT_PAREN AS t=term ty=ty RIGHT_PAREN
+    { A.cast t ~ty }
+  | LEFT_PAREN FORALL LEFT_PAREN vars=typed_var+ RIGHT_PAREN
+    f=term
+    RIGHT_PAREN
+    { A.forall vars f }
+  | LEFT_PAREN EXISTS LEFT_PAREN vars=typed_var+ RIGHT_PAREN
+    f=term
+    RIGHT_PAREN
+    { A.exists vars f }
+
+%%

src/smtlib/jbuild

@@ -0,0 +1,21 @@
+; vim:ft=lisp:
+
+(jbuild_version 1)
+
+; main binary
+(library
+  ((name dagon_smtlib)
+   (public_name dagon.smtlib)
+   (optional) ; only if deps present
+   (libraries (containers dagon.smt dagon.util zarith))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8
+           -safe-string -color always -open Dagon_util))
+   (ocamlopt_flags (:standard -O3 -color always -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+(menhir
+  ((modules (Parser))))
+
+(ocamllex
+  (Lexer))

src/th_sat/Dagon_th_sat.ml

@@ -5,5 +5,5 @@ Copyright 2016 Guillaume Bury
 
 module Th = Th_sat
 
-include CDCL.Make(Th)
+include DAgon_sat.Make(Th)
 

src/th_sat/Dagon_th_sat.mli

@@ -11,6 +11,6 @@ Copyright 2016 Guillaume Bury
 
 module Th = Th_sat
 
-include module type of CDCL.Make(Th)
+include module type of Dagon_sat.Make(Th)
 (** A functor that can generate as many solvers as needed. *)
 

src/th_sat/jbuild

@@ -0,0 +1,13 @@
+; vim:ft=lisp:
+
+(library
+  ((name Dagon_th_sat)
+   (public_name dagon.th_sat)
+   (libraries (dagon.sat cdcl.tseitin))
+   (synopsis "sat interface")
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL))
+   (ocamlopt_flags (:standard -O3 -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+

src/tseitin/jbuild

@@ -2,7 +2,7 @@
 
 (library
   ((name CDCL_tseitin)
-   (public_name cdcl.tseitin)
+   (public_name dagon.tseitin)
    (synopsis "Tseitin transformation for CDCL")
    (libraries ())
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))

src/util/ID.ml

@@ -38,3 +38,8 @@ end
 module Map = CCMap.Make(AsKey)
 module Set = CCSet.Make(AsKey)
 module Tbl = CCHashtbl.Make(AsKey)
+
+module B = struct
+  let int = make "int"
+  let rat = make "rat"
+end

src/util/ID.mli

@@ -24,3 +24,12 @@ val pp_name : t CCFormat.printer
 module Map : CCMap.S with type key = t
 module Set : CCSet.S with type elt = t
 module Tbl : CCHashtbl.S with type key = t
+
+
+module B : sig
+  val rat : t
+  val int : t
+
+end
+
+

src/util/Util.ml

@@ -32,3 +32,10 @@ let () = Printexc.register_printer
       | _ -> None)
 
 let errorf msg = Fmt.ksprintf msg ~f:(fun s -> raise (Error s))
+
+let setup_gc () =
+  let g = Gc.get () in
+  g.Gc.space_overhead <- 3_000; (* major gc *)
+  g.Gc.max_overhead <- 10_000; (* compaction *)
+  g.Gc.minor_heap_size <- 500_000; (* ×8 to obtain bytes on 64 bits -->  *)
+  Gc.set g

src/util/Util.mli

@@ -19,3 +19,6 @@ exception Error of string
 
 val errorf : ('a, Format.formatter, unit, 'b) format4 -> 'a
 (** @raise Error when called *)
+
+val setup_gc : unit -> unit
+(** Change parameters of the GC *)

src/util/jbuild

@@ -1,11 +1,8 @@
-; vim:ft=lisp:
-
 (library
-  ((name CDCL)
-   (public_name cdcl)
-   (synopsis "core data structures and algorithms for cdcl")
-   (libraries ())
+  ((name dagon_util)
+   (public_name dagon.util)
+   (libraries (containers sequence))
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
    (ocamlopt_flags (:standard -O3 -bin-annot
                     -unbox-closures -unbox-closures-factor 20))
-  ))
+   ))

tests/jbuild

@@ -2,7 +2,7 @@
 
 (executable
   ((name test_api)
-   (libraries (cdcl cdcl.tseitin cdcl.backend cdcl.sat))
+   (libraries (dagon cdcl.tseitin cdcl.backend cdcl.sat))
    (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string))
    (ocamlopt_flags (:standard -O3 -color always
                     -unbox-closures -unbox-closures-factor 20))