From 24bbe97ceb5c4ac1023f7f16af6fc47737f4b8d3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 19:28:41 -0500 Subject: [PATCH] rename to sidekick --- README.md | 10 +++---- dagon.opam => sidekick.opam | 8 +++--- src/backend/jbuild | 10 +++---- src/dimacs/Lexer.mll | 2 +- src/dimacs/Parser.mly | 2 +- .../{Dagon_dimacs.ml => Sidekick_dimacs.ml} | 0 .../{Dagon_dimacs.mli => Sidekick_dimacs.mli} | 0 src/dimacs/jbuild | 6 ++--- src/main/jbuild | 10 +++---- src/main/main.ml | 26 +++++++++---------- src/main_test/jbuild | 4 +-- src/sat/{Dagon_sat.ml => Sidekick_sat.ml} | 0 src/sat/{Dagon_sat.mld => Sidekick_sat.mld} | 0 src/sat/jbuild | 10 +++---- src/smt/Congruence_closure.ml | 4 +-- src/smt/Lit.ml | 2 +- src/smt/Lit.mli | 2 +- src/smt/Model.ml | 2 +- src/smt/Solver.ml | 6 ++--- src/smt/Solver.mli | 2 +- src/smt/Theory_combine.ml | 2 +- src/smt/Theory_combine.mli | 2 +- src/smt/jbuild | 8 +++--- .../{Dagon_th_bool.ml => Sidekick_th_bool.ml} | 2 +- ...Dagon_th_bool.mli => Sidekick_th_bool.mli} | 4 +-- src/smt/th_bool/jbuild | 8 +++--- src/smtlib/Process.ml | 4 +-- src/smtlib/Process.mli | 2 +- .../{Dagon_smtlib.ml => Sidekick_smtlib.ml} | 2 +- .../{Dagon_smtlib.mli => Sidekick_smtlib.mli} | 2 +- src/smtlib/Typecheck.ml | 4 +-- src/smtlib/Typecheck.mli | 2 +- src/smtlib/jbuild | 8 +++--- .../{Dagon_th_sat.ml => Sidekick_th_sat.ml} | 0 .../{Dagon_th_sat.mli => Sidekick_th_sat.mli} | 2 +- src/th_sat/jbuild | 6 ++--- src/tseitin/jbuild | 2 +- src/util/jbuild | 4 +-- 38 files changed, 85 insertions(+), 85 deletions(-) rename dagon.opam => sidekick.opam (72%) rename src/dimacs/{Dagon_dimacs.ml => Sidekick_dimacs.ml} (100%) rename src/dimacs/{Dagon_dimacs.mli => Sidekick_dimacs.mli} (100%) rename src/sat/{Dagon_sat.ml => Sidekick_sat.ml} (100%) rename src/sat/{Dagon_sat.mld => Sidekick_sat.mld} (100%) rename src/smt/th_bool/{Dagon_th_bool.ml => Sidekick_th_bool.ml} (99%) rename src/smt/th_bool/{Dagon_th_bool.mli => Sidekick_th_bool.mli} (96%) rename src/smtlib/{Dagon_smtlib.ml => Sidekick_smtlib.ml} (97%) rename src/smtlib/{Dagon_smtlib.mli => Sidekick_smtlib.mli} (91%) rename src/th_sat/{Dagon_th_sat.ml => Sidekick_th_sat.ml} (100%) rename src/th_sat/{Dagon_th_sat.mli => Sidekick_th_sat.mli} (87%) diff --git a/README.md b/README.md index 9e4bc0b5..69933324 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -# dagon [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL) +# Sidekick [![Build Status](https://travis-ci.org/c-cube/sidekick.svg?branch=master)](https://travis-ci.org/c-cube/sidekick) -Dagon is an OCaml library with a functor to create SMT solvers following +Sidekick 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/dagon/ +See https://c-cube.github.io/sidekick/ ## Installation ### Via opam -Once the package is on [opam](http://opam.ocaml.org), just `opam install dagon`. +Once the package is on [opam](http://opam.ocaml.org), just `opam install sidekick`. For the development version, use: - opam pin add dagon https://github.com/c-cube/dagon.git + opam pin https://github.com/c-cube/sidekick.git ### Manual installation diff --git a/dagon.opam b/sidekick.opam similarity index 72% rename from dagon.opam rename to sidekick.opam index b15a6c00..c3935394 100644 --- a/dagon.opam +++ b/sidekick.opam @@ -1,5 +1,5 @@ opam-version: "1.2" -name: "dagon" +name: "sidekick" license: "Apache" version: "dev" author: ["Simon Cruanes" "Guillaume Bury" "Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer"] @@ -19,7 +19,7 @@ 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/" +homepage: "https://github.com/c-cube/sidekick" +dev-repo: "https://github.com/c-cube/sidekick.git" +bug-reports: "https://github.com/c-cube/sidekick/issues/" diff --git a/src/backend/jbuild b/src/backend/jbuild index 67043e55..172bb385 100644 --- a/src/backend/jbuild +++ b/src/backend/jbuild @@ -2,11 +2,11 @@ ; main binary (library - ((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)) + ((name Sidekick_backend) + (public_name sidekick.backend) + (synopsis "proof backends for Sidekick") + (libraries (sidekick.sat)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/dimacs/Lexer.mll b/src/dimacs/Lexer.mll index 9a4bb861..09b9c420 100644 --- a/src/dimacs/Lexer.mll +++ b/src/dimacs/Lexer.mll @@ -1,6 +1,6 @@ (* Copyright 2005 INRIA *) { - open Dagon_util + open Sidekick_util open Parser } diff --git a/src/dimacs/Parser.mly b/src/dimacs/Parser.mly index 2386ae2f..1e776952 100644 --- a/src/dimacs/Parser.mly +++ b/src/dimacs/Parser.mly @@ -1,7 +1,7 @@ /* Copyright 2005 INRIA */ %{ - open Dagon_util + open Sidekick_util let lnum pos = pos.Lexing.pos_lnum let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol diff --git a/src/dimacs/Dagon_dimacs.ml b/src/dimacs/Sidekick_dimacs.ml similarity index 100% rename from src/dimacs/Dagon_dimacs.ml rename to src/dimacs/Sidekick_dimacs.ml diff --git a/src/dimacs/Dagon_dimacs.mli b/src/dimacs/Sidekick_dimacs.mli similarity index 100% rename from src/dimacs/Dagon_dimacs.mli rename to src/dimacs/Sidekick_dimacs.mli diff --git a/src/dimacs/jbuild b/src/dimacs/jbuild index fbc40f44..98cb83df 100644 --- a/src/dimacs/jbuild +++ b/src/dimacs/jbuild @@ -4,10 +4,10 @@ ; main binary (library - ((name dagon_dimacs) - (public_name dagon.dimacs) + ((name sidekick_dimacs) + (public_name sidekick.dimacs) (optional) ; only if deps present - (libraries (containers dagon.util)) + (libraries (containers sidekick.util)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8)) (ocamlopt_flags (:standard -O3 -color always -bin-annot -unbox-closures -unbox-closures-factor 20)) diff --git a/src/main/jbuild b/src/main/jbuild index 1d585f3b..83bf9120 100644 --- a/src/main/jbuild +++ b/src/main/jbuild @@ -5,13 +5,13 @@ ; main binary (executable ((name main) - (public_name dagon) - (package dagon) + (public_name sidekick) + (package sidekick) (libraries (containers sequence result - dagon.sat dagon.smt dagon.smtlib dagon.backend - dagon.dimacs)) + sidekick.sat sidekick.smt sidekick.smtlib sidekick.backend + sidekick.dimacs)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -safe-string -color always -open Dagon_util)) + -safe-string -color always -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/main/main.ml b/src/main/main.ml index 22a21ef5..a5a8bd07 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -8,10 +8,10 @@ open CCResult.Infix module E = CCResult module Fmt = CCFormat -module Term = Dagon_smt.Term -module Ast = Dagon_smt.Ast -module Solver = Dagon_smt.Solver -module Process = Dagon_smtlib.Process +module Term = Sidekick_smt.Term +module Ast = Sidekick_smt.Ast +module Solver = Sidekick_smt.Solver +module Process = Sidekick_smtlib.Process type 'a or_error = ('a, string) E.t @@ -34,7 +34,7 @@ let p_progress = ref false let hyps : Ast.term list ref = ref [] -module Dot = Dagon_backend.Dot.Make(Solver.Sat_solver.Proof)(Dagon_backend.Dot.Default(Solver.Sat_solver.Proof)) +module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver.Proof)(Sidekick_backend.Dot.Default(Solver.Sat_solver.Proof)) let check_model _state = let check_clause _c = @@ -43,7 +43,7 @@ let check_model _state = let l = List.map (fun a -> - Dagon_sat.Log.debugf 99 + Sidekick_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 @@ -98,7 +98,7 @@ let argspec = Arg.align [ "-no-p", Arg.Clear p_progress, " no progress bar"; "-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 Dagon_sat.Log.set_debug, " sets the debug verbose level"; + "-v", Arg.Int Sidekick_sat.Log.set_debug, " sets the debug verbose level"; ] type syntax = @@ -122,19 +122,19 @@ let main () = let solver = let theories = match syn with | Dimacs -> - [Dagon_th_bool.th] + [Sidekick_th_bool.th] | Smtlib -> - [Dagon_th_bool.th] (* TODO: more theories *) + [Sidekick_th_bool.th] (* TODO: more theories *) in - Dagon_smt.Solver.create ~theories () + Sidekick_smt.Solver.create ~theories () in let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in begin match syn with | Smtlib -> (* parse pb *) - Dagon_smtlib.parse !file + Sidekick_smtlib.parse !file | Dimacs -> - Dagon_dimacs.parse !file >|= fun cs -> + Sidekick_dimacs.parse !file >|= fun cs -> List.rev_append (List.rev_map (fun c -> Ast.Assert_bool c) cs) [Ast.CheckSat] @@ -155,7 +155,7 @@ let main () = E.return() in if !p_stat then ( - Format.printf "%a@." Dagon_smt.Solver.pp_stats solver; + Format.printf "%a@." Sidekick_smt.Solver.pp_stats solver; ); if !p_gc_stat then ( Printf.printf "(gc_stats\n%t)\n" Gc.print_stat; diff --git a/src/main_test/jbuild b/src/main_test/jbuild index b5000f9d..7ec5a8eb 100644 --- a/src/main_test/jbuild +++ b/src/main_test/jbuild @@ -2,8 +2,8 @@ (executable ((name main_test) - (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)) + (libraries (sidekick_sat sidekick.backend sidekick.th_sat dolmen)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/sat/Dagon_sat.ml b/src/sat/Sidekick_sat.ml similarity index 100% rename from src/sat/Dagon_sat.ml rename to src/sat/Sidekick_sat.ml diff --git a/src/sat/Dagon_sat.mld b/src/sat/Sidekick_sat.mld similarity index 100% rename from src/sat/Dagon_sat.mld rename to src/sat/Sidekick_sat.mld diff --git a/src/sat/jbuild b/src/sat/jbuild index 3e9f5b90..102c2661 100644 --- a/src/sat/jbuild +++ b/src/sat/jbuild @@ -1,12 +1,12 @@ ; vim:ft=lisp: (library - ((name Dagon_sat) - (public_name dagon.sat) - (synopsis "core SAT solver for Dagon") - (libraries (dagon.util)) + ((name Sidekick_sat) + (public_name sidekick.sat) + (synopsis "core SAT solver for Sidekick") + (libraries (sidekick.util)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -color always -safe-string -open Dagon_util)) + -color always -safe-string -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index a5c8753c..92f15484 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -1,6 +1,6 @@ -module Vec = Dagon_sat.Vec -module Log = Dagon_sat.Log +module Vec = Sidekick_sat.Vec +module Log = Sidekick_sat.Log open Solver_types type node = Equiv_class.t diff --git a/src/smt/Lit.ml b/src/smt/Lit.ml index 0b3f35ce..ed1e1890 100644 --- a/src/smt/Lit.ml +++ b/src/smt/Lit.ml @@ -53,7 +53,7 @@ let pp = pp_lit let print = pp let norm l = - if l.lit_sign then l, Dagon_sat.Same_sign else neg l, Dagon_sat.Negated + if l.lit_sign then l, Sidekick_sat.Same_sign else neg l, Sidekick_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) diff --git a/src/smt/Lit.mli b/src/smt/Lit.mli index d0569339..f877b444 100644 --- a/src/smt/Lit.mli +++ b/src/smt/Lit.mli @@ -28,7 +28,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 * Dagon_sat.negated +val norm : t -> t * Sidekick_sat.negated module Set : CCSet.S with type elt = t module Tbl : CCHashtbl.S with type key = t diff --git a/src/smt/Model.ml b/src/smt/Model.ml index 4b82c068..b3ae3171 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -162,7 +162,7 @@ let equal_as_values (_:A.term) (_:A.term) : partial_eq = @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 = - Dagon_sat.Log.debugf 5 + Sidekick_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); diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 3c769653..332a2a8b 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -11,7 +11,7 @@ let get_time : unit -> float = Sys.time type level = int -module Sat_solver = Dagon_sat.Make(Theory_combine) +module Sat_solver = Sidekick_sat.Make(Theory_combine) let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t = Sat_solver.Clause.atoms c @@ -407,14 +407,14 @@ type unsat_core = Sat.clause list let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res = let r = Sat_solver.solve ~assumptions (solver self) () in match r with - | Sat_solver.Sat (Dagon_sat.Sat_state _st) -> + | Sat_solver.Sat (Sidekick_sat.Sat_state _st) -> Log.debugf 0 (fun k->k "SAT"); Unknown U_incomplete (* TODO *) (* let env = Ast.env_empty in let m = Model.make ~env Sat m *) - | Sat_solver.Unsat (Dagon_sat.Unsat_state us) -> + | Sat_solver.Unsat (Sidekick_sat.Unsat_state us) -> let pr = us.get_proof () in Unsat pr diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index 652abed9..39c2a66f 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -5,7 +5,7 @@ The solving algorithm, based on MCSat *) -module Sat_solver : Dagon_sat.S +module Sat_solver : Sidekick_sat.S with type formula = Lit.t and type theory = Theory_combine.t and type Proof.lemma = Theory_combine.proof diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index e720b1b8..e345ce19 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -3,7 +3,7 @@ (** Combine the congruence closure with a number of plugins *) -module Sat_solver = Dagon_sat +module Sat_solver = Sidekick_sat open Solver_types module Proof = struct diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index 1ff40d89..72d83002 100644 --- a/src/smt/Theory_combine.mli +++ b/src/smt/Theory_combine.mli @@ -7,7 +7,7 @@ module Proof : sig type t = Proof end -include Dagon_sat.Theory_intf.S +include Sidekick_sat.Theory_intf.S with type formula = Lit.t and type proof = Proof.t diff --git a/src/smt/jbuild b/src/smt/jbuild index 322736dc..928bcb10 100644 --- a/src/smt/jbuild +++ b/src/smt/jbuild @@ -1,10 +1,10 @@ ; vim:ft=lisp: (library - ((name Dagon_smt) - (public_name dagon.smt) - (libraries (containers containers.data sequence dagon.util dagon.sat zarith)) + ((name Sidekick_smt) + (public_name sidekick.smt) + (libraries (containers containers.data sequence sidekick.util sidekick.sat zarith)) (flags (:standard -w +a-4-44-48-58-60@8 - -color always -safe-string -short-paths -open Dagon_util)) + -color always -safe-string -short-paths -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)))) diff --git a/src/smt/th_bool/Dagon_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml similarity index 99% rename from src/smt/th_bool/Dagon_th_bool.ml rename to src/smt/th_bool/Sidekick_th_bool.ml index 7af479d2..a1521407 100644 --- a/src/smt/th_bool/Dagon_th_bool.ml +++ b/src/smt/th_bool/Sidekick_th_bool.ml @@ -1,7 +1,7 @@ (** {1 Theory of Booleans} *) -open Dagon_smt +open Sidekick_smt module Fmt = CCFormat diff --git a/src/smt/th_bool/Dagon_th_bool.mli b/src/smt/th_bool/Sidekick_th_bool.mli similarity index 96% rename from src/smt/th_bool/Dagon_th_bool.mli rename to src/smt/th_bool/Sidekick_th_bool.mli index 51e58086..64575a92 100644 --- a/src/smt/th_bool/Dagon_th_bool.mli +++ b/src/smt/th_bool/Sidekick_th_bool.mli @@ -1,7 +1,7 @@ (** {1 Theory of Booleans} *) -open Dagon_smt +open Sidekick_smt type term = Term.t @@ -45,4 +45,4 @@ module Lit : sig val neq : Term.state -> term -> term -> t end -val th : Dagon_smt.Theory.t +val th : Sidekick_smt.Theory.t diff --git a/src/smt/th_bool/jbuild b/src/smt/th_bool/jbuild index 976ae248..73c5e85d 100644 --- a/src/smt/th_bool/jbuild +++ b/src/smt/th_bool/jbuild @@ -1,10 +1,10 @@ ; vim:ft=lisp: (library - ((name Dagon_th_bool) - (public_name dagon.smt.th_bool) - (libraries (containers dagon.smt)) + ((name Sidekick_th_bool) + (public_name sidekick.smt.th_bool) + (libraries (containers sidekick.smt)) (flags (:standard -w +a-4-44-48-58-60@8 - -color always -safe-string -short-paths -open Dagon_util)) + -color always -safe-string -short-paths -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)))) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index aa05e71d..21e999b0 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -1,13 +1,13 @@ (** {2 Conversion into {!Term.t}} *) -open Dagon_smt +open Sidekick_smt type 'a or_error = ('a, string) CCResult.t module E = CCResult module A = Ast -module Form = Dagon_th_bool +module Form = Sidekick_th_bool module Fmt = CCFormat module Subst = struct diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 9c5bc346..978cc1b2 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -1,7 +1,7 @@ (** {1 Process Statements} *) -open Dagon_smt +open Sidekick_smt type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Dagon_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml similarity index 97% rename from src/smtlib/Dagon_smtlib.ml rename to src/smtlib/Sidekick_smtlib.ml index a5fa6fe8..4ce7e17e 100644 --- a/src/smtlib/Dagon_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -2,7 +2,7 @@ (** {1 Process Statements} *) module Fmt = CCFormat -module Ast = Dagon_smt.Ast +module Ast = Sidekick_smt.Ast module E = CCResult module Loc = Locations module Process = Process diff --git a/src/smtlib/Dagon_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli similarity index 91% rename from src/smtlib/Dagon_smtlib.mli rename to src/smtlib/Sidekick_smtlib.mli index f2e027ea..aea16d17 100644 --- a/src/smtlib/Dagon_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -7,7 +7,7 @@ type 'a or_error = ('a, string) CCResult.t -module Ast = Dagon_smt.Ast +module Ast = Sidekick_smt.Ast module Process = Process val parse : string -> Ast.statement list or_error diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index f1f05c71..e9c9804b 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -6,7 +6,7 @@ module Loc = Locations module Fmt = CCFormat -module A = Dagon_smt.Ast +module A = Sidekick_smt.Ast module PA = Parse_ast type 'a or_error = ('a, string) CCResult.t @@ -314,7 +314,7 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with 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); + Sidekick_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 diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index cbbf74a8..9c295dfa 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -16,7 +16,7 @@ module Ctx : sig end module PA = Parse_ast -module A = Dagon_smt.Ast +module A = Sidekick_smt.Ast val conv_term : Ctx.t -> PA.term -> A.term diff --git a/src/smtlib/jbuild b/src/smtlib/jbuild index 0797cd0e..810b5e93 100644 --- a/src/smtlib/jbuild +++ b/src/smtlib/jbuild @@ -4,12 +4,12 @@ ; main binary (library - ((name dagon_smtlib) - (public_name dagon.smtlib) + ((name sidekick_smtlib) + (public_name sidekick.smtlib) (optional) ; only if deps present - (libraries (containers dagon.smt dagon.util dagon.smt.th_bool zarith)) + (libraries (containers sidekick.smt sidekick.util sidekick.smt.th_bool zarith)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 - -safe-string -color always -open Dagon_util)) + -safe-string -color always -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -color always -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/th_sat/Dagon_th_sat.ml b/src/th_sat/Sidekick_th_sat.ml similarity index 100% rename from src/th_sat/Dagon_th_sat.ml rename to src/th_sat/Sidekick_th_sat.ml diff --git a/src/th_sat/Dagon_th_sat.mli b/src/th_sat/Sidekick_th_sat.mli similarity index 87% rename from src/th_sat/Dagon_th_sat.mli rename to src/th_sat/Sidekick_th_sat.mli index a9f72702..cdd20ab8 100644 --- a/src/th_sat/Dagon_th_sat.mli +++ b/src/th_sat/Sidekick_th_sat.mli @@ -11,6 +11,6 @@ Copyright 2016 Guillaume Bury module Th = Th_sat -include module type of Dagon_sat.Make(Th) +include module type of Sidekick_sat.Make(Th) (** A functor that can generate as many solvers as needed. *) diff --git a/src/th_sat/jbuild b/src/th_sat/jbuild index 63e3f05f..f1b21eb0 100644 --- a/src/th_sat/jbuild +++ b/src/th_sat/jbuild @@ -1,9 +1,9 @@ ; vim:ft=lisp: (library - ((name Dagon_th_sat) - (public_name dagon.th_sat) - (libraries (dagon.sat cdcl.tseitin)) + ((name Sidekick_th_sat) + (public_name sidekick.th_sat) + (libraries (sidekick.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 diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild index a3e3208a..29c01d08 100644 --- a/src/tseitin/jbuild +++ b/src/tseitin/jbuild @@ -2,7 +2,7 @@ (library ((name CDCL_tseitin) - (public_name dagon.tseitin) + (public_name sidekick.tseitin) (synopsis "Tseitin transformation for CDCL") (libraries ()) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) diff --git a/src/util/jbuild b/src/util/jbuild index fb3f9256..66c487fa 100644 --- a/src/util/jbuild +++ b/src/util/jbuild @@ -1,6 +1,6 @@ (library - ((name dagon_util) - (public_name dagon.util) + ((name sidekick_util) + (public_name sidekick.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