From 4a337a85d3a6851c4062bb016b96e709ad54c983 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 18 Jul 2021 01:29:28 -0400 Subject: [PATCH] cleanup msat --- src/{sat/src => }/backend/Backend_intf.ml | 0 src/{sat/src => }/backend/Coq.ml | 0 src/{sat/src => }/backend/Coq.mli | 0 src/{sat/src => }/backend/Dedukti.ml | 0 src/{sat/src => }/backend/Dedukti.mli | 0 src/{sat/src => }/backend/Dot.ml | 0 src/{sat/src => }/backend/Dot.mli | 0 src/{sat/src => }/backend/dune | 0 .../src => }/backtrack/Backtrackable_ref.ml | 0 .../src => }/backtrack/Backtrackable_ref.mli | 0 src/{sat/src => }/backtrack/Msat_backtrack.ml | 0 src/{sat/src => }/backtrack/dune | 0 src/msat-solver/dune | 2 +- src/sat/{src/core => }/Heap.ml | 0 src/sat/{src/core => }/Heap.mli | 0 src/sat/{src/core => }/Heap_intf.ml | 0 src/sat/{src/core => }/Internal.ml | 0 src/sat/{src/core => }/Log.ml | 0 src/sat/{src/core => }/Log.mli | 0 src/sat/{src/core => }/Msat.ml | 0 src/sat/{src/core => }/Solver.ml | 0 src/sat/{src/core => }/Solver.mli | 0 src/sat/{src/core => }/Solver_intf.ml | 0 src/sat/{src/core => }/Vec.ml | 0 src/sat/{src/core => }/Vec.mli | 0 src/sat/dune | 18 +- src/sat/{src/core => }/msat.mld | 0 src/sat/src/core/dune | 10 - src/sat/src/dune | 4 - src/sat/src/index.mld | 121 ------- src/sat/src/main/Dimacs_lex.mll | 20 -- src/sat/src/main/Dimacs_parse.mly | 34 -- src/sat/src/main/dune | 14 - src/sat/src/main/main.ml | 186 ---------- src/sat/src/sat/Int_lit.ml | 66 ---- src/sat/src/sat/Int_lit.mli | 33 -- src/sat/src/sat/Msat_sat.ml | 11 - src/sat/src/sat/Msat_sat.mli | 19 - src/sat/src/sat/dune | 11 - src/sat/src/sudoku/dune | 9 - src/sat/src/sudoku/sudoku_solve.ml | 331 ------------------ src/sat/src/tseitin/Msat_tseitin.ml | 326 ----------------- src/sat/src/tseitin/Msat_tseitin.mli | 22 -- src/sat/src/tseitin/Tseitin_intf.ml | 85 ----- src/sat/src/tseitin/dune | 11 - 45 files changed, 10 insertions(+), 1323 deletions(-) rename src/{sat/src => }/backend/Backend_intf.ml (100%) rename src/{sat/src => }/backend/Coq.ml (100%) rename src/{sat/src => }/backend/Coq.mli (100%) rename src/{sat/src => }/backend/Dedukti.ml (100%) rename src/{sat/src => }/backend/Dedukti.mli (100%) rename src/{sat/src => }/backend/Dot.ml (100%) rename src/{sat/src => }/backend/Dot.mli (100%) rename src/{sat/src => }/backend/dune (100%) rename src/{sat/src => }/backtrack/Backtrackable_ref.ml (100%) rename src/{sat/src => }/backtrack/Backtrackable_ref.mli (100%) rename src/{sat/src => }/backtrack/Msat_backtrack.ml (100%) rename src/{sat/src => }/backtrack/dune (100%) rename src/sat/{src/core => }/Heap.ml (100%) rename src/sat/{src/core => }/Heap.mli (100%) rename src/sat/{src/core => }/Heap_intf.ml (100%) rename src/sat/{src/core => }/Internal.ml (100%) rename src/sat/{src/core => }/Log.ml (100%) rename src/sat/{src/core => }/Log.mli (100%) rename src/sat/{src/core => }/Msat.ml (100%) rename src/sat/{src/core => }/Solver.ml (100%) rename src/sat/{src/core => }/Solver.mli (100%) rename src/sat/{src/core => }/Solver_intf.ml (100%) rename src/sat/{src/core => }/Vec.ml (100%) rename src/sat/{src/core => }/Vec.mli (100%) rename src/sat/{src/core => }/msat.mld (100%) delete mode 100644 src/sat/src/core/dune delete mode 100644 src/sat/src/dune delete mode 100644 src/sat/src/index.mld delete mode 100644 src/sat/src/main/Dimacs_lex.mll delete mode 100644 src/sat/src/main/Dimacs_parse.mly delete mode 100644 src/sat/src/main/dune delete mode 100644 src/sat/src/main/main.ml delete mode 100644 src/sat/src/sat/Int_lit.ml delete mode 100644 src/sat/src/sat/Int_lit.mli delete mode 100644 src/sat/src/sat/Msat_sat.ml delete mode 100644 src/sat/src/sat/Msat_sat.mli delete mode 100644 src/sat/src/sat/dune delete mode 100644 src/sat/src/sudoku/dune delete mode 100644 src/sat/src/sudoku/sudoku_solve.ml delete mode 100644 src/sat/src/tseitin/Msat_tseitin.ml delete mode 100644 src/sat/src/tseitin/Msat_tseitin.mli delete mode 100644 src/sat/src/tseitin/Tseitin_intf.ml delete mode 100644 src/sat/src/tseitin/dune diff --git a/src/sat/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml similarity index 100% rename from src/sat/src/backend/Backend_intf.ml rename to src/backend/Backend_intf.ml diff --git a/src/sat/src/backend/Coq.ml b/src/backend/Coq.ml similarity index 100% rename from src/sat/src/backend/Coq.ml rename to src/backend/Coq.ml diff --git a/src/sat/src/backend/Coq.mli b/src/backend/Coq.mli similarity index 100% rename from src/sat/src/backend/Coq.mli rename to src/backend/Coq.mli diff --git a/src/sat/src/backend/Dedukti.ml b/src/backend/Dedukti.ml similarity index 100% rename from src/sat/src/backend/Dedukti.ml rename to src/backend/Dedukti.ml diff --git a/src/sat/src/backend/Dedukti.mli b/src/backend/Dedukti.mli similarity index 100% rename from src/sat/src/backend/Dedukti.mli rename to src/backend/Dedukti.mli diff --git a/src/sat/src/backend/Dot.ml b/src/backend/Dot.ml similarity index 100% rename from src/sat/src/backend/Dot.ml rename to src/backend/Dot.ml diff --git a/src/sat/src/backend/Dot.mli b/src/backend/Dot.mli similarity index 100% rename from src/sat/src/backend/Dot.mli rename to src/backend/Dot.mli diff --git a/src/sat/src/backend/dune b/src/backend/dune similarity index 100% rename from src/sat/src/backend/dune rename to src/backend/dune diff --git a/src/sat/src/backtrack/Backtrackable_ref.ml b/src/backtrack/Backtrackable_ref.ml similarity index 100% rename from src/sat/src/backtrack/Backtrackable_ref.ml rename to src/backtrack/Backtrackable_ref.ml diff --git a/src/sat/src/backtrack/Backtrackable_ref.mli b/src/backtrack/Backtrackable_ref.mli similarity index 100% rename from src/sat/src/backtrack/Backtrackable_ref.mli rename to src/backtrack/Backtrackable_ref.mli diff --git a/src/sat/src/backtrack/Msat_backtrack.ml b/src/backtrack/Msat_backtrack.ml similarity index 100% rename from src/sat/src/backtrack/Msat_backtrack.ml rename to src/backtrack/Msat_backtrack.ml diff --git a/src/sat/src/backtrack/dune b/src/backtrack/dune similarity index 100% rename from src/sat/src/backtrack/dune rename to src/backtrack/dune diff --git a/src/msat-solver/dune b/src/msat-solver/dune index 2a945b95..8e6100cd 100644 --- a/src/msat-solver/dune +++ b/src/msat-solver/dune @@ -2,5 +2,5 @@ (name Sidekick_msat_solver) (public_name sidekick.msat-solver) (libraries containers iter sidekick.core sidekick.util - sidekick.cc msat msat.backend) + sidekick.cc sidekick.sat) (flags :standard -open Sidekick_util)) diff --git a/src/sat/src/core/Heap.ml b/src/sat/Heap.ml similarity index 100% rename from src/sat/src/core/Heap.ml rename to src/sat/Heap.ml diff --git a/src/sat/src/core/Heap.mli b/src/sat/Heap.mli similarity index 100% rename from src/sat/src/core/Heap.mli rename to src/sat/Heap.mli diff --git a/src/sat/src/core/Heap_intf.ml b/src/sat/Heap_intf.ml similarity index 100% rename from src/sat/src/core/Heap_intf.ml rename to src/sat/Heap_intf.ml diff --git a/src/sat/src/core/Internal.ml b/src/sat/Internal.ml similarity index 100% rename from src/sat/src/core/Internal.ml rename to src/sat/Internal.ml diff --git a/src/sat/src/core/Log.ml b/src/sat/Log.ml similarity index 100% rename from src/sat/src/core/Log.ml rename to src/sat/Log.ml diff --git a/src/sat/src/core/Log.mli b/src/sat/Log.mli similarity index 100% rename from src/sat/src/core/Log.mli rename to src/sat/Log.mli diff --git a/src/sat/src/core/Msat.ml b/src/sat/Msat.ml similarity index 100% rename from src/sat/src/core/Msat.ml rename to src/sat/Msat.ml diff --git a/src/sat/src/core/Solver.ml b/src/sat/Solver.ml similarity index 100% rename from src/sat/src/core/Solver.ml rename to src/sat/Solver.ml diff --git a/src/sat/src/core/Solver.mli b/src/sat/Solver.mli similarity index 100% rename from src/sat/src/core/Solver.mli rename to src/sat/Solver.mli diff --git a/src/sat/src/core/Solver_intf.ml b/src/sat/Solver_intf.ml similarity index 100% rename from src/sat/src/core/Solver_intf.ml rename to src/sat/Solver_intf.ml diff --git a/src/sat/src/core/Vec.ml b/src/sat/Vec.ml similarity index 100% rename from src/sat/src/core/Vec.ml rename to src/sat/Vec.ml diff --git a/src/sat/src/core/Vec.mli b/src/sat/Vec.mli similarity index 100% rename from src/sat/src/core/Vec.mli rename to src/sat/Vec.mli diff --git a/src/sat/dune b/src/sat/dune index 8b682629..85a23d9a 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,10 +1,10 @@ -(alias - (name runtest) - (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src)) - (locks test) - (package msat) - (action (progn - (run mdx test README.md) - (diff? README.md README.md.corrected)))) - +(library + (name msat) + (public_name msat) + (libraries iter) + (synopsis "core data structures and algorithms for msat") + (flags :standard -warn-error -3 -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) + ) diff --git a/src/sat/src/core/msat.mld b/src/sat/msat.mld similarity index 100% rename from src/sat/src/core/msat.mld rename to src/sat/msat.mld diff --git a/src/sat/src/core/dune b/src/sat/src/core/dune deleted file mode 100644 index 85a23d9a..00000000 --- a/src/sat/src/core/dune +++ /dev/null @@ -1,10 +0,0 @@ - -(library - (name msat) - (public_name msat) - (libraries iter) - (synopsis "core data structures and algorithms for msat") - (flags :standard -warn-error -3 -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) - ) diff --git a/src/sat/src/dune b/src/sat/src/dune deleted file mode 100644 index 05c64298..00000000 --- a/src/sat/src/dune +++ /dev/null @@ -1,4 +0,0 @@ - -(documentation - (package msat) - (mld_files :standard)) diff --git a/src/sat/src/index.mld b/src/sat/src/index.mld deleted file mode 100644 index 38b0a9cc..00000000 --- a/src/sat/src/index.mld +++ /dev/null @@ -1,121 +0,0 @@ - - -{1 mSAT: a Modular SAT Solver} - -(The entry point of this library is the module: {!module-Msat}.) - -A modular implementation of the SMT algorithm can be found in the {!Msat.Solver} module, -as a functor which takes two modules : - -- A representation of formulas (which implements the `Formula_intf.S` signature) - -- A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions. - -- A dummy empty module to ensure generativity of the solver (solver modules heavily relies on -side effects to their internal state) - -{3 Sat Solver} - -A ready-to-use SAT solver is available in the {!Msat_sat} module -using the [msat.sat] library (see {!module-Msat_sat}). It can be loaded -as shown in the following code : - -{[ -# #require "msat";; -# #require "msat.sat";; -# #print_depth 0;; (* do not print details *) -]} - -Then we can create a solver and create some boolean variables: - -{[ -module Sat = Msat_sat -module E = Sat.Int_lit (* expressions *) - -let solver = Sat.create() - -(* We create here two distinct atoms *) -let a = E.fresh () (* A 'new_atom' is always distinct from any other atom *) -let b = E.make 1 (* Atoms can be created from integers *) -]} - -We can try and check the satisfiability of some clauses — here, the clause [a or b]. -[Sat.assume] adds a list of clauses to the solver. Calling [Sat.solve] -will check the satisfiability of the current set of clauses, here "Sat". - -{[ -# a <> b;; -- : bool = true -# Sat.assume solver [[a; b]] ();; -- : unit = () -# let res = Sat.solve solver;; -val res : Sat.res = Sat.Sat ... -]} - -The Sat solver has an incremental mutable state, so we still have -the clause `a or b` in our assumptions. -We add `not a` and `not b` to the state, and get "Unsat". - -{[ -# Sat.assume solver [[E.neg a]; [E.neg b]] () ;; -- : unit = () -# let res = Sat.solve solver ;; -val res : Sat.res = Sat.Unsat ... -]} - -{3 Formulas API} - -Writing clauses by hand can be tedious and error-prone. -The functor {!Msat_tseitin.Make} in the library [msat.tseitin] (see {!module-Msat_tseitin}). -proposes a formula AST (parametrized by -atoms) and a function to convert these formulas into clauses: - -{[ -# #require "msat.tseitin";; -]} - -{[ -(* Module initialization *) -module F = Msat_tseitin.Make(E) - -let solver = Sat.create () - -(* We create here two distinct atoms *) -let a = E.fresh () (* A fresh atom is always distinct from any other atom *) -let b = E.make 1 (* Atoms can be created from integers *) - -(* Let's create some formulas *) -let p = F.make_atom a -let q = F.make_atom b -let r = F.make_and [p; q] -let s = F.make_or [F.make_not p; F.make_not q] -]} - -We can try and check the satisfiability of the given formulas, by turning -it into clauses using `make_cnf`: - -{[ -# Sat.assume solver (F.make_cnf r) ();; -- : unit = () -# Sat.solve solver;; -- : Sat.res = Sat.Sat ... -]} - -{[ -# Sat.assume solver (F.make_cnf s) ();; -- : unit = () -# Sat.solve solver ;; -- : Sat.res = Sat.Unsat ... -]} - -{3 Backtracking utils} - -The library {!module-Msat_backtrack} contains some backtrackable -data structures that are useful for implementing theories. - -{3 Library msat.backend} - -This is used for proof backends: - -The entry point of this library is the module: -{!module-Msat_backend}. diff --git a/src/sat/src/main/Dimacs_lex.mll b/src/sat/src/main/Dimacs_lex.mll deleted file mode 100644 index 67850c1f..00000000 --- a/src/sat/src/main/Dimacs_lex.mll +++ /dev/null @@ -1,20 +0,0 @@ -{ - open Dimacs_parse -} - -let number = ['1' - '9'] ['0' - '9']* - -rule token = parse - | eof { EOF } - | "c" { comment lexbuf } - | [' ' '\t' '\r'] { token lexbuf } - | 'p' { P } - | "cnf" { CNF } - | '\n' { Lexing.new_line lexbuf; token lexbuf } - | '0' { ZERO } - | '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) } - | _ { failwith @@ Printf.sprintf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) } - -and comment = parse - | '\n' { Lexing.new_line lexbuf; token lexbuf } - | [^'\n'] { comment lexbuf } diff --git a/src/sat/src/main/Dimacs_parse.mly b/src/sat/src/main/Dimacs_parse.mly deleted file mode 100644 index 408b8db9..00000000 --- a/src/sat/src/main/Dimacs_parse.mly +++ /dev/null @@ -1,34 +0,0 @@ -/* Copyright 2005 INRIA */ - -%{ - let lnum pos = pos.Lexing.pos_lnum - let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol - let pp_pos out (start,stop) = - Format.fprintf out "(at %d:%d - %d:%d)" - (lnum start) (cnum start) (lnum stop) (cnum stop) -%} - -%token LIT -%token ZERO -%token P CNF EOF - -%start file -%type file - -%% - -/* DIMACS syntax */ - -prelude: - | P CNF LIT LIT { () } - -clauses: - | { [] } - | clause clauses { $1 :: $2 } - -file: - | prelude clauses EOF { $2 } - -clause: - | ZERO { [] } - | LIT clause { $1 :: $2 } diff --git a/src/sat/src/main/dune b/src/sat/src/main/dune deleted file mode 100644 index 073ec30f..00000000 --- a/src/sat/src/main/dune +++ /dev/null @@ -1,14 +0,0 @@ - -; main binary -(executable - (name main) - (public_name msat) - (package msat-bin) - (libraries containers camlzip msat msat.sat msat.backend) - (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) - (ocamlopt_flags :standard -O3 -color always - -unbox-closures -unbox-closures-factor 20) - ) - -(ocamlyacc (modules Dimacs_parse)) -(ocamllex (modules Dimacs_lex)) diff --git a/src/sat/src/main/main.ml b/src/sat/src/main/main.ml deleted file mode 100644 index ddc1d856..00000000 --- a/src/sat/src/main/main.ml +++ /dev/null @@ -1,186 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Incorrect_model -exception Out_of_time -exception Out_of_space - -let file = ref "" -let p_cnf = ref false -let p_check = ref false -let p_dot_proof = ref "" -let p_proof_print = ref false -let time_limit = ref 300. -let size_limit = ref 1000_000_000. -let no_proof = ref false - -module S = Msat_sat - -module Process() = struct - module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S)) - - let hyps = ref [] - - let st = S.create ~store_proof:(not !no_proof) ~size:`Big () - - let check_model sat = - let check_clause c = - let l = List.map (function a -> - Log.debugf 99 - (fun k -> k "Checking value of %a" S.Formula.pp a); - sat.Msat.eval 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 - - let prove ~assumptions () = - let res = S.solve ~assumptions st in - let t = Sys.time () in - begin match res with - | S.Sat state -> - if !p_check then - if not (check_model state) then - raise Incorrect_model; - let t' = Sys.time () -. t in - Format.printf "Sat (%f/%f)@." t t' - | S.Unsat state -> - if !p_check then ( - let p = state.Msat.get_proof () in - S.Proof.check_empty_conclusion p; - S.Proof.check p; - if !p_dot_proof <> "" then ( - let oc = open_out !p_dot_proof in - let fmt = Format.formatter_of_out_channel oc in - Format.fprintf fmt "%a@?" D.pp p; - flush oc; close_out_noerr oc; - ) - ); - let t' = Sys.time () -. t in - Format.printf "Unsat (%f/%f)@." t t' - end - - let conv_c c = List.rev_map S.Int_lit.make c - - let add_clauses cs = - S.assume st (CCList.map conv_c cs) () -end[@@inline] - -let parse_file f = - let module L = Lexing in - CCIO.with_in f - (fun ic -> - let buf = - if CCString.suffix ~suf:".gz" f - then ( - let gic = Gzip.open_in_chan ic in - L.from_function (fun bytes len -> Gzip.input gic bytes 0 len) - ) else L.from_channel ic - in - buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;}; - Dimacs_parse.file Dimacs_lex.token buf) - -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 () - -(* 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 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_check, - " Build, check and print the proof (if output is set), if unsat"; - "-dot", Arg.Set_string p_dot_proof, - " If provided, print the dot proof in the given file"; - "-gc", Arg.Unit setup_gc_stat, - " Outputs statistics about the GC"; - "-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"; - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - "-no-proof", Arg.Set no_proof, " disable proof logging"; - ] - -(* 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 - -let main () = - (* Administrative duties *) - Arg.parse argspec input_file usage; - if !file = "" then ( - Arg.usage argspec usage; - exit 2 - ); - let al = Gc.create_alarm check in - - let module P = Process() in - - (* Interesting stuff happening *) - let clauses = parse_file !file in - P.add_clauses clauses; - P.prove ~assumptions:[] (); - Gc.delete_alarm al; - () - -let () = - try - main () - with - | 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 - | S.Proof.Resolution_error msg -> - Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg; - exit 5 - diff --git a/src/sat/src/sat/Int_lit.ml b/src/sat/src/sat/Int_lit.ml deleted file mode 100644 index 9f01aaeb..00000000 --- a/src/sat/src/sat/Int_lit.ml +++ /dev/null @@ -1,66 +0,0 @@ - -exception Bad_atom -(** Exception raised if an atom cannot be created *) - -type t = int -(** Atoms are represented as integers. [-i] begin the negation of [i]. - Additionally, since we nee dot be able to create fresh atoms, we - use even integers for user-created atoms, and odd integers for the - fresh atoms. *) - -let max_lit = max_int - -(* Counters *) -let max_index = ref 0 -let max_fresh = ref (-1) - -(** Internal function for creating atoms. - Updates the internal counters *) -let _make i = - if i <> 0 && (abs i) < max_lit then begin - max_index := max !max_index (abs i); - i - end else - raise Bad_atom - -let to_int i = i - -(** *) -let neg a = - a - -let norm a = - abs a, if a < 0 then - Solver_intf.Negated - else - Solver_intf.Same_sign - -let abs = abs - -let sign i = i > 0 - -let apply_sign b i = if b then i else neg i - -let set_sign b i = if b then abs i else neg (abs i) - -let hash (a:int) = a land max_int -let equal (a:int) b = a=b -let compare (a:int) b = compare a b - -let make i = _make (2 * i) - -let fresh () = - incr max_fresh; - _make (2 * !max_fresh + 1) - -(* -let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f j - done -*) - -let pp fmt a = - Format.fprintf fmt "%s%s%d" - (if a < 0 then "~" else "") - (if a mod 2 = 0 then "v" else "f") - ((abs a) / 2) diff --git a/src/sat/src/sat/Int_lit.mli b/src/sat/src/sat/Int_lit.mli deleted file mode 100644 index 6845d161..00000000 --- a/src/sat/src/sat/Int_lit.mli +++ /dev/null @@ -1,33 +0,0 @@ - -(** {1 The module defining formulas} *) - -(** SAT Formulas - - This modules implements formuals adequate for use in a pure SAT Solver. - Atomic formuals are represented using integers, that should allow - near optimal efficiency (both in terms of space and time). -*) - -include Solver_intf.FORMULA -(** This modules implements the requirements for implementing an SAT Solver. *) - -val make : int -> t -(** Make a proposition from an integer. *) - -val to_int : t -> int - -val fresh : unit -> t -(** Make a fresh atom *) - -val compare : t -> t -> int -(** Compare atoms *) - -val sign : t -> bool -(** Is the given atom positive ? *) - -val apply_sign : bool -> t -> t -(** [apply_sign b] is the identity if [b] is [true], and the negation - function if [b] is [false]. *) - -val set_sign : bool -> t -> t -(** Return the atom with the sign set. *) diff --git a/src/sat/src/sat/Msat_sat.ml b/src/sat/src/sat/Msat_sat.ml deleted file mode 100644 index 91cc70c6..00000000 --- a/src/sat/src/sat/Msat_sat.ml +++ /dev/null @@ -1,11 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -module Int_lit = Int_lit -include Msat.Make_pure_sat(struct - module Formula = Int_lit - type proof = unit - end) - diff --git a/src/sat/src/sat/Msat_sat.mli b/src/sat/src/sat/Msat_sat.mli deleted file mode 100644 index 0517e913..00000000 --- a/src/sat/src/sat/Msat_sat.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -(** Sat solver - - This modules instanciates a pure sat solver using integers to represent - atomic propositions. -*) - -module Int_lit = Int_lit - -include Msat.S - with type Formula.t = Int_lit.t - and type theory = unit - and type lemma = unit -(** A functor that can generate as many solvers as needed. *) - diff --git a/src/sat/src/sat/dune b/src/sat/src/sat/dune deleted file mode 100644 index 624b2a57..00000000 --- a/src/sat/src/sat/dune +++ /dev/null @@ -1,11 +0,0 @@ - -(library - (name msat_sat) - (public_name msat.sat) - (synopsis "purely boolean interface to Msat") - (libraries msat) - (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) - (ocamlopt_flags :standard -O3 -color always - -unbox-closures -unbox-closures-factor 20) - ) - diff --git a/src/sat/src/sudoku/dune b/src/sat/src/sudoku/dune deleted file mode 100644 index 000c407f..00000000 --- a/src/sat/src/sudoku/dune +++ /dev/null @@ -1,9 +0,0 @@ - -(executable - (name sudoku_solve) - (modes native) - (libraries msat msat.backtrack iter containers) - (flags :standard -warn-error -a -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) -) diff --git a/src/sat/src/sudoku/sudoku_solve.ml b/src/sat/src/sudoku/sudoku_solve.ml deleted file mode 100644 index a75ace03..00000000 --- a/src/sat/src/sudoku/sudoku_solve.ml +++ /dev/null @@ -1,331 +0,0 @@ - -(** {1 simple sudoku solver} *) - -module Fmt = CCFormat -module Log = Msat.Log -module Vec = Msat.Vec - -let errorf msg = CCFormat.kasprintf failwith msg - -module Cell : sig - type t = private int - val equal : t -> t -> bool - val neq : t -> t -> bool - val hash : t -> int - val empty : t - val is_empty : t -> bool - val is_full : t -> bool - val make : int -> t - val pp : t Fmt.printer -end = struct - type t = int - let empty = 0 - let[@inline] make i = assert (i >= 0 && i <= 9); i - let[@inline] is_empty x = x = 0 - let[@inline] is_full x = x > 0 - let hash = CCHash.int - let[@inline] equal (a:t) b = a=b - let[@inline] neq (a:t) b = a<>b - let pp out i = if i=0 then Fmt.char out '.' else Fmt.int out i -end - -module Grid : sig - type t - - val get : t -> int -> int -> Cell.t - val set : t -> int -> int -> Cell.t -> t - - (** A set of related cells *) - type set = (int*int*Cell.t) Iter.t - - val rows : t -> set Iter.t - val cols : t -> set Iter.t - val squares : t -> set Iter.t - - val all_cells : t -> (int*int*Cell.t) Iter.t - - val parse : string -> t - val is_full : t -> bool - val is_valid : t -> bool - val matches : pat:t -> t -> bool - val pp : t Fmt.printer -end = struct - type t = Cell.t array - - let[@inline] get (s:t) i j = s.(i*9 + j) - - let[@inline] set (s:t) i j n = - let s' = Array.copy s in - s'.(i*9 + j) <- n; - s' - - (** A set of related cells *) - type set = (int*int*Cell.t) Iter.t - - open Iter.Infix - - let all_cells (g:t) = - 0 -- 8 >>= fun i -> - 0 -- 8 >|= fun j -> (i,j,get g i j) - - let rows (g:t) = - 0 -- 8 >|= fun i -> - ( 0 -- 8 >|= fun j -> (i,j,get g i j)) - - let cols g = - 0 -- 8 >|= fun j -> - ( 0 -- 8 >|= fun i -> (i,j,get g i j)) - - let squares g = - 0 -- 2 >>= fun sq_i -> - 0 -- 2 >|= fun sq_j -> - ( 0 -- 2 >>= fun off_i -> - 0 -- 2 >|= fun off_j -> - let i = 3*sq_i + off_i in - let j = 3*sq_j + off_j in - (i,j,get g i j)) - - let is_full g = Array.for_all Cell.is_full g - - let is_valid g = - let all_distinct (s:set) = - (s >|= fun (_,_,c) -> c) - |> Iter.diagonal - |> Iter.for_all (fun (c1,c2) -> Cell.neq c1 c2) - in - Iter.for_all all_distinct @@ rows g && - Iter.for_all all_distinct @@ cols g && - Iter.for_all all_distinct @@ squares g - - let matches ~pat:g1 g2 : bool = - all_cells g1 - |> Iter.filter (fun (_,_,c) -> Cell.is_full c) - |> Iter.for_all (fun (x,y,c) -> Cell.equal c @@ get g2 x y) - - let pp out g = - Fmt.fprintf out "@["; - Array.iteri - (fun i n -> - Cell.pp out n; - if i mod 9 = 8 then Fmt.fprintf out "@,") - g; - Fmt.fprintf out "@]" - - let parse (s:string) : t = - if String.length s < 81 then ( - errorf "line is too short, expected 81 chars, not %d" (String.length s); - ); - let a = Array.make 81 Cell.empty in - for i = 0 to 80 do - let c = String.get s i in - let n = if c = '.' then 0 else Char.code c - Char.code '0' in - if n < 0 || n > 9 then errorf "invalid char %c" c; - a.(i) <- Cell.make n - done; - a -end - -module B_ref = Msat_backtrack.Ref - -module Solver : sig - type t - val create : Grid.t -> t - val solve : t -> Grid.t option -end = struct - open Msat.Solver_intf - - (* formulas *) - module F = struct - type t = bool*int*int*Cell.t - let equal (sign1,x1,y1,c1)(sign2,x2,y2,c2) = - sign1=sign2 && x1=x2 && y1=y2 && Cell.equal c1 c2 - let hash (sign,x,y,c) = CCHash.(combine4 (bool sign)(int x)(int y)(Cell.hash c)) - let pp out (sign,x,y,c) = - Fmt.fprintf out "[@[(%d,%d) %s %a@]]" x y (if sign then "=" else "!=") Cell.pp c - let neg (sign,x,y,c) = (not sign,x,y,c) - let norm ((sign,_,_,_) as f) = - if sign then f, Same_sign else neg f, Negated - - let make sign x y (c:Cell.t) : t = (sign,x,y,c) - end - - module Theory = struct - type proof = unit - module Formula = F - type t = { - grid: Grid.t B_ref.t; - } - - let create g : t = {grid=B_ref.create g} - let[@inline] grid self : Grid.t = B_ref.get self.grid - let[@inline] set_grid self g : unit = B_ref.set self.grid g - - let push_level self = B_ref.push_level self.grid - let pop_levels self n = B_ref.pop_levels self.grid n - - let pp_c_ = Fmt.(list ~sep:(return "@ ∨ ")) F.pp - let[@inline] logs_conflict kind c : unit = - Log.debugf 4 (fun k->k "(@[conflict.%s@ %a@])" kind pp_c_ c) - - (* check that all cells are full *) - let check_full_ (self:t) acts : unit = - Grid.all_cells (grid self) - (fun (x,y,c) -> - if Cell.is_empty c then ( - let c = - CCList.init 9 - (fun c -> F.make true x y (Cell.make (c+1))) - in - Log.debugf 4 (fun k->k "(@[add-clause@ %a@])" pp_c_ c); - acts.acts_add_clause ~keep:true c (); - )) - - (* check constraints *) - let check_ (self:t) acts : unit = - Log.debugf 4 (fun k->k "(@[sudoku.check@ @[:g %a@]@])" Grid.pp (B_ref.get self.grid)); - let[@inline] all_diff kind f = - let pairs = - f (grid self) - |> Iter.flat_map - (fun set -> - set - |> Iter.filter (fun (_,_,c) -> Cell.is_full c) - |> Iter.diagonal) - in - pairs - (fun ((x1,y1,c1),(x2,y2,c2)) -> - if Cell.equal c1 c2 then ( - assert (x1<>x2 || y1<>y2); - let c = [F.make false x1 y1 c1; F.make false x2 y2 c2] in - logs_conflict ("all-diff." ^ kind) c; - acts.acts_raise_conflict c () - )) - in - all_diff "rows" Grid.rows; - all_diff "cols" Grid.cols; - all_diff "squares" Grid.squares; - () - - let trail_ (acts:_ Msat.acts) = - acts.acts_iter_assumptions - |> Iter.map - (function - | Assign _ -> assert false - | Lit f -> f) - - (* update current grid with the given slice *) - let add_slice (self:t) acts : unit = - trail_ acts - (function - | false,_,_,_ -> () - | true,x,y,c -> - assert (Cell.is_full c); - let grid = grid self in - let c' = Grid.get grid x y in - if Cell.is_empty c' then ( - set_grid self (Grid.set grid x y c); - ) else if Cell.neq c c' then ( - (* conflict: at most one value *) - let c = [F.make false x y c; F.make false x y c'] in - logs_conflict "at-most-one" c; - acts.acts_raise_conflict c () - ) - ) - - let partial_check (self:t) acts : unit = - Log.debugf 4 - (fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])" - (Fmt.list F.pp) (trail_ acts |> Iter.to_list)); - add_slice self acts; - check_ self acts - - let final_check (self:t) acts : unit = - Log.debugf 4 (fun k->k "(@[sudoku.final-check@])"); - check_full_ self acts; - check_ self acts - - end - - module S = Msat.Make_cdcl_t(Theory) - - type t = { - grid0: Grid.t; - solver: S.t; - } - - let solve (self:t) : _ option = - let assumptions = - Grid.all_cells self.grid0 - |> Iter.filter (fun (_,_,c) -> Cell.is_full c) - |> Iter.map (fun (x,y,c) -> F.make true x y c) - |> Iter.map (S.make_atom self.solver) - |> Iter.to_rev_list - in - Log.debugf 2 - (fun k->k "(@[sudoku.solve@ :assumptions %a@])" (Fmt.Dump.list S.Atom.pp) assumptions); - let r = - match S.solve self.solver ~assumptions with - | S.Sat _ -> Some (Theory.grid (S.theory self.solver)) - | S.Unsat _ -> None - in - (* TODO: print some stats *) - r - - let create g : t = - { solver=S.create ~store_proof:false (Theory.create g); grid0=g } -end - -let solve_grid (g:Grid.t) : Grid.t option = - let s = Solver.create g in - Solver.solve s - -let solve_file file = - Format.printf "solve grids in file %S@." file; - let start = Sys.time() in - let grids = - CCIO.with_in file CCIO.read_lines_l - |> CCList.filter_map - (fun s -> - let s = String.trim s in - if s="" then None - else match Grid.parse s with - | g -> Some g - | exception e -> - errorf "cannot parse sudoku %S: %s@." s (Printexc.to_string e)) - in - Format.printf "parsed %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start); - List.iter - (fun g -> - Format.printf "@[@,#########################@,@[<2>solve grid:@ %a@]@]@." Grid.pp g; - let start=Sys.time() in - match solve_grid g with - | None -> Format.printf "no solution (in %.3fs)@." (Sys.time()-.start) - | Some g' when not @@ Grid.is_full g' -> - errorf "grid %a@ is not full" Grid.pp g' - | Some g' when not @@ Grid.is_valid g' -> - errorf "grid %a@ is not valid" Grid.pp g' - | Some g' when not @@ Grid.matches ~pat:g g' -> - errorf "grid %a@ @[<2>does not match original@ %a@]" Grid.pp g' Grid.pp g - | Some g' -> - Format.printf "@[@[<2>solution (in %.3fs):@ %a@]@,###################@]@." - (Sys.time()-.start) Grid.pp g') - grids; - Format.printf "@.solved %d grids (in %.3fs)@." (List.length grids) (Sys.time()-.start); - () - -let () = - Fmt.set_color_default true; - let files = ref [] in - let debug = ref 0 in - let opts = [ - "--debug", Arg.Set_int debug, " debug"; - "-d", Arg.Set_int debug, " debug"; - ] |> Arg.align in - Arg.parse opts (fun f -> files := f :: !files) "sudoku_solve [options] "; - Msat.Log.set_debug !debug; - try - List.iter (fun f -> solve_file f) !files; - with - | Failure msg | Invalid_argument msg -> - Format.printf "@{Error@}:@.%s@." msg; - exit 1 diff --git a/src/sat/src/tseitin/Msat_tseitin.ml b/src/sat/src/tseitin/Msat_tseitin.ml deleted file mode 100644 index 3f162c8d..00000000 --- a/src/sat/src/tseitin/Msat_tseitin.ml +++ /dev/null @@ -1,326 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module type Arg = Tseitin_intf.Arg - -module type S = Tseitin_intf.S - -module Make (F : Tseitin_intf.Arg) = struct - - exception Empty_Or - type combinator = And | Or | Imp | Not - - type atom = F.t - type t = - | True - | Lit of atom - | Comb of combinator * t list - - let rec pp fmt phi = - match phi with - | True -> Format.fprintf fmt "true" - | Lit a -> F.pp fmt a - | Comb (Not, [f]) -> - Format.fprintf fmt "not (%a)" pp f - | Comb (And, l) -> Format.fprintf fmt "(%a)" (pp_list "and") l - | Comb (Or, l) -> Format.fprintf fmt "(%a)" (pp_list "or") l - | Comb (Imp, [f1; f2]) -> - Format.fprintf fmt "(%a => %a)" pp f1 pp f2 - | _ -> assert false - and pp_list sep fmt = function - | [] -> () - | [f] -> pp fmt f - | f::l -> Format.fprintf fmt "%a %s %a" pp f sep (pp_list sep) l - - let make comb l = Comb (comb, l) - - let make_atom p = Lit p - - let f_true = True - let f_false = Comb(Not, [True]) - - let rec flatten comb acc = function - | [] -> acc - | (Comb (c, l)) :: r when c = comb -> - flatten comb (List.rev_append l acc) r - | a :: r -> - flatten comb (a :: acc) r - - let rec opt_rev_map f acc = function - | [] -> acc - | a :: r -> begin match f a with - | None -> opt_rev_map f acc r - | Some b -> opt_rev_map f (b :: acc) r - end - - let remove_true l = - let aux = function - | True -> None - | f -> Some f - in - opt_rev_map aux [] l - - let remove_false l = - let aux = function - | Comb(Not, [True]) -> None - | f -> Some f - in - opt_rev_map aux [] l - - - let make_not f = make Not [f] - - let make_and l = - let l' = remove_true (flatten And [] l) in - if List.exists ((=) f_false) l' then - f_false - else - make And l' - - let make_or l = - let l' = remove_false (flatten Or [] l) in - if List.exists ((=) f_true) l' then - f_true - else match l' with - | [] -> raise Empty_Or - | [a] -> a - | _ -> Comb (Or, l') - - let make_imply f1 f2 = make Imp [f1; f2] - let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1] - let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ]; - make_and [ f1; make_not f2 ] ] - - (* simplify formula *) - let (%%) f g x = f (g x) - - let rec sform f k = match f with - | True | Comb (Not, [True]) -> k f - | Comb (Not, [Lit a]) -> k (Lit (F.neg a)) - | Comb (Not, [Comb (Not, [f])]) -> sform f k - | Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and) - | Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or) - | Comb (And, l) -> sform_list [] l (k %% make_and) - | Comb (Or, l) -> sform_list [] l (k %% make_or) - | Comb (Imp, [f1; f2]) -> - sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2']))) - | Comb (Not, [Comb (Imp, [f1; f2])]) -> - sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2']))) - | Comb ((Imp | Not), _) -> assert false - | Lit _ -> k f - and sform_list acc l k = match l with - | [] -> k acc - | f :: tail -> - sform f (fun f' -> sform_list (f'::acc) tail k) - and sform_list_not acc l k = match l with - | [] -> k acc - | f :: tail -> - sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k) - - let ( @@ ) l1 l2 = List.rev_append l1 l2 - (* let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) *) - - (* - let distrib l_and l_or = - let l = - if l_or = [] then l_and - else - List.rev_map - (fun x -> - match x with - | Lit _ -> Comb (Or, x::l_or) - | Comb (Or, l) -> Comb (Or, l @@ l_or) - | _ -> assert false - ) l_and - in - Comb (And, l) - - let rec flatten_or = function - | [] -> [] - | Comb (Or, l)::r -> l @@ (flatten_or r) - | Lit a :: r -> (Lit a)::(flatten_or r) - | _ -> assert false - - let rec flatten_and = function - | [] -> [] - | Comb (And, l)::r -> l @@ (flatten_and r) - | a :: r -> a::(flatten_and r) - - - let rec cnf f = - match f with - | Comb (Or, l) -> - begin - let l = List.rev_map cnf l in - let l_and, l_or = - List.partition (function Comb(And,_) -> true | _ -> false) l in - match l_and with - | [ Comb(And, l_conj) ] -> - let u = flatten_or l_or in - distrib l_conj u - - | Comb(And, l_conj) :: r -> - let u = flatten_or l_or in - cnf (Comb(Or, (distrib l_conj u)::r)) - - | _ -> - begin - match flatten_or l_or with - | [] -> assert false - | [r] -> r - | v -> Comb (Or, v) - end - end - | Comb (And, l) -> - Comb (And, List.rev_map cnf l) - | f -> f - - let rec mk_cnf = function - | Comb (And, l) -> - List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l - - | Comb (Or, [f1;f2]) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf f2 in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Comb (Or, f1 :: l) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf (Comb (Or, l)) in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Lit a -> [[a]] - | Comb (Not, [Lit a]) -> [[F.neg a]] - | _ -> assert false - - - let rec unfold mono f = - match f with - | Lit a -> a::mono - | Comb (Not, [Lit a]) -> - (F.neg a)::mono - | Comb (Or, l) -> - List.fold_left unfold mono l - | _ -> assert false - - let rec init monos f = - match f with - | Comb (And, l) -> - List.fold_left init monos l - | f -> (unfold [] f)::monos - - let make_cnf f = - let sfnc = cnf (sform f) in - init [] sfnc - *) - - let mk_proxy = F.fresh - - let acc_or = ref [] - let acc_and = ref [] - - (* build a clause by flattening (if sub-formulas have the - same combinator) and proxy-ing sub-formulas that have the - opposite operator. *) - let rec cnf f = match f with - | Lit a -> None, [a] - | Comb (Not, [Lit a]) -> None, [F.neg a] - - | Comb (And, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | _cmb, [a] -> Some And, a :: acc - | Some And, l -> - Some And, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_and := (proxy, l) :: !acc_and; *) - (* proxy :: acc *) - | Some Or, l -> - let proxy = mk_proxy () in - acc_or := (proxy, l) :: !acc_or; - Some And, proxy :: acc - | None, l -> Some And, l @@ acc - | _ -> assert false - ) (None, []) l - - | Comb (Or, l) -> - List.fold_left - (fun (_, acc) f -> - match cnf f with - | _, [] -> assert false - | _cmb, [a] -> Some Or, a :: acc - | Some Or, l -> - Some Or, l @@ acc - (* let proxy = mk_proxy () in *) - (* acc_or := (proxy, l) :: !acc_or; *) - (* proxy :: acc *) - | Some And, l -> - let proxy = mk_proxy () in - acc_and := (proxy, l) :: !acc_and; - Some Or, proxy :: acc - | None, l -> Some Or, l @@ acc - | _ -> assert false - ) (None, []) l - | _ -> assert false - - let cnf f = - let acc = match f with - | True -> [] - | Comb(Not, [True]) -> [[]] - | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l - | _ -> [snd (cnf f)] - in - let proxies = ref [] in - (* encore clauses that make proxies in !acc_and equivalent to - their clause *) - let acc = - List.fold_left - (fun acc (p,l) -> - proxies := p :: !proxies; - let np = F.neg p in - (* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]] - also add clauses [p => l1], [p => l2], etc. *) - let cl, acc = - List.fold_left - (fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc) - ([p],acc) l in - cl :: acc - ) acc !acc_and - in - (* encore clauses that make proxies in !acc_or equivalent to - their clause *) - let acc = - List.fold_left - (fun acc (p,l) -> - proxies := p :: !proxies; - (* add clause [p => l1 | l2 | ... | ln], and add clauses - [l1 => p], [l2 => p], etc. *) - let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc) - acc l in - (F.neg p :: l) :: acc - ) acc !acc_or - in - acc - - let make_cnf f = - acc_or := []; - acc_and := []; - cnf (sform f (fun f' -> f')) - - (* Naive CNF XXX remove??? - let make_cnf f = mk_cnf (sform f) - *) -end diff --git a/src/sat/src/tseitin/Msat_tseitin.mli b/src/sat/src/tseitin/Msat_tseitin.mli deleted file mode 100644 index 498667c5..00000000 --- a/src/sat/src/tseitin/Msat_tseitin.mli +++ /dev/null @@ -1,22 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Tseitin CNF conversion - - This modules implements Tseitin's Conjunctive Normal Form conversion, i.e. - the ability to transform an arbitrary boolean formula into an equi-satisfiable - CNF, that can then be fed to a SAT/SMT/McSat solver. -*) - -module type Arg = Tseitin_intf.Arg -(** The implementation of formulas required to implement Tseitin's CNF conversion. *) - -module type S = Tseitin_intf.S -(** The exposed interface of Tseitin's CNF conversion. *) - -module Make : functor (F : Arg) -> S with type atom = F.t -(** This functor provides an implementation of Tseitin's CNF conversion. *) - diff --git a/src/sat/src/tseitin/Tseitin_intf.ml b/src/sat/src/tseitin/Tseitin_intf.ml deleted file mode 100644 index 99805c35..00000000 --- a/src/sat/src/tseitin/Tseitin_intf.ml +++ /dev/null @@ -1,85 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -(** Interfaces for Tseitin's CNF conversion *) - -module type Arg = sig - (** Formulas - - This defines what is needed of formulas in order to implement - Tseitin's CNF conversion. - *) - - type t - (** Type of atomic formulas. *) - - val neg : t -> t - (** Negation of atomic formulas. *) - - val fresh : unit -> t - (** Generate fresh formulas (that are different from any other). *) - - val pp : Format.formatter -> t -> unit - (** Print the given formula. *) - -end - -module type S = sig - (** CNF conversion - - This modules converts arbitrary boolean formulas into CNF. - *) - - type atom - (** The type of atomic formulas. *) - - type t - (** The type of arbitrary boolean formulas. Arbitrary boolean formulas - can be built using functions in this module, and then converted - to a CNF, which is a list of clauses that only use atomic formulas. *) - - val f_true : t - (** The [true] formula, i.e a formula that is always satisfied. *) - - val f_false : t - (** The [false] formula, i.e a formula that cannot be satisfied. *) - - val make_atom : atom -> t - (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *) - - val make_not : t -> t - (** Creates the negation of a boolean formula. *) - - val make_and : t list -> t - (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *) - - val make_or : t list -> t - (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *) - - val make_xor : t -> t -> t - (** [make_xor p q] creates the boolean formula "[p] xor [q]". *) - - val make_imply : t -> t -> t - (** [make_imply p q] creates the boolean formula "[p] implies [q]". *) - - val make_equiv : t -> t -> t - (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *) - - val make_cnf : t -> atom list list - (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a - list (which is a conjunction) of lists (which are disjunctions) of - atomic formulas. *) - - val pp : Format.formatter -> t -> unit - (** [print fmt f] prints the formula on the formatter [fmt].*) - -end diff --git a/src/sat/src/tseitin/dune b/src/sat/src/tseitin/dune deleted file mode 100644 index 0a35225d..00000000 --- a/src/sat/src/tseitin/dune +++ /dev/null @@ -1,11 +0,0 @@ - -(library - (name msat_tseitin) - (public_name msat.tseitin) - (synopsis "Tseitin transformation for msat") - (libraries msat) - (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) - ) -