diff --git a/Makefile b/Makefile index cf1b8dfb..26047ca6 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= DIRS=-Is sat,smt,util,util/smtlib DOC=msat.docdir/index.html -TEST=sat_solve.native +TEST=sat_solve.native smt_solve.native NAME=msat diff --git a/msat.mlpack b/msat.mlpack index c68f4682..71440c17 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -1,3 +1,4 @@ +# Sat Modules Explanation Formula_intf Res @@ -8,6 +9,11 @@ Theory_intf Tseitin Tseitin_intf +# Smt Modules +Unionfind +Smt + +# Old modules #Arith #Cc #Combine diff --git a/sat/res.ml b/sat/res.ml index 6d009487..19e13e65 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -344,7 +344,7 @@ module Make(St : Solver_types.S) = struct print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion | Lemma _ -> let aux fmt () = - Format.fprintf fmt "%aLemma%s" + Format.fprintf fmt "%aLemma%s" print_clause p.conclusion St.(p.conclusion.name) in print_dot_rule "BGCOLOR=\"RED\"" aux () fmt p.conclusion diff --git a/sat/sat.mli b/sat/sat.mli index fc17df9f..15c3acce 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -1,4 +1,8 @@ -(* Copyright 2014 Guillaume Bury *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module Fsat : Formula_intf.S diff --git a/sat/solver.ml b/sat/solver.ml index 522a0c18..9bb01a88 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -373,7 +373,7 @@ module Make (F : Formula_intf.S) propagate () | Th.Unsat (l, p) -> let l = List.rev_map St.add_atom l in - let c = St.make_clause (St.fresh_name ()) l (List.length l) true (History []) in + let c = St.make_clause (St.fresh_name ()) l (List.length l) true (Lemma p) in Some c and propagate () = @@ -501,6 +501,7 @@ module Make (F : Formula_intf.S) let report_unsat ({atoms=atoms} as confl) = + Log.debug 5 "Unsat conflict : %a" St.pp_clause confl; env.unsat_conflict <- Some confl; env.is_unsat <- true; raise Unsat @@ -646,6 +647,7 @@ module Make (F : Formula_intf.S) if env.is_unsat then raise Unsat; let init_name = string_of_int cnumber in let init0 = make_clause init_name atoms (List.length atoms) false (History []) in + Log.debug 10 "New clause : %a" St.pp_clause init0; try let atoms, init = if decision_level () = 0 then diff --git a/smt/.merlin b/smt/.merlin new file mode 100644 index 00000000..95182585 --- /dev/null +++ b/smt/.merlin @@ -0,0 +1,8 @@ +S ./ +S ../sat/ +S ../util/ + +B ../_build/ +B ../_build/sat/ +B ../_build/smt/ +B ../_build/util/ diff --git a/smt/smt.ml b/smt/smt.ml new file mode 100644 index 00000000..7ea0aeff --- /dev/null +++ b/smt/smt.ml @@ -0,0 +1,155 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Fsmt = struct + + exception Invalid_var + + type var = string + type t = + | Fresh of int + | Equal of var * var + | Distinct of var * var + + let dummy = Fresh 0 + + let max_fresh = ref 0 + let fresh () = + incr max_fresh; + Fresh !max_fresh + + let mk_var i = + if i <> "" then + i + else + raise Invalid_var + + let mk_eq i j = Equal (mk_var i, mk_var j) + let mk_neq i j = Distinct (mk_var i, mk_var j) + + let neg = function + | Fresh i -> Fresh (-i) + | Equal (a, b) -> Distinct (a, b) + | Distinct (a, b) -> Equal (a, b) + + let norm = function + | Fresh i -> Fresh (abs i), i < 0 + | Equal (a, b) -> Equal (min a b, max a b), false + | Distinct (a, b) -> Equal (min a b, max a b), true + + (* Only used after normalisation, so usual functions should work *) + let hash = Hashtbl.hash + let equal = (=) + let compare = Pervasives.compare + + let s = Hstring.make "" + let label _ = s + let add_label _ _ = () + + let print fmt = function + | Fresh i -> Format.fprintf fmt "%sv%d" (if i < 0 then "¬ " else "") (abs i) + | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b + | Distinct (a, b) -> Format.fprintf fmt "%s <> %s" a b + +end + +module Tseitin = Tseitin.Make(Fsmt) + +module Tsmt = struct + + module U = Unionfind.Make(String) + + type formula = Fsmt.t + type proof = unit + type slice = { + start : int; + length : int; + get : int -> formula; + push : formula -> formula list -> proof -> unit; + } + type level = U.t + + type res = + | Sat of level + | Unsat of formula list * proof + + let dummy = U.empty + + let env = ref U.empty + + let current_level () = !env + + let temp = ref [] + + let assume s = + try + for i = s.start to s.start + s.length - 1 do + match s.get i with + | Fsmt.Fresh _ -> () + | Fsmt.Equal (i, j) as f -> + temp := f :: !temp; + env := U.union !env i j + | Fsmt.Distinct (i, j) as f -> + temp := f :: !temp; + env := U.forbid !env i j + | _ -> assert false + done; + Sat (current_level ()) + with U.Unsat -> + match !temp with + | _ :: _ -> Unsat (List.rev_map Fsmt.neg !temp, ()) + | _ -> assert false + + let backtrack l = env := l + +end + +module Make(Dummy:sig end) = struct + module SmtSolver = Solver.Make(Fsmt)(Tsmt) + + type atom = Fsmt.t + type clause = SmtSolver.St.clause + type proof = SmtSolver.Proof.proof + + type res = + | Sat + | Unsat + + let _i = ref 0 + + let make_eq = Fsmt.mk_eq + let make_neq = Fsmt.mk_neq + + let neg = Fsmt.neg + + let hash = Fsmt.hash + let equal = Fsmt.equal + let compare = Fsmt.compare + + let solve () = + try + SmtSolver.solve (); + Sat + with SmtSolver.Unsat -> Unsat + + let assume l = + incr _i; + try + SmtSolver.assume l !_i + with SmtSolver.Unsat -> () + + let get_proof () = + SmtSolver.Proof.learn (SmtSolver.history ()); + match SmtSolver.unsat_conflict () with + | None -> assert false + | Some c -> SmtSolver.Proof.prove_unsat c + + let unsat_core = SmtSolver.Proof.unsat_core + + let print_atom = Fsmt.print + let print_clause = SmtSolver.St.print_clause + let print_proof = SmtSolver.Proof.print_dot +end diff --git a/smt/smt.mli b/smt/smt.mli new file mode 100644 index 00000000..4ecc42e6 --- /dev/null +++ b/smt/smt.mli @@ -0,0 +1,69 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module Fsmt : sig + include Formula_intf.S + val mk_eq : string -> string -> t + val mk_neq : string -> string -> t +end + +module Tseitin : Tseitin.S with type atom = Fsmt.t + +module Make(Dummy: sig end) : sig + (** Fonctor to make a pure SAT Solver module with built-in literals. *) + + type atom = Fsmt.t + (** Type for atoms, i.e boolean literals. *) + + type clause + (** Abstract type for clauses *) + + type proof + (** Abstract type for resolution proofs *) + + type res = Sat | Unsat + (** Type of results returned by the solve function. *) + + val make_eq : string -> string -> atom + (** Returns the literal corresponding to equality of the given variables + @raise Invalid_var if given [0] as argument.*) + + val make_neq : string -> string -> atom + (** Returns the literal corresponding to disequality of the given variables + @raise Invalid_var if given [0] as argument.*) + + val neg : atom -> atom + (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) + + val hash : atom -> int + val equal : atom -> atom -> bool + val compare : atom -> atom -> int + (** Usual hash and comparison functions. For now, directly uses + [Pervasives] and [Hashtbl] builtins. *) + + val solve : unit -> res + (** Returns the satisfiability status of the current set of assumptions. *) + + val assume : atom list list -> unit + (** Add a list of clauses to the set of assumptions. *) + + val get_proof : unit -> proof + (** Returns the resolution proof found, if [solve] returned [Unsat]. *) + + val unsat_core : proof -> clause list + (** Returns the unsat-core of the proof. *) + + val print_atom : Format.formatter -> atom -> unit + (** Print the atom on the given formatter. *) + + val print_clause : Format.formatter -> clause -> unit + (** Print the clause on the given formatter. *) + + val print_proof : Format.formatter -> proof -> unit + (** Print the given proof in dot format. *) + +end + diff --git a/smt/unionfind.ml b/smt/unionfind.ml new file mode 100644 index 00000000..92764b95 --- /dev/null +++ b/smt/unionfind.ml @@ -0,0 +1,84 @@ + +module type OrderedType = sig + type t + val compare : t -> t -> int +end + +(* Union-find Module *) +module Make(T : OrderedType) = struct + exception Unsat + + type var = T.t + module M = Map.Make(T) + +type t = { + rank : int M.t; + forbid : ((var * var) list); + mutable parent : var M.t; +} + +let empty = { + rank = M.empty; + forbid = []; + parent = M.empty; +} + +let find_map m i default = + try + M.find i m + with Not_found -> + default + +let rec find_aux f i = + let fi = find_map f i i in + if fi = i then + (f, i) + else + let f, r = find_aux f fi in + let f = M.add i r f in + (f, r) + +let find h x = + let f, cx = find_aux h.parent x in + h.parent <- f; + cx + +(* Highly ineficient treatment of inequalities *) +let possible h = + let aux (a, b) = + let ca = find h a in + let cb = find h b in + ca != cb + in + if List.for_all aux h.forbid then + h + else + raise Unsat + +let union_aux h x y = + let cx = find h x in + let cy = find h y in + if cx != cy then begin + let rx = find_map h.rank cx 0 in + let ry = find_map h.rank cy 0 in + if rx > ry then + { h with parent = M.add cy cx h.parent } + else if ry > rx then + { h with parent = M.add cx cy h.parent } + else + { rank = M.add cx (rx + 1) h.rank; + parent = M.add cy cx h.parent; + forbid = h.forbid; } + end else + h + +let union h x y = possible (union_aux h x y) + +let forbid h x y = + let cx = find h x in + let cy = find h y in + if cx = cy then + raise Unsat + else + { h with forbid = (x, y) :: h.forbid } +end diff --git a/smt/unionfind.mli b/smt/unionfind.mli new file mode 100644 index 00000000..7416751a --- /dev/null +++ b/smt/unionfind.mli @@ -0,0 +1,14 @@ +module type OrderedType = sig + type t + val compare : t -> t -> int +end + +module Make(T : OrderedType) : sig + type t + exception Unsat + val empty : t + val find : t -> T.t -> T.t + val union : t -> T.t -> T.t -> t + val forbid : t -> T.t -> T.t -> t +end + diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 1d6fef4c..5e098748 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -61,7 +61,7 @@ let format_of_filename s = let parse_with_input file = function | Auto -> assert false | Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file) - | Smtlib -> rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file) + | Smtlib -> rev_flat_map Sat.Tseitin.make_cnf [] (Satlib.parse file) let parse_input file = parse_with_input file (match !input with diff --git a/util/smt_solve.ml b/util/smt_solve.ml new file mode 100644 index 00000000..66315f9d --- /dev/null +++ b/util/smt_solve.ml @@ -0,0 +1,198 @@ + +module S = Smt.Make(struct end) + +exception Out_of_time +exception Out_of_space + +(* IO wrappers *) +(* Types for input/output languages *) +type sat_input = + | Auto + | Smtlib + +type sat_output = + | Standard (* Only output problem status *) + | Dot + +let input = ref Auto +let output = ref Standard + +let input_list = [ + "auto", Auto; + "smtlib", Smtlib; +] +let output_list = [ + "dot", Dot; +] + +let error_msg opt arg l = + Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a" + arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l; + Format.flush_str_formatter () + +let set_io opt arg flag l = + try + flag := List.assoc arg l + with Not_found -> + invalid_arg (error_msg opt arg l) + +let set_input s = set_io "Input" s input input_list +let set_output s = set_io "Output" s output output_list + +(* Input Parsing *) +let rec rev_flat_map f acc = function + | [] -> acc + | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r + +let format_of_filename s = + let last n = + try String.sub s (String.length s - n) n + with Invalid_argument _ -> "" + in + if last 5 = ".smt2" then + Smtlib + else (* Default choice *) + Smtlib + +let parse_with_input file = function + | Auto -> assert false + | Smtlib -> rev_flat_map Smt.Tseitin.make_cnf [] (Smtlib.parse file) + +let parse_input file = + parse_with_input file (match !input with + | Auto -> format_of_filename file + | f -> f) + +(* Printing wrappers *) +let std = Format.std_formatter + +let print format = match !output with + | Standard -> Format.fprintf std "%( fmt %)@." format + | Dot -> Format.fprintf std "/* %( fmt %) */@." format + +let print_proof proof = match !output with + | Standard -> () + | Dot -> S.print_proof std proof + +let rec print_cl fmt = function + | [] -> Format.fprintf fmt "[]" + | [a] -> Smt.Fsmt.print fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Smt.Fsmt.print a print_cl r + +let print_lcl l = + List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l + +let print_lclause l = + List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l + +(* Arguments parsing *) +let file = ref "" +let p_cnf = ref false +let p_proof_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 = + 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 "float_of_string" -> raise (Arg.Bad "bad numeric argument") + +let setup_gc_stat () = + at_exit (fun () -> + Gc.print_stat stdout; + ) + +let input_file = fun s -> file := s + +let usage = "Usage : main [options] " +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 p_proof_check, + " Build, check and print the proof (if output is set), if unsat"; + "-gc", Arg.Unit setup_gc_stat, + " Outputs statistics about the GC"; + "-i", Arg.String set_input, + " Sets the input format (default auto)"; + "-o", Arg.String set_output, + " Sets the output format (default none)"; + "-size", Arg.String (int_arg size_limit), + "[kMGT] Sets the size limit for the sat solver"; + "-time", Arg.String (int_arg time_limit), + "[smhd] Sets the time limit for the sat solver"; + "-u", Arg.Set p_unsat_core, + " Prints the unsat-core explanation of the unsat proof (if used with -check)"; + "-v", Arg.Int (fun i -> Log.set_debug i), + " Sets the debug verbose level"; + ] + +(* Limits alarm *) +let check () = + let t = Sys.time () in + let heap_size = (Gc.quick_stat ()).Gc.heap_words in + let s = float heap_size *. float Sys.word_size /. 8. in + if t > !time_limit then + raise Out_of_time + else if s > !size_limit then + raise Out_of_space + +(* Entry file parsing *) +let get_cnf () = parse_input !file + +let main () = + (* Administrative duties *) + Arg.parse argspec input_file usage; + if !file = "" then begin + Arg.usage argspec usage; + exit 2 + end; + ignore(Gc.create_alarm check); + + (* Interesting stuff happening *) + let cnf = get_cnf () in + if !p_cnf then + print_lcl cnf; + S.assume cnf; + match S.solve () with + | S.Sat -> + print "Sat"; + | S.Unsat -> + print "Unsat"; + if !p_proof_check then begin + let p = S.get_proof () in + print_proof p; + if !p_unsat_core then + print_lclause (S.unsat_core p) + end + +let () = + try + main () + with + | Out_of_time -> + print "Time limit exceeded"; + exit 2 + | Out_of_space -> + print "Size limit exceeded"; + exit 3 diff --git a/util/smtlib/satlib.ml b/util/smtlib/satlib.ml new file mode 100644 index 00000000..56f1196e --- /dev/null +++ b/util/smtlib/satlib.ml @@ -0,0 +1,103 @@ +(* Copyright 2014 INRIA **) + +open Smtlib_syntax + +module F = Sat.Fsat +module T = Sat.Tseitin + +exception Bad_arity of string +exception Unknown_command +exception Incomplete_translation + +(* Environment *) +let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; +Hashtbl.add env "true" T.f_true;; +Hashtbl.add env "false" T.f_false;; + +let get_var = + fun s -> + try + Hashtbl.find env s + with Not_found -> + let f = T.make_atom (F.fresh ()) in + Hashtbl.add env s f; + f + +(* Term translation *) +let translate_const = function + | SpecConstsDec(_, s) + | SpecConstNum(_, s) + | SpecConstString(_, s) + | SpecConstsHex(_, s) + | SpecConstsBinary(_, s) -> get_var s + +let translate_symbol = function + | Symbol(_, s) + | SymbolWithOr(_, s) -> s + +let translate_id = function + | IdSymbol(_, s) -> translate_symbol s + | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation + +let translate_sort = function + | SortIdentifier(_, id) -> + let s = translate_id id in + if s <> "Bool" then raise Incomplete_translation + | _ -> raise Incomplete_translation + +let translate_qualid = function + | QualIdentifierId(_, id) -> translate_id id + | QualIdentifierAs(_, id, s) -> raise Incomplete_translation + +let left_assoc s f = function + | x :: r -> List.fold_left f x r + | _ -> raise (Bad_arity s) + +let right_assoc s f = function + | x :: r -> List.fold_right f r x + | _ -> raise (Bad_arity s) + +let rec translate_term = function + | TermSpecConst(_, const) -> translate_const const + | TermQualIdentifier(_, id) -> get_var (translate_qualid id) + | TermQualIdTerm(_, f, (_, l)) -> + begin match (translate_qualid f), (List.map translate_term l) with + (* CORE theory translation - '=', 'distinct','ite' not yet implemented *) + | "not", [e] -> T.make_not e + | "not", _ -> raise (Bad_arity "not") + | "and", l -> T.make_and l + | "or", l -> T.make_or l + | "xor" as s, l -> left_assoc s T.make_xor l + | "=>" as s, l -> right_assoc s T.make_imply l + | _ -> raise Unknown_command + end + | _ -> raise Incomplete_translation + +(* Command Translation *) +let translate_command = function + | CommandDeclareFun(_, s, (_, []), ret) -> + ignore (translate_sort ret); + ignore (get_var (translate_symbol s)); + None + | CommandAssert(_, t) -> + Some (translate_term t) + | _ -> None + +let rec translate_command_list acc = function + | [] -> acc + | c :: r -> + begin match translate_command c with + | None -> translate_command_list acc r + | Some t -> translate_command_list (t :: acc) r + end + +let translate = function + | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) + | None -> [] + +let parse file = + let f = open_in file in + let lexbuf = Lexing.from_channel f in + let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in + close_in f; + translate commands diff --git a/util/smtlib/satlib.mli b/util/smtlib/satlib.mli new file mode 100644 index 00000000..19ff02bc --- /dev/null +++ b/util/smtlib/satlib.mli @@ -0,0 +1,3 @@ +(* Copyright 2014 INRIA *) + +val parse : string -> Sat.Tseitin.t list diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index 56f1196e..f472908c 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -2,8 +2,8 @@ open Smtlib_syntax -module F = Sat.Fsat -module T = Sat.Tseitin +module F = Smt.Fsmt +module T = Smt.Tseitin exception Bad_arity of string exception Unknown_command @@ -14,8 +14,7 @@ let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; Hashtbl.add env "true" T.f_true;; Hashtbl.add env "false" T.f_false;; -let get_var = - fun s -> +let get_var s = try Hashtbl.find env s with Not_found -> @@ -29,7 +28,7 @@ let translate_const = function | SpecConstNum(_, s) | SpecConstString(_, s) | SpecConstsHex(_, s) - | SpecConstsBinary(_, s) -> get_var s + | SpecConstsBinary(_, s) -> s let translate_symbol = function | Symbol(_, s) @@ -39,12 +38,6 @@ let translate_id = function | IdSymbol(_, s) -> translate_symbol s | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation -let translate_sort = function - | SortIdentifier(_, id) -> - let s = translate_id id in - if s <> "Bool" then raise Incomplete_translation - | _ -> raise Incomplete_translation - let translate_qualid = function | QualIdentifierId(_, id) -> translate_id id | QualIdentifierAs(_, id, s) -> raise Incomplete_translation @@ -57,27 +50,36 @@ let right_assoc s f = function | x :: r -> List.fold_right f r x | _ -> raise (Bad_arity s) -let rec translate_term = function +let translate_atom = function | TermSpecConst(_, const) -> translate_const const - | TermQualIdentifier(_, id) -> get_var (translate_qualid id) + | TermQualIdentifier(_, id) -> translate_qualid id + | _ -> raise Incomplete_translation + +let rec translate_term = function | TermQualIdTerm(_, f, (_, l)) -> - begin match (translate_qualid f), (List.map translate_term l) with - (* CORE theory translation - '=', 'distinct','ite' not yet implemented *) - | "not", [e] -> T.make_not e - | "not", _ -> raise (Bad_arity "not") - | "and", l -> T.make_and l - | "or", l -> T.make_or l - | "xor" as s, l -> left_assoc s T.make_xor l - | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> raise Unknown_command + begin match (translate_qualid f) with + | "=" -> + begin match (List.map translate_atom l) with + | [a; b] -> T.make_atom (F.mk_eq a b) + | _ -> assert false + end + | s -> + begin match s, (List.map translate_term l) with + (* CORE theory translation - 'distinct','ite' not yet implemented *) + | "not", [e] -> T.make_not e + | "not", _ -> raise (Bad_arity "not") + | "and", l -> T.make_and l + | "or", l -> T.make_or l + | "xor" as s, l -> left_assoc s T.make_xor l + | "=>" as s, l -> right_assoc s T.make_imply l + | _ -> raise Unknown_command + end end | _ -> raise Incomplete_translation (* Command Translation *) let translate_command = function - | CommandDeclareFun(_, s, (_, []), ret) -> - ignore (translate_sort ret); - ignore (get_var (translate_symbol s)); + | CommandDeclareFun(_, s, (_, []), _) -> None | CommandAssert(_, t) -> Some (translate_term t) diff --git a/util/smtlib/smtlib.mli b/util/smtlib/smtlib.mli index 19ff02bc..14d06003 100644 --- a/util/smtlib/smtlib.mli +++ b/util/smtlib/smtlib.mli @@ -1,3 +1,3 @@ (* Copyright 2014 INRIA *) -val parse : string -> Sat.Tseitin.t list +val parse : string -> Smt.Tseitin.t list