From 19d65b406989927bd7b5425b74bf50d09021d2c3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 6 Jun 2019 10:45:09 -0500 Subject: [PATCH] remove dimacs stuff --- src/dimacs/Lexer.mll | 22 ----------------- src/dimacs/Parser.mly | 43 ---------------------------------- src/dimacs/Sidekick_dimacs.ml | 15 ------------ src/dimacs/Sidekick_dimacs.mli | 13 ---------- src/dimacs/dune | 14 ----------- src/main/dune | 22 ++++++++--------- src/main/main.ml | 30 ++++-------------------- src/smtlib/Ast.ml | 4 +--- src/smtlib/Ast.mli | 1 - src/smtlib/Process.ml | 12 ---------- 10 files changed, 15 insertions(+), 161 deletions(-) delete mode 100644 src/dimacs/Lexer.mll delete mode 100644 src/dimacs/Parser.mly delete mode 100644 src/dimacs/Sidekick_dimacs.ml delete mode 100644 src/dimacs/Sidekick_dimacs.mli delete mode 100644 src/dimacs/dune diff --git a/src/dimacs/Lexer.mll b/src/dimacs/Lexer.mll deleted file mode 100644 index f1b2ce31..00000000 --- a/src/dimacs/Lexer.mll +++ /dev/null @@ -1,22 +0,0 @@ -(* Copyright 2005 INRIA *) -{ - open Sidekick_util - open Parser -} - -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)) } - | _ { Error.errorf "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/dimacs/Parser.mly b/src/dimacs/Parser.mly deleted file mode 100644 index 80da0670..00000000 --- a/src/dimacs/Parser.mly +++ /dev/null @@ -1,43 +0,0 @@ -/* Copyright 2005 INRIA */ - -%{ - open Sidekick_util - - 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 { () } - | error - { - Error.errorf "expected prelude %a" pp_pos ($startpos,$endpos) - } - -clauses: - | l=clause* { l } - | error - { - Error.errorf "expected list of clauses %a" - pp_pos ($startpos,$endpos) - } - -file: - | prelude l=clauses EOF { l } - -clause: - | l=LIT+ ZERO { l } diff --git a/src/dimacs/Sidekick_dimacs.ml b/src/dimacs/Sidekick_dimacs.ml deleted file mode 100644 index a8adc4f0..00000000 --- a/src/dimacs/Sidekick_dimacs.ml +++ /dev/null @@ -1,15 +0,0 @@ - -(** {1 Main for dimacs} *) - -type 'a or_error = ('a, string) CCResult.t - -let parse file : int list list or_error = - try - CCIO.with_in file - (fun ic -> - let lexbuf = Lexing.from_channel ic in - Parser.file Lexer.token lexbuf) - |> CCResult.return - with e -> - CCResult.of_exn_trace e - diff --git a/src/dimacs/Sidekick_dimacs.mli b/src/dimacs/Sidekick_dimacs.mli deleted file mode 100644 index e57e16e1..00000000 --- a/src/dimacs/Sidekick_dimacs.mli +++ /dev/null @@ -1,13 +0,0 @@ - -(** {1 Main for dimacs} *) - -(** This library provides a parser for DIMACS files, to represent - SAT problems. - - http://www.satcompetition.org/2009/format-benchmarks2009.html -*) - -type 'a or_error = ('a, string) CCResult.t - -val parse : string -> int list list or_error -(** Parse a file into a list of clauses. *) diff --git a/src/dimacs/dune b/src/dimacs/dune deleted file mode 100644 index 006975c2..00000000 --- a/src/dimacs/dune +++ /dev/null @@ -1,14 +0,0 @@ - -; main binary -(library - (name sidekick_dimacs) - (public_name sidekick.dimacs) - (optional) ; only if deps present - (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) - ) - -(menhir (modules Parser)) -(ocamllex (modules Lexer)) diff --git a/src/main/dune b/src/main/dune index 3dbe68e6..5c45b6cf 100644 --- a/src/main/dune +++ b/src/main/dune @@ -1,14 +1,12 @@ - ; main binary -(executable - (name main) - (public_name sidekick) - (package sidekick) - (libraries containers iter result msat sidekick.core - sidekick.base-term sidekick.msat-solver sidekick.smtlib sidekick.dimacs) - (flags :standard -w +a-4-42-44-48-50-58-32-60@8 - -safe-string -color always -open Sidekick_util) - (ocamlopt_flags :standard -O3 -color always - -unbox-closures -unbox-closures-factor 20) - ) +(executable + (name main) + (public_name sidekick) + (package sidekick) + (libraries containers iter result msat sidekick.core sidekick.base-term + sidekick.msat-solver sidekick.smtlib) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -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 59c33d5f..bb795e03 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -82,14 +82,6 @@ let argspec = Arg.align [ "-v", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; ] -type syntax = - | Dimacs - | Smtlib - -let syntax_of_file file = - if CCString.suffix ~suf:".cnf" file then Dimacs - else Smtlib - (* Limits alarm *) let check_limits () = let t = Sys.time () in @@ -109,31 +101,17 @@ let main () = exit 2 ); let al = Gc.create_alarm check_limits in - let syn = syntax_of_file !file in Util.setup_gc(); let tst = Term.create ~size:4_096 () in let solver = - let theories = match syn with - | Dimacs -> - [Process.th_bool ] - | Smtlib -> - [Process.th_bool ; - ] (* TODO: more theories *) + let theories = [ + Process.th_bool ; + ] (* TODO: more theories *) in Process.Solver.create ~store_proof:!check ~theories tst () in let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in - begin match syn with - | Smtlib -> - (* parse pb *) - Sidekick_smtlib.parse !file - | Dimacs -> - Sidekick_dimacs.parse !file >|= fun cs -> - List.rev_append - (List.rev_map (fun c -> Ast.Assert_bool c) cs) - [Ast.CheckSat] - end - >>= fun input -> + Sidekick_smtlib.parse !file >>= fun input -> (* process statements *) let res = try diff --git a/src/smtlib/Ast.ml b/src/smtlib/Ast.ml index 8a1bfe39..46f44c56 100644 --- a/src/smtlib/Ast.ml +++ b/src/smtlib/Ast.ml @@ -160,7 +160,6 @@ type statement = | Decl of ID.t * Ty.t | Define of definition list | Assert of term - | Assert_bool of int list | Goal of var list * term | CheckSat | Exit @@ -437,7 +436,6 @@ let pp_statement out = function Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])" ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t - | Assert_bool l -> Fmt.fprintf out "(@[assert-bool@ %a@])" (Util.pp_list Fmt.int) l | Goal (vars,g) -> Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g)) | Exit -> Fmt.string out "(exit)" @@ -481,7 +479,7 @@ let env_add_statement env st = List.fold_left (fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map) env l - | Goal _ | Assert _ | Assert_bool _ | CheckSat | Exit + | Goal _ | Assert _ | CheckSat | Exit | SetLogic _ | SetOption _ | SetInfo _ -> env diff --git a/src/smtlib/Ast.mli b/src/smtlib/Ast.mli index 5e71174d..e2574826 100644 --- a/src/smtlib/Ast.mli +++ b/src/smtlib/Ast.mli @@ -130,7 +130,6 @@ type statement = | Decl of ID.t * Ty.t | Define of definition list | Assert of term - | Assert_bool of int list | Goal of var list * term | CheckSat | Exit diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index f3118500..81034575 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -510,13 +510,6 @@ let solve (* NOTE: hack for testing with dimacs. Proper treatment should go into scoping in Ast, or having theory-specific state in `Term.state` *) -let mk_iatom = - let tbl = Util.Int_tbl.create 6 in (* for atoms *) - fun tst i -> - let c = Util.Int_tbl.get_or_add tbl ~k:(abs i) - ~f:(fun i -> Fun.mk_undef_const (ID.makef "a_%d" i) Ty.bool) in - Lit.atom tst ~sign:(i>0) @@ Term.const tst c - (* process a single statement *) let process_stmt ?hyps @@ -573,11 +566,6 @@ let process_stmt CCOpt.iter (fun h -> Vec.push h [atom]) hyps; Solver.add_clause_lits solver (IArray.singleton atom); E.return() - | A.Assert_bool l -> - let c = List.rev_map (mk_iatom tst) l in - CCOpt.iter (fun h -> Vec.push h c) hyps; - Solver.add_clause_lits_l solver c; - E.return () | A.Goal (_, _) -> Error.errorf "cannot deal with goals yet" | A.Data _ ->