From 80b50e8744bf5e8405be8d274852f1a451f18855 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 3 Jul 2021 22:28:57 -0400 Subject: [PATCH] refactor: add solver instance in sidekick base move some functor instantiations from `sidekick-bin.smtlib` to `sidekick-base.solver` so they're usable from a library. --- doc/deploy | 28 ------ doc/index.txt | 10 -- doc/release | 34 ------- sidekick-base.opam | 1 + src/{smtlib => base-solver}/Form.ml | 10 ++ src/base-solver/dune | 9 ++ src/base-solver/sidekick_base_solver.ml | 119 ++++++++++++++++++++++++ src/base/Sidekick_base.ml | 5 + src/smtlib/Process.ml | 103 +------------------- src/smtlib/dune | 6 +- 10 files changed, 150 insertions(+), 175 deletions(-) delete mode 100755 doc/deploy delete mode 100644 doc/index.txt delete mode 100755 doc/release rename src/{smtlib => base-solver}/Form.ml (93%) create mode 100644 src/base-solver/dune create mode 100644 src/base-solver/sidekick_base_solver.ml diff --git a/doc/deploy b/doc/deploy deleted file mode 100755 index 8a1cb92c..00000000 --- a/doc/deploy +++ /dev/null @@ -1,28 +0,0 @@ -#!/bin/bash -e - -# Ensure we are on master branch -git checkout master - -# Generate documentation -make doc -(cd doc && asciidoc index.txt) - -# Checkout gh-pages -git checkout gh-pages -git pull - -# Copy doc to the right locations -cp doc/index.html ./ -cp msat.docdir/* ./dev/ - -# Add potentially new pages -git add ./dev/* -git add ./index.html - -# Commit it all & push -git commit -m 'Doc update' -git push - -# Get back to master branch -git checkout master - diff --git a/doc/index.txt b/doc/index.txt deleted file mode 100644 index 504ff7c5..00000000 --- a/doc/index.txt +++ /dev/null @@ -1,10 +0,0 @@ - -mSAT -==== -Guillaume Bury - -* link:dev[] -* link:0.5[] -* link:0.5.1[] -* link:0.6[] - diff --git a/doc/release b/doc/release deleted file mode 100755 index c4564484..00000000 --- a/doc/release +++ /dev/null @@ -1,34 +0,0 @@ -#!/bin/bash -e - -# Get current verison number -version=`cat VERSION` - -# Enssure we are on master branch -git checkout master - -# Generate documentation -make doc -(cd doc && asciidoc index.txt) - -# Checkout gh-pages -git checkout gh-pages -git pull - -# Create doc folder if it does not exists -mkdir -p ./$version - -# Copy doc to the right locations -cp doc/index.html ./ -cp msat.docdir/* ./$version/ - -# Add potentially new pages -git add ./$version/* -git add ./index.html - -# Commit it all & push -git commit -m "Doc release $version" -git push - -# Get back to master branch -git checkout master - diff --git a/sidekick-base.opam b/sidekick-base.opam index 09a600e6..db06be6c 100644 --- a/sidekick-base.opam +++ b/sidekick-base.opam @@ -20,6 +20,7 @@ depends: [ "alcotest" {with-test} "qcheck" {with-test & >= "0.16" } "odoc" {with-doc} + "ocaml-mdx" {with-test} ] tags: [ "sat" "smt" ] homepage: "https://github.com/c-cube/sidekick" diff --git a/src/smtlib/Form.ml b/src/base-solver/Form.ml similarity index 93% rename from src/smtlib/Form.ml rename to src/base-solver/Form.ml index 74e68e33..f23b8e5b 100644 --- a/src/smtlib/Form.ml +++ b/src/base-solver/Form.ml @@ -1,3 +1,13 @@ + +(** Formulas (boolean terms). + + This module defines function symbols, constants, and views + to manipulate boolean formulas in {!Sidekick_base}. + This is useful to have the ability to use boolean connectives instead + of being limited to clauses; by using {!Sidekick_th_bool_static}, + the formulas are turned into clauses automatically for you. +*) + open Sidekick_base module T = Term diff --git a/src/base-solver/dune b/src/base-solver/dune new file mode 100644 index 00000000..1134e584 --- /dev/null +++ b/src/base-solver/dune @@ -0,0 +1,9 @@ +(library + (name sidekick_base_solver) + (public_name sidekick-base.solver) + (synopsis "Instantiation of solver and theories for Sidekick_base") + (libraries sidekick-base sidekick.core sidekick.msat-solver + sidekick.th-bool-static + sidekick.mini-cc sidekick.th-data + sidekick.arith-lra sidekick.zarith) + (flags :standard -warn-error -a+8 -safe-string -color always -open Sidekick_util)) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml new file mode 100644 index 00000000..cc810e20 --- /dev/null +++ b/src/base-solver/sidekick_base_solver.ml @@ -0,0 +1,119 @@ + +(** SMT Solver and Theories for [Sidekick_base]. + + This contains instances of the SMT solver, and theories, + from {!Sidekick_core}, using data structures from + {!Sidekick_base}. *) + +open Sidekick_base + +module Form = Form + +(** Argument to the SMT solver *) +module Solver_arg = struct + module T = Sidekick_base + + let cc_view = Term.cc_view + let is_valid_literal _ = true + module P = Proof +end + +(** SMT solver, obtained from {!Sidekick_msat_solver} *) +module Solver = Sidekick_msat_solver.Make(Solver_arg) + +(** Theory of datatypes *) +module Th_data = Sidekick_th_data.Make(struct + module S = Solver + open Base_types + open Sidekick_th_data + module Cstor = Cstor + + let as_datatype ty = match Ty.view ty with + | Ty_atomic {def=Ty_data data;_} -> + Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values} + | Ty_atomic {def=_;args;finite=_} -> + Ty_app{args=Iter.of_list args} + | Ty_bool | Ty_real -> Ty_app {args=Iter.empty} + + let view_as_data t = match Term.view t with + | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args) + | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) -> + assert (IArray.length args=1); + T_select (sel.select_cstor, sel.select_i, IArray.get args 0) + | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) -> + assert (IArray.length args=1); + T_is_a (c, IArray.get args 0) + | _ -> T_other t + + let mk_eq = Term.eq + let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args + let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u) + let mk_is_a tst c u : Term.t = + if c.cstor_arity=0 then ( + Term.eq tst u (Term.const tst (Fun.cstor c)) + ) else ( + Term.app_fun tst (Fun.is_a c) (IArray.singleton u) + ) + + let ty_is_finite = Ty.finite + let ty_set_is_finite = Ty.set_finite + + let proof_isa_disj = Proof.isa_disj + let proof_isa_split = Proof.isa_split + let proof_cstor_inj = Proof.cstor_inj + end) + +(** Reducing boolean formulas to clauses *) +module Th_bool = Sidekick_th_bool_static.Make(struct + module S = Solver + type term = S.T.Term.t + include Form + let proof_bool_eq = Proof.bool_eq + let proof_bool_c = Proof.bool_c + let proof_ite_true = Proof.ite_true + let proof_ite_false = Proof.ite_false +end) + +(** Theory of Linear Rational Arithmetic *) +module Th_lra = Sidekick_arith_lra.Make(struct + module S = Solver + module T = Term + module Q = Sidekick_zarith.Rational + type term = S.T.Term.t + type ty = S.T.Ty.t + + let mk_eq = Form.eq + let mk_lra = T.lra + let mk_bool = T.bool + let view_as_lra t = match T.view t with + | T.LRA l -> l + | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b) + | _ -> LRA_other t + + let ty_lra _st = Ty.real() + let has_ty_real t = Ty.equal (T.ty t) (Ty.real()) + + let proof_lra = Proof.lra + let proof_lra_l = Proof.lra_l + + module Gensym = struct + type t = { + tst: T.state; + mutable fresh: int; + } + + let create tst : t = {tst; fresh=0} + let tst self = self.tst + let copy s = {s with tst=s.tst} + + let fresh_term (self:t) ~pre (ty:Ty.t) : T.t = + let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in + self.fresh <- 1 + self.fresh; + let id = ID.make name in + Term.const self.tst @@ Fun.mk_undef_const id ty + end +end) + +let th_bool : Solver.theory = Th_bool.theory +let th_data : Solver.theory = Th_data.theory +let th_lra : Solver.theory = Th_lra.theory diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index 6d50cdcf..d06e407b 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -31,6 +31,11 @@ module Data = Base_types.Data module Select = Base_types.Select module Proof = Proof +(** Concrete implementation of {!Sidekick_core.TERM} + + this module gathers most definitions above in a form + that is compatible with what Sidekick expects for terms, functions, etc. +*) module Arg : Sidekick_core.TERM with type Term.t = Term.t diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index f972aa17..fdbee65c 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -3,6 +3,7 @@ module BT = Sidekick_base module Profile = Sidekick_util.Profile open Sidekick_base +module SBS = Sidekick_base_solver [@@@ocaml.warning "-32"] @@ -11,15 +12,7 @@ type 'a or_error = ('a, string) CCResult.t module E = CCResult module Fmt = CCFormat -(* instantiate solver here *) -module Solver_arg = struct - module T = Sidekick_base - - let cc_view = Term.cc_view - let is_valid_literal _ = true - module P = Proof -end -module Solver = Sidekick_msat_solver.Make(Solver_arg) +module Solver = SBS.Solver module Check_cc = struct module Lit = Solver.Solver_internal.Lit @@ -312,95 +305,9 @@ let process_stmt Error.errorf "cannot deal with definitions yet" end -module Th_data = Sidekick_th_data.Make(struct - module S = Solver - open Base_types - open Sidekick_th_data - module Cstor = Cstor - - let as_datatype ty = match Ty.view ty with - | Ty_atomic {def=Ty_data data;_} -> - Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values} - | Ty_atomic {def=_;args;finite=_} -> - Ty_app{args=Iter.of_list args} - | Ty_bool | Ty_real -> Ty_app {args=Iter.empty} - - let view_as_data t = match Term.view t with - | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args) - | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) -> - assert (IArray.length args=1); - T_select (sel.select_cstor, sel.select_i, IArray.get args 0) - | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) -> - assert (IArray.length args=1); - T_is_a (c, IArray.get args 0) - | _ -> T_other t - - let mk_eq = Term.eq - let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args - let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u) - let mk_is_a tst c u : Term.t = - if c.cstor_arity=0 then ( - Term.eq tst u (Term.const tst (Fun.cstor c)) - ) else ( - Term.app_fun tst (Fun.is_a c) (IArray.singleton u) - ) - - let ty_is_finite = Ty.finite - let ty_set_is_finite = Ty.set_finite - - let proof_isa_disj = Proof.isa_disj - let proof_isa_split = Proof.isa_split - let proof_cstor_inj = Proof.cstor_inj - end) - -module Th_bool = Sidekick_th_bool_static.Make(struct - module S = Solver - type term = S.T.Term.t - include Form - let proof_bool_eq = Proof.bool_eq - let proof_bool_c = Proof.bool_c - let proof_ite_true = Proof.ite_true - let proof_ite_false = Proof.ite_false -end) - -module Th_lra = Sidekick_arith_lra.Make(struct - module S = Solver - module T = BT.Term - module Q = Sidekick_zarith.Rational - type term = S.T.Term.t - type ty = S.T.Ty.t - - let mk_eq = Form.eq - let mk_lra = T.lra - let mk_bool = T.bool - let view_as_lra t = match T.view t with - | T.LRA l -> l - | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) -> LRA_pred (Eq, a, b) - | _ -> LRA_other t - - let ty_lra _st = Ty.real() - let has_ty_real t = Ty.equal (T.ty t) (Ty.real()) - - let proof_lra = Proof.lra - let proof_lra_l = Proof.lra_l - - module Gensym = struct - type t = { - tst: T.state; - mutable fresh: int; - } - - let create tst : t = {tst; fresh=0} - let tst self = self.tst - let copy s = {s with tst=s.tst} - - let fresh_term (self:t) ~pre (ty:Ty.t) : T.t = - let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in - self.fresh <- 1 + self.fresh; - let id = ID.make name in - BT.Term.const self.tst @@ Fun.mk_undef_const id ty - end -end) +module Th_data = SBS.Th_data +module Th_bool = SBS.Th_bool +module Th_lra = SBS.Th_lra let th_bool : Solver.theory = Th_bool.theory let th_data : Solver.theory = Th_data.theory diff --git a/src/smtlib/dune b/src/smtlib/dune index 0ed9ebdd..318b0cda 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -2,11 +2,7 @@ (name sidekick_smtlib) (public_name sidekick-bin.smtlib) (libraries containers zarith msat sidekick.core sidekick.util - sidekick.msat-solver - sidekick.th-bool-static - sidekick.mini-cc sidekick.th-data - sidekick.arith-lra sidekick.zarith - sidekick-base + sidekick-base sidekick-base.solver msat.backend smtlib-utils sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util))