From d73684902f41070d1084d6cfee94e70bb0916816 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 5 Feb 2018 23:09:13 -0600 Subject: [PATCH] wip: have a proper smtlib parser --- Makefile | 32 +- README.md | 17 +- TODO.md | 4 +- cdcl.opam | 25 - dagon.opam | 25 + main.exe | 2 +- src/backend/jbuild | 10 +- src/main/jbuild | 17 + src/main/main.ml | 183 +++++++ src/main_test/jbuild | 4 +- src/{core/CDCL.ml => sat/Dagon_sat.ml} | 0 src/{core/CDCL.mld => sat/Dagon_sat.mld} | 0 src/{core => sat}/Internal.ml | 0 src/{core => sat}/Res.ml | 0 src/{core => sat}/Res.mli | 0 src/{core => sat}/Res_intf.ml | 0 src/{core => sat}/Solver.ml | 0 src/{core => sat}/Solver.mli | 0 src/{core => sat}/Solver_intf.ml | 0 src/{core => sat}/Solver_types.ml | 0 src/{core => sat}/Solver_types.mli | 0 src/{core => sat}/Solver_types_intf.ml | 0 src/{core => sat}/Theory_intf.ml | 0 src/sat/jbuild | 13 +- src/smt/Ast.ml | 272 ++++++++--- src/smt/Ast.mli | 58 ++- src/smt/Congruence_closure.ml | 3 +- src/smt/Explanation.ml | 1 - src/smt/Lit.ml | 2 +- src/smt/Lit.mli | 3 +- src/smt/Model.ml | 154 +++--- src/smt/Solver.ml | 28 +- src/smt/Solver.mli | 22 +- src/smt/Solver_types.ml | 2 - src/smt/Term.mli | 1 - src/smt/Theory.ml | 2 - src/smt/Theory_combine.ml | 47 +- src/smt/Theory_combine.mli | 2 +- src/smt/Ty.ml | 1 - src/smt/Ty.mli | 2 - src/smt/Ty_card.mli | 2 - src/smt/jbuild | 9 +- src/smtlib/Convert.ml | 455 +++++++++++++++++ src/smtlib/Convert.mli | 24 + src/smtlib/Dagon_smtlib.ml | 456 ++++++++++++++++++ src/smtlib/Dagon_smtlib.mli | 34 ++ src/smtlib/Lexer.mll | 95 ++++ src/smtlib/Locations.ml | 71 +++ src/smtlib/Parse_ast.ml | 294 +++++++++++ src/smtlib/Parser.mly | 377 +++++++++++++++ src/smtlib/jbuild | 21 + .../CDCL_sat.ml => th_sat/Dagon_th_sat.ml} | 2 +- .../CDCL_sat.mli => th_sat/Dagon_th_sat.mli} | 2 +- src/{sat => th_sat}/Th_sat.ml | 0 src/{sat => th_sat}/Th_sat.mli | 0 src/th_sat/jbuild | 13 + src/tseitin/jbuild | 2 +- src/{core => util}/BitField.ml | 0 src/{core => util}/BitField.mli | 0 src/{core => util}/Heap.ml | 0 src/{core => util}/Heap.mli | 0 src/{core => util}/Heap_intf.ml | 0 src/{smt => util}/IArray.ml | 0 src/{smt => util}/IArray.mli | 0 src/{smt => util}/ID.ml | 5 + src/{smt => util}/ID.mli | 9 + src/{smt => util}/Intf.ml | 0 src/{core => util}/Log.ml | 0 src/{core => util}/Log.mli | 0 src/{smt => util}/Util.ml | 7 + src/{smt => util}/Util.mli | 3 + src/{core => util}/Vec.ml | 0 src/{core => util}/Vec.mli | 0 src/{core => util}/jbuild | 11 +- tests/jbuild | 2 +- 75 files changed, 2490 insertions(+), 336 deletions(-) delete mode 100644 cdcl.opam create mode 100644 dagon.opam create mode 100644 src/main/jbuild create mode 100644 src/main/main.ml rename src/{core/CDCL.ml => sat/Dagon_sat.ml} (100%) rename src/{core/CDCL.mld => sat/Dagon_sat.mld} (100%) rename src/{core => sat}/Internal.ml (100%) rename src/{core => sat}/Res.ml (100%) rename src/{core => sat}/Res.mli (100%) rename src/{core => sat}/Res_intf.ml (100%) rename src/{core => sat}/Solver.ml (100%) rename src/{core => sat}/Solver.mli (100%) rename src/{core => sat}/Solver_intf.ml (100%) rename src/{core => sat}/Solver_types.ml (100%) rename src/{core => sat}/Solver_types.mli (100%) rename src/{core => sat}/Solver_types_intf.ml (100%) rename src/{core => sat}/Theory_intf.ml (100%) create mode 100644 src/smtlib/Convert.ml create mode 100644 src/smtlib/Convert.mli create mode 100644 src/smtlib/Dagon_smtlib.ml create mode 100644 src/smtlib/Dagon_smtlib.mli create mode 100644 src/smtlib/Lexer.mll create mode 100644 src/smtlib/Locations.ml create mode 100644 src/smtlib/Parse_ast.ml create mode 100644 src/smtlib/Parser.mly create mode 100644 src/smtlib/jbuild rename src/{sat/CDCL_sat.ml => th_sat/Dagon_th_sat.ml} (82%) rename src/{sat/CDCL_sat.mli => th_sat/Dagon_th_sat.mli} (87%) rename src/{sat => th_sat}/Th_sat.ml (100%) rename src/{sat => th_sat}/Th_sat.mli (100%) create mode 100644 src/th_sat/jbuild rename src/{core => util}/BitField.ml (100%) rename src/{core => util}/BitField.mli (100%) rename src/{core => util}/Heap.ml (100%) rename src/{core => util}/Heap.mli (100%) rename src/{core => util}/Heap_intf.ml (100%) rename src/{smt => util}/IArray.ml (100%) rename src/{smt => util}/IArray.mli (100%) rename src/{smt => util}/ID.ml (92%) rename src/{smt => util}/ID.mli (91%) rename src/{smt => util}/Intf.ml (100%) rename src/{core => util}/Log.ml (100%) rename src/{core => util}/Log.mli (100%) rename src/{smt => util}/Util.ml (78%) rename src/{smt => util}/Util.mli (90%) rename src/{core => util}/Vec.ml (100%) rename src/{core => util}/Vec.mli (100%) rename src/{core => util}/jbuild (59%) diff --git a/Makefile b/Makefile index ad91e0a6..7f69cdbf 100644 --- a/Makefile +++ b/Makefile @@ -1,36 +1,22 @@ # copyright (c) 2014, guillaume bury # copyright (c) 2017, simon cruanes -BIN=main.native -TEST_BIN=tests/test_api.native +.PHONY: clean build build-dev NAME=msat J?=3 TIMEOUT?=30 -TARGETS=src/bin/main.exe +TARGETS=src/main/main.exe OPTS= -j $(J) -LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) - -all: build test -all-dev: build-dev test - build: - jbuilder build $(OPTS) @install + jbuilder build $(TARGETS) $(OPTS) + +build-install: + jbuilder build @install build-dev: - jbuilder build $(OPTS) @install --dev - -build-test: build - jbuilder build $(OPTS) src/main_test/main_test.exe - -test: build-test - @echo "run API tests…" - jbuilder runtest - @echo "run benchmarks…" - @/usr/bin/time -f "%e" ./tests/run sat - #@/usr/bin/time -f "%e" ./tests/run smt - # @/usr/bin/time -f "%e" ./tests/run mcsat + jbuilder build $(TARGETS) $(OPTS) --dev enable_log: cd src/core; ln -sf log_real.ml log.ml @@ -63,9 +49,9 @@ reindent: ocp-indent @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i -WATCH=all +WATCH=build watch: - while find src/ tests/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ echo "============ at `date` ==========" ; \ make $(WATCH); \ done diff --git a/README.md b/README.md index 3e7332de..9e4bc0b5 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -# CDCL [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL) +# dagon [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL) -CDCL is an OCaml library with a functor to create SMT solvers following +Dagon 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/cdcl/ +See https://c-cube.github.io/dagon/ ## Installation ### Via opam -Once the package is on [opam](http://opam.ocaml.org), just `opam install cdcl`. +Once the package is on [opam](http://opam.ocaml.org), just `opam install dagon`. For the development version, use: - opam pin add msat https://github.com/c-cube/cdcl.git + opam pin add dagon https://github.com/c-cube/dagon.git ### Manual installation @@ -26,13 +26,6 @@ You will need jbuilder. The command is: make install -## Usage - -The main module is `CDCL`. - -A modular implementation of the SMT algorithm can be found in the `CDCL.Make` functor, -as a functor which takes a `Theory_intf.S` module - ## Copyright This program is distributed under the Apache Software License version diff --git a/TODO.md b/TODO.md index 060fdf6e..2456a1cf 100644 --- a/TODO.md +++ b/TODO.md @@ -2,7 +2,7 @@ ## TODO -- typing and translation Ast -> Term +- typing and translation Ast -> Term (from mc2?) - main executable for SMT solver - theory of boolean constructs (on the fly Tseitin using local clauses) - make CC work on QF_UF @@ -10,6 +10,8 @@ * basic notion of activity for `ite`? - have `CDCL.push_local` work properly +- remove tseitin lib + - write Shostak theory of datatypes (without acyclicity) with local case splits - design evaluation system (guards + `eval_bool:(term -> bool) option` in custom TC) - compilation of rec functions to defined constants diff --git a/cdcl.opam b/cdcl.opam deleted file mode 100644 index 7510703c..00000000 --- a/cdcl.opam +++ /dev/null @@ -1,25 +0,0 @@ -opam-version: "1.2" -name: "cdcl" -license: "Apache" -version: "dev" -author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] -maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: ["jbuilder" "build" "@install" "-p" name] -build-doc: ["jbuilder" "build" "@doc" "-p" name] -install: ["jbuilder" "install" name] -remove: ["jbuilder" "uninstall" name] -depends: [ - "ocamlfind" {build} - "jbuilder" {build} -] -depopts: [ - "dolmen" -] -available: [ - ocaml-version >= "4.03.0" -] -tags: [ "sat" "smt" ] -homepage: "https://github.com/c-cube/cdcl" -dev-repo: "https://github.com/c-cube/cdcl.git" -bug-reports: "https://github.com/c-cube/cdcl/issues/" - diff --git a/dagon.opam b/dagon.opam new file mode 100644 index 00000000..b15a6c00 --- /dev/null +++ b/dagon.opam @@ -0,0 +1,25 @@ +opam-version: "1.2" +name: "dagon" +license: "Apache" +version: "dev" +author: ["Simon Cruanes" "Guillaume Bury" "Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer"] +maintainer: ["simon.cruanes.2007@m4x.org"] +build: ["jbuilder" "build" "@install" "-p" name] +build-doc: ["jbuilder" "build" "@doc" "-p" name] +depends: [ + "ocamlfind" {build} + "jbuilder" {build} + "containers" + "sequence" +] +depopts: [ + "dolmen" +] +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/" + diff --git a/main.exe b/main.exe index 25e5011f..cceb9ac3 120000 --- a/main.exe +++ b/main.exe @@ -1 +1 @@ -_build/default/src/main_test/main_test.exe \ No newline at end of file +_build/default/src/main/main.exe \ No newline at end of file diff --git a/src/backend/jbuild b/src/backend/jbuild index f0d1cae6..67043e55 100644 --- a/src/backend/jbuild +++ b/src/backend/jbuild @@ -2,11 +2,11 @@ ; main binary (library - ((name CDCL_backend) - (public_name cdcl.backend) - (synopsis "proof backends for cdcl") - (libraries (cdcl)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) + ((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)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/main/jbuild b/src/main/jbuild new file mode 100644 index 00000000..a621ea0d --- /dev/null +++ b/src/main/jbuild @@ -0,0 +1,17 @@ +; vim:ft=lisp: + +(jbuild_version 1) + +; main binary +(executable + ((name main) + (public_name dagon) + (package dagon) + (libraries (containers sequence result + dagon.sat dagon.smt dagon.smtlib dagon.backend)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 + -safe-string -color always -open Dagon_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 new file mode 100644 index 00000000..6122d918 --- /dev/null +++ b/src/main/main.ml @@ -0,0 +1,183 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +open CCResult.Infix + +module E = CCResult +module Fmt = CCFormat +module Term = Dagon_smt.Term +module Ast = Dagon_smt.Ast + +type 'a or_error = ('a, string) E.t + +exception Out_of_time +exception Out_of_space + +let file = ref "" +let p_cnf = ref false +let p_dot_proof = ref "" +let p_proof_print = ref false +let p_model = ref false +let check = ref true +let time_limit = ref 300. +let size_limit = ref 1000_000_000. +let restarts = ref true +let gc = ref true +let p_stat = ref false +let p_gc_stat = ref false +let p_progress = ref false + +(* FIXME +module Dot = CDCL_backend.Dot.Make(CDCL_backend.Dot.Default(Sat)) + *) + +let hyps : Ast.term list ref = ref [] + +let check_model _state = + let check_clause _c = + true + (* FIXME + let l = + List.map + (fun a -> + Dagon_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 + in + List.exists (fun x -> x) l + *) + in + let l = List.map check_clause !hyps in + List.for_all (fun x -> x) l + +(* 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 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 check, " build, check and print the proof (if output is set), if unsat"; + "-no-check", Arg.Clear check, " inverse of -check"; + "-gc", Arg.Set gc, " enable garbage collection"; + "-no-gc", Arg.Clear gc, " disable garbage collection"; + "-restarts", Arg.Set restarts, " enable restarts"; + "-no-restarts", Arg.Clear restarts, " disable restarts"; + "-dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file"; + "-stat", Arg.Set p_stat, " print statistics"; + "-model", Arg.Set p_model, " print model"; + "-no-model", Arg.Clear p_model, " do not print model"; + "-gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC"; + "-p", Arg.Set p_progress, " print progress bar"; + "-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"; + ] + +type syntax = + | Dimacs + | Smtlib + +let syntax_of_file file = + if CCString.suffix ~suf:".cnf" file then Dimacs + else Smtlib + +let main () = + CCFormat.set_color_default true; + (* Administrative duties *) + Arg.parse argspec input_file usage; + if !file = "" then ( + Arg.usage argspec usage; + exit 2 + ); + let syn = syntax_of_file !file in + Util.setup_gc(); + let solver = + let theories = match syn with + | Dimacs -> [] + | Smtlib -> + [] (* TODO: more theories *) + in + Dagon_smt.Solver.create ~theories () + in + let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in + let res = match syn with + | Smtlib -> + (* parse pb *) + Dagon_smtlib.parse !file >>= fun input -> + (* TODO: parse list of plugins on CLI *) + (* process statements *) + begin + try + E.fold_l + (fun () -> + Dagon_smtlib.process_stmt + ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf + ~time:!time_limit ~memory:!size_limit + ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress + solver) + () input + with Exit -> + E.return() + end + | Dimacs -> + assert false (* TODO *) + in + if !p_stat then ( + Format.printf "%a@." Dagon_smt.Solver.pp_stats solver; + ); + if !p_gc_stat then ( + Printf.printf "(gc_stats\n%t)\n" Gc.print_stat; + ); + res + +let () = match main() with + | E.Ok () -> () + | E.Error msg -> + print_endline msg; + exit 1 + | exception e -> + let b = Printexc.get_backtrace () in + begin match e with + | Util.Error msg -> + print_endline msg; + ignore @@ exit 1 + | Out_of_time -> + Format.printf "Timeout@."; + exit 2 + | Out_of_space -> + Format.printf "Spaceout@."; + exit 3 + | _ -> raise e + end; + if Printexc.backtrace_status () then ( + Format.fprintf Format.std_formatter "%s@." b + ) + diff --git a/src/main_test/jbuild b/src/main_test/jbuild index 11b6586f..b5000f9d 100644 --- a/src/main_test/jbuild +++ b/src/main_test/jbuild @@ -2,8 +2,8 @@ (executable ((name main_test) - (libraries (cdcl cdcl.backend cdcl.tseitin cdcl.sat dolmen)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) + (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)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/core/CDCL.ml b/src/sat/Dagon_sat.ml similarity index 100% rename from src/core/CDCL.ml rename to src/sat/Dagon_sat.ml diff --git a/src/core/CDCL.mld b/src/sat/Dagon_sat.mld similarity index 100% rename from src/core/CDCL.mld rename to src/sat/Dagon_sat.mld diff --git a/src/core/Internal.ml b/src/sat/Internal.ml similarity index 100% rename from src/core/Internal.ml rename to src/sat/Internal.ml diff --git a/src/core/Res.ml b/src/sat/Res.ml similarity index 100% rename from src/core/Res.ml rename to src/sat/Res.ml diff --git a/src/core/Res.mli b/src/sat/Res.mli similarity index 100% rename from src/core/Res.mli rename to src/sat/Res.mli diff --git a/src/core/Res_intf.ml b/src/sat/Res_intf.ml similarity index 100% rename from src/core/Res_intf.ml rename to src/sat/Res_intf.ml diff --git a/src/core/Solver.ml b/src/sat/Solver.ml similarity index 100% rename from src/core/Solver.ml rename to src/sat/Solver.ml diff --git a/src/core/Solver.mli b/src/sat/Solver.mli similarity index 100% rename from src/core/Solver.mli rename to src/sat/Solver.mli diff --git a/src/core/Solver_intf.ml b/src/sat/Solver_intf.ml similarity index 100% rename from src/core/Solver_intf.ml rename to src/sat/Solver_intf.ml diff --git a/src/core/Solver_types.ml b/src/sat/Solver_types.ml similarity index 100% rename from src/core/Solver_types.ml rename to src/sat/Solver_types.ml diff --git a/src/core/Solver_types.mli b/src/sat/Solver_types.mli similarity index 100% rename from src/core/Solver_types.mli rename to src/sat/Solver_types.mli diff --git a/src/core/Solver_types_intf.ml b/src/sat/Solver_types_intf.ml similarity index 100% rename from src/core/Solver_types_intf.ml rename to src/sat/Solver_types_intf.ml diff --git a/src/core/Theory_intf.ml b/src/sat/Theory_intf.ml similarity index 100% rename from src/core/Theory_intf.ml rename to src/sat/Theory_intf.ml diff --git a/src/sat/jbuild b/src/sat/jbuild index 7d2cf448..3e9f5b90 100644 --- a/src/sat/jbuild +++ b/src/sat/jbuild @@ -1,13 +1,12 @@ ; vim:ft=lisp: (library - ((name CDCL_sat) - (public_name cdcl.sat) - (libraries (cdcl cdcl.tseitin)) - (synopsis "sat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) + ((name Dagon_sat) + (public_name dagon.sat) + (synopsis "core SAT solver for Dagon") + (libraries (dagon.util)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 + -color always -safe-string -open Dagon_util)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) - - diff --git a/src/smt/Ast.ml b/src/smt/Ast.ml index 71697e11..3e34fbc6 100644 --- a/src/smt/Ast.ml +++ b/src/smt/Ast.ml @@ -4,22 +4,9 @@ (** {1 Preprocessing AST} *) module Fmt = CCFormat -module S = CCSexp type 'a or_error = ('a, string) CCResult.t -exception Error of string -exception Ill_typed of string - -let () = Printexc.register_printer - (function - | Error msg -> Some ("ast error: " ^ msg) - | Ill_typed msg -> Some ("ill-typed: " ^ msg) - | _ -> None) - -let errorf msg = - CCFormat.ksprintf ~f:(fun e -> raise (Error e)) msg - (** {2 Types} *) module Var = struct @@ -43,28 +30,33 @@ end module Ty = struct type t = | Prop - | Const of ID.t + | App of ID.t * t list | Arrow of t * t let prop = Prop - let const id = Const id + let app id l = App (id,l) + let const id = app id [] let arrow a b = Arrow (a,b) let arrow_l = List.fold_right arrow + let int = const ID.B.int + let rat = const ID.B.rat + let to_int_ = function | Prop -> 0 - | Const _ -> 1 + | App _ -> 1 | Arrow _ -> 2 let () = CCOrd.() let rec compare a b = match a, b with | Prop, Prop -> 0 - | Const a, Const b -> ID.compare a b + | App (a,la), App (b,lb) -> + CCOrd.(ID.compare a b (list compare, la, lb)) | Arrow (a1,a2), Arrow (b1,b2) -> compare a1 b1 (compare, a2,b2) | Prop, _ - | Const _, _ + | App _, _ | Arrow _, _ -> CCInt.compare (to_int_ a) (to_int_ b) let equal a b = compare a b = 0 @@ -80,7 +72,8 @@ module Ty = struct let rec pp out = function | Prop -> Fmt.string out "prop" - | Const id -> ID.pp out id + | App (id,[]) -> ID.pp out id + | App (id,l) -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp) l | Arrow _ as ty -> let args, ret = unfold ty in Fmt.fprintf out "(@[-> %a@ %a@])" @@ -93,22 +86,6 @@ module Ty = struct data_cstors: t ID.Map.t; } - (* FIXME - let data_to_sexp d = - let cstors = - ID.Map.fold - (fun c ty acc -> - let ty_args, _ = unfold ty in - let c_sexp = match ty_args with - | [] -> ID.to_sexp c - | _::_ -> S.of_list (ID.to_sexp c :: List.map to_sexp ty_args) - in - c_sexp :: acc) - d.data_cstors [] - in - S.of_list (ID.to_sexp d.data_id :: cstors) - *) - module Map = CCMap.Make(struct type _t = t type t = _t @@ -116,18 +93,27 @@ module Ty = struct end) let ill_typed fmt = - CCFormat.ksprintf - ~f:(fun s -> raise (Ill_typed s)) - fmt + Util.errorf ("ill-typed: " ^^ fmt) end type var = Ty.t Var.t -type binop = +type op = | And | Or | Imply | Eq + | Distinct + +type arith_op = + | Leq + | Lt + | Geq + | Gt + | Add + | Minus + | Mult + | Div type binder = | Fun @@ -142,16 +128,17 @@ type term = { and term_cell = | Var of var | Const of ID.t - | Unknown of var (* meta var *) + | Num_z of Z.t + | Num_q of Q.t | App of term * term list | If of term * term * term - | Select of select * term | Match of term * (var list * term) ID.Map.t - | Switch of term * term ID.Map.t (* switch on constants *) + | Select of select * term | Bind of binder * var * term - | Let of var * term * term + | Arith of arith_op * term list + | Let of (var * term) list * term | Not of term - | Binop of binop * term * term + | Op of op * term list | Asserting of term * term | Undefined_value | Bool of bool @@ -162,32 +149,98 @@ and select = { select_i: int; } + type definition = ID.t * Ty.t * term type statement = + | SetLogic of string + | SetOption of string list + | SetInfo of string list | Data of Ty.data list - | TyDecl of ID.t (* new atomic cstor *) + | TyDecl of ID.t * int (* new atomic cstor *) | Decl of ID.t * Ty.t | Define of definition list | Assert of term | Goal of var list * term + | CheckSat + | Exit -(** {2 Helper} *) +(** {2 Helpers} *) -let unfold_fun t = +let is_true = function {term=Bool true;_} -> true | _ -> false +let is_false = function {term=Bool false;_} -> true | _ -> false + +let unfold_binder b t = let rec aux acc t = match t.term with - | Bind (Fun, v, t') -> aux (v::acc) t' + | Bind (b', v, t') when b=b' -> aux (v::acc) t' | _ -> List.rev acc, t in aux [] t -(* TODO *) +let unfold_fun = unfold_binder Fun -let pp_term out _ = Fmt.string out "todo:term" +let pp_binder out = function + | Forall -> Fmt.string out "forall" + | Exists -> Fmt.string out "exists" + | Fun -> Fmt.string out "lambda" + | Mu -> Fmt.string out "mu" -let pp_ty out _ = Fmt.string out "todo:ty" +let pp_op out = function + | And -> Fmt.string out "and" + | Or -> Fmt.string out "or" + | Imply -> Fmt.string out "=>" + | Eq -> Fmt.string out "=" + | Distinct -> Fmt.string out "distinct" -let pp_statement out _ = Fmt.string out "todo:stmt" +let pp_arith out = function + | Leq -> Fmt.string out "<=" + | Lt -> Fmt.string out "<" + | Geq -> Fmt.string out ">=" + | Gt -> Fmt.string out ">" + | Add -> Fmt.string out "+" + | Minus -> Fmt.string out "-" + | Mult -> Fmt.string out "*" + | Div -> Fmt.string out "/" + +let pp_term = + let rec pp out t = match t.term with + | Var v -> Var.pp out v + | Const id -> ID.pp out id + | App (f, l) -> Fmt.fprintf out "(@[%a@ %a@])" pp f (Util.pp_list pp) l + | If (a,b,c) -> Fmt.fprintf out "(@[ite@ %a@ %a@ %a@])" pp a pp b pp c + | Match (u, m) -> + let pp_case out (id,(vars,rhs)) = + if vars=[] then Fmt.fprintf out "(@[<2>case %a@ %a@])" ID.pp id pp rhs + else Fmt.fprintf out "(@[<2>case (@[%a@ %a@])@ %a@])" + ID.pp id (Util.pp_list Var.pp) vars pp rhs + in + Fmt.fprintf out "(@[match %a@ %a@])" + pp u (Util.pp_list pp_case) (ID.Map.to_list m) + | Select (s, t) -> + Fmt.fprintf out "(@[select_%a_%d@ %a@])" + ID.pp s.select_cstor s.select_i pp t + | Bool b -> Fmt.fprintf out "%B" b + | Not t -> Fmt.fprintf out "(@[<1>not@ %a@])" pp t + | Op (o,l) -> Fmt.fprintf out "(@[%a@ %a@])" pp_op o (Util.pp_list pp) l + | Bind (b,v,u) -> + Fmt.fprintf out "(@[<1>%a ((@[%a@ %a@]))@ %a@])" + pp_binder b Var.pp v Ty.pp (Var.ty v) pp u + | Let (vbs,u) -> + Fmt.fprintf out "(@[<1>let (@[%a@])@ %a@])" pp_vbs vbs pp u + | Num_z z -> Z.pp_print out z + | Num_q z -> Q.pp_print out z + | Arith (op, l) -> + Fmt.fprintf out "(@[%a@ %a@])" pp_arith op (Util.pp_list pp) l + | Undefined_value -> Fmt.string out "" + | Asserting (t, g) -> + Fmt.fprintf out "(@[asserting@ %a@ %a@])" pp t pp g + + and pp_vbs out l = + let pp_vb out (v,t) = Fmt.fprintf out "(@[%a@ %a@])" Var.pp v pp t in + Util.pp_list pp_vb out l + in pp + +let pp_ty = Ty.pp (** {2 Constructors} *) @@ -200,7 +253,7 @@ let rec app_ty_ ty l : Ty.t = match ty, l with then app_ty_ ty_rest tail else Ty.ill_typed "expected `@[%a@]`,@ got `@[%a : %a@]`" Ty.pp ty_a pp_term a Ty.pp a.ty - | (Ty.Prop | Ty.Const _), a::_ -> + | (Ty.Prop | Ty.App _), a::_ -> Ty.ill_typed "cannot apply ty `@[%a@]`@ to `@[%a@]`" Ty.pp ty pp_term a let mk_ term ty = {term; ty} @@ -217,12 +270,8 @@ let asserting t g = mk_ (Asserting (t,g)) t.ty let var v = mk_ (Var v) (Var.ty v) -let unknown v = mk_ (Unknown v) (Var.ty v) - let const id ty = mk_ (Const id) ty -let select (s:select) (t:term) ty = mk_ (Select (s,t)) ty - let app f l = match f.term, l with | _, [] -> f | App (f1, l1), _ -> @@ -255,22 +304,25 @@ let match_ t m = m; mk_ (Match (t,m)) rhs1.ty -let switch u m = - try - let _, t1 = ID.Map.choose m in - mk_ (Switch (u,m)) t1.ty - with Not_found -> - invalid_arg "Ast.switch: empty list of cases" +let let_l vbs t = match vbs with + | [] -> t + | _::_ -> + List.iter + (fun (v,t) -> + if not (Ty.equal (Var.ty v) t.ty) then ( + Ty.ill_typed + "let: variable %a : @[%a@]@ and bounded term : %a@ should have same type" + Var.pp v Ty.pp (Var.ty v) Ty.pp t.ty; + );) + vbs; + mk_ (Let (vbs,t)) t.ty -let let_ v t u = - if not (Ty.equal (Var.ty v) t.ty) - then Ty.ill_typed - "let: variable %a : @[%a@]@ and bounded term : %a@ should have same type" - Var.pp v Ty.pp (Var.ty v) Ty.pp t.ty; - mk_ (Let (v,t,u)) u.ty +let let_ v t u = let_l [v,t] u let bind ~ty b v t = mk_ (Bind(b,v,t)) ty +let select ~ty (s:select) (t:term) = mk_ (Select (s,t)) ty + let fun_ v t = let ty = Ty.arrow (Var.ty v) t.ty in mk_ (Bind (Fun,v,t)) ty @@ -303,16 +355,17 @@ let eq a b = if not (Ty.equal a.ty b.ty) then Ty.ill_typed "eq: `@[%a@]` and `@[%a@]` do not have the same type" pp_term a pp_term b; - mk_ (Binop (Eq,a,b)) Ty.prop + mk_ (Op (Eq,[a;b])) Ty.prop let check_prop_ t = - if not (Ty.equal t.ty Ty.prop) - then Ty.ill_typed "expected prop, got `@[%a : %a@]`" pp_term t Ty.pp t.ty + if not (Ty.equal t.ty Ty.prop) then ( + Ty.ill_typed "expected prop, got `@[%a : %a@]`" pp_term t Ty.pp t.ty + ) -let binop op a b = mk_ (Binop (op, a, b)) Ty.prop -let binop_prop op a b = +let op op l = mk_ (Op (op, l)) Ty.prop +let binop_prop o a b = check_prop_ a; check_prop_ b; - binop op a b + op o [a;b] let and_ = binop_prop And let or_ = binop_prop Or @@ -321,17 +374,75 @@ let imply = binop_prop Imply let and_l = function | [] -> true_ | [f] -> f - | a :: l -> List.fold_left and_ a l + | l -> op And l let or_l = function | [] -> false_ | [f] -> f - | a :: l -> List.fold_left or_ a l + | l -> op Or l let not_ t = check_prop_ t; mk_ (Not t) Ty.prop +let arith ty op l = mk_ (Arith (op,l)) ty + +let num_q ty z = mk_ (Num_q z) ty +let num_z ty z = mk_ (Num_z z) ty + +let parse_num ~where (s:string) : [`Q of Q.t | `Z of Z.t] = + let fail() = + Util.errorf "%sexpected number, got `%s`" (Lazy.force where) s + in + begin match Z.of_string s with + | n -> `Z n + | exception _ -> + begin match Q.of_string s with + | n -> `Q n + | exception _ -> + if String.contains s '.' then ( + let p1, p2 = CCString.Split.left_exn ~by:"." s in + let n1, n2 = + try Z.of_string p1, Z.of_string p2 + with _ -> fail() + in + let factor_10 = Z.pow (Z.of_int 10) (String.length p2) in + (* [(p1·10^{length p2}+p2) / 10^{length p2}] *) + let n = + Q.div + (Q.of_bigint (Z.add n2 (Z.mul n1 factor_10))) + (Q.of_bigint factor_10) + in + `Q n + ) else fail() + end + end + +let num_str ty s = + begin match parse_num ~where:(Lazy.from_val "") s with + | `Q x -> num_q ty x + | `Z x -> num_z ty x + end + +(** {2 More IO} *) + +let pp_statement out = function + | SetLogic s -> Fmt.fprintf out "(set-logic %s)" s + | SetOption l -> Fmt.fprintf out "(@[set-logic@ %a@])" (Util.pp_list Fmt.string) l + | SetInfo l -> Fmt.fprintf out "(@[set-info@ %a@])" (Util.pp_list Fmt.string) l + | CheckSat -> Fmt.string out "(check-sat)" + | TyDecl (s,n) -> Fmt.fprintf out "(@[declare-sort@ %a %d@])" ID.pp s n + | Decl (id,ty) -> + let args, ret = Ty.unfold ty in + 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 + | Goal (vars,g) -> + Fmt.fprintf out "(@[assert-not@ %a@])" pp_term (forall_l vars (not_ g)) + | Exit -> Fmt.string out "(exit)" + | Data _ -> assert false (* TODO *) + | Define _ -> assert false (* TODO *) + (** {2 Environment} *) type env_entry = @@ -363,14 +474,15 @@ let env_add_statement env st = (fun c_id c_ty map -> add_def c_id (E_cstor c_ty) map) data_cstors map) env l - | TyDecl id -> add_def id E_uninterpreted_ty env + | TyDecl (id,_) -> add_def id E_uninterpreted_ty env | Decl (id,ty) -> add_def id (E_const ty) env | Define l -> List.fold_left (fun map (id,ty,def) -> add_def id (E_defined (ty,def)) map) env l - | Goal _ - | Assert _ -> env + | Goal _ | Assert _ | CheckSat | Exit + | SetLogic _ | SetOption _ | SetInfo _ + -> env let env_of_statements seq = Sequence.fold env_add_statement env_empty seq diff --git a/src/smt/Ast.mli b/src/smt/Ast.mli index 2a4f578c..fcd4a19c 100644 --- a/src/smt/Ast.mli +++ b/src/smt/Ast.mli @@ -7,9 +7,6 @@ type 'a or_error = ('a, string) CCResult.t (** {2 Types} *) -exception Error of string -exception Ill_typed of string - module Var : sig type 'ty t = private { id: ID.t; @@ -17,6 +14,7 @@ module Var : sig } val make : ID.t -> 'ty -> 'ty t + val makef : ty:'a -> ('b, Format.formatter, unit, 'a t) format4 -> 'b val copy : 'a t -> 'a t val id : _ t -> ID.t val ty : 'a t -> 'a @@ -29,14 +27,18 @@ end module Ty : sig type t = | Prop - | Const of ID.t + | App of ID.t * t list | Arrow of t * t val prop : t val const : ID.t -> t + val app : ID.t -> t list -> t val arrow : t -> t -> t val arrow_l : t list -> t -> t + val rat : t + val int : t + include Intf.EQ with type t := t include Intf.ORD with type t := t include Intf.HASH with type t := t @@ -63,11 +65,22 @@ end type var = Ty.t Var.t -type binop = +type op = | And | Or | Imply | Eq + | Distinct + +type arith_op = + | Leq + | Lt + | Geq + | Gt + | Add + | Minus + | Mult + | Div type binder = | Fun @@ -82,16 +95,17 @@ type term = private { and term_cell = | Var of var | Const of ID.t - | Unknown of var + | Num_z of Z.t + | Num_q of Q.t | App of term * term list | If of term * term * term - | Select of select * term | Match of term * (var list * term) ID.Map.t - | Switch of term * term ID.Map.t (* switch on constants *) + | Select of select * term | Bind of binder * var * term - | Let of var * term * term + | Arith of arith_op * term list + | Let of (var * term) list * term | Not of term - | Binop of binop * term * term + | Op of op * term list | Asserting of term * term | Undefined_value | Bool of bool @@ -107,12 +121,17 @@ and select = { type definition = ID.t * Ty.t * term type statement = + | SetLogic of string + | SetOption of string list + | SetInfo of string list | Data of Ty.data list - | TyDecl of ID.t (* new atomic cstor *) + | TyDecl of ID.t * int (* new atomic cstor *) | Decl of ID.t * Ty.t | Define of definition list | Assert of term | Goal of var list * term + | CheckSat + | Exit (** {2 Constructors} *) @@ -121,15 +140,14 @@ val ty : term -> Ty.t val var : var -> term val const : ID.t -> Ty.t -> term -val unknown : var -> term val app : term -> term list -> term val app_a : term -> term array -> term -val select : select -> term -> Ty.t -> term val if_ : term -> term -> term -> term val match_ : term -> (var list * term) ID.Map.t -> term -val switch : term -> term ID.Map.t -> term val let_ : var -> term -> term -> term +val let_l : (var * term) list -> term -> term val bind : ty:Ty.t -> binder -> var -> term -> term +val select : ty:Ty.t -> select -> term -> term val fun_ : var -> term -> term val fun_l : var list -> term -> term val fun_a : var array -> term -> term @@ -140,7 +158,7 @@ val exists_l : var list -> term -> term val mu : var -> term -> term val eq : term -> term -> term val not_ : term -> term -val binop : binop -> term -> term -> term +val op : op -> term list -> term val and_ : term -> term -> term val and_l : term list -> term val or_ : term -> term -> term @@ -150,7 +168,17 @@ val true_ : term val false_ : term val undefined_value : Ty.t -> term val asserting : term -> term -> term +val num_z : Ty.t -> Z.t -> term +val num_q : Ty.t -> Q.t -> term +val num_str : Ty.t -> string -> term (** parses int + {!num} *) +val arith : Ty.t -> arith_op -> term list -> term +(** {2 helpers} *) + +val is_true : term -> bool +val is_false : term -> bool + +val unfold_binder : binder -> term -> var list * term val unfold_fun : term -> var list * term (** {2 Printing} *) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index bcf5d956..97d6c847 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -1,5 +1,6 @@ -open CDCL +module Vec = Dagon_sat.Vec +module Log = Dagon_sat.Log open Solver_types type node = Equiv_class.t diff --git a/src/smt/Explanation.ml b/src/smt/Explanation.ml index f344b79a..9c5264be 100644 --- a/src/smt/Explanation.ml +++ b/src/smt/Explanation.ml @@ -1,5 +1,4 @@ -open CDCL open Solver_types type t = explanation diff --git a/src/smt/Lit.ml b/src/smt/Lit.ml index 964c455b..db4caee2 100644 --- a/src/smt/Lit.ml +++ b/src/smt/Lit.ml @@ -47,7 +47,7 @@ let pp = pp_lit let print = pp let norm l = - if l.lit_sign then l, CDCL.Same_sign else neg l, CDCL.Negated + if l.lit_sign then l, Dagon_sat.Same_sign else neg l, Dagon_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 193b7ee3..0269f3e4 100644 --- a/src/smt/Lit.mli +++ b/src/smt/Lit.mli @@ -12,7 +12,6 @@ val fresh_with : ID.t -> t val fresh : unit -> t val dummy : t val atom : ?sign:bool -> term -> t -val cstor_test : data_cstor -> term -> t val eq : Term.state -> term -> term -> t val neq : Term.state -> term -> term -> t val cstor_test : Term.state -> data_cstor -> term -> t @@ -22,7 +21,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 * CDCL.negated +val norm : t -> t * Dagon_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 b6e42f7d..9b0aab2f 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -3,8 +3,6 @@ (** {1 Model} *) -open CDCL - module A = Ast type term = A.term @@ -104,28 +102,21 @@ let rec as_cstor_app env t = match A.term_view t with CCOpt.map (fun (id,ty,l') -> id,ty,l'@l) (as_cstor_app env f) | _ -> None -let as_domain_elt env t = match A.term_view t with - | A.Const id -> - begin match A.env_find_def env id with - | Some A.E_uninterpreted_cst -> Some id - | _ -> None - end - | _ -> None - let pp_stack out (l:term list) : unit = let ppt out t = Format.fprintf out "(@[%a@ :ty %a@])" A.pp_term t A.Ty.pp t.A.ty in CCFormat.(within "[" "]" (hvbox (list ppt))) out l let apply_subst (subst:subst) t = let rec aux subst t = match A.term_view t with + | A.Num_z _ | A.Num_q _ -> t | A.Var v -> begin match VarMap.get v subst with | None -> t | Some (lazy t') -> t' end | A.Undefined_value - | A.Bool _ | A.Const _ | A.Unknown _ -> t - | A.Select (sel, t) -> A.select sel (aux subst t) t.A.ty + | A.Bool _ | A.Const _ -> t + | A.Select (sel, t) -> A.select ~ty:t.A.ty sel (aux subst t) | A.App (f,l) -> A.app (aux subst f) (List.map (aux subst) l) | A.If (a,b,c) -> A.if_ (aux subst a) (aux subst b) (aux subst c) | A.Match (u,m) -> @@ -134,38 +125,56 @@ let apply_subst (subst:subst) t = (fun (vars,rhs) -> let subst, vars = rename_vars subst vars in vars, aux subst rhs) m) - | A.Switch (u,m) -> - A.switch (aux subst u) (ID.Map.map (aux subst) m) - | A.Let (x,t,u) -> - let subst', x' = rename_var subst x in - A.let_ x' (aux subst t) (aux subst' u) + | A.Let (vbs,u) -> + let subst', vbs' = + CCList.fold_map + (fun subst' (x,t) -> + let t = aux subst t in + let subst', x' = rename_var subst' x in + subst', (x',t)) + subst vbs + in + A.let_l vbs' (aux subst' u) | A.Bind (A.Mu, _,_) -> assert false | A.Bind (b, x,body) -> let subst', x' = rename_var subst x in A.bind ~ty:(A.ty t) b x' (aux subst' body) | A.Not f -> A.not_ (aux subst f) - | A.Binop (op,a,b) -> A.binop op (aux subst a)(aux subst b) + | A.Op (op,l) -> A.op op (List.map (aux subst) l) | A.Asserting (t,g) -> A.asserting (aux subst t)(aux subst g) + | A.Arith (op,l) -> + let ty = A.ty t in + A.arith ty op (List.map (aux subst) l) in if VarMap.is_empty subst then t else aux subst t +type partial_eq = + | Eq + | Neq + | Unknown + +let equal_as_values (_:A.term) (_:A.term) : partial_eq = + Unknown (* TODO *) + (* Weak Head Normal Form. @param m the model @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 = - Log.debugf 5 + Dagon_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); let st = t :: st in try eval_whnf_rec m st subst t - with A.Ill_typed msg -> + with Util.Error msg -> errorf "@[<2>Model:@ internal type error `%s`@ in %a@]" msg pp_stack st and eval_whnf_rec m st subst t = match A.term_view t with - | A.Undefined_value | A.Bool _ | A.Unknown _ -> t + | A.Num_q _ + | A.Num_z _ -> t + | A.Undefined_value | A.Bool _ -> t | A.Var v -> begin match VarMap.get v subst with | None -> t @@ -196,10 +205,15 @@ and eval_whnf_rec m st subst t = match A.term_view t with | A.Bind (A.Mu,v,body) -> let subst' = VarMap.add v (lazy t) subst in eval_whnf m st subst' body - | A.Let (x,t,u) -> - let t = lazy (eval_whnf m st subst t) in - let subst' = VarMap.add x t subst in - eval_whnf m st subst' u + | A.Let (vbs,u) -> + let subst = + List.fold_left + (fun subst (x,t) -> + let t = lazy (eval_whnf m st subst t) in + VarMap.add x t subst) + subst vbs + in + eval_whnf m st subst u | A.Bind (A.Fun,_,_) -> apply_subst subst t | A.Bind ((A.Forall | A.Exists) as b,v,body) -> let ty = A.Var.ty v in @@ -227,7 +241,7 @@ and eval_whnf_rec m st subst t = match A.term_view t with eval_whnf m st subst t' | A.Select (sel, u) -> let u = eval_whnf m st subst u in - let t' = A.select sel u t.A.ty in + let t' = A.select ~ty:t.A.ty sel u in begin match as_cstor_app m.env u with | None -> t' | Some (cstor, _, args) -> @@ -266,20 +280,6 @@ and eval_whnf_rec m st subst t = match A.term_view t with in eval_whnf m st subst' rhs end - | A.Switch (u, map) -> - let u = eval_whnf m st subst u in - begin match as_domain_elt m.env u with - | None -> - let map = ID.Map.map (apply_subst subst) map in - A.switch u map - | Some cst -> - begin match ID.Map.get cst map with - | Some rhs -> eval_whnf m st subst rhs - | None -> - let map = ID.Map.map (apply_subst subst) map in - A.switch u map - end - end | A.Not f -> let f = eval_whnf m st subst f in begin match A.term_view f with @@ -295,59 +295,41 @@ and eval_whnf_rec m st subst t = match A.term_view t with A.undefined_value u.A.ty (* assertion failed, uncharted territory! *) | _ -> A.asserting u g' end - | A.Binop (op, a, b) -> - let a = eval_whnf m st subst a in - let b = eval_whnf m st subst b in + | A.Op (op, l) -> + let l = List.map (eval_whnf m st subst) l in begin match op with | A.And -> - begin match A.term_view a, A.term_view b with - | A.Bool true, A.Bool true -> A.true_ - | A.Bool false, _ - | _, A.Bool false -> A.false_ - | _ -> A.and_ a b - end + if List.exists A.is_false l then A.false_ + else if List.for_all A.is_true l then A.true_ + else A.and_l l | A.Or -> - begin match A.term_view a, A.term_view b with - | A.Bool true, _ - | _, A.Bool true -> A.true_ - | A.Bool false, A.Bool false -> A.false_ - | _ -> A.or_ a b - end + if List.exists A.is_true l then A.true_ + else if List.for_all A.is_false l then A.false_ + else A.or_l l | A.Imply -> - begin match A.term_view a, A.term_view b with - | _, A.Bool true - | A.Bool false, _ -> A.true_ - | A.Bool true, A.Bool false -> A.false_ - | _ -> A.imply a b - end + assert false (* TODO *) | A.Eq -> - begin match A.term_view a, A.term_view b with - | A.Bool true, A.Bool true - | A.Bool false, A.Bool false -> A.true_ - | A.Bool true, A.Bool false - | A.Bool false, A.Bool true -> A.false_ - | A.Var v1, A.Var v2 when A.Var.equal v1 v2 -> A.true_ - | A.Const id1, A.Const id2 when ID.equal id1 id2 -> A.true_ - | _ -> - begin match as_cstor_app m.env a, as_cstor_app m.env b with - | Some (c1,_,l1), Some (c2,_,l2) -> - if ID.equal c1 c2 then ( - assert (List.length l1 = List.length l2); - eval_whnf m st subst (A.and_l (List.map2 A.eq l1 l2)) - ) else A.false_ - | _ -> - begin match as_domain_elt m.env a, as_domain_elt m.env b with - | Some c1, Some c2 -> - (* domain elements: they are all distinct *) - if ID.equal c1 c2 - then A.true_ - else A.false_ - | _ -> - A.eq a b - end - end + begin match l with + | [] -> assert false + | x :: tail -> + if List.for_all (fun y -> equal_as_values x y = Eq) tail + then A.true_ + else if List.exists (fun y -> equal_as_values x y = Neq) tail + then A.false_ + else A.op A.Eq l end + | A.Distinct -> + if + Sequence.diagonal_l l + |> Sequence.exists (fun (t,u) -> equal_as_values t u = Eq) + then A.false_ + else if + Sequence.diagonal_l l + |> Sequence.for_all (fun (t,u) -> equal_as_values t u = Neq) + then A.true_ + else A.op A.Distinct l end + | A.Arith (_, _) -> assert false (* TODO *) (* beta-reduce [f l] while [f] is a function,constant or variable *) and eval_whnf_app m st subst_f subst_l f l = match A.term_view f, l with | A.Bind (A.Fun,v, body), arg :: tail -> diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index bc11187d..28d5b73f 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -21,21 +21,23 @@ let get_time : unit -> float = Sys.time type level = int -module Sat = CDCL.Make(Theory_combine) +module Sat_solver = Dagon_sat.Make(Theory_combine) (* main solver state *) type t = { - solver: Sat.t; + solver: Sat_solver.t; stat: Stat.t; config: Config.t } -let th_combine (self:t) : Theory_combine.t = - Sat.theory self.solver +let solver self = self.solver +let th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver +let add_theory self th = Theory_combine.add_theory (th_combine self) th +let stats self = self.stat let create ?size ?(config=Config.empty) ~theories () : t = let self = { - solver=Sat.create ?size (); + solver=Sat_solver.create ?size (); stat=Stat.create (); config; } in @@ -706,11 +708,11 @@ end (** {2 Main} *) -let[@inline] clause_of_mclause (c:Sat.clause): Clause.t = - Sat.Clause.atoms_l c |> Clause.make +let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t = + Sat_solver.Clause.atoms_l c |> Clause.make (* convert unsat-core *) -let clauses_of_unsat_core (core:Sat.clause list): Clause.t Sequence.t = +let clauses_of_unsat_core (core:Sat_solver.clause list): Clause.t Sequence.t = Sequence.of_list core |> Sequence.map clause_of_mclause @@ -747,20 +749,20 @@ let add_statement_l (_:t) _ = () (* TODO: move this into submodule *) let pp_proof out p = let pp_step_res out p = - let {Sat.Proof.conclusion; _ } = Sat.Proof.expand p in + let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in let conclusion = clause_of_mclause conclusion in Clause.pp out conclusion in let pp_step out = function - | Sat.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])" - | Sat.Proof.Resolution (p1, p2, _) -> + | Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])" + | Sat_solver.Proof.Resolution (p1, p2, _) -> Format.fprintf out "(@[<1>resolution@ %a@ %a@])" pp_step_res p1 pp_step_res p2 | _ -> Fmt.string out "" in Format.fprintf out "(@["; - Sat.Proof.fold - (fun () {Sat.Proof.conclusion; step } -> + Sat_solver.Proof.fold + (fun () {Sat_solver.Proof.conclusion; step } -> let conclusion = clause_of_mclause conclusion in Format.fprintf out "(@[step@ %a@ @[<1>from:@ %a@]@])@," Clause.pp conclusion pp_step step) diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index d94460a6..fc63402b 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -5,18 +5,6 @@ The solving algorithm, based on MCSat *) -open CDCL - -type term -type cst -type ty = Solver_types.ty (** types *) -type ty_def = Solver_types.ty_def - -type ty_cell = Solver_types.ty_cell = - | Prop - | Atomic of ID.t * ty_def - | Arrow of ty * ty - (** {2 Result} *) type model = Model.t @@ -31,6 +19,11 @@ type res = | Unsat (* TODO: proof *) | Unknown of unknown +module Sat_solver : Dagon_sat.S + with type formula = Lit.t + and type theory = Theory_combine.t + and type Proof.lemma = Theory_combine.proof + (** {2 Main} *) type t @@ -42,6 +35,11 @@ val create : theories:Theory.t list -> unit -> t +val solver : t -> Sat_solver.t +val th_combine : t -> Theory_combine.t +val add_theory : t -> Theory.t -> unit +val stats : t -> Stat.t + val add_statement_l : t -> Ast.statement list -> unit val solve : diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 8e4f2a60..5de9d809 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -1,6 +1,4 @@ -open CDCL - module Fmt = CCFormat module Node_bits = CCBitField.Make(struct end) diff --git a/src/smt/Term.mli b/src/smt/Term.mli index 45765a31..c8ae454f 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -1,5 +1,4 @@ -open CDCL open Solver_types type t = term diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index 02f76de5..2093b892 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -1,6 +1,4 @@ -open Solver_types - (** Runtime state of a theory, with all the operations it provides *) type state = { on_merge: Equiv_class.t -> Equiv_class.t -> Explanation.t -> unit; diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index fe4aa1a6..37c240a4 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -3,6 +3,7 @@ (** Combine the congruence closure with a number of plugins *) +module Sat_solver = Dagon_sat open Solver_types module Proof = struct @@ -21,7 +22,7 @@ type conflict = Explanation.t Bag.t exception Exn_conflict of conflict type t = { - cdcl_acts: (formula,proof) CDCL.actions; + cdcl_acts: (formula,proof) Sat_solver.actions; (** actions provided by the SAT solver *) tst: Term.state; (** state for managing terms *) @@ -49,7 +50,7 @@ let[@inline] theories (self:t) : Theory.state Sequence.t = (* handle a literal assumed by the SAT solver *) let assume_lit (self:t) (lit:Lit.t) : unit = - CDCL.Log.debugf 2 + Sat_solver.Log.debugf 2 (fun k->k "(@[<1>@{theory_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit); (* check consistency first *) begin match Lit.view lit with @@ -65,26 +66,26 @@ let assume_lit (self:t) (lit:Lit.t) : unit = (* push clauses from {!lemma_queue} into the slice *) let push_new_clauses_into_cdcl (self:t) : unit = - let CDCL.Actions r = self.cdcl_acts in + let Sat_solver.Actions r = self.cdcl_acts in (* persistent lemmas *) while not (Queue.is_empty self.lemma_q) do let c = Queue.pop self.lemma_q in - CDCL.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c); + Sat_solver.Log.debugf 5 (fun k->k "(@[<2>push_lemma@ %a@])" Clause.pp c); r.push c Proof.default done; (* local splits *) while not (Queue.is_empty self.split_q) do let c = Queue.pop self.split_q in - CDCL.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c); + Sat_solver.Log.debugf 5 (fun k->k "(@[<2>split_on@ %a@])" Clause.pp c); r.push_local c Proof.default done (* return result to the SAT solver *) -let cdcl_return_res (self:t) : _ CDCL.res = +let cdcl_return_res (self:t) : _ Sat_solver.res = begin match self.conflict with | None -> push_new_clauses_into_cdcl self; - CDCL.Sat + Sat_solver.Sat | Some c -> let lit_set = Bag.to_seq c @@ -95,19 +96,19 @@ let cdcl_return_res (self:t) : _ CDCL.res = |> List.map Lit.neg |> Clause.make in - CDCL.Log.debugf 3 + Sat_solver.Log.debugf 3 (fun k->k "(@[<1>conflict@ clause: %a@])" Clause.pp conflict_clause); - CDCL.Unsat (Clause.lits conflict_clause, Proof.default) + Sat_solver.Unsat (Clause.lits conflict_clause, Proof.default) end let[@inline] check (self:t) : unit = Congruence_closure.check (cc self) (* propagation from the bool solver *) -let assume_real (self:t) (slice:_ CDCL.slice_actions) = +let assume_real (self:t) (slice:_ Sat_solver.slice_actions) = (* TODO if Config.progress then print_progress(); *) - let CDCL.Slice_acts slice = slice in + let Sat_solver.Slice_acts slice = slice in begin try slice.slice_iter (assume_lit self); @@ -120,7 +121,7 @@ let assume_real (self:t) (slice:_ CDCL.slice_actions) = cdcl_return_res self (* propagation from the bool solver *) -let assume (self:t) (slice:_ CDCL.slice_actions) = +let assume (self:t) (slice:_ Sat_solver.slice_actions) = match self.conflict with | None -> assume_real self slice | Some _ -> @@ -128,11 +129,11 @@ let assume (self:t) (slice:_ CDCL.slice_actions) = cdcl_return_res self (* perform final check of the model *) -let if_sat (self:t) (slice:_) : _ CDCL.res = +let if_sat (self:t) (slice:_) : _ Sat_solver.res = Congruence_closure.final_check (cc self); (* all formulas in the SAT solver's trail *) let forms = - let CDCL.Slice_acts r = slice in + let Sat_solver.Slice_acts r = slice in r.slice_iter in (* final check for each theory *) @@ -144,13 +145,13 @@ let if_sat (self:t) (slice:_) : _ CDCL.res = (* forward propagations from CC or theories directly to the SMT core *) let act_propagate (self:t) f guard : unit = - let CDCL.Actions r = self.cdcl_acts in + let Sat_solver.Actions r = self.cdcl_acts in let guard = Bag.to_seq guard |> Congruence_closure.explain_unfold (cc self) |> Lit.Set.to_list in - CDCL.Log.debugf 2 + Sat_solver.Log.debugf 2 (fun k->k "(@[@{propagate@}@ %a@ :guard %a@])" Lit.pp f Clause.pp guard); r.propagate f guard Proof.default @@ -165,7 +166,7 @@ let on_merge_from_cc (self:t) r1 r2 e : unit = (fun th -> th.Theory.on_merge r1 r2 e) let mk_cc_actions (self:t) : Congruence_closure.actions = - let CDCL.Actions r = self.cdcl_acts in + let Sat_solver.Actions r = self.cdcl_acts in { Congruence_closure. on_backtrack = r.on_backtrack; @@ -178,8 +179,8 @@ let mk_cc_actions (self:t) : Congruence_closure.actions = (** {2 Main} *) (* create a new theory combination *) -let create (cdcl_acts:_ CDCL.actions) : t = - CDCL.Log.debug 5 "theory_combine.create"; +let create (cdcl_acts:_ Sat_solver.actions) : t = + Sat_solver.Log.debug 5 "theory_combine.create"; let rec self = { cdcl_acts; tst=Term.create ~size:1024 (); @@ -210,18 +211,18 @@ let act_find self t = |> Congruence_closure.find (cc self) let act_case_split self (c:Clause.t) = - CDCL.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c); + Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_split@ @[%a@]@])" Clause.pp c); Queue.push c self.split_q (* push one clause into [M], in the current level (not a lemma but an axiom) *) let act_add_axiom self (c:Clause.t): unit = - CDCL.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c); + Sat_solver.Log.debugf 2 (fun k->k "(@[<1>add_axiom@ @[%a@]@])" Clause.pp c); (* TODO incr stat_num_clause_push; *) Queue.push c self.lemma_q let mk_theory_actions (self:t) : Theory.actions = - let CDCL.Actions r = self.cdcl_acts in + let Sat_solver.Actions r = self.cdcl_acts in { Theory. on_backtrack = r.on_backtrack; @@ -236,7 +237,7 @@ let mk_theory_actions (self:t) : Theory.actions = } let add_theory (self:t) (th:Theory.t) : unit = - CDCL.Log.debugf 2 + Sat_solver.Log.debugf 2 (fun k->k "(@[theory_combine.add_th@ :name %S@])" th.Theory.name); let th_s = th.Theory.make self.tst (mk_theory_actions self) in self.theories <- th_s :: self.theories diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index 25ccdd30..1ff40d89 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 CDCL.Theory_intf.S +include Dagon_sat.Theory_intf.S with type formula = Lit.t and type proof = Proof.t diff --git a/src/smt/Ty.ml b/src/smt/Ty.ml index 319231f0..73995cea 100644 --- a/src/smt/Ty.ml +++ b/src/smt/Ty.ml @@ -1,5 +1,4 @@ -open CDCL open Solver_types type t = ty diff --git a/src/smt/Ty.mli b/src/smt/Ty.mli index ae7f45a1..39989fa0 100644 --- a/src/smt/Ty.mli +++ b/src/smt/Ty.mli @@ -1,8 +1,6 @@ (** {1 Hashconsed Types} *) -open CDCL - type t = Solver_types.ty type cell = Solver_types.ty_cell type def = Solver_types.ty_def diff --git a/src/smt/Ty_card.mli b/src/smt/Ty_card.mli index 07569e71..478333b3 100644 --- a/src/smt/Ty_card.mli +++ b/src/smt/Ty_card.mli @@ -1,8 +1,6 @@ (** {1 Type Cardinality} *) -open CDCL - type t = Solver_types.ty_card val (+) : t -> t -> t diff --git a/src/smt/jbuild b/src/smt/jbuild index 599e08d1..322736dc 100644 --- a/src/smt/jbuild +++ b/src/smt/jbuild @@ -1,9 +1,10 @@ ; vim:ft=lisp: (library - ((name CDCL_smt) - (public_name cdcl.smt) - (libraries (containers containers.data sequence cdcl)) - (flags (:standard -w +a-4-44-48-58-60@8 -color always -safe-string -short-paths)) + ((name Dagon_smt) + (public_name dagon.smt) + (libraries (containers containers.data sequence dagon.util dagon.sat zarith)) + (flags (:standard -w +a-4-44-48-58-60@8 + -color always -safe-string -short-paths -open Dagon_util)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)))) diff --git a/src/smtlib/Convert.ml b/src/smtlib/Convert.ml new file mode 100644 index 00000000..f1f05c71 --- /dev/null +++ b/src/smtlib/Convert.ml @@ -0,0 +1,455 @@ + +(* This file is free software. See file "license" for more details. *) + +(** {1 Preprocessing AST} *) + +module Loc = Locations +module Fmt = CCFormat + +module A = Dagon_smt.Ast +module PA = Parse_ast + +type 'a or_error = ('a, string) CCResult.t + +let pp_loc_opt = Loc.pp_opt + +(** {2 Parsing} *) + +module StrTbl = CCHashtbl.Make(struct + type t = string + let equal = CCString.equal + let hash = CCString.hash + end) + +module Ctx = struct + type kind = + | K_ty of ty_kind + | K_fun of A.Ty.t + | K_var of A.var (* local *) + | K_cstor of A.Ty.t + | K_select of A.Ty.t * A.select + + and ty_kind = + | K_uninterpreted (* uninterpreted type *) + | K_other + | K_bool + | K_data (* data type *) + + type t = { + names: ID.t StrTbl.t; + kinds: kind ID.Tbl.t; + data: (ID.t * A.Ty.t) list ID.Tbl.t; (* data -> cstors *) + mutable loc: Loc.t option; (* current loc *) + } + + let create () : t = { + names=StrTbl.create 64; + kinds=ID.Tbl.create 64; + data=ID.Tbl.create 64; + loc=None; + } + + let loc t = t.loc + let set_loc ?loc t = t.loc <- loc + + let add_id t (s:string) (k:kind): ID.t = + let id = ID.make s in + StrTbl.add t.names s id; + ID.Tbl.add t.kinds id k; + id + + let add_data t (id:ID.t) cstors: unit = + ID.Tbl.add t.data id cstors + + let with_var t (s:string) (ty:A.Ty.t) (f:A.var -> 'a): 'a = + let id = ID.make s in + StrTbl.add t.names s id; + let v = A.Var.make id ty in + ID.Tbl.add t.kinds id (K_var v); + CCFun.finally1 f v + ~h:(fun () -> StrTbl.remove t.names s) + + let with_vars t (l:(string*A.Ty.t) list) (f:A.var list -> 'a): 'a = + let rec aux ids l f = match l with + | [] -> f (List.rev ids) + | (s,ty) :: l' -> with_var t s ty (fun id -> aux (id::ids) l' f) + in + aux [] l f + + let find_kind t (id:ID.t) : kind = + try ID.Tbl.find t.kinds id + with Not_found -> Util.errorf "did not find kind of ID `%a`" ID.pp id + + let as_data t (ty:A.Ty.t) : (ID.t * A.Ty.t) list = match ty with + | A.Ty.App (id,_) -> + begin match ID.Tbl.get t.data id with + | Some l -> l + | None -> Util.errorf "expected %a to be a datatype" A.Ty.pp ty + end + | _ -> Util.errorf "expected %a to be a constant type" A.Ty.pp ty + + let pp_kind out = function + | K_ty _ -> Format.fprintf out "type" + | K_cstor ty -> + Format.fprintf out "(@[cstor : %a@])" A.Ty.pp ty + | K_select (ty,s) -> + Format.fprintf out "(@[select-%a-%d : %a@])" + ID.pp s.A.select_cstor s.A.select_i A.Ty.pp ty + | K_fun ty -> + Format.fprintf out "(@[fun : %a@])" A.Ty.pp ty + | K_var v -> + Format.fprintf out "(@[var : %a@])" A.Ty.pp (A.Var.ty v) + + let pp out t = + Format.fprintf out "ctx {@[%a@]}" + Fmt.(seq ~sep:(return "@ ") @@ pair ID.pp pp_kind) (ID.Tbl.to_seq t.kinds) +end + +let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx) +let errorf_ctx ctx msg = + Util.errorf ("at %a:@ " ^^ msg) pp_loc_opt (Ctx.loc ctx) + +let check_bool_ t = + if not (A.Ty.equal (A.ty t) A.Ty.prop) then ( + A.Ty.ill_typed "expected bool, got `@[%a : %a@]`" A.pp_term t A.Ty.pp (A.ty t) + ) + +let find_id_ ctx (s:string): ID.t = + try StrTbl.find ctx.Ctx.names s + with Not_found -> errorf_ctx ctx "name `%s` not in scope" s + +(* parse a type *) +let rec conv_ty ctx (t:PA.ty) : A.Ty.t * _ = match t with + | PA.Ty_bool -> A.Ty.prop, Ctx.K_ty Ctx.K_bool + | PA.Ty_app ("Rat",[]) -> A.Ty.rat, Ctx.K_ty Ctx.K_other + | PA.Ty_app ("Int",[]) -> A.Ty.int , Ctx.K_ty Ctx.K_other + | PA.Ty_app (f, l) -> + let id = find_id_ ctx f in + let l = List.map (conv_ty_fst ctx) l in + A.Ty.app id l, Ctx.find_kind ctx id + | PA.Ty_arrow (args, ret) -> + let args = List.map (conv_ty_fst ctx) args in + let ret, _ = conv_ty ctx ret in + A.Ty.arrow_l args ret, Ctx.K_ty Ctx.K_other + +and conv_ty_fst ctx t = fst (conv_ty ctx t) + +let conv_var ctx (v,ty) = v, conv_ty_fst ctx ty +let conv_vars ctx l = List.map (fun (v,ty) -> v, conv_ty_fst ctx ty) l + +let is_num s = + let is_digit_or_dot = function '0' .. '9' | '.' -> true | _ -> false in + if s.[0] = '-' + then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1)) + else CCString.for_all is_digit_or_dot s + +let rec conv_term ctx (t:PA.term) : A.term = match t with + | PA.True -> A.true_ + | PA.False -> A.false_ + | PA.Const s when is_num s -> A.num_str A.Ty.rat s (* numeral *) + | PA.Const f -> + let id = find_id_ ctx f in + begin match Ctx.find_kind ctx id with + | Ctx.K_var v -> A.var v + | Ctx.K_fun ty -> A.const id ty + | Ctx.K_ty _ -> + errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id + | Ctx.K_cstor ty -> A.const id ty + | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported" + end + | PA.If (a,b,c) -> + let a = conv_term ctx a in + let b = conv_term ctx b in + let c = conv_term ctx c in + A.if_ a b c + | PA.Fun (v, body) -> + let v = conv_var ctx v in + Ctx.with_var ctx (fst v)(snd v) + (fun v -> + let body = conv_term ctx body in + A.fun_ v body) + | PA.Forall _ | PA.Exists _ -> + errorf_ctx ctx "cannot process quantifiers in %a" PA.pp_term t + | PA.Let (vbs, u) -> + let vars, terms = + List.map + (fun (v,t) -> + let t = conv_term ctx t in + (v,A.ty t), t) + vbs + |> List.split + in + Ctx.with_vars ctx vars + (fun vars -> + let vbs = List.combine vars terms in + let u = conv_term ctx u in + A.let_l vbs u) + | PA.Distinct l -> + let l = List.map (conv_term ctx) l in + A.op A.Distinct l + | PA.And l -> + let l = List.map (conv_term ctx) l in + A.and_l l + | PA.Or l -> + let l = List.map (conv_term ctx) l in + A.or_l l + | PA.Not a -> + let a = conv_term ctx a in + A.not_ a + | PA.Eq (a,b) -> + let a = conv_term ctx a in + let b = conv_term ctx b in + A.eq a b + | PA.Imply (a,b) -> + let a = conv_term ctx a in + let b = conv_term ctx b in + A.imply a b + | PA.Xor (a,b) -> + let a = conv_term ctx a in + let b = conv_term ctx b in + A.or_ (A.and_ a (A.not_ b)) (A.and_ (A.not_ a) b) + | PA.Match (lhs, l) -> + (* + errorf_ctx ctx "TODO: support match in %a" PA.pp_term t + assert false + *) + (* convert a regular case *) + let conv_case c vars rhs = + let c_id = find_id_ ctx c in + (* obtain the type *) + let ty_args, _ty_ret = match Ctx.find_kind ctx c_id with + | Ctx.K_cstor ty -> A.Ty.unfold ty + | _ -> + errorf_ctx ctx "expected `@[%a@]`@ to be a constructor" ID.pp c_id + in + (* pair variables with their type *) + if List.length vars <> List.length ty_args then ( + errorf_ctx ctx + "in @[%a@] for case %a,@ wrong number of arguments (expected %d)" + PA.pp_term t ID.pp c_id (List.length ty_args); + ); + let vars = List.combine vars ty_args in + Ctx.with_vars ctx vars + (fun vars -> + let rhs = conv_term ctx rhs in + c_id, vars, rhs) + in + (* convert default case, where [m] contains the partial map. We have + to complete this map *) + let lhs = conv_term ctx lhs in + let default, cases = + List.fold_left + (fun (def,cases) branch -> match branch with + | PA.Match_case (c,vars,rhs) -> + let c, vars, rhs = conv_case c vars rhs in + (* no duplicate *) + if ID.Map.mem c cases + then errorf_ctx ctx "constructor %a occurs twice" ID.pp c; + def, ID.Map.add c (vars,rhs) cases + | PA.Match_default rhs -> + (* check there is only one "default" case *) + begin match def with + | Some _ -> errorf_ctx ctx "cannot have two `default` cases" + | None -> + let rhs = conv_term ctx rhs in + Some rhs, cases + end) + (None,ID.Map.empty) l + in + (* now fill the blanks, check exhaustiveness *) + let all_cstors = Ctx.as_data ctx lhs.A.ty in + let cases = match default with + | None -> + (* check exhaustiveness *) + let missing = + all_cstors + |> List.filter (fun (cstor,_) -> not (ID.Map.mem cstor cases)) + |> List.map fst + in + if missing<>[] then ( + errorf_ctx ctx + "missing cases in `@[%a@]`: @[%a@]" + PA.pp_term t (Util.pp_list ID.pp) missing; + ); + cases + | Some def_rhs -> + List.fold_left + (fun cases (cstor,ty_cstor) -> + if ID.Map.mem cstor cases then cases + else ( + let args, _ = A.Ty.unfold ty_cstor in + let vars = List.mapi (fun i ty -> A.Var.makef ~ty "_%d" i) args in + ID.Map.add cstor (vars, def_rhs) cases + )) + cases all_cstors + in + A.match_ lhs cases + | PA.Arith (op, l) -> + let l = List.map (conv_term ctx) l in + List.iter + (fun t -> + if not (A.Ty.equal A.Ty.rat (A.ty t)) then ( + errorf_ctx ctx "expected rational term,@ got `%a`" A.pp_term t + )) + l; + let ty, op = match op with + | PA.Leq -> A.Ty.prop, A.Leq + | PA.Lt -> A.Ty.prop,A. Lt + | PA.Geq -> A.Ty.prop, A.Geq + | PA.Gt -> A.Ty.prop, A.Gt + | PA.Add -> A.Ty.rat, A.Add + | PA.Minus -> A.Ty.rat, A.Minus + | PA.Mult -> A.Ty.rat, A.Mult + | PA.Div -> A.Ty.rat, A.Div + in + A.arith ty op l + | PA.Cast (t, ty_expect) -> + let t = conv_term ctx t in + let ty_expect = conv_ty_fst ctx ty_expect in + if not (A.Ty.equal (A.ty t) ty_expect) then ( + A.Ty.ill_typed "term `%a`@ should have type `%a`" A.pp_term t A.Ty.pp ty_expect + ); + t + | _ -> + 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); + let abs_path = Filename.concat dir name in + if Sys.file_exists abs_path + then Some abs_path + else None + +let conv_fun_decl ctx f : string * A.Ty.t = + if f.PA.fun_ty_vars <> [] then ( + errorf_ctx ctx "cannot convert polymorphic function@ %a" + (PA.pp_fun_decl PA.pp_ty) f + ); + let args = List.map (conv_ty_fst ctx) f.PA.fun_args in + let ty = A.Ty.arrow_l args (conv_ty_fst ctx f.PA.fun_ret) in + f.PA.fun_name, ty + +let conv_fun_def ctx f_decl body : string * A.Ty.t * (unit -> A.term) = + if f_decl.PA.fun_ty_vars <> [] then ( + errorf_ctx ctx "cannot convert polymorphic function@ %a" + (PA.pp_fun_decl PA.pp_typed_var) f_decl; + ); + let args = conv_vars ctx f_decl.PA.fun_args in + let ty = + A.Ty.arrow_l + (List.map snd args) + (conv_ty_fst ctx f_decl.PA.fun_ret) + in + (* delayed body, for we need to declare the functions in the recursive block first *) + let conv_body() = + Ctx.with_vars ctx args + (fun args -> + A.fun_l args (conv_term ctx body)) + in + f_decl.PA.fun_name, ty, conv_body + +let conv_fun_defs ctx decls bodies : A.definition list = + let l = List.map2 (conv_fun_def ctx) decls bodies in + let ids = List.map (fun (f,ty,_) -> Ctx.add_id ctx f (Ctx.K_fun ty)) l in + let defs = List.map2 (fun id (_,ty,body) -> id, ty, body()) ids l in + (* parse id,ty and declare them before parsing the function bodies *) + defs + +let rec conv_statement ctx (s:PA.statement): A.statement list = + Log.debugf 4 (fun k->k "(@[<1>statement_of_ast@ %a@])" PA.pp_stmt s); + Ctx.set_loc ctx ?loc:(PA.loc s); + conv_statement_aux ctx s + +and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.view stmt with + | PA.Stmt_set_logic s -> [A.SetLogic s] + | PA.Stmt_set_option l -> [A.SetOption l] + | PA.Stmt_set_info l -> [A.SetInfo l] + | PA.Stmt_exit -> [A.Exit] + | PA.Stmt_decl_sort (s,n) -> + let id = Ctx.add_id ctx s (Ctx.K_ty Ctx.K_uninterpreted) in + [A.TyDecl (id,n)] + | PA.Stmt_decl fr -> + let f, ty = conv_fun_decl ctx fr in + let id = Ctx.add_id ctx f (Ctx.K_fun ty) in + [A.Decl (id, ty)] + | PA.Stmt_data ([],l) -> + (* first, read and declare each datatype (it can occur in the other + datatypes' construtors) *) + let pre_parse (data_name,cases) = + let data_id = Ctx.add_id ctx data_name (Ctx.K_ty Ctx.K_data) in + data_id, cases + in + let l = List.map pre_parse l in + (* now parse constructors *) + let l = + List.map + (fun (data_id, (cstors:PA.cstor list)) -> + let data_ty = A.Ty.const data_id in + let parse_case {PA.cstor_name=c; cstor_args} = + let selectors = + List.map (fun (n,ty) -> Some n, conv_ty_fst ctx ty) cstor_args + in + let ty_args = List.map snd selectors in + (* declare cstor *) + let ty_c = A.Ty.arrow_l ty_args data_ty in + let id_c = Ctx.add_id ctx c (Ctx.K_cstor ty_c) in + (* now declare selectors *) + List.iteri + (fun i (name_opt,ty) -> match name_opt with + | None -> () + | Some select_str -> + (* declare this selector *) + let rec select_name = lazy + (Ctx.add_id ctx select_str + (Ctx.K_select (ty, + {A.select_name; select_cstor=id_c; select_i=i}))) + in + ignore (Lazy.force select_name)) + selectors; + (* return cstor *) + id_c, ty_c + in + let cstors = List.map parse_case cstors in + (* update info on [data] *) + Ctx.add_data ctx data_id cstors; + {A.Ty.data_id; data_cstors=ID.Map.of_list cstors}) + l + in + [A.Data l] + | PA.Stmt_data _ -> + errorf_ctx ctx "not implemented: parametric datatypes" PA.pp_stmt stmt + | PA.Stmt_funs_rec defs -> + (* errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt *) + let {PA.fsr_decls=decls; fsr_bodies=bodies} = defs in + if List.length decls <> List.length bodies then ( + errorf_ctx ctx "declarations and bodies should have same length"; + ); + let defs = conv_fun_defs ctx decls bodies in + [A.Define defs] + | PA.Stmt_fun_def + {PA.fr_decl={PA.fun_ty_vars=[]; fun_args=[]; fun_name; fun_ret}; fr_body} -> + (* turn [def f : ret := body] into [decl f : ret; assert f=body] *) + let ret = conv_ty_fst ctx fun_ret in + let id = Ctx.add_id ctx fun_name (Ctx.K_fun ret) in + let rhs = conv_term ctx fr_body in + [ A.Decl (id,ret); + A.Assert (A.eq (A.const id ret) rhs); + ] + | PA.Stmt_fun_rec _ + | PA.Stmt_fun_def _ + -> errorf_ctx ctx "unsupported definition: %a" PA.pp_stmt stmt + | PA.Stmt_assert t -> + let t = conv_term ctx t in + check_bool_ t; + [A.Assert t] + | PA.Stmt_assert_not ([], t) -> + let vars, t = A.unfold_binder A.Forall (conv_term ctx t) in + let g = A.not_ t in (* negate *) + [A.Goal (vars, g)] + | PA.Stmt_assert_not (_::_, _) -> + errorf_ctx ctx "cannot convert polymorphic goal@ `@[%a@]`" + PA.pp_stmt stmt + | PA.Stmt_lemma _ -> + errorf_ctx ctx "smbc does not know how to handle `lemma` statements" + | PA.Stmt_check_sat -> [A.CheckSat] + diff --git a/src/smtlib/Convert.mli b/src/smtlib/Convert.mli new file mode 100644 index 00000000..cbbf74a8 --- /dev/null +++ b/src/smtlib/Convert.mli @@ -0,0 +1,24 @@ + +(* This file is free software. See file "license" for more details. *) + +(** {1 Preprocessing AST} *) + +module Loc = Locations + +type 'a or_error = ('a, string) CCResult.t + +(** {2 Parsing and Typing} *) + +module Ctx : sig + type t + val create: unit -> t + val pp : t CCFormat.printer +end + +module PA = Parse_ast +module A = Dagon_smt.Ast + +val conv_term : Ctx.t -> PA.term -> A.term + +val conv_statement : Ctx.t -> PA.statement -> A.statement list + diff --git a/src/smtlib/Dagon_smtlib.ml b/src/smtlib/Dagon_smtlib.ml new file mode 100644 index 00000000..8095f1ae --- /dev/null +++ b/src/smtlib/Dagon_smtlib.ml @@ -0,0 +1,456 @@ + +(** {1 Process Statements} *) + +open Dagon_smt + +module Fmt = CCFormat +module A = Ast +module PA = Parse_ast +module E = CCResult +module Loc = Locations + +type 'a or_error = ('a, string) CCResult.t + +module Parse = struct + let parse_chan_exn ?(filename="") ic = + let lexbuf = Lexing.from_channel ic in + Loc.set_file lexbuf filename; + Parser.parse_list Lexer.token lexbuf + + let parse_chan ?filename ic = + try Result.Ok (parse_chan_exn ?filename ic) + with e -> Result.Error (Printexc.to_string e) + + let parse_file_exn file : PA.statement list = + CCIO.with_in file (parse_chan_exn ~filename:file) + + let parse_file file = + try Result.Ok (parse_file_exn file) + with e -> Result.Error (Printexc.to_string e) + + let parse_file_exn ctx file : Ast.statement list = + (* delegate parsing to [Tip_parser] *) + parse_file_exn file + |> CCList.flat_map (Convert.conv_statement ctx) + + let parse file = + let ctx = Convert.Ctx.create () in + try Result.Ok (parse_file_exn ctx file) + with e -> Result.Error (Printexc.to_string e) + + let parse_stdin () = + let ctx = Convert.Ctx.create () in + try + parse_chan_exn ~filename:"" stdin + |> CCList.flat_map (Convert.conv_statement ctx) + |> CCResult.return + with e -> Result.Error (Printexc.to_string e) +end + +let parse = Parse.parse +let parse_stdin = Parse.parse_stdin + +(** {2 Conversion into {!Term.t}} *) + +module Subst = struct + type 'a t = 'a ID.Map.t + let empty = ID.Map.empty + let mem subst v = ID.Map.mem (A.Var.id v) subst + let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out + let add subst v t = + if mem subst v then ( + Util.errorf "%a already bound" A.Var.pp v; + ); + ID.Map.add (A.Var.id v) t subst + let find subst v = ID.Map.get (A.Var.id v) subst + let find_exn subst v = ID.Map.find (A.Var.id v) subst +end + +let mk_ite_id = + let n = ref 0 in + fun () -> ID.makef "ite_%d" (CCRef.incr_then_get n) + +let mk_sub_form = + let n = ref 0 in + fun () -> ID.makef "sub_form_%d" (CCRef.incr_then_get n) + +let mk_lra_id = + let n = ref 0 in + fun () -> ID.makef "lra_%d" (CCRef.incr_then_get n) + +type term_or_form = + | T of A.term + | Rat of RLE.t (* rational linear expression *) + +let[@inline] ret_t t = T t +let[@inline] ret_f f = F f +let[@inline] ret_rat t = Rat t +let[@inline] ret_any t = if Term.is_bool t then F (F.atom (Term.Bool.pa t)) else T t + +let conv_ty (reg:Reg.t) (ty:A.Ty.t) : Type.t = + let mk_ty = Reg.find_exn reg Mc2_unin_sort.k_make in + (* convert a type *) + let rec aux_ty (ty:A.Ty.t) : Type.t = match ty with + | A.Ty.Ty_bool -> Type.bool + | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat + | A.Ty.Atomic (id, args) -> mk_ty id (List.map aux_ty args) + | A.Ty.Arrow _ -> + Util.errorf "cannot convert arrow type `%a`" A.Ty.pp ty + in + aux_ty ty + +let conv_bool_term (reg:Reg.t) (t:A.term): atom list list = + let decl = Reg.find_exn reg Mc2_uf.k_decl in + (* polymorphic equality *) + let[@inline] mk_eq_ t u = Term.mk_eq t u in + let mk_app = Reg.find_exn reg Mc2_uf.k_app in + let mk_const = Reg.find_exn reg Mc2_uf.k_const in + let fresh = Reg.find_exn reg Mc2_propositional.k_fresh in + let mk_eq t u = Term.Bool.pa (mk_eq_ t u) in + let mk_neq t u = Term.Bool.na (mk_eq_ t u) in + let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in + let mk_lra_eq t u = mk_lra_pred Mc2_lra.Eq0 (RLE.diff t u) |> Term.Bool.pa in + let side_clauses : atom list list ref = ref [] in + (* introduce intermediate variable for LRA sub-expression *) + let mk_lra_expr (e:RLE.t): term = match RLE.as_const e, RLE.as_singleton e with + | Some n, _ -> Reg.find_exn reg Mc2_lra.k_make_const n + | None, Some (n,t) when Q.equal n Q.one -> t + | _ -> + let id = mk_lra_id() in + Log.debugf 30 + (fun k->k"(@[smtlib.name_lra@ %a@ :as %a@])" RLE.pp e ID.pp id); + decl id [] (Reg.find_exn reg Mc2_lra.k_rat); + let t = mk_const id in + side_clauses := [mk_lra_eq (RLE.singleton1 t) e] :: !side_clauses; + t + in + (* adaptative equality *) + let mk_eq_t_tf (t:term) (u:term_or_form) : F.t = match u with + | F u -> F.equiv (F.atom (Term.Bool.pa t)) u + | T u when Term.is_bool u -> + F.equiv (F.atom (Term.Bool.pa t)) (F.atom (Term.Bool.pa u)) + | T u -> mk_eq t u |> F.atom + | Rat u -> mk_lra_eq (RLE.singleton1 t) u |> F.atom + and mk_eq_tf_tf (t:term_or_form) (u:term_or_form) = match t, u with + | T t, T u -> mk_eq t u |> F.atom + | T t, Rat u | Rat u, T t -> mk_lra_eq (RLE.singleton1 t) u |> F.atom + | Rat t, Rat u -> mk_lra_eq t u |> F.atom + | F t, F u -> F.equiv t u + | _ -> assert false + in + (* convert term *) + let rec aux (subst:term_or_form Subst.t) (t:A.term) : term_or_form = + begin match A.term_view t with + | A.Var v -> + begin match Subst.find subst v with + | None -> Util.errorf "variable %a not bound" A.Var.pp v + | Some t -> t + end + | A.Const id -> mk_const id |> ret_any + | A.App (f, l) -> + let l = List.map (aux_t subst) l in + begin match A.term_view f with + | A.Const id -> mk_app id l |> ret_any + | _ -> Util.errorf "cannot process HO application %a" A.pp_term t + end + | A.If (a,b,c) -> + let a = aux_form subst a in + let b = aux subst b in + let c = aux subst c in + let ty_b = match b with + | F _ -> Type.bool + | T t -> Term.ty t + | Rat _ -> Reg.find_exn reg Mc2_lra.k_rat + in + let placeholder_id = mk_ite_id () in + Log.debugf 30 + (fun k->k"(@[smtlib.name_term@ %a@ :as %a@])" A.pp_term t ID.pp placeholder_id); + decl placeholder_id [] ty_b; + let placeholder = mk_const placeholder_id in + (* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *) + let form = + F.and_ + [ F.imply a (mk_eq_t_tf placeholder b); + F.imply (F.not_ a) (mk_eq_t_tf placeholder c); + ] + in + side_clauses := List.rev_append (mk_cnf form) !side_clauses; + ret_t placeholder + | A.Let (v,t,u) -> + let subst = Subst.add subst v (aux subst t) in + aux subst u + | A.Op (A.And, l) -> F.and_ (List.map (aux_form subst) l) |> ret_f + | A.Op (A.Or, l) -> F.or_ (List.map (aux_form subst) l) |> ret_f + | A.Op (A.Imply, l) -> + let rec curry_imply_ = function + | [] -> assert false + | [a] -> aux_form subst a + | a :: b -> F.imply (aux_form subst a) (curry_imply_ b) + in + curry_imply_ l |> ret_f + | A.Op (A.Eq, l) -> + let l = List.map (aux subst) l in + let rec curry_eq = function + | [] | [_] -> assert false + | [a;b] -> [mk_eq_tf_tf a b] + | a :: b :: tail -> + mk_eq_tf_tf a b :: curry_eq (b::tail) + in + F.and_ (curry_eq l) |> ret_f + | A.Op (A.Distinct, l) -> + (* TODO: more efficient "distinct"? *) + List.map (aux_t subst) l + |> CCList.diagonal + |> List.map (fun (t,u) -> mk_neq t u |> F.atom) + |> F.and_ |> ret_f + | A.Not f -> F.not_ (aux_form subst f) |> ret_f + | A.Bool_term true -> ret_f F.true_ + | A.Bool_term false -> ret_f F.false_ + | A.Num_q n -> Mc2_lra.LE.const n |> ret_rat + | A.Num_z n -> Mc2_lra.LE.const (Q.of_bigint n) |> ret_rat + | A.Arith (op, l) -> + let l = List.map (aux_rat subst) l in + begin match op, l with + | A.Minus, [a] -> RLE.neg a |> ret_rat + | _, [] | _, [_] -> + Util.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t + | A.Leq, [a;b] -> + let e = RLE.diff a b in + mk_lra_pred Mc2_lra.Leq0 e |> ret_any + | A.Geq, [a;b] -> + let e = RLE.diff b a in + mk_lra_pred Mc2_lra.Leq0 e |> ret_any + | A.Lt, [a;b] -> + let e = RLE.diff a b in + mk_lra_pred Mc2_lra.Lt0 e |> ret_any + | A.Gt, [a;b] -> + let e = RLE.diff b a in + mk_lra_pred Mc2_lra.Lt0 e |> ret_any + | (A.Leq | A.Lt | A.Geq | A.Gt), _ -> + Util.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t + | A.Add, _ -> + let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in + mk_lra_expr e |> ret_t + | A.Minus, a::tail -> + let e = + List.fold_left + (fun n t -> RLE.diff n t) + a tail + in + mk_lra_expr e |> ret_t + | A.Mult, _::_::_ -> + let coeffs, terms = + CCList.partition_map + (fun t -> match RLE.as_const t with + | None -> `Right t + | Some c -> `Left c) + l + in + begin match coeffs, terms with + | c::c_tail, [] -> + List.fold_right RLE.mult c_tail (RLE.const c) |> ret_rat + | _, [t] -> + List.fold_right RLE.mult coeffs t |> ret_rat + | _ -> + Util.errorf "non-linear expr:@ `%a`" A.pp_term t + end + | A.Div, (first::l) -> + (* support t/a/b/c where only [t] is a rational *) + let coeffs = + List.map + (fun c -> match RLE.as_const c with + | None -> + Util.errorf "non-linear expr:@ `%a`" A.pp_term t + | Some c -> Q.inv c) + l + in + List.fold_right RLE.mult coeffs first |> ret_rat + end + | A.Select _ -> assert false (* TODO *) + | A.Match _ -> assert false (* TODO *) + | A.Bind _ -> assert false (* TODO *) + end + + (* expect a term *) + and aux_t subst (t:A.term) : term = match aux subst t with + | T t -> t + | Rat e -> mk_lra_expr e + | F (F.Lit a) when Atom.is_pos a -> Atom.term a + | F f -> + (* name the sub-formula and add CNF *) + let placeholder_id = mk_sub_form() in + decl placeholder_id [] Type.bool; + let placeholder = mk_const placeholder_id in + (* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *) + let form = F.equiv (F.atom (Term.Bool.pa placeholder)) f in + side_clauses := List.rev_append (mk_cnf form) !side_clauses; + placeholder + + (* convert formula *) + and aux_form subst (t:A.term): F.t = match aux subst t with + | T t -> F.atom (Term.Bool.pa t) + | F f -> f + | Rat _ -> Util.errorf "expected proposition,@ got %a" A.pp_term t + + (* expect a rational expr *) + and aux_rat subst (t:A.term) : RLE.t = match aux subst t with + | Rat e -> e + | T t -> RLE.singleton1 t + | F _ -> assert false + + and mk_cnf (f:F.t) : atom list list = + F.cnf ~fresh f + in + let cs = aux_form Subst.empty t |> mk_cnf in + List.rev_append !side_clauses cs + +(** {2 Processing Statements} *) + +(* list of (local) hypothesis *) +let hyps = ref [] + +let check_model state : bool = + Log.debug 4 "checking model"; + let check_clause c = + Log.debugf 15 + (fun k -> k "(@[check.clause@ %a@])" Clause.debug_atoms c); + let ok = + List.exists (fun t -> Solver.Sat_state.eval_opt state t = Some true) c + in + if not ok then ( + Log.debugf 0 + (fun k->k "(@[check.fail:@ clause %a@ not satisfied in model@])" Clause.debug_atoms c); + ); + ok + in + Solver.Sat_state.check_model state && + List.for_all check_clause !hyps + +module Dot = Mc2_backend.Dot.Make(Mc2_backend.Dot.Default) + +(* call the solver to check-sat *) +let solve + ?gc ?restarts ?dot_proof + ?(pp_model=false) ?(check=false) ?time ?memory ?progress + ~assumptions s : unit = + let t1 = Sys.time() in + let res = Solver.solve ?gc ?restarts ?time ?memory ?progress s ~assumptions in + let t2 = Sys.time () in + begin match res with + | Solver.Sat state -> + if pp_model then ( + let pp_t out = function + | A_bool (t,b) -> Fmt.fprintf out "(@[%a@ %B@])" Term.pp t b + | A_semantic (t,v) -> Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Value.pp v + in + Format.printf "(@[model@ %a@])@." + (Util.pp_list pp_t) (Solver.Sat_state.model state) + ); + if check then ( + if not (check_model state) then ( + Util.error "invalid model" + ) + ); + let t3 = Sys.time () -. t2 in + Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; + | Solver.Unsat state -> + if check then ( + let p = Solver.Unsat_state.get_proof state in + Proof.check p; + begin match dot_proof with + | None -> () + | Some file -> + CCIO.with_out file + (fun oc -> + Log.debugf 1 (fun k->k "write proof into `%s`" file); + let fmt = Format.formatter_of_out_channel oc in + Dot.print fmt p; + Format.pp_print_flush fmt (); flush oc) + end + ); + let t3 = Sys.time () -. t2 in + Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; + end + +(* process a single statement *) +let process_stmt + ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check + ?time ?memory ?progress + (solver:Solver.t) + (stmt:Ast.statement) : unit or_error = + Log.debugf 5 + (fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt); + let decl_sort = Solver.get_service_exn solver Mc2_unin_sort.k_decl_sort in + let decl = Solver.get_service_exn solver Mc2_uf.k_decl in + let conv_ty = conv_ty (Solver.services solver) in + begin match stmt with + | A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return () + | A.SetLogic s -> + Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s); + E.return () + | A.SetOption l -> + Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l); + E.return () + | A.SetInfo _ -> E.return () + | A.Exit -> + Log.debug 1 "exit"; + raise Exit + | A.CheckSat -> + solve ?gc ?restarts ?dot_proof ?check ?pp_model ?time ?memory ?progress + solver ~assumptions:[]; + E.return() + | A.TyDecl (id,n) -> + decl_sort id n; + E.return () + | A.Decl (f,ty) -> + let ty_args, ty_ret = A.Ty.unfold ty in + let ty_args = List.map conv_ty ty_args in + let ty_ret = conv_ty ty_ret in + decl f ty_args ty_ret; + E.return () + | A.Assert t -> + let clauses = + conv_bool_term (Solver.services solver) t + in + if pp_cnf then ( + Format.printf "(@[assert@ %a@])@." + (Util.pp_list Clause.pp_atoms) clauses; + ); + hyps := clauses @ !hyps; + Solver.assume solver clauses; + E.return() + | A.Goal (_, _) -> + Util.errorf "cannot deal with goals yet" + + (* + | Dolmen.Statement.Def (id, t) -> T.def id t + | Dolmen.Statement.Decl (id, t) -> T.decl id t + | Dolmen.Statement.Consequent t -> + let cnf = T.consequent t in + pp_cnf solver cnf; + hyps := cnf @ !hyps; + S.assume s cnf + | Dolmen.Statement.Antecedent t -> + let cnf = T.antecedent t in + pp_cnf cnf; + hyps := cnf @ !hyps; + S.assume cnf + | Dolmen.Statement.Pack [ + { Dolmen.Statement.descr = Dolmen.Statement.Push 1; _ }; + { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; _ }; + { Dolmen.Statement.descr = Dolmen.Statement.Prove; _ }; + { Dolmen.Statement.descr = Dolmen.Statement.Pop 1; _ }; + ] -> + let assumptions = T.assumptions f in + prove solver ~assumptions + | Dolmen.Statement.Prove -> + prove solver ~assumptions:[] + | Dolmen.Statement.Set_info _ + | Dolmen.Statement.Set_logic _ -> () + | Dolmen.Statement.Exit -> exit 0 + | _ -> + Format.printf "Command not supported:@\n%a@." + Dolmen.Statement.print s + *) + end + diff --git a/src/smtlib/Dagon_smtlib.mli b/src/smtlib/Dagon_smtlib.mli new file mode 100644 index 00000000..f6f73029 --- /dev/null +++ b/src/smtlib/Dagon_smtlib.mli @@ -0,0 +1,34 @@ + +(** {1 SMTLib-2 Interface} *) + +(** This library provides a parser, a type-checker, and a solver interface + for processing SMTLib-2 problems. +*) + +type 'a or_error = ('a, string) CCResult.t + +module Ast = Ast + +val parse : string -> Dagon_smt.Ast.statement list or_error + +val parse_stdin : unit -> Dagon_smt.Ast.statement list or_error + +val conv_bool_term : Dagon_smt.Term.state -> Dagon_smt.Ast.term -> Dagon_smt.Lit.t list list +(** Convert a boolean term into CNF *) + +val process_stmt : + ?gc:bool -> + ?restarts:bool -> + ?pp_cnf:bool -> + ?dot_proof:string -> + ?pp_model:bool -> + ?check:bool -> + ?time:float -> + ?memory:float -> + ?progress:bool -> + Dagon_smt.Solver.t -> + Dagon_smt.Ast.statement -> + unit or_error +(** Process the given statement. + @raise Incorrect_model if model is not correct +*) diff --git a/src/smtlib/Lexer.mll b/src/smtlib/Lexer.mll new file mode 100644 index 00000000..72d7b7cd --- /dev/null +++ b/src/smtlib/Lexer.mll @@ -0,0 +1,95 @@ + +(* This file is free software. See file "license" for more details. *) + +(** {1 Lexer for TIP} *) + +{ + module A = Parse_ast + module Loc = Locations + open Parser (* for tokens *) + +} + +let printable_char = [^ '\n'] +let comment_line = ';' printable_char* + +let sym = [^ '"' '(' ')' '\\' ' ' '\t' '\r' '\n'] + +let ident = sym+ + +let quoted = '"' ([^ '"'] | '\\' '"')* '"' +let escaped = '|' [^ '|']* '|' + +rule token = parse + | eof { EOI } + | '\n' { Lexing.new_line lexbuf; token lexbuf } + | [' ' '\t' '\r'] { token lexbuf } + | comment_line { token lexbuf } + | '(' { LEFT_PAREN } + | ')' { RIGHT_PAREN } + | "true" { TRUE } + | "false" { FALSE } + | "or" { OR } + | "and" { AND } + | "not" { NOT } + | "xor" { XOR } + | "distinct" { DISTINCT } + | "ite" { IF } + | "as" { AS } + | "match" { MATCH } + | "case" { CASE } + | "default" { DEFAULT } + | "lambda" { FUN } + | "let" { LET } + | "par" { PAR } + | "=>" { ARROW } + | "=" { EQ } + | "@" { AT } + | "+" { ADD } + | "-" { MINUS } + | "*" { PROD } + | "/" { DIV } + | "<=" { LEQ } + | "<" { LT } + | ">=" { GEQ } + | ">" { GT } + | "declare-datatypes" { DATA } + | "assert" { ASSERT } + | "lemma" { LEMMA } + | "assert-not" { ASSERT_NOT } + | "declare-sort" { DECLARE_SORT } + | "declare-fun" { DECLARE_FUN } + | "declare-const" { DECLARE_CONST } + | "define-fun" { DEFINE_FUN } + | "define-fun-rec" { DEFINE_FUN_REC } + | "define-funs-rec" { DEFINE_FUNS_REC } + | "forall" { FORALL } + | "exists" { EXISTS } + | "check-sat" { CHECK_SAT } + | "set-logic" { SET_LOGIC } + | "set-option" { SET_OPTION } + | "set-info" { SET_INFO } + | "exit" { EXIT } + | ident { + let s = Lexing.lexeme lexbuf in + IDENT(s) + } + | quoted { + (* TODO: unescape *) + let s = Lexing.lexeme lexbuf in + let s = String.sub s 1 (String.length s -2) in (* remove " " *) + QUOTED s } + | escaped { + let s = Lexing.lexeme lexbuf in + CCString.iter (function '\n' -> Lexing.new_line lexbuf | _ -> ()) s; + let s = String.sub s 1 (String.length s -2) in (* remove "|" *) + ESCAPED s } + | _ as c + { + let loc = Loc.of_lexbuf lexbuf in + A.parse_errorf ~loc "unexpected char '%c'" c + } + +{ + +} diff --git a/src/smtlib/Locations.ml b/src/smtlib/Locations.ml new file mode 100644 index 00000000..34f7efb5 --- /dev/null +++ b/src/smtlib/Locations.ml @@ -0,0 +1,71 @@ + +(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *) + +(** {1 Locations} *) + +type t = { + file : string; + start_line : int; + start_column : int; + stop_line : int; + stop_column : int; +} + +let mk file start_line start_column stop_line stop_column = + { file; start_line; start_column; stop_line; stop_column; } + +let mk_pair file (a,b)(c,d) = mk file a b c d + +let mk_pos start stop = + let open Lexing in + mk + start.pos_fname + start.pos_lnum (start.pos_cnum - start.pos_bol) + stop.pos_lnum (stop.pos_cnum - stop.pos_bol) + +let equal = (=) + +let pp out pos = + if pos.start_line = pos.stop_line + then + Format.fprintf out "file '%s': line %d, col %d to %d" + pos.file pos.start_line pos.start_column pos.stop_column + else + Format.fprintf out "file '%s': line %d, col %d to line %d, col %d" + pos.file + pos.start_line pos.start_column + pos.stop_line pos.stop_column + +let pp_opt out = function + | None -> Format.fprintf out "" + | Some pos -> pp out pos + +let pp_to_string pp x = + let buf = Buffer.create 64 in + let fmt = Format.formatter_of_buffer buf in + pp fmt x; + Format.pp_print_flush fmt (); + Buffer.contents buf + +let to_string_opt = pp_to_string pp_opt + +(** {2 Lexbuf} *) + +let set_file buf filename = + let open Lexing in + buf.lex_curr_p <- {buf.lex_curr_p with pos_fname=filename;}; + () + +let get_file buf = + let open Lexing in + buf.lex_curr_p.pos_fname + +let of_lexbuf lexbuf = + let start = Lexing.lexeme_start_p lexbuf in + let end_ = Lexing.lexeme_end_p lexbuf in + let s_l = start.Lexing.pos_lnum in + let s_c = start.Lexing.pos_cnum - start.Lexing.pos_bol in + let e_l = end_.Lexing.pos_lnum in + let e_c = end_.Lexing.pos_cnum - end_.Lexing.pos_bol in + let file = get_file lexbuf in + mk file s_l s_c e_l e_c diff --git a/src/smtlib/Parse_ast.ml b/src/smtlib/Parse_ast.ml new file mode 100644 index 00000000..821730dc --- /dev/null +++ b/src/smtlib/Parse_ast.ml @@ -0,0 +1,294 @@ + +(* This file is free software. See file "license" for more details. *) + +(** {1 Simple AST for parsing} *) + +module Loc = Locations +module Fmt = CCFormat + +let pp_str = Format.pp_print_string + +let pp_to_string pp x = + let buf = Buffer.create 64 in + let fmt = Format.formatter_of_buffer buf in + pp fmt x; + Format.pp_print_flush fmt (); + Buffer.contents buf + +type var = string +type ty_var = string + +(** Polymorphic types *) +type ty = + | Ty_bool + | Ty_app of ty_var * ty list + | Ty_arrow of ty list * ty + +type typed_var = var * ty + +type arith_op = + | Leq + | Lt + | Geq + | Gt + | Add + | Minus + | Mult + | Div + +(** {2 AST: S-expressions with locations} *) +type term = + | True + | False + | Const of string + | Arith of arith_op * term list + | App of string * term list + | HO_app of term * term (* higher-order application *) + | Match of term * match_branch list + | If of term * term * term + | Let of (var * term) list * term + | Fun of typed_var * term + | Eq of term * term + | Imply of term * term + | And of term list + | Or of term list + | Not of term + | Xor of term * term + | Distinct of term list + | Cast of term * ty (* type cast *) + | Forall of (var * ty) list * term + | Exists of (var * ty) list * term + +and match_branch = + | Match_default of term + | Match_case of string * var list * term + +type cstor = { + cstor_name: string; + cstor_args: (string * ty) list; (* selector+type *) +} + +type 'arg fun_decl = { + fun_ty_vars: ty_var list; + fun_name: string; + fun_args: 'arg list; + fun_ret: ty; +} + +type fun_def = { + fr_decl: typed_var fun_decl; + fr_body: term; +} + +type funs_rec_def = { + fsr_decls: typed_var fun_decl list; + fsr_bodies: term list; +} + +type statement = { + stmt: stmt; + loc: Loc.t option; +} + +and stmt = + | Stmt_decl_sort of string * int (* arity *) + | Stmt_decl of ty fun_decl + | Stmt_fun_def of fun_def + | Stmt_fun_rec of fun_def + | Stmt_funs_rec of funs_rec_def + | Stmt_data of ty_var list * (string * cstor list) list + | Stmt_assert of term + | Stmt_lemma of term + | Stmt_assert_not of ty_var list * term + | Stmt_set_logic of string + | Stmt_set_option of string list + | Stmt_set_info of string list + | Stmt_check_sat + | Stmt_exit + +let ty_bool = Ty_bool +let ty_app s l = Ty_app (s,l) +let ty_const s = ty_app s [] +let ty_arrow_l args ret = if args=[] then ret else Ty_arrow (args, ret) +let ty_arrow a b = ty_arrow_l [a] b + +let true_ = True +let false_ = False +let const s = Const s +let app f l = App (f,l) +let ho_app a b = HO_app (a,b) +let ho_app_l a l = List.fold_left ho_app a l +let match_ u l = Match (u,l) +let if_ a b c = If(a,b,c) +let fun_ v t = Fun (v,t) +let fun_l = List.fold_right fun_ +let let_ l t = Let (l,t) +let eq a b = Eq (a,b) +let imply a b = Imply(a,b) +let xor a b = Xor (a,b) +let and_ l = And l +let or_ l = Or l +let distinct l = Distinct l +let cast t ~ty = Cast (t, ty) +let forall vars f = match vars with [] -> f | _ -> Forall (vars, f) +let exists vars f = match vars with [] -> f | _ -> Exists (vars, f) +let rec not_ t = match t with + | Forall (vars,u) -> exists vars (not_ u) + | Exists (vars,u) -> forall vars (not_ u) + | _ -> Not t + +let arith op l = Arith (op,l) + +let _mk ?loc stmt = { loc; stmt } + +let mk_cstor name l : cstor = { cstor_name=name; cstor_args=l } +let mk_fun_decl ~ty_vars f args ret = + { fun_ty_vars=ty_vars; fun_name=f; + fun_args=args; fun_ret=ret; } +let mk_fun_rec ~ty_vars f args ret body = + { fr_decl=mk_fun_decl ~ty_vars f args ret; fr_body=body; } + +let decl_sort ?loc s ~arity = _mk ?loc (Stmt_decl_sort (s, arity)) +let decl_fun ?loc ~tyvars f ty_args ty_ret = + let d = {fun_ty_vars=tyvars; fun_name=f; fun_args=ty_args; fun_ret=ty_ret} in + _mk ?loc (Stmt_decl d) +let fun_def ?loc fr = _mk ?loc (Stmt_fun_def fr) +let fun_rec ?loc fr = _mk ?loc (Stmt_fun_rec fr) +let funs_rec ?loc decls bodies = _mk ?loc (Stmt_funs_rec {fsr_decls=decls; fsr_bodies=bodies}) +let data ?loc tyvars l = _mk ?loc (Stmt_data (tyvars,l)) +let assert_ ?loc t = _mk ?loc (Stmt_assert t) +let lemma ?loc t = _mk ?loc (Stmt_lemma t) +let assert_not ?loc ~ty_vars t = _mk ?loc (Stmt_assert_not (ty_vars, t)) +let set_logic ?loc s = _mk ?loc (Stmt_set_logic s) +let set_option ?loc l = _mk ?loc (Stmt_set_option l) +let set_info ?loc l = _mk ?loc (Stmt_set_info l) +let check_sat ?loc () = _mk ?loc Stmt_check_sat +let exit ?loc () = _mk ?loc Stmt_exit + +let loc t = t.loc +let view t = t.stmt + +let fpf = Format.fprintf + + +let pp_tyvar = pp_str + +let rec pp_ty out (ty:ty) = match ty with + | Ty_bool -> pp_str out "Bool" + | Ty_app (s,[]) -> pp_str out s + | Ty_app (s,l) -> Format.fprintf out "(@[%s@ %a@])" s (Util.pp_list pp_ty) l + | Ty_arrow (args,ret) -> + fpf out "(@[=>@ %a@ %a@])" (Util.pp_list pp_ty) args pp_ty ret + +let pp_arith out = function + | Leq -> Fmt.string out "<=" + | Lt -> Fmt.string out "<" + | Geq -> Fmt.string out ">=" + | Gt -> Fmt.string out ">" + | Add -> Fmt.string out "+" + | Minus -> Fmt.string out "-" + | Mult -> Fmt.string out "*" + | Div -> Fmt.string out "/" + +let rec pp_term out (t:term) = match t with + | True -> pp_str out "true" + | False -> pp_str out "false" + | Arith (op,l) -> + Fmt.fprintf out "(@[%a@ %a@])" pp_arith op (Util.pp_list pp_term) l + | Const s -> pp_str out s + | App (f,l) -> fpf out "(@[<1>%s@ %a@])" f (Util.pp_list pp_term) l + | HO_app (a,b) -> fpf out "(@[<1>@@@ %a@ %a@])" pp_term a pp_term b + | Match (lhs,cases) -> + let pp_case out = function + | Match_default rhs -> fpf out "(@[<1>case default@ %a@])" pp_term rhs + | Match_case (c,[],rhs) -> + fpf out "(@[<1>case %s@ %a@])" c pp_term rhs + | Match_case (c,vars,rhs) -> + fpf out "(@[<1>case@ (@[%s@ %a@])@ %a@])" c (Util.pp_list pp_str) vars pp_term rhs + in + fpf out "(@[<1>match@ %a@ @[%a@]@])" pp_term lhs + (Util.pp_list pp_case) cases + | If (a,b,c) -> fpf out "(@[ite %a@ %a@ %a@])" pp_term a pp_term b pp_term c + | Fun (v,body) -> fpf out "(@[<1>lambda @ (%a)@ %a@])" pp_typed_var v pp_term body + | Let (l,t) -> + let pp_binding out (v,t) = fpf out "(@[%s@ %a@])" v pp_term t in + fpf out "(@[let@ (@[%a@])@ %a@])" (Util.pp_list pp_binding) l pp_term t + | Eq (a,b) -> fpf out "(@[=@ %a@ %a@])" pp_term a pp_term b + | Imply (a,b) -> fpf out "(@[=>@ %a@ %a@])" pp_term a pp_term b + | Xor(a,b) -> fpf out "(@[xor@ %a@ %a@])" pp_term a pp_term b + | And l -> fpf out "(@[and@ %a@])" (Util.pp_list pp_term) l + | Or l -> fpf out "(@[or@ %a@])" (Util.pp_list pp_term) l + | Not t -> fpf out "(not %a)" pp_term t + | Distinct l -> fpf out "(@[distinct@ %a@])" (Util.pp_list pp_term) l + | Cast (t, ty) -> fpf out "(@[as@ @[%a@]@ @[%a@]@])" pp_term t pp_ty ty + | Forall (vars,f) -> + fpf out "(@[forall@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f + | Exists (vars,f) -> + fpf out "(@[exists@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f +and pp_typed_var out (v,ty) = + fpf out "(@[%s@ %a@])" v pp_ty ty + +let pp_par pp_x out (ty_vars,x) = match ty_vars with + | [] -> pp_x out x + | _ -> + fpf out "(@[<1>par (@[%a@])@ (%a)@])" (Util.pp_list pp_tyvar) ty_vars pp_x x + +let pp_fun_decl pp_arg out fd = + fpf out "%s@ (@[%a@])@ %a" + fd.fun_name (Util.pp_list pp_arg) fd.fun_args pp_ty fd.fun_ret + +let pp_fr out fr = + fpf out "@[<1>%a@ %a@]" (pp_fun_decl pp_typed_var) fr.fr_decl pp_term fr.fr_body + +let pp_stmt out (st:statement) = match view st with + | Stmt_set_logic s -> fpf out "(@[declare-logic@ %s@])" s + | Stmt_set_option l -> fpf out "(@[set-option@ %a@])" (Util.pp_list CCFormat.string) l + | Stmt_set_info l -> fpf out "(@[set-info@ %a@])" (Util.pp_list CCFormat.string) l + | Stmt_decl_sort (s,n) -> fpf out "(@[declare-sort@ %s %d@])" s n + | Stmt_assert t -> fpf out "(@[assert@ %a@])" pp_term t + | Stmt_lemma t -> fpf out "(@[lemma@ %a@])" pp_term t + | Stmt_assert_not (ty_vars,t) -> + fpf out "(@[assert-not@ %a@])" (pp_par pp_term) (ty_vars,t) + | Stmt_decl d -> + fpf out "(@[declare-fun@ %a@])" + (pp_par (pp_fun_decl pp_ty)) (d.fun_ty_vars,d) + | Stmt_fun_def fr -> + fpf out "(@[<1>define-fun@ %a@])" + (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr) + | Stmt_fun_rec fr -> + fpf out "(@[<1>define-fun-rec@ %a@])" + (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr) + | Stmt_funs_rec fsr -> + let pp_decl' out d = fpf out "(@[<1>%a@])" (pp_fun_decl pp_typed_var) d in + fpf out "(@[define-funs-rec@ (@[%a@])@ (@[%a@])@])" + (Util.pp_list pp_decl') fsr.fsr_decls (Util.pp_list pp_term) fsr.fsr_bodies + | Stmt_data (tyvars,l) -> + let pp_cstor_arg out (sel,ty) = fpf out "(@[%s %a@])" sel pp_ty ty in + let pp_cstor out c = + if c.cstor_args = [] + then fpf out "(%s)" c.cstor_name + else fpf out "(@[<1>%s@ %a@])" c.cstor_name (Util.pp_list pp_cstor_arg) c.cstor_args + in + let pp_data out (s,cstors) = + fpf out "(@[<1>%s@ @[%a@]@])" s (Util.pp_list pp_cstor) cstors + in + fpf out "(@[declare-datatypes@ (@[%a@])@ (@[%a@])@])" + (Util.pp_list pp_tyvar) tyvars (Util.pp_list pp_data) l + | Stmt_check_sat -> pp_str out "(check-sat)" + | Stmt_exit -> pp_str out "(exit)" + +(** {2 Errors} *) + +exception Parse_error of Loc.t option * string + +let () = Printexc.register_printer + (function + | Parse_error (loc, msg) -> + let pp out () = + Format.fprintf out "parse error at %a:@ %s" Loc.pp_opt loc msg + in + Some (pp_to_string pp ()) + | _ -> None) + +let parse_error ?loc msg = raise (Parse_error (loc, msg)) +let parse_errorf ?loc msg = Format.ksprintf (parse_error ?loc) msg diff --git a/src/smtlib/Parser.mly b/src/smtlib/Parser.mly new file mode 100644 index 00000000..df5e193b --- /dev/null +++ b/src/smtlib/Parser.mly @@ -0,0 +1,377 @@ + + +(* This file is free software, part of tip-parser. See file "license" for more details. *) + +(** {1 Parser for TIP} *) + +(* vim:SyntasticToggleMode: + vim:set ft=yacc: *) + +%{ + module A = Parse_ast + module Loc = Locations + +%} + +%token EOI + +%token LEFT_PAREN +%token RIGHT_PAREN + +%token PAR +%token ARROW + +%token TRUE +%token FALSE +%token OR +%token AND +%token XOR +%token DISTINCT +%token NOT +%token EQ +%token IF +%token MATCH +%token CASE +%token DEFAULT +%token FUN +%token LET +%token AS +%token AT + +%token LEQ +%token LT +%token GEQ +%token GT +%token ADD +%token MINUS +%token PROD +%token DIV + +%token SET_LOGIC +%token SET_OPTION +%token SET_INFO +%token DATA +%token ASSERT +%token LEMMA +%token ASSERT_NOT +%token FORALL +%token EXISTS +%token DECLARE_SORT +%token DECLARE_CONST +%token DECLARE_FUN +%token DEFINE_FUN +%token DEFINE_FUN_REC +%token DEFINE_FUNS_REC +%token CHECK_SAT +%token EXIT + +%token IDENT +%token QUOTED +%token ESCAPED + +%start parse_term +%start parse_ty +%start parse +%start parse_list + +%% + +parse_list: l=stmt* EOI {l} +parse: t=stmt EOI { t } +parse_term: t=term EOI { t } +parse_ty: t=ty EOI { t } + +cstor_arg: + | LEFT_PAREN name=id ty=ty RIGHT_PAREN { name, ty } + +cstor: + | LEFT_PAREN c=id RIGHT_PAREN { A.mk_cstor c [] } + | LEFT_PAREN c=id l=cstor_arg+ RIGHT_PAREN + { A.mk_cstor c l } + +data: + | LEFT_PAREN s=id l=cstor+ RIGHT_PAREN { s,l } + +fun_def_mono: + | f=id + LEFT_PAREN args=typed_var* RIGHT_PAREN + ret=ty + { f, args, ret } + +fun_decl_mono: + | f=id + LEFT_PAREN args=ty* RIGHT_PAREN + ret=ty + { f, args, ret } + +fun_decl: + | tup=fun_decl_mono { let f, args, ret = tup in [], f, args, ret } + | LEFT_PAREN + PAR + LEFT_PAREN tyvars=tyvar* RIGHT_PAREN + LEFT_PAREN tup=fun_decl_mono RIGHT_PAREN + RIGHT_PAREN + { let f, args, ret = tup in tyvars, f, args, ret } + +fun_rec: + | tup=fun_def_mono body=term + { + let f, args, ret = tup in + A.mk_fun_rec ~ty_vars:[] f args ret body + } + | LEFT_PAREN + PAR + LEFT_PAREN l=tyvar* RIGHT_PAREN + LEFT_PAREN tup=fun_def_mono body=term RIGHT_PAREN + RIGHT_PAREN + { + let f, args, ret = tup in + A.mk_fun_rec ~ty_vars:l f args ret body + } + +funs_rec_decl: + | LEFT_PAREN tup=fun_def_mono RIGHT_PAREN + { + let f, args, ret = tup in + A.mk_fun_decl ~ty_vars:[] f args ret + } + | LEFT_PAREN + PAR + LEFT_PAREN l=tyvar* RIGHT_PAREN + LEFT_PAREN tup=fun_def_mono RIGHT_PAREN + RIGHT_PAREN + { + let f, args, ret = tup in + A.mk_fun_decl ~ty_vars:l f args ret + } + +assert_not: + | LEFT_PAREN + PAR LEFT_PAREN tyvars=tyvar+ RIGHT_PAREN t=term + RIGHT_PAREN + { tyvars, t } + | t=term + { [], t } + +id: + | s=IDENT { s } + | s=QUOTED { s } + | s=ESCAPED { s } + +stmt: + | LEFT_PAREN SET_LOGIC s=id RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.set_logic ~loc s + } + | LEFT_PAREN SET_OPTION l=id+ RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.set_option ~loc l + } + | LEFT_PAREN SET_INFO l=id+ RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.set_info ~loc l + } + | LEFT_PAREN ASSERT t=term RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.assert_ ~loc t + } + | LEFT_PAREN LEMMA t=term RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.lemma ~loc t + } + | LEFT_PAREN DECLARE_SORT s=id n=id RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + try + let n = int_of_string n in + A.decl_sort ~loc s ~arity:n + with Failure _ -> + A.parse_errorf ~loc "expected arity to be an integer, not `%s`" n + } + | LEFT_PAREN DATA + LEFT_PAREN vars=tyvar* RIGHT_PAREN + LEFT_PAREN l=data+ RIGHT_PAREN + RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.data ~loc vars l + } + | LEFT_PAREN DECLARE_FUN tup=fun_decl RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + let tyvars, f, args, ret = tup in + A.decl_fun ~loc ~tyvars f args ret + } + | LEFT_PAREN DECLARE_CONST f=id ty=ty RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.decl_fun ~loc ~tyvars:[] f [] ty + } + | LEFT_PAREN DEFINE_FUN f=fun_rec RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.fun_def ~loc f + } + | LEFT_PAREN + DEFINE_FUN_REC + f=fun_rec + RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.fun_rec ~loc f + } + | LEFT_PAREN + DEFINE_FUNS_REC + LEFT_PAREN decls=funs_rec_decl+ RIGHT_PAREN + LEFT_PAREN bodies=term+ RIGHT_PAREN + RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.funs_rec ~loc decls bodies + } + | LEFT_PAREN + ASSERT_NOT + tup=assert_not + RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + let ty_vars, f = tup in + A.assert_not ~loc ~ty_vars f + } + | LEFT_PAREN CHECK_SAT RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.check_sat ~loc () + } + | LEFT_PAREN EXIT RIGHT_PAREN + { + let loc = Loc.mk_pos $startpos $endpos in + A.exit ~loc () + } + | error + { + let loc = Loc.mk_pos $startpos $endpos in + A.parse_errorf ~loc "expected statement" + } + +var: + | s=id { s } +tyvar: + | s=id { s } + +ty: + | s=id { + begin match s with + | "Bool" -> A.ty_bool + | _ -> A.ty_const s + end + } + | LEFT_PAREN s=id args=ty+ RIGHT_PAREN + { A.ty_app s args } + | LEFT_PAREN ARROW tup=ty_arrow_args RIGHT_PAREN + { + let args, ret = tup in + A.ty_arrow_l args ret } + | error + { + let loc = Loc.mk_pos $startpos $endpos in + A.parse_errorf ~loc "expected type" + } + +ty_arrow_args: + | a=ty ret=ty { [a], ret } + | a=ty tup=ty_arrow_args { a :: fst tup, snd tup } + +typed_var: + | LEFT_PAREN s=id ty=ty RIGHT_PAREN { s, ty } + +case: + | LEFT_PAREN + CASE + c=id + rhs=term + RIGHT_PAREN + { A.Match_case (c, [], rhs) } + | LEFT_PAREN + CASE + LEFT_PAREN c=id vars=var+ RIGHT_PAREN + rhs=term + RIGHT_PAREN + { A.Match_case (c, vars, rhs) } + | LEFT_PAREN + CASE DEFAULT rhs=term + RIGHT_PAREN + { A.Match_default rhs } + +binding: + | LEFT_PAREN v=var t=term RIGHT_PAREN { v, t } + +term: + | TRUE { A.true_ } + | FALSE { A.false_ } + | s=id { A.const s } + | t=composite_term { t } + | error + { + let loc = Loc.mk_pos $startpos $endpos in + A.parse_errorf ~loc "expected term" + } + +%inline arith_op: + | ADD { A.Add } + | MINUS { A.Minus } + | PROD { A.Mult } + | DIV { A.Div } + | LEQ { A.Leq } + | LT { A.Lt } + | GEQ { A.Geq } + | GT { A.Gt } + +composite_term: + | LEFT_PAREN IF a=term b=term c=term RIGHT_PAREN { A.if_ a b c } + | LEFT_PAREN OR l=term+ RIGHT_PAREN { A.or_ l } + | LEFT_PAREN AND l=term+ RIGHT_PAREN { A.and_ l } + | LEFT_PAREN NOT t=term RIGHT_PAREN { A.not_ t } + | LEFT_PAREN DISTINCT l=term+ RIGHT_PAREN { A.distinct l } + | LEFT_PAREN EQ a=term b=term RIGHT_PAREN { A.eq a b } + | LEFT_PAREN ARROW a=term b=term RIGHT_PAREN { A.imply a b } + | LEFT_PAREN XOR a=term b=term RIGHT_PAREN { A.xor a b } + | LEFT_PAREN f=id args=term+ RIGHT_PAREN { A.app f args } + | LEFT_PAREN o=arith_op args=term+ RIGHT_PAREN { A.arith o args } + | LEFT_PAREN f=composite_term args=term+ RIGHT_PAREN { A.ho_app_l f args } + | LEFT_PAREN AT f=term arg=term RIGHT_PAREN { A.ho_app f arg } + | LEFT_PAREN + MATCH + lhs=term + l=case+ + RIGHT_PAREN + { A.match_ lhs l } + | LEFT_PAREN + FUN + LEFT_PAREN vars=typed_var+ RIGHT_PAREN + body=term + RIGHT_PAREN + { A.fun_l vars body } + | LEFT_PAREN + LET + LEFT_PAREN l=binding+ RIGHT_PAREN + r=term + RIGHT_PAREN + { A.let_ l r } + | LEFT_PAREN AS t=term ty=ty RIGHT_PAREN + { A.cast t ~ty } + | LEFT_PAREN FORALL LEFT_PAREN vars=typed_var+ RIGHT_PAREN + f=term + RIGHT_PAREN + { A.forall vars f } + | LEFT_PAREN EXISTS LEFT_PAREN vars=typed_var+ RIGHT_PAREN + f=term + RIGHT_PAREN + { A.exists vars f } + +%% diff --git a/src/smtlib/jbuild b/src/smtlib/jbuild new file mode 100644 index 00000000..eb430fb0 --- /dev/null +++ b/src/smtlib/jbuild @@ -0,0 +1,21 @@ +; vim:ft=lisp: + +(jbuild_version 1) + +; main binary +(library + ((name dagon_smtlib) + (public_name dagon.smtlib) + (optional) ; only if deps present + (libraries (containers dagon.smt dagon.util zarith)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 + -safe-string -color always -open Dagon_util)) + (ocamlopt_flags (:standard -O3 -color always -bin-annot + -unbox-closures -unbox-closures-factor 20)) + )) + +(menhir + ((modules (Parser)))) + +(ocamllex + (Lexer)) diff --git a/src/sat/CDCL_sat.ml b/src/th_sat/Dagon_th_sat.ml similarity index 82% rename from src/sat/CDCL_sat.ml rename to src/th_sat/Dagon_th_sat.ml index c418ae5d..8a710fe4 100644 --- a/src/sat/CDCL_sat.ml +++ b/src/th_sat/Dagon_th_sat.ml @@ -5,5 +5,5 @@ Copyright 2016 Guillaume Bury module Th = Th_sat -include CDCL.Make(Th) +include DAgon_sat.Make(Th) diff --git a/src/sat/CDCL_sat.mli b/src/th_sat/Dagon_th_sat.mli similarity index 87% rename from src/sat/CDCL_sat.mli rename to src/th_sat/Dagon_th_sat.mli index 231b1cb3..a9f72702 100644 --- a/src/sat/CDCL_sat.mli +++ b/src/th_sat/Dagon_th_sat.mli @@ -11,6 +11,6 @@ Copyright 2016 Guillaume Bury module Th = Th_sat -include module type of CDCL.Make(Th) +include module type of Dagon_sat.Make(Th) (** A functor that can generate as many solvers as needed. *) diff --git a/src/sat/Th_sat.ml b/src/th_sat/Th_sat.ml similarity index 100% rename from src/sat/Th_sat.ml rename to src/th_sat/Th_sat.ml diff --git a/src/sat/Th_sat.mli b/src/th_sat/Th_sat.mli similarity index 100% rename from src/sat/Th_sat.mli rename to src/th_sat/Th_sat.mli diff --git a/src/th_sat/jbuild b/src/th_sat/jbuild new file mode 100644 index 00000000..63e3f05f --- /dev/null +++ b/src/th_sat/jbuild @@ -0,0 +1,13 @@ +; vim:ft=lisp: + +(library + ((name Dagon_th_sat) + (public_name dagon.th_sat) + (libraries (dagon.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 + -unbox-closures -unbox-closures-factor 20)) + )) + + diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild index de0d8941..a3e3208a 100644 --- a/src/tseitin/jbuild +++ b/src/tseitin/jbuild @@ -2,7 +2,7 @@ (library ((name CDCL_tseitin) - (public_name cdcl.tseitin) + (public_name dagon.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/core/BitField.ml b/src/util/BitField.ml similarity index 100% rename from src/core/BitField.ml rename to src/util/BitField.ml diff --git a/src/core/BitField.mli b/src/util/BitField.mli similarity index 100% rename from src/core/BitField.mli rename to src/util/BitField.mli diff --git a/src/core/Heap.ml b/src/util/Heap.ml similarity index 100% rename from src/core/Heap.ml rename to src/util/Heap.ml diff --git a/src/core/Heap.mli b/src/util/Heap.mli similarity index 100% rename from src/core/Heap.mli rename to src/util/Heap.mli diff --git a/src/core/Heap_intf.ml b/src/util/Heap_intf.ml similarity index 100% rename from src/core/Heap_intf.ml rename to src/util/Heap_intf.ml diff --git a/src/smt/IArray.ml b/src/util/IArray.ml similarity index 100% rename from src/smt/IArray.ml rename to src/util/IArray.ml diff --git a/src/smt/IArray.mli b/src/util/IArray.mli similarity index 100% rename from src/smt/IArray.mli rename to src/util/IArray.mli diff --git a/src/smt/ID.ml b/src/util/ID.ml similarity index 92% rename from src/smt/ID.ml rename to src/util/ID.ml index 8f928002..3614d9ae 100644 --- a/src/smt/ID.ml +++ b/src/util/ID.ml @@ -38,3 +38,8 @@ end module Map = CCMap.Make(AsKey) module Set = CCSet.Make(AsKey) module Tbl = CCHashtbl.Make(AsKey) + +module B = struct + let int = make "int" + let rat = make "rat" +end diff --git a/src/smt/ID.mli b/src/util/ID.mli similarity index 91% rename from src/smt/ID.mli rename to src/util/ID.mli index 494d13fc..8f2b1e76 100644 --- a/src/smt/ID.mli +++ b/src/util/ID.mli @@ -24,3 +24,12 @@ val pp_name : t CCFormat.printer module Map : CCMap.S with type key = t module Set : CCSet.S with type elt = t module Tbl : CCHashtbl.S with type key = t + + +module B : sig + val rat : t + val int : t + +end + + diff --git a/src/smt/Intf.ml b/src/util/Intf.ml similarity index 100% rename from src/smt/Intf.ml rename to src/util/Intf.ml diff --git a/src/core/Log.ml b/src/util/Log.ml similarity index 100% rename from src/core/Log.ml rename to src/util/Log.ml diff --git a/src/core/Log.mli b/src/util/Log.mli similarity index 100% rename from src/core/Log.mli rename to src/util/Log.mli diff --git a/src/smt/Util.ml b/src/util/Util.ml similarity index 78% rename from src/smt/Util.ml rename to src/util/Util.ml index 56843058..f9392e06 100644 --- a/src/smt/Util.ml +++ b/src/util/Util.ml @@ -32,3 +32,10 @@ let () = Printexc.register_printer | _ -> None) let errorf msg = Fmt.ksprintf msg ~f:(fun s -> raise (Error s)) + +let setup_gc () = + let g = Gc.get () in + g.Gc.space_overhead <- 3_000; (* major gc *) + g.Gc.max_overhead <- 10_000; (* compaction *) + g.Gc.minor_heap_size <- 500_000; (* ×8 to obtain bytes on 64 bits --> *) + Gc.set g diff --git a/src/smt/Util.mli b/src/util/Util.mli similarity index 90% rename from src/smt/Util.mli rename to src/util/Util.mli index 165082ed..75f43af8 100644 --- a/src/smt/Util.mli +++ b/src/util/Util.mli @@ -19,3 +19,6 @@ exception Error of string val errorf : ('a, Format.formatter, unit, 'b) format4 -> 'a (** @raise Error when called *) + +val setup_gc : unit -> unit +(** Change parameters of the GC *) diff --git a/src/core/Vec.ml b/src/util/Vec.ml similarity index 100% rename from src/core/Vec.ml rename to src/util/Vec.ml diff --git a/src/core/Vec.mli b/src/util/Vec.mli similarity index 100% rename from src/core/Vec.mli rename to src/util/Vec.mli diff --git a/src/core/jbuild b/src/util/jbuild similarity index 59% rename from src/core/jbuild rename to src/util/jbuild index d8abd569..fb3f9256 100644 --- a/src/core/jbuild +++ b/src/util/jbuild @@ -1,11 +1,8 @@ -; vim:ft=lisp: - (library - ((name CDCL) - (public_name cdcl) - (synopsis "core data structures and algorithms for cdcl") - (libraries ()) + ((name dagon_util) + (public_name dagon.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 -unbox-closures -unbox-closures-factor 20)) - )) + )) diff --git a/tests/jbuild b/tests/jbuild index e9fae11e..e9038eb9 100644 --- a/tests/jbuild +++ b/tests/jbuild @@ -2,7 +2,7 @@ (executable ((name test_api) - (libraries (cdcl cdcl.tseitin cdcl.backend cdcl.sat)) + (libraries (dagon cdcl.tseitin cdcl.backend cdcl.sat)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20))