[WIP] All is setup, remains to have real theories

Architecture is now all setup, but theories for the smt and mcsat
solvers are currently dummy ones that are not doing anything.

.merlin

@@ -2,6 +2,7 @@ S src/core
 S src/solver
 S src/sat
 S src/smt
+S src/mcsat
 S src/backend
 S src/util
 S tests
@@ -11,6 +12,7 @@ B _build/src/core
 B _build/src/solver
 B _build/src/sat
 B _build/src/smt
+B _build/src/mcsat
 B _build/src/util
 B _build/src/backend
 B _build/tests

_tags

@@ -23,6 +23,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 # Testing dependencies
 <src/main.*>: package(dolmen)
 <src/util/type.*>: package(dolmen)
+<src/sat/type_sat.*>: package(dolmen)
+<src/smt/type_smt.*>: package(dolmen)
 
 # more warnings
 <src/**/*.ml>: warn_K, warn_Y, warn_X

src/main.ml

@@ -4,28 +4,77 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Sat = Sat.Make(struct end)
+exception Incorrect_model
-module Smt = Smt.Make(struct end)
+exception Out_of_time
-module Mcsat = Mcsat.Make(struct end)
+exception Out_of_space
+
+let file = ref ""
+let p_cnf = ref false
+let p_check = ref false
+let p_proof_print = ref false
+let p_unsat_core = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
 
 module P =
   Dolmen.Logic.Make(Dolmen.ParseLocation)
     (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement)
 
-exception Incorrect_model
+module type S = sig
-exception Out_of_time
+  val do_task : Dolmen.Statement.t -> unit
-exception Out_of_space
+end
 
-type solver =
+module Make
-  | Sat
+    (S : External.S)
-  | Smt
+    (T : Type.S with type atom := S.atom)
-  | Mcsat
+= struct
 
-let solver = ref Smt
+  let hyps = ref []
+
+  let do_task s =
+    match s.Dolmen.Statement.descr with
+    | Dolmen.Statement.Def (id, t) -> T.def id t
+    | Dolmen.Statement.Decl (id, t) -> T.decl id t
+    | Dolmen.Statement.Consequent t ->
+      let cnf = T.consequent t in
+      hyps := cnf @ !hyps;
+      S.assume cnf
+    | Dolmen.Statement.Antecedent t ->
+      let cnf = T.antecedent t in
+      hyps := cnf @ !hyps;
+      S.assume cnf
+    | Dolmen.Statement.Prove ->
+      let res = S.solve () in
+      let t = Sys.time () in
+      begin match res with
+        | S.Sat state ->
+          if !p_check then
+            if not (List.for_all (List.exists state.Solver_intf.eval) !hyps) then
+              raise Incorrect_model;
+          let t' = Sys.time () -. t in
+          Format.printf "Sat (%f/%f)@." t t'
+        | S.Unsat state ->
+          if !p_check then begin
+            let p = state.Solver_intf.get_proof () in
+            S.Proof.check p;
+          end;
+          let t' = Sys.time () -. t in
+          Format.printf "Unsat (%f/%f)@." t t'
+      end
+    | _ ->
+      Format.printf "Command not supported:@\n%a@."
+        Dolmen.Statement.print s
+end
+
+module Sat = Make(Sat.Make(struct end))(Type_sat)
+module Smt = Make(Smt.Make(struct end))(Type_smt)
+module Mcsat = Make(Mcsat.Make(struct end))(Type_smt)
+
+let solver = ref (module Sat : S)
 let solver_list = [
-  "sat", Sat;
+  "sat", (module Sat : S);
-  "smt", Smt;
+  "smt", (module Smt : S);
-  "mcsat", Mcsat;
+  "mcsat", (module Mcsat : S);
 ]
 
 let error_msg opt arg l =
@@ -42,14 +91,6 @@ let set_flag opt arg flag l =
 let set_solver s = set_flag "Solver" s solver solver_list
 
 (* Arguments parsing *)
-let file = ref ""
-let p_cnf = ref false
-let p_check = ref false
-let p_proof_print = ref false
-let p_unsat_core = ref false
-let time_limit = ref 300.
-let size_limit = ref 1000_000_000.
-
 let int_arg r arg =
   let l = String.length arg in
   let multiplier m =
@@ -111,30 +152,6 @@ let check () =
   else if s > !size_limit then
     raise Out_of_space
 
-module Make
-    (T : Type.S)
-    (S : External.S with type St.formula = T.atom) = struct
-
-  let do_task s =
-    match s.Dolmen.Statement.descr with
-    | Dolmen.Statement.Def (id, t) -> T.def id t
-    | Dolmen.Statement.Decl (id, t) -> T.decl id t
-    | Dolmen.Statement.Consequent t ->
-      let cnf = T.consequent t in
-      S.assume cnf
-    | Dolmen.Statement.Antecedent t ->
-      let cnf = T.antecedent t in
-      S.assume cnf
-    | Dolmen.Statement.Prove ->
-      begin match S.solve () with
-        | S.Sat _ -> ()
-        | S.Unsat _ -> ()
-      end
-    | _ ->
-      Format.printf "Command not supported:@\n%a@."
-        Dolmen.Statement.print s
-end
-
 
 let main () =
   (* Administrative duties *)
@@ -146,73 +163,35 @@ let main () =
   let al = Gc.create_alarm check in
 
   (* Interesting stuff happening *)
-  let _, _input = P.parse_file !file in
+  let lang, input = P.parse_file !file in
+  let module S = (val !solver : S) in
+  List.iter S.do_task input;
+  (* Small hack for dimacs, which do not output a "Prove" statement *)
+  begin match lang with
+    | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat ()
+    | _ -> ()
+  end;
   Gc.delete_alarm al;
   ()
 
-(* Old code ...
-
-   let cnf = get_cnf () in
-   if !p_cnf then
-   print_cnf cnf;
-   match !solver with
-   | Smt ->
-   Smt.assume cnf;
-   let res = Smt.solve () in
-   Gc.delete_alarm al;
-   begin match res with
-    | Smt.Sat sat ->
-      let t = Sys.time () in
-      if !p_check then
-        if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
-          raise Incorrect_model;
-      print "Sat (%f/%f)" t (Sys.time () -. t)
-    | Smt.Unsat us ->
-      let t = Sys.time () in
-      if !p_check then begin
-        let p = us.Solver_intf.get_proof () in
-        Smt.Proof.check p;
-        print_proof p;
-        if !p_unsat_core then
-          print_unsat_core (Smt.unsat_core p)
-      end;
-      print "Unsat (%f/%f)" t (Sys.time () -. t)
-   end
-   | Mcsat ->
-   Mcsat.assume cnf;
-   let res = Mcsat.solve () in
-   begin match res with
-    | Mcsat.Sat sat ->
-      let t = Sys.time () in
-      if !p_check then
-        if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
-          raise Incorrect_model;
-      print "Sat (%f/%f)" t (Sys.time () -. t)
-    | Mcsat.Unsat us ->
-      let t = Sys.time () in
-      if !p_check then begin
-        let p = us.Solver_intf.get_proof () in
-        Mcsat.Proof.check p;
-        print_mcproof p;
-        if !p_unsat_core then
-          print_mc_unsat_core (Mcsat.unsat_core p)
-      end;
-      print "Unsat (%f/%f)" t (Sys.time () -. t)
-   end
-
-*)
-
 let () =
   try
     main ()
   with
-  | Incorrect_model ->
-    Format.printf "Internal error : incorrect *sat* model@.";
-    exit 4
   | Out_of_time ->
     Format.printf "Timeout@.";
     exit 2
   | Out_of_space ->
     Format.printf "Spaceout@.";
     exit 3
+  | Incorrect_model ->
+    Format.printf "Internal error : incorrect *sat* model@.";
+    exit 4
+  | Type_sat.Typing_error (msg, t)
+  | Type_smt.Typing_error (msg, t) ->
+    let loc = match t.Dolmen.Term.loc with
+      | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0
+    in
+    Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@."
+      Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg
 

src/sat/expr_sat.mli

@@ -6,3 +6,6 @@ Copyright 2016 Simon Cruanes
 
 include Formula_intf.S
 
+val make : int -> t
+(** Make a proposition from an integer. *)
+

src/sat/type_sat.ml

@@ -0,0 +1,73 @@
+
+(* Log&Module Init *)
+(* ************************************************************************ *)
+
+module Id = Dolmen.Id
+module Ast = Dolmen.Term
+module H = Hashtbl.Make(Id)
+module Formula = Tseitin.Make(Expr_sat)
+
+(* Exceptions *)
+(* ************************************************************************ *)
+
+exception Typing_error of string * Dolmen.Term.t
+
+(* Identifiers *)
+(* ************************************************************************ *)
+
+let symbols = H.create 42
+
+let find_id id =
+  try
+    H.find symbols id
+  with Not_found ->
+    let res = Expr_sat.fresh () in
+    H.add symbols id res;
+    res
+
+(* Actual parsing *)
+(* ************************************************************************ *)
+
+let rec parse = function
+  | { Ast.term = Ast.Builtin Ast.True } ->
+    Formula.f_true
+  | { Ast.term = Ast.Builtin Ast.False } ->
+    Formula.f_false
+  | { Ast.term = Ast.Symbol id } ->
+    let s = find_id id in
+    Formula.make_atom s
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } ->
+    Formula.make_not (parse p)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } ->
+    Formula.make_and (List.map parse l)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } ->
+    Formula.make_or (List.map parse l)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } ->
+    Formula.make_imply (parse p) (parse q)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } ->
+    Formula.make_equiv (parse p) (parse q)
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } ->
+    Formula.make_xor (parse p) (parse q)
+  | t ->
+    raise (Typing_error ("Term is not a pure proposition", t))
+
+(* Exported functions *)
+(* ************************************************************************ *)
+
+let decl _ t =
+  raise (Typing_error ("Declarations are not allowed in pure sat", t))
+
+let def _ t =
+  raise (Typing_error ("Definitions are not allowed in pure sat", t))
+
+let antecedent t =
+  let f = parse t in
+  Formula.make_cnf f
+
+let consequent t =
+  let f = parse t in
+  Formula.make_cnf @@ Formula.make_not f
+

src/sat/type_sat.mli

@@ -0,0 +1,7 @@
+
+(** Typechecking of terms from Dolmen.Term.t
+    This module provides functions to parse terms from the untyped syntax tree
+    defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
+
+include Type.S with type atom := Expr_sat.t
+

src/smt/expr_smt.ml

@@ -133,8 +133,11 @@ module Print = struct
 
   let atom_aux fmt f =
     match f.atom with
-    | Equal (a, b) -> Format.fprintf fmt "%a = %a" term a term b
+    | Equal (a, b) ->
-    | Pred t -> Format.fprintf fmt "%a" term t
+      Format.fprintf fmt "%a %s %a"
+        term a (if f.sign then "=" else "<>") term b
+    | Pred t ->
+      Format.fprintf fmt "%s%a" (if f.sign then "" else "¬ ") term t
 
   let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f
 

src/smt/type_smt.ml

@@ -6,6 +6,7 @@ module Ast = Dolmen.Term
 module Id = Dolmen.Id
 module M = Map.Make(Id)
 module H = Hashtbl.Make(Id)
+module Expr = Expr_smt
 
 (* Types *)
 (* ************************************************************************ *)
@@ -287,6 +288,9 @@ let infer env s args =
 
 let rec parse_expr (env : env) t =
   match t with
+  (* Base Type *)
+  | { Ast.term = Ast.Symbol { Id.name = "Bool" } } ->
+    Ty (Expr_smt.Ty.prop)
 
   (* Basic formulas *)
   | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
@@ -297,10 +301,12 @@ let rec parse_expr (env : env) t =
   | { Ast.term = Ast.Builtin Ast.False } ->
     Formula Expr.Formula.f_false
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } ->
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" }}, l) } ->
     Formula (Expr.Formula.make_and (List.map (parse_formula env) l))
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
+  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) }
+  | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" }}, l) } ->
     Formula (Expr.Formula.make_or (List.map (parse_formula env) l))
 
   | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t ->
@@ -330,7 +336,8 @@ let rec parse_expr (env : env) t =
       | _ -> _bad_arity "<=>" 2 t
     end
 
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t)
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" }}, l) } as t) ->
     begin match l with
       | [p] ->
         Formula (Expr.Formula.make_not (parse_formula env p))
@@ -338,7 +345,8 @@ let rec parse_expr (env : env) t =
     end
 
   (* (Dis)Equality *)
-  | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t)
+  | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=" }}, l) } as t) ->
     begin match l with
       | [a; b] ->
         Formula (
@@ -607,9 +615,9 @@ let formula t =
   Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
   parse_formula env t
 
-let consequent t =
+let antecedent t =
   Expr.Formula.make_cnf (formula t)
 
-let antecedent t =
+let consequent t =
   Expr.Formula.make_cnf (Expr.Formula.make_not (formula t))
 

src/smt/type_smt.mli

@@ -1,7 +1,7 @@
 
 (** Typechecking of terms from Dolmen.Term.t
     This module provides functions to parse terms from the untyped syntax tree
-    defined in Dolmen, and generate formulas as defined in the Expr module. *)
+    defined in Dolmen, and generate formulas as defined in the Expr_smt module. *)
 
-include Type.S with type atom = Expr.atom
+include Type.S with type atom := Expr_smt.Atom.t
 

tests/test_api.ml

@@ -6,18 +6,11 @@ Copyright 2014 Simon Cruanes
 
 (* Tests that require the API *)
 
-module F = Expr
+module F = Expr_sat
-module T = Cnf.S
+module T = Tseitin.Make(F)
 
 let (|>) x f = f x
 
-type solver = Smt | Mcsat
-let solver_list = [
-  "smt", Smt;
-  "mcsat", Mcsat;
-]
-
-let solver = ref Smt
 let p_check = ref false
 let time_limit = ref 300.
 let size_limit = ref 1000_000_000.
@@ -32,59 +25,38 @@ let set_flag opt arg flag l =
     flag := List.assoc arg l
   with Not_found ->
     invalid_arg (error_msg opt arg l)
-let set_solver s = set_flag "Solver" s solver solver_list
 
 let usage = "Usage : test_api [options]"
 let argspec = Arg.align [
     "-check", Arg.Set p_check,
     " Build, check and print the proof (if output is set), if unsat";
-    "-s", Arg.String set_solver,
-    "{smt,mcsat} Sets the solver to use (default smt)";
     "-v", Arg.Int (fun i -> Log.set_debug i),
     "<lvl> Sets the debug verbose level";
   ]
 
-let string_of_solver = function
-  | Mcsat -> "mcsat"
-  | Smt -> "smt"
-
 type solver_res =
   | R_sat
   | R_unsat
 
+exception Incorrect_model
+
 module type BASIC_SOLVER = sig
   val solve : ?assumptions:F.t list -> unit -> solver_res
   val assume : ?tag:int -> F.t list list -> unit
 end
 
-exception Incorrect_model
+let mk_solver (): (module BASIC_SOLVER) =
-
+  let module S = struct
-let mk_solver (s:solver): (module BASIC_SOLVER) =
+    include Sat.Make(struct end)
-  match s with
+    let solve ?assumptions ()= match solve ?assumptions() with
-    | Smt ->
+      | Sat _ ->
-      let module S = struct
+        R_sat
-        include Smt.Make(struct end)
+      | Unsat us ->
-        let solve ?assumptions ()= match solve ?assumptions() with
+        let p = us.Solver_intf.get_proof () in
-          | Sat _ ->
+        Proof.check p;
-            R_sat
+        R_unsat
-          | Unsat us ->
+  end
-            let p = us.Solver_intf.get_proof () in
+  in (module S)
-            Proof.check p;
-            R_unsat
-      end
-      in (module S)
-    | Mcsat ->
-      let module S = struct
-        include Mcsat.Make(struct end)
-        let solve ?assumptions ()= match solve ?assumptions() with
-          | Sat _ ->
-            R_sat
-          | Unsat us ->
-            let p = us.Solver_intf.get_proof () in
-            Proof.check p;
-            R_unsat
-      end
-      in (module S)
 
 exception Error of string
 
@@ -102,19 +74,19 @@ module Test = struct
   }
 
   let mk_test name l = {name; actions=l}
-  let assume l = A_assume (List.map (List.map F.mk_prop) l)
+  let assume l = A_assume (List.map (List.map F.make) l)
   let assume1 c = assume [c]
   let solve ?(assumptions=[]) e =
-    let assumptions = List.map F.mk_prop assumptions in
+    let assumptions = List.map F.make assumptions in
     A_solve (assumptions, e)
 
   type result =
     | Pass
     | Fail of string
 
-  let run (solver:solver) (t:t): result =
+  let run (t:t): result =
   (* Interesting stuff happening *)
-    let (module S: BASIC_SOLVER) = mk_solver solver in
+    let (module S: BASIC_SOLVER) = mk_solver () in
     try
       List.iter
         (function
@@ -190,17 +162,14 @@ let main () =
   Arg.parse argspec (fun _ -> ()) usage;
   let failed = ref false in
   List.iter
-    (fun solver ->
+    (fun test ->
-       List.iter
+       Printf.printf "%-10s... %!" test.Test.name;
-         (fun test ->
+       match Test.run test with
-            Printf.printf "(%-6s) %-10s... %!" (string_of_solver solver) test.Test.name;
+       | Test.Pass -> Printf.printf "ok\n%!"
-            match Test.run solver test with
+       | Test.Fail msg ->
-              | Test.Pass -> Printf.printf "ok\n%!"
+         failed := true;
-              | Test.Fail msg ->
+         Printf.printf "fail (%s)\n%!" msg)
-                failed := true;
+    Test.suite;
-                Printf.printf "fail (%s)\n%!" msg)
-         Test.suite)
-    [Smt; Mcsat];
   if !failed then exit 1
 
 let () = main()