simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-23 18:06:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'wip-drup-check'

Browse source
This commit is contained in:
Simon Cruanes 2021-08-24 18:09:31 -04:00
commit 5017d9f8bf
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1575 changed files with 835533 additions and 2752 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/main.yml vendored
View file

@ -1,8 +1,6 @@
name: Build sidekick-bin
on:
push:
branches:
- master
pull_request:
branches:
- master

9
Makefile
View file

@ -5,7 +5,7 @@
J?=3
TIMEOUT?=30
OPTS= -j $(J)
OPTS= -j $(J) --profile=release
dev: build-dev
@ -13,7 +13,7 @@ dev: build-dev
#dev: build-dev test
build-install:
@dune build $(OPTS) @install --profile=release
@dune build $(OPTS) @install
build: build-install
@ -35,6 +35,9 @@ snapshots:
$(TESTTOOL)-quick: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick
$(TESTTOOL)-local: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/quick-$(DATE).csv --task sidekick-smt-local
$(TESTTOOL)-smt-QF_UF: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_UF-$(DATE).csv --task sidekick-smt-nodir tests/QF_UF
@ -67,7 +70,7 @@ reindent:
WATCH=@all
watch:
@dune build $(WATCH) -w $(OPTS) --profile=release
@dune build $(WATCH) -w $(OPTS)
#@dune build @all -w # TODO: once tests pass
.PHONY: clean doc all bench install uninstall remove reinstall bin test

30
doc/guide.md
View file

@ -100,7 +100,6 @@ for legibility:
# #install_printer Ty.pp;;
# #install_printer Fun.pp;;
# #install_printer Model.pp;;
# #install_printer Solver.Atom.pp;;
# #install_printer Solver.Model.pp;;
# #install_printer Proof.pp_debug;;
Proof.pp_debug has a wrong type for a printing function.
@ -203,6 +202,11 @@ val solver : Solver.t = <abstr>
# Solver.add_theory;;
- : Solver.t -> Solver.theory -> unit = <fun>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
```
Alright, let's do some solving now ⚙️. We're going to assert
@ -221,8 +225,8 @@ Sidekick_base_solver.Solver.Sat
(model
(true := true)
(false := false)
(p := false)
(q := false)
(p := true)
(q := true)
(_tseitin_equiv_0 := true))
```
@ -258,8 +262,8 @@ Sidekick_base_solver.Solver.Sat
(model
(true := true)
(false := false)
(p := false)
(q := false)
(p := true)
(q := true)
(_tseitin_equiv_0 := true))
```
@ -276,9 +280,9 @@ Sidekick_base_solver.Solver.Sat
(model
(true := true)
(false := false)
(p := false)
(q := false)
(r := false)
(p := true)
(q := true)
(r := true)
(_tseitin_equiv_0 := true)
(_tseitin_implies_1 := true))
```
@ -313,6 +317,11 @@ Let's create a new solver and add the theory of reals to it.
```ocaml
# let solver = Solver.create ~theories:[th_bool; th_lra] tstore () ();;
val solver : Solver.t = <abstr>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
```
Create a few arithmetic constants.
@ -406,6 +415,11 @@ Anyway, Sidekick knows how to reason about functions.
# let solver = Solver.create ~theories:[] tstore () ();;
val solver : Solver.t = <abstr>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
# (* helper *)
let appf1 x = Term.app_fun_l tstore f1 x;;
val appf1 : Term.t list -> Term.t = <fun>

1
sidekick.opam
View file

@ -15,6 +15,7 @@ depends: [
"containers" { >= "3.0" & < "4.0" }
"iter" { >= "1.0" & < "2.0" }
"ocaml" { >= "4.04" }
"zarith" { with-test }
"alcotest" {with-test}
"odoc" {with-doc}
]

27
src/backend/Backend_intf.ml
View file

@ -1,27 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Backend interface
This modules defines the interface of the modules providing
export of proofs.
*)
module type S = sig
(** Proof exporting
Currently, exporting a proof means printing it into a file
according to the conventions of a given format.
*)
type t
(** The type of proofs. *)
val pp : Format.formatter -> t -> unit
(** A function for printing proofs in the desired format. *)
end

191
src/backend/Dot.ml
View file

@ -1,191 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Output interface for the backend *)
module type S = Backend_intf.S
(** Input module for the backend *)
module type Arg = sig
type atom
(* Type of atoms *)
type hyp
type lemma
type assumption
(** Types for hypotheses, lemmas, and assumptions. *)
val print_atom : Format.formatter -> atom -> unit
(** Printing function for atoms *)
val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
(** Functions to return information about hypotheses and lemmas *)
end
module Default(S : Sidekick_sat.S) = struct
module Atom = S.Atom
module Clause = S.Clause
let print_atom = Atom.pp
let hyp_info c =
"hypothesis", Some "LIGHTBLUE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
let lemma_info c =
"lemma", Some "BLUE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
let assumption_info c =
"assumption", Some "PURPLE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
end
(** Functor to provide dot printing *)
module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) = struct
module Atom = S.Atom
module Clause = S.Clause
module P = S.Proof
let node_id n = Clause.short_name n.P.conclusion
let proof_id p = node_id (P.expand p)
let res_nn_id n1 n2 = node_id n1 ^ "_" ^ node_id n2 ^ "_res"
let res_np_id n1 n2 = node_id n1 ^ "_" ^ proof_id n2 ^ "_res"
let print_clause fmt c =
let v = Clause.atoms c in
if Array.length v = 0 then
Format.fprintf fmt "⊥"
else
let n = Array.length v in
for i = 0 to n - 1 do
Format.fprintf fmt "%a" A.print_atom v.(i);
if i < n - 1 then
Format.fprintf fmt ", "
done
let print_edge fmt i j =
Format.fprintf fmt "%s -> %s;@\n" j i
let print_edges fmt n =
match P.(n.step) with
| P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
| P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
print_edge fmt (res_np_id n p0) (proof_id hr_init);
List.iter
(fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2))
l;
| _ -> ()
let table_options fmt color =
Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
let table fmt (c, rule, color, l) =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
match l with
| [] ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
| f :: r ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
color (List.length l) rule f ();
List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
let print_dot_node fmt id color c rule rule_color l =
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
id table_options color table (c, rule, rule_color, l)
let print_dot_res_node fmt id a =
Format.fprintf fmt "%s [label=<%a>];@\n" id A.print_atom a
let ttify f c = fun fmt () -> f fmt c
let print_contents fmt n =
match P.(n.step) with
(* Leafs of the proof tree *)
| P.Hypothesis _ ->
let rule, color, l = A.hyp_info P.(n.conclusion) in
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Assumption ->
let rule, color, l = A.assumption_info P.(n.conclusion) in
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Lemma _ ->
let rule, color, l = A.lemma_info P.(n.conclusion) in
let color = match color with None -> "YELLOW" | Some c -> c in
print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l
(* Tree nodes *)
| P.Duplicate (p, l) ->
print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
List.map (ttify A.print_atom) l);
print_edge fmt (node_id n) (node_id (P.expand p))
| P.Hyper_res {P.hr_steps=l; _} ->
print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY"
[(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
List.iter
(fun (a,p2) ->
print_dot_res_node fmt (res_np_id n p2) a;
print_edge fmt (node_id n) (res_np_id n p2))
l
let print_node fmt n =
print_contents fmt n;
print_edges fmt n
let pp fmt p =
Format.fprintf fmt "digraph proof {@\n";
P.fold (fun () -> print_node fmt) () p;
Format.fprintf fmt "}@."
end
module Simple(S : Sidekick_sat.S)
(A : Arg with type atom := S.formula
and type hyp = S.formula list
and type lemma := S.lemma
and type assumption = S.formula) =
Make(S)(struct
module Atom = S.Atom
module Clause = S.Clause
module P = S.Proof
(* Some helpers *)
let lit = Atom.formula
let get_assumption c =
match S.Clause.atoms_l c with
| [ x ] -> x
| _ -> assert false
let get_lemma c =
match P.expand (P.prove c) with
| {P.step=P.Lemma p;_} -> p
| _ -> assert false
(* Actual functions *)
let print_atom fmt a =
A.print_atom fmt (lit a)
let hyp_info c =
A.hyp_info (List.map lit (S.Clause.atoms_l c))
let lemma_info c =
A.lemma_info (get_lemma c)
let assumption_info c =
A.assumption_info (lit (get_assumption c))
end)

70
src/backend/Dot.mli
View file

@ -1,70 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Dot backend for proofs
This module provides functions to export proofs into the dot graph format.
Graphs in dot format can be used to generates images using the graphviz tool.
*)
module type S = Backend_intf.S
(** Interface for exporting proofs. *)
module type Arg = sig
(** Term printing for DOT
This module defines what functions are required in order to export
a proof to the DOT format.
*)
type atom
(** The type of atomic formuals *)
type hyp
type lemma
type assumption
(** The type of theory-specifi proofs (also called lemmas). *)
val print_atom : Format.formatter -> atom -> unit
(** Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on). *)
val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list
val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list
(** Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet [(rule, color, l)], such that:
- [rule] is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)
- [color] is a color name (optional) understood by DOT
- [l] is a list of printers that will be called to print some additional information
*)
end
module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause
(** Provides a reasonnable default to instantiate the [Make] functor, assuming
the original printing functions are compatible with DOT html labels. *)
module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type assumption := S.clause) : S with type t := S.Proof.t
(** Functor for making a module to export proofs to the DOT format. *)
module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula
and type hyp = S.formula list
and type lemma := S.lemma
and type assumption = S.formula) : S with type t := S.Proof.t
(** Functor for making a module to export proofs to the DOT format.
The substitution of the hyp type is non-destructive due to a restriction
of destructive substitutions on earlier versions of ocaml. *)

6
src/backend/dune
View file

@ -1,6 +0,0 @@
(library
(name sidekick_backend)
(public_name sidekick.backend)
(synopsis "Proof backends for sidekick")
(libraries sidekick.sat))

8
src/base-solver/dune
View file

@ -2,8 +2,8 @@
(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)
(libraries sidekick-base sidekick.core sidekick.smt-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))

29
src/base-solver/sidekick_base_solver.ml
View file

@ -9,21 +9,24 @@ open Sidekick_base
(** Argument to the SMT solver *)
module Solver_arg = struct
module T = Sidekick_base
module T = Sidekick_base.Solver_arg
module Lit = Sidekick_base.Lit
let cc_view = Term.cc_view
let is_valid_literal _ = true
module P = Proof
module P = Proof_stub
type proof = P.t
end
(** SMT solver, obtained from {!Sidekick_msat_solver} *)
module Solver = Sidekick_msat_solver.Make(Solver_arg)
(** SMT solver, obtained from {!Sidekick_smt_solver} *)
module Solver = Sidekick_smt_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 Proof = Proof_stub
module Cstor = Cstor
let as_datatype ty = match Ty.view ty with
@ -56,9 +59,9 @@ module Th_data = Sidekick_th_data.Make(struct
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
let lemma_isa_disj p lits = Proof.lemma_isa_disj p lits
let lemma_isa_split p lits = Proof.lemma_isa_split p lits
let lemma_cstor_inj p lits = Proof.lemma_cstor_inj p lits
end)
(** Reducing boolean formulas to clauses *)
@ -66,10 +69,11 @@ 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
let lemma_bool_tauto = Proof_stub.lemma_bool_tauto
let lemma_bool_c = Proof_stub.lemma_bool_c
let lemma_bool_equiv = Proof_stub.lemma_bool_equiv
let lemma_ite_true = Proof_stub.lemma_ite_true
let lemma_ite_false = Proof_stub.lemma_ite_false
end)
(** Theory of Linear Rational Arithmetic *)
@ -91,8 +95,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
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
let lemma_lra = Proof_stub.lemma_lra
module Gensym = struct
type t = {

2
src/base/Lit.ml Normal file
View file

@ -0,0 +1,2 @@
include Sidekick_lit.Make(Solver_arg)

2
src/base/Lit.mli Normal file
View file

@ -0,0 +1,2 @@
include Sidekick_core.LIT with module T = Solver_arg

30
src/base/Proof_stub.ml Normal file
View file

@ -0,0 +1,30 @@
open Base_types
type lit = Lit.t
type term = Term.t
type t = unit
type dproof = t -> unit
let create () : t = ()
let with_proof _ _ = ()
let begin_subproof _ = ()
let end_subproof _ = ()
let del_clause _ _ = ()
let emit_redundant_clause _ _ = ()
let emit_input_clause _ _ = ()
let define_term _ _ _ = ()
let lemma_preprocess _ _ _ = ()
let lemma_true _ _ = ()
let lemma_cc _ _ = ()
let lemma_lra _ _ = ()
let lemma_cstor_inj _ _ = ()
let lemma_isa_disj _ _ = ()
let lemma_isa_split _ _ = ()
let lemma_bool_tauto _ _ = ()
let lemma_bool_c _ _ _ = ()
let lemma_bool_equiv _ _ _ = ()
let lemma_ite_true ~a:_ ~ite:_ _ = ()
let lemma_ite_false ~a:_ ~ite:_ _ = ()

22
src/base/Proof_stub.mli Normal file
View file

@ -0,0 +1,22 @@
(** Dummy proof module that does nothing. *)
open Base_types
include Sidekick_core.PROOF
with type lit = Lit.t
and type term = Term.t
val create : unit -> t
val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
val lemma_bool_c : string -> term list -> t -> unit
val lemma_bool_equiv : term -> term -> t -> unit
val lemma_ite_true : a:term -> ite:term -> t -> unit
val lemma_ite_false : a:term -> ite:term -> t -> unit
val lemma_lra : Lit.t Iter.t -> t -> unit
val lemma_isa_split : Lit.t Iter.t -> t -> unit
val lemma_isa_disj : Lit.t Iter.t -> t -> unit
val lemma_cstor_inj : Lit.t Iter.t -> t -> unit

22
src/base/Sidekick_base.ml
View file

@ -29,25 +29,11 @@ module Ty = Base_types.Ty
module Statement = Base_types.Statement
module Data = Base_types.Data
module Select = Base_types.Select
module Proof = Proof
module Form = Form
module Solver_arg = Solver_arg
module Lit = Lit
module Proof_stub = Proof_stub
(* re-export *)
module IArray = IArray
(** 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
and type Fun.t = Fun.t
and type Ty.t = Ty.t
and type Term.store = Term.store
= struct
module Term = Term
module Fun = Fun
module Ty = Ty
end

6
src/base/Solver_arg.ml Normal file
View file

@ -0,0 +1,6 @@
open Base_types
module Term = Term
module Fun = Fun
module Ty = Ty

15
src/base/Solver_arg.mli Normal file
View file

@ -0,0 +1,15 @@
(** 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.
*)
open Base_types
include Sidekick_core.TERM
with type Term.t = Term.t
and type Fun.t = Fun.t
and type Ty.t = Ty.t
and type Term.store = Term.store
and type Ty.store = Ty.store

2
src/base/dune
View file

@ -2,7 +2,7 @@
(name sidekick_base)
(public_name sidekick-base)
(synopsis "Base term definitions for the standalone SMT solver and library")
(libraries containers sidekick.core sidekick.util
(libraries containers sidekick.core sidekick.util sidekick.lit
sidekick.arith-lra sidekick.th-bool-static
sidekick.zarith zarith)
(flags :standard -w -32 -open Sidekick_util))

0
src/main/Dimacs_lexer.mll → src/bin-lib/Dimacs_lexer.mll
View file

0
src/main/Dimacs_parser.ml → src/bin-lib/Dimacs_parser.ml
View file

0
src/main/Dimacs_parser.mli → src/bin-lib/Dimacs_parser.mli
View file

22
src/bin-lib/Drup_lexer.mll Normal file
View file

@ -0,0 +1,22 @@
{
type token = EOF | ZERO | LIT of int | D | R | I
}
let number = ['1' - '9'] ['0' - '9']*
rule token = parse
| eof { EOF }
| "c" { comment lexbuf }
| [' ' '\t' '\r'] { token lexbuf }
| "d" { D }
| "r" { R }
| "i" { I }
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| '0' { ZERO }
| '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) }
| _ { Error.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
and comment = parse
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| [^'\n'] { comment lexbuf }

49
src/bin-lib/Drup_parser.ml Normal file
View file

@ -0,0 +1,49 @@
module L = Drup_lexer
type event =
| Input of int list
| Add of int list
| Delete of int list
type t = {
buf: Lexing.lexbuf;
}
let create_string s : t =
{ buf=Lexing.from_string s }
let create_chan (ic:in_channel) : t =
{ buf = Lexing.from_channel ic }
let next self : _ option =
let rec get_clause acc = match L.token self.buf with
| L.EOF -> Error.errorf "unexpected EOF in a clause"
| L.ZERO -> List.rev acc
| L.LIT i -> get_clause (i::acc)
| _ -> Error.errorf "expected clause"
in
begin match L.token self.buf with
| L.EOF -> None
| L.I ->
let c = get_clause [] in
Some (Input c)
| L.D ->
let c = get_clause [] in
Some (Delete c)
| L.R ->
let c = get_clause [] in
Some (Add c)
| L.ZERO -> Some (Add [])
| L.LIT i ->
let c = get_clause [i] in
Some (Add c)
end
let iter self k =
let rec loop () =
match next self with
| None -> ()
| Some ev -> k ev; loop ()
in
loop ()

18
src/bin-lib/Drup_parser.mli Normal file
View file

@ -0,0 +1,18 @@
(** {1 DRUP parser} *)
type t
type event =
| Input of int list
| Add of int list
| Delete of int list
val create_chan : in_channel -> t
val create_string : string -> t
val next : t -> event option
val iter : t -> event Iter.t

8
src/bin-lib/Sidekick_bin_lib.ml Normal file
View file

@ -0,0 +1,8 @@
(** Library for the Sidekick executables *)
module Dimacs_lexer = Dimacs_lexer
module Dimacs_parser = Dimacs_parser
module Drup_lexer = Drup_lexer
module Drup_parser = Drup_parser

9
src/bin-lib/dune Normal file
View file

@ -0,0 +1,9 @@
(library
(name sidekick_bin_lib)
(public_name sidekick-bin.lib)
(synopsis "Utils for the sidekick binaries")
(libraries containers sidekick.util)
(flags :standard -warn-error -a+8 -open Sidekick_util))
(ocamllex (modules Dimacs_lexer Drup_lexer))

68
src/cc/Sidekick_cc.ml
View file

@ -15,18 +15,19 @@ module type S = Sidekick_core.CC_S
module Make (A: CC_ARG)
: S with module T = A.T
and module Lit = A.Lit
and module P = A.P
and type proof = A.proof
and module Actions = A.Actions
= struct
module T = A.T
module P = A.P
module Lit = A.Lit
module Actions = A.Actions
module P = Actions.P
type term = T.Term.t
type term_store = T.Term.store
type lit = Lit.t
type fun_ = T.Fun.t
type proof = P.t
type proof = A.proof
type dproof = proof -> unit
type actions = Actions.t
module Term = T.Term
@ -95,7 +96,6 @@ module Make (A: CC_ARG)
| E_congruence of node * node (* caused by normal congruence *)
| E_and of explanation * explanation
| E_theory of explanation
| E_proof of P.t
type repr = node
@ -169,7 +169,6 @@ module Make (A: CC_ARG)
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
| E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
| E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" (P.pp_debug ~sharing:false) p
| E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
@ -179,7 +178,6 @@ module Make (A: CC_ARG)
let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
let[@inline] mk_lit l : t = E_lit l
let mk_theory e = E_theory e
let mk_proof p = E_proof p
let rec mk_list l =
match l with
@ -283,7 +281,7 @@ module Make (A: CC_ARG)
and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
and ev_on_new_term = t -> N.t -> term -> unit
and ev_on_conflict = t -> th:bool -> lit list -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list * (proof -> unit)) -> unit
and ev_on_is_subterm = N.t -> term -> unit
let[@inline] size_ (r:repr) = r.n_size
@ -310,18 +308,6 @@ module Make (A: CC_ARG)
Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
let ret_cc_lemma _what _lits p_lits =
let p = P.cc_lemma p_lits in
(* useful to debug bad lemmas
let n_pos = Iter.of_list p_lits |> Iter.filter P.lit_sign |> Iter.length in
if n_pos <> 1 then (
Log.debugf 0 (fun k->k"emit (n-pos=%d) :from %s@ %a@ :lits %a"
n_pos what
(P.pp_debug ~sharing:false) p Fmt.(Dump.list Lit.pp) lits);
);
*)
p
(* print full state *)
let pp_full out (cc:t) : unit =
let pp_next out n =
@ -473,9 +459,6 @@ module Make (A: CC_ARG)
| E_lit lit -> lit :: acc
| E_theory e' ->
th := true; explain_decompose_expl cc ~th acc e'
| E_proof _p ->
(* FIXME: need to also return pairs of [t, u, |-t=u] as part of explanation *)
assert false
| E_merge (a,b) -> explain_equal cc ~th acc a b
| E_merge_t (a,b) ->
(* find nodes for [a] and [b] on the fly *)
@ -600,10 +583,10 @@ module Make (A: CC_ARG)
let rec update_tasks (cc:t) (acts:actions) : unit =
while not (Vec.is_empty cc.pending && Vec.is_empty cc.combine) do
while not @@ Vec.is_empty cc.pending do
task_pending_ cc (Vec.pop cc.pending);
task_pending_ cc (Vec.pop_exn cc.pending);
done;
while not @@ Vec.is_empty cc.combine do
task_combine_ cc acts (Vec.pop cc.combine);
task_combine_ cc acts (Vec.pop_exn cc.combine);
done;
done
@ -675,16 +658,10 @@ module Make (A: CC_ARG)
let lits = explain_decompose_expl cc ~th [] e_ab in
let lits = explain_equal cc ~th lits a ra in
let lits = explain_equal cc ~th lits b rb in
let proof =
let p_lits =
lits
|> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
P.lit_mk (not sign) t)
in
ret_cc_lemma "true-eq-false" lits p_lits
in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof
let emit_proof p =
let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
P.lemma_cc p_lits p in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
);
(* We will merge [r_from] into [r_into].
we try to ensure that [size ra <= size rb] in general, but always
@ -799,15 +776,12 @@ module Make (A: CC_ARG)
let e = lazy (
let lazy (th, acc) = half_expl in
let lits = explain_equal cc ~th acc u1 t1 in
let p_lits =
let emit_proof p =
(* make a tautology, not a true guard *)
let tauto = lit :: List.rev_map Lit.neg lits in
tauto |> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
A.P.(lit_mk sign t))
let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
P.lemma_cc p_lits p
in
let p = ret_cc_lemma "bool-parent" lits p_lits in
lits, p
lits, emit_proof
) in
fun () -> Lazy.force e
in
@ -874,15 +848,11 @@ module Make (A: CC_ARG)
let th = ref true in
let lits = explain_decompose_expl cc ~th [] expl in
let lits = List.rev_map Lit.neg lits in
let proof =
let p_lits =
lits |> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
P.lit_mk sign t)
in
ret_cc_lemma "from-expl" lits p_lits
let emit_proof p =
let p_lits = Iter.of_list lits in
P.lemma_cc p_lits p
in
raise_conflict_ cc ~th:!th acts lits proof
raise_conflict_ cc ~th:!th acts lits emit_proof
let merge cc n1 n2 expl =
Log.debugf 5

4
src/cc/Sidekick_cc.mli
View file

@ -4,7 +4,7 @@ open Sidekick_core
module type S = Sidekick_core.CC_S
module Make (A: CC_ARG)
: S with module T = A.T
: S with module T = A.T
and module Lit = A.Lit
and module P = A.P
and type proof = A.proof
and module Actions = A.Actions

162
src/checker/drup_check.ml Normal file
View file

@ -0,0 +1,162 @@
include Sidekick_drup.Make()
(** A DRUP trace, as a series of operations *)
module Trace : sig
type t
val create : Clause.store -> t
val cstore : t -> Clause.store
val add_clause : t -> clause -> unit
val add_input_clause : t -> clause -> unit
val del_clause : t -> clause -> unit
(** Operator on the set of clauses *)
type op =
| Input of clause
| Redundant of clause
| Delete of clause
val iteri : t -> f:(int -> op -> unit) -> unit
val ops : t -> op Iter.t
val size : t -> int
val get : t -> int -> op
val pp_op : op Fmt.printer
val dump : out_channel -> t -> unit
end = struct
type op =
| Input of clause
| Redundant of clause
| Delete of clause
type t = {
cstore: Clause.store;
ops: op Vec.t;
}
let create cstore : t =
{ cstore; ops=Vec.create() }
let cstore self = self.cstore
let add_clause self c = Vec.push self.ops (Redundant c)
let add_input_clause self c = Vec.push self.ops (Input c)
let del_clause self c = Vec.push self.ops (Delete c)
let get self i = Vec.get self.ops i
let size self = Vec.size self.ops
let ops self = Vec.to_seq self.ops
let iteri self ~f = Vec.iteri f self.ops
let pp_op out = function
| Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c
| Redundant c -> Fmt.fprintf out "(@[Redundant %a@])" Clause.pp c
| Delete c -> Fmt.fprintf out "(@[Delete %a@])" Clause.pp c
let dump oc self : unit =
let fpf = Printf.fprintf in
let pp_c out c = Clause.iter c ~f:(fun a -> fpf oc "%d " (a:atom:>int)); in
Vec.iter
(function
| Input c -> fpf oc "i %a0\n" pp_c c;
| Redundant c -> fpf oc "%a0\n" pp_c c;
| Delete c -> fpf oc "d %a0\n" pp_c c;
)
self.ops
end
(** Forward checking.
Each event is checked by reverse-unit propagation on previous events. *)
module Fwd_check : sig
type error =
[ `Bad_steps of VecI32.t
| `No_empty_clause
]
val pp_error : Trace.t -> error Fmt.printer
(** [check tr] checks the trace and returns [Ok ()] in case of
success. In case of error it returns [Error idxs] where [idxs] are the
indexes in the trace of the steps that failed. *)
val check : Trace.t -> (unit, error) result
end = struct
module ISet = CCSet.Make(CCInt)
type t = {
checker: Checker.t;
errors: VecI32.t;
}
let create cstore : t = {
checker=Checker.create cstore;
errors=VecI32.create();
}
(* check event, return [true] if it's valid *)
let check_op (self:t) i (op:Trace.op) : bool =
Profile.with_ "check-op" @@ fun() ->
Log.debugf 20 (fun k->k"(@[check-op :idx %d@ :op %a@])" i Trace.pp_op op);
begin match op with
| Trace.Input c ->
Checker.add_clause self.checker c;
true
| Trace.Redundant c ->
let ok = Checker.is_valid_drup self.checker c in
Checker.add_clause self.checker c; (* now add clause *)
ok
| Trace.Delete c ->
Checker.del_clause self.checker c;
true
end
type error =
[ `Bad_steps of VecI32.t
| `No_empty_clause
]
let pp_error trace out = function
| `No_empty_clause -> Fmt.string out "no empty clause found"
| `Bad_steps bad ->
let n0 = VecI32.get bad 0 in
Fmt.fprintf out
"@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
(VecI32.size bad) n0
Trace.pp_op (Trace.get trace n0)
let check trace : _ result =
let self = create (Trace.cstore trace) in
(* check each event in turn *)
let has_false = ref false in
Trace.iteri trace
~f:(fun i op ->
let ok = check_op self i op in
if ok then (
Log.debugf 50
(fun k->k"(@[check.step.ok@ :idx %d@ :op %a@])" i Trace.pp_op op);
(* check if op adds the empty clause *)
begin match op with
| (Trace.Redundant c | Trace.Input c) when Clause.size c = 0 ->
has_false := true
| _ -> ()
end;
) else (
Log.debugf 10
(fun k->k"(@[check.step.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
VecI32.push self.errors i
));
Log.debugf 10 (fun k->k"found %d errors" (VecI32.size self.errors));
if not !has_false then Error `No_empty_clause
else if VecI32.size self.errors > 0 then Error (`Bad_steps self.errors)
else Ok ()
end

8
src/checker/dune Normal file
View file

@ -0,0 +1,8 @@
(executable
(name main)
(public_name sidekick-checker)
(package sidekick-bin)
(libraries containers sidekick-bin.lib
sidekick.util sidekick.tef sidekick.drup)
(flags :standard -warn-error -a+8 -open Sidekick_util))

104
src/checker/main.ml Normal file
View file

@ -0,0 +1,104 @@
module BL = Sidekick_bin_lib
let clause_of_int_l store atoms : Drup_check.clause =
atoms
|> Iter.of_list
|> Iter.map Drup_check.Atom.of_int_dimacs
|> Drup_check.Clause.of_iter store
let check ?pb proof : bool =
Profile.with_ "check" @@ fun() ->
let cstore = Drup_check.Clause.create() in
let trace = Drup_check.Trace.create cstore in
(* add problem to trace, if provided *)
begin match pb with
| None -> ()
| Some f when Filename.extension f = ".cnf" ->
Profile.with_ "parse-pb.cnf" @@ fun() ->
CCIO.with_in f
(fun ic ->
let parser_ = BL.Dimacs_parser.create ic in
BL.Dimacs_parser.iter parser_
(fun atoms ->
let c = clause_of_int_l cstore atoms in
Drup_check.Trace.add_input_clause trace c))
| Some f ->
(* TODO: handle .cnf.gz *)
Error.errorf "unknown problem file extension '%s'" (Filename.extension f)
end;
let add_proof_from_chan ic =
let p = BL.Drup_parser.create_chan ic in
BL.Drup_parser.iter p
(function
| BL.Drup_parser.Input c ->
let c = clause_of_int_l cstore c in
Drup_check.Trace.add_input_clause trace c
| BL.Drup_parser.Add c ->
let c = clause_of_int_l cstore c in
Drup_check.Trace.add_clause trace c
| BL.Drup_parser.Delete c ->
let c = clause_of_int_l cstore c in
Drup_check.Trace.del_clause trace c)
in
(* add proof to trace *)
begin match proof with
| f when Filename.extension f = ".drup" ->
(* read file *)
Profile.with_ "parse-proof.drup" @@ fun() ->
CCIO.with_in f add_proof_from_chan
| f when Filename.extension f = ".gz" ->
(* read compressed proof *)
Profile.with_ "parse-proof.drup" @@ fun() ->
(* TODO: more graceful failure mode here *)
assert (Filename.extension @@ Filename.chop_extension f = ".drup");
let cmd = Printf.sprintf "gzip --keep -d -c \"%s\"" f in
Log.debugf 1 (fun k->k"command to open proof: %s" cmd);
let p = Unix.open_process_in cmd in
CCFun.finally ~h:(fun () -> ignore (Unix.close_process_in p))
~f:(fun () -> add_proof_from_chan p)
| f ->
Error.errorf "unknown proof file extension '%s'" (Filename.extension f)
end;
(* check proof *)
Log.debugf 1 (fun k->k"checking proof (%d steps)" (Drup_check.Trace.size trace));
begin match Drup_check.Fwd_check.check trace with
| Ok () -> true
| Error err ->
Format.eprintf "%a@." (Drup_check.Fwd_check.pp_error trace) err;
false
end
let () =
let files = ref [] in
let opts = [
"-d", Arg.Int Log.set_debug, " set debug level";
] |> Arg.align in
Printexc.record_backtrace true;
Sidekick_tef.setup();
let t1 = Unix.gettimeofday() in
Arg.parse opts (fun f -> files := f :: !files) "checker [opt]* [file]+";
let ok =
match List.rev !files with
| [pb; proof] ->
Log.debugf 1 (fun k->k"checker: problem `%s`, proof `%s`" pb proof);
check ~pb proof
| [proof] ->
Log.debugf 1 (fun k->k"checker: proof `%s`" proof);
check ?pb:None proof
| _ -> Error.errorf "expected <problem>? <proof>"
in
let t2 = Unix.gettimeofday() -. t1 in
Format.printf "c %s@." (if ok then "OK" else "FAIL");
Format.printf "c elapsed time: %.3fs@." t2;
if not ok then exit 1

405
src/core/Sidekick_core.ml
View file

@ -145,7 +145,51 @@ module type TERM = sig
end
end
(** Proofs of unsatisfiability *)
(** Proofs for the congruence closure *)
module type CC_PROOF = sig
type t
type lit
val lemma_cc : lit Iter.t -> t -> unit
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
of uninterpreted functions. *)
end
(** Signature for SAT-solver proof emission, using DRUP.
We do not store the resolution steps, just the stream of clauses deduced.
See {!Sidekick_drup} for checking these proofs. *)
module type SAT_PROOF = sig
type t
(** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
type lit
(** A boolean literal for the proof trace *)
type dproof = t -> unit
(** A delayed proof, used to produce proofs on demand from theories. *)
val with_proof : t -> (t -> unit) -> unit
(** If proof is enabled, call [f] on it to emit steps.
if proof is disabled, the callback won't even be called. *)
val emit_input_clause : lit Iter.t -> t -> unit
(** Emit an input clause. *)
val emit_redundant_clause : lit Iter.t -> t -> unit
(** Emit a clause deduced by the SAT solver, redundant wrt axioms.
The clause must be RUP wrt previous clauses. *)
val del_clause : lit Iter.t -> t -> unit
(** Forget a clause. Only useful for performance considerations. *)
(* TODO: replace with something index-based? *)
end
(** Proofs of unsatisfiability.
We use DRUP(T)-style traces where we simply emit clauses as we go,
annotating enough for the checker to reconstruct them.
This allows for low overhead proof production. *)
module type PROOF = sig
type t
(** The abstract representation of a proof. A proof always proves
@ -153,80 +197,36 @@ module type PROOF = sig
of the problem's assertions, and the theories) *)
type term
type ty
type hres_step
(** hyper-resolution steps: resolution, unit resolution;
bool paramodulation, unit bool paramodulation *)
val r : t -> pivot:term -> hres_step
(** Resolution step on given pivot term *)
val r1 : t -> hres_step
(** Unit resolution; pivot is obvious *)
val p : t -> lhs:term -> rhs:term -> hres_step
(** Paramodulation using proof whose conclusion has a literal [lhs=rhs] *)
val p1 : t -> hres_step
(** Unit paramodulation *)
type lit
(** Proof representation of literals *)
val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
include CC_PROOF
with type t := t
and type lit := lit
type composite_step
include SAT_PROOF
with type t := t
and type lit := lit
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step (** define a (new) atomic term *)
val begin_subproof : t -> unit
(** Begins a subproof. The result of this will only be the
clause with which {!end_subproof} is called; all other intermediate
steps will be discarded. *)
val is_trivial_refl : t -> bool
(** is this a proof of [|- t=t]? This can be used to remove
some trivial steps that would build on the proof (e.g. rewriting
using [refl t] is useless). *)
val end_subproof : t -> unit
(** [end_subproof p] ends the current active subproof, the last result
of which is kept. *)
val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t (* named clause, see {!defc} *)
val assertion_c_l : lit list -> t
val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
val hres_l : t -> hres_step list -> t (* hyper-res *)
val res : pivot:term -> t -> t -> t (* resolution with pivot *)
val res1 : t -> t -> t (* unit resolution *)
val refl : term -> t (* proof of [| t=t] *)
val true_is_true : t (* proof of [|- true] *)
val true_neq_false : t (* proof of [|- not (true=false)] *)
val nn : t -> t (* negation normalization *)
val cc_lemma : lit list -> t (* equality tautology, unsigned *)
val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
val composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?assms:(string * lit) list -> composite_step list -> t
val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val sorry_c : lit Iter.t -> t
[@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val define_term : term -> term -> t -> unit
(** [define_term p cst u] defines the new constant [cst] as being equal
to [u]. *)
val sorry_c_l : lit list -> t
val lemma_true : term -> t -> unit
(** [lemma_true p (true)] asserts the clause [(true)] *)
val default : t [@@alert cstor "do not use default constructor"]
val pp_debug : sharing:bool -> t Fmt.printer
(** Pretty print a proof.
@param sharing if true, try to compact the proof by introducing
definitions for common terms, clauses, and steps as needed. Safe to ignore. *)
module Quip : sig
val output : out_channel -> t -> unit
(** Printer in Quip format (experimental) *)
end
val lemma_preprocess : term -> term -> t -> unit
(** [lemma_preprocess p t u] asserts that [t = u] is a tautology
and that [t] has been preprocessed into [u].
From now on, [t] and [u] will be used interchangeably. *)
end
(** Literals
@ -257,6 +257,17 @@ module type LIT = sig
(** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
val signed_term : t -> T.Term.t * bool
(** Return the atom and the sign *)
val atom : T.Term.store -> ?sign:bool -> T.Term.t -> t
(** [atom store t] makes a literal out of a term, possibly normalizing
its sign in the process.
@param sign if provided, and [sign=false], negate the resulting lit. *)
val norm_sign : t -> t * bool
(** [norm_sign (+t)] is [+t, true],
and [norm_sign (-t)] is [+t, false].
In both cases the term is positive, and the boolean reflects the initial sign. *)
val equal : t -> t -> bool
val hash : t -> int
@ -273,20 +284,22 @@ module type CC_ACTIONS = sig
module T : TERM
module Lit : LIT with module T = T
module P : PROOF with type term = T.Term.t
type proof
type dproof = proof -> unit
module P : CC_PROOF with type lit = Lit.t and type t = proof
type t
(** An action handle. It is used by the congruence closure
to perform the actions below. How it performs the actions
is not specified and is solver-specific. *)
val raise_conflict : t -> Lit.t list -> P.t -> 'a
val raise_conflict : t -> Lit.t list -> dproof -> 'a
(** [raise_conflict acts c pr] declares that [c] is a tautology of
the theory of congruence. This does not return (it should raise an
exception).
@param pr the proof of [c] being a tautology *)
val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * P.t) -> unit
val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * dproof) -> unit
(** [propagate acts lit ~reason pr] declares that [reason() => lit]
is a tautology.
@ -300,15 +313,19 @@ end
(** Arguments to a congruence closure's implementation *)
module type CC_ARG = sig
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit
type proof
module P : CC_PROOF with type lit = Lit.t and type t = proof
module Actions : CC_ACTIONS
with module T=T
and module Lit = Lit
and type proof = proof
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
(** View the term through the lens of the congruence closure *)
end
(** Main congruence closure.
(** Main congruence closure signature.
The congruence closure handles the theory QF_UF (uninterpreted
function symbols).
@ -328,14 +345,18 @@ module type CC_S = sig
(** first, some aliases. *)
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P
type proof
type dproof = proof -> unit
module P : CC_PROOF with type lit = Lit.t and type t = proof
module Actions : CC_ACTIONS
with module T = T
and module Lit = Lit
and type proof = proof
type term_store = T.Term.store
type term = T.Term.t
type fun_ = T.Fun.t
type lit = Lit.t
type proof = P.t
type actions = Actions.t
type t
@ -420,7 +441,6 @@ module type CC_S = sig
val mk_merge_t : term -> term -> t
val mk_lit : lit -> t
val mk_list : t list -> t
val mk_proof : P.t -> t
val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *)
end
@ -473,7 +493,7 @@ module type CC_S = sig
participating in the conflict are purely syntactic theories
like injectivity of constructors. *)
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
type ev_on_propagate = t -> lit -> (unit -> lit list * dproof) -> unit
(** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
@ -619,13 +639,18 @@ end
new lemmas, propagate literals, access the congruence closure, etc. *)
module type SOLVER_INTERNAL = sig
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
type ty = T.Ty.t
type term = T.Term.t
type term_store = T.Term.store
type ty_store = T.Ty.store
type proof = P.t
type proof
type dproof = proof -> unit
(** Delayed proof. This is used to build a proof step on demand. *)
(** {3 Proofs} *)
module P : PROOF with type lit = Lit.t and type term = term and type t = proof
(** {3 Main type for a solver} *)
type t
@ -635,18 +660,13 @@ module type SOLVER_INTERNAL = sig
val ty_st : t -> ty_store
val stats : t -> Stat.t
val with_proof : t -> (proof -> unit) -> unit
(** {3 Actions for the theories} *)
type actions
type theory_actions
(** Handle that the theories can use to perform actions. *)
(** {3 Literals}
A literal is a (preprocessed) term along with its sign.
It is directly manipulated by the SAT solver.
*)
module Lit : LIT with module T = T
type lit = Lit.t
(** {3 Proof helpers} *)
@ -661,9 +681,11 @@ module type SOLVER_INTERNAL = sig
(** Congruence closure instance *)
module CC : CC_S
with module T = T
and module P = P
and module Lit = Lit
and type Actions.t = actions
and type proof = proof
and type P.t = proof
and type P.lit = lit
and type Actions.t = theory_actions
val cc : t -> CC.t
(** Congruence closure for this solver *)
@ -680,19 +702,21 @@ module type SOLVER_INTERNAL = sig
val clear : t -> unit
(** Reset internal cache, etc. *)
type hook = t -> term -> (term * proof) option
val with_proof : t -> (proof -> unit) -> unit
type hook = t -> term -> term option
(** Given a term, try to simplify it. Return [None] if it didn't change.
A simple example could be a hook that takes a term [t],
and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
returns [Some (const (x+y))], and [None] otherwise. *)
val normalize : t -> term -> (term * P.t) option
val normalize : t -> term -> term option
(** Normalize a term using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside
the term. *)
val normalize_t : t -> term -> term * P.t
val normalize_t : t -> term -> term
(** Normalize a term using all the hooks, along with a proof that the
simplification is correct.
returns [t, refl t] if no simplification occurred. *)
@ -705,58 +729,99 @@ module type SOLVER_INTERNAL = sig
val simplifier : t -> Simplify.t
val simplify_t : t -> term -> (term * proof) option
(** Simplify input term, returns [Some (u, |- t=u)] if some
val simplify_t : t -> term -> term option
(** Simplify input term, returns [Some u] if some
simplification occurred. *)
val simp_t : t -> term -> term * proof
(** [simp_t si t] returns [u, |- t=u] even if no simplification occurred
val simp_t : t -> term -> term
(** [simp_t si t] returns [u] even if no simplification occurred
(in which case [t == u] syntactically).
It emits [|- t=u].
(see {!simplifier}) *)
(** {3 Preprocessors}
These preprocessors turn mixed, raw literals (possibly simplified) into
literals suitable for reasoning.
Typically some clauses are also added to the solver. *)
module type PREPROCESS_ACTS = sig
val mk_lit : ?sign:bool -> term -> lit
(** creates a new literal for a boolean term. *)
val add_clause : lit list -> dproof -> unit
(** pushes a new clause into the SAT solver. *)
val add_lit : ?default_pol:bool -> lit -> unit
(** Ensure the literal will be decided/handled by the SAT solver. *)
end
type preprocess_actions = (module PREPROCESS_ACTS)
(** Actions available to the preprocessor *)
type preprocess_hook =
t ->
preprocess_actions ->
term -> term option
(** Given a term, try to preprocess it. Return [None] if it didn't change,
or [Some (u)] if [t=u].
Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable
to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
adding clauses that encode their meaning in the same move.
@param preprocess_actions actions available during preprocessing.
*)
val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *)
val preprocess_acts_of_acts : t -> theory_actions -> preprocess_actions
(** Obtain preprocessor actions, from theory actions *)
(** {3 hooks for the theory} *)
val raise_conflict : t -> actions -> lit list -> proof -> 'a
val raise_conflict : t -> theory_actions -> lit list -> dproof -> 'a
(** Give a conflict clause to the solver *)
val push_decision : t -> actions -> lit -> unit
val push_decision : t -> theory_actions -> lit -> unit
(** Ask the SAT solver to decide the given literal in an extension of the
current trail. This is useful for theory combination.
If the SAT solver backtracks, this (potential) decision is removed
and forgotten. *)
val propagate: t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit
val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * dproof) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: t -> actions -> lit -> lit list -> proof -> unit
val propagate_l: t -> theory_actions -> lit -> lit list -> dproof -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_clause_temp : t -> actions -> lit list -> proof -> unit
val add_clause_temp : t -> theory_actions -> lit list -> dproof -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_clause_permanent : t -> actions -> lit list -> proof -> unit
val add_clause_permanent : t -> theory_actions -> lit list -> dproof -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
val mk_lit : t -> actions -> ?sign:bool -> term -> lit
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
(** Create a literal. This automatically preprocesses the term. *)
val preprocess_term :
t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof
(** Preprocess a term. *)
val preprocess_term : t -> preprocess_actions -> term -> term
(** Preprocess a term. The preprocessing proof is automatically emitted. *)
val add_lit : t -> actions -> lit -> unit
val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
(** Add the given literal to the SAT solver, so it gets assigned
a boolean value *)
a boolean value.
@param default_pol default polarity for the corresponding atom *)
val add_lit_t : t -> actions -> ?sign:bool -> term -> unit
val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit
(** Add the given (signed) bool term to the SAT solver, so it gets assigned
a boolean value *)
val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a
val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a
(** Raise a conflict with the given congruence closure explanation.
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
@ -767,12 +832,12 @@ module type SOLVER_INTERNAL = sig
val cc_are_equal : t -> term -> term -> bool
(** Are these two terms equal in the congruence closure? *)
val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
(** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *)
val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit
val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit
(** Merge these two terms in the congruence closure, given this explanation.
See {!cc_merge} *)
@ -784,10 +849,10 @@ module type SOLVER_INTERNAL = sig
(** Return [true] if the term is explicitly in the congruence closure.
To be used in theories *)
val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
val on_cc_pre_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
(** Callback for when two classes containing data for this key are merged (called before) *)
val on_cc_post_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> unit) -> unit
val on_cc_post_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit) -> unit
(** Callback for when two classes containing data for this key are merged (called after)*)
val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit
@ -801,10 +866,10 @@ module type SOLVER_INTERNAL = sig
val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
(** Callback called on every CC conflict *)
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> unit) -> unit
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit
(** Callback called on every CC propagation *)
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
(** Register callbacked to be called with the slice of literals
newly added on the trail.
@ -812,7 +877,7 @@ module type SOLVER_INTERNAL = sig
to be complete, only correct. It's given only the slice of
the trail consisting in new literals. *)
val on_final_check: t -> (t -> actions -> lit Iter.t -> unit) -> unit
val on_final_check: t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
(** Register callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is
@ -820,31 +885,6 @@ module type SOLVER_INTERNAL = sig
is given the whole trail.
*)
(** {3 Preprocessors}
These preprocessors turn mixed, raw literals (possibly simplified) into
literals suitable for reasoning.
Typically some clauses are also added to the solver. *)
type preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> proof -> unit) ->
term -> (term * proof) option
(** Given a term, try to preprocess it. Return [None] if it didn't change,
or [Some (u,p)] if [t=u] and [p] is a proof of [t=u].
Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable
to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
adding clauses that encode their meaning in the same move.
@param mk_lit creates a new literal for a boolean term.
@param add_clause pushes a new clause into the SAT solver.
*)
val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *)
(** {3 Model production} *)
type model_hook =
@ -871,15 +911,16 @@ end
Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
module type SOLVER = sig
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
type proof
module P : PROOF with type lit = Lit.t and type t = proof and type term = T.Term.t
module Solver_internal
: SOLVER_INTERNAL
with module T = T
and module P = P
and module Lit = Lit
and type proof = proof
and module P = P
(** Internal solver, available to theories. *)
type t
@ -889,7 +930,8 @@ module type SOLVER = sig
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
type proof = P.t
type dproof = proof -> unit
(** Delayed proof. This is used to build a proof step on demand. *)
(** {3 A theory}
@ -948,22 +990,6 @@ module type SOLVER = sig
theory
(** Helper to create a theory. *)
(** {3 Boolean Atoms}
Atoms are the SAT solver's version of our boolean literals
(they may have a different representation). *)
module Atom : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val pp : t CCFormat.printer
val neg : t -> t
val formula : t -> lit
val sign : t -> bool
end
(** Models
A model can be produced when the solver is found to be in a
@ -1004,7 +1030,7 @@ module type SOLVER = sig
?stat:Stat.t ->
?size:[`Big | `Tiny | `Small] ->
(* TODO? ?config:Config.t -> *)
?store_proof:bool ->
proof:proof ->
theories:theory list ->
T.Term.store ->
T.Ty.store ->
@ -1033,27 +1059,18 @@ module type SOLVER = sig
val add_theory_l : t -> theory list -> unit
val mk_atom_lit : t -> lit -> Atom.t * P.t
(** [mk_atom_lit _ lit] returns [atom, pr]
where [atom] is an internal atom for the solver,
and [pr] is a proof of [|- lit = atom] *)
val mk_lit_t : t -> ?sign:bool -> term -> lit
(** [mk_lit_t _ ~sign t] returns [lit'],
where [lit'] is [preprocess(lit)] and [lit] is
an internal representation of [± t].
val mk_atom_lit' : t -> lit -> Atom.t
(** Like {!mk_atom_t} but skips the proof *)
The proof of [|- lit = lit'] is directly added to the solver's proof. *)
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.t
(** [mk_atom_t _ ~sign t] returns [atom, pr]
where [atom] is an internal representation of [± t],
and [pr] is a proof of [|- atom = (± t)] *)
val mk_atom_t' : t -> ?sign:bool -> term -> Atom.t
(** Like {!mk_atom_t} but skips the proof *)
val add_clause : t -> Atom.t IArray.t -> P.t -> unit
val add_clause : t -> lit IArray.t -> dproof -> unit
(** [add_clause solver cs] adds a boolean clause to the solver.
Subsequent calls to {!solve} will need to satisfy this clause. *)
val add_clause_l : t -> Atom.t list -> P.t -> unit
val add_clause_l : t -> lit list -> dproof -> unit
(** Add a clause to the solver, given as a list. *)
val assert_terms : t -> term list -> unit
@ -1064,42 +1081,22 @@ module type SOLVER = sig
(** Helper that turns the term into an atom, before adding the result
to the solver as a unit clause assertion *)
(** {2 Internal representation of proofs}
A type or state convertible into {!P.t} *)
module Pre_proof : sig
type t
val output : out_channel -> t -> unit
(** Output onto a channel, efficiently *)
val pp_debug : t Fmt.printer
val pp_dot : t Fmt.printer option
(** Optional printer into DOT/graphviz *)
val check : t -> unit
(** Check the proof (to an unspecified level of confidence;
this can be a no-op). May fail. *)
val to_proof : t -> P.t
end
(** Result of solving for the current set of clauses *)
type res =
| Sat of Model.t (** Satisfiable *)
| Unsat of {
proof: Pre_proof.t option lazy_t; (** proof of unsat *)
unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *)
unsat_core: unit -> lit Iter.t; (** subset of assumptions responsible for unsat *)
} (** Unsatisfiable *)
| Unknown of Unknown.t
(** Unknown, obtained after a timeout, memory limit, etc. *)
(* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *)
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
?on_progress:(t -> unit) ->
assumptions:Atom.t list ->
assumptions:lit list ->
t ->
res
(** [solve s] checks the satisfiability of the clauses added so far to [s].

7
src/drup/dune Normal file
View file

@ -0,0 +1,7 @@
(library
(name sidekick_drup)
(public_name sidekick.drup)
(synopsis "Checker for DRUP (propositional) proofs")
(libraries sidekick.util containers iter)
(flags :standard -warn-error -a+8 -open Sidekick_util))

419
src/drup/sidekick_drup.ml Normal file
View file

@ -0,0 +1,419 @@
(** DRUP trace checker.
This module provides a checker for DRUP traces, including step-by-step
checking for traces that interleave DRUP steps with other kinds of steps.
*)
module Fmt = CCFormat
module VecI32 = VecI32
(* TODO: resolution proof construction, optionally *)
(* TODO: backward checking + pruning of traces *)
(** An instance of the checker *)
module type S = sig
module Atom : sig
type t = private int
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val neg : t -> t
val sign : t -> bool
val pp : t Fmt.printer
type atom = t
val of_int_dimacs : int -> t
(** Turn a signed integer into an atom. Positive integers are
positive atoms, and [-i] is [neg (of_int i)].
@raise Invalid_argument if the argument is 0 *)
end
type atom = Atom.t
module Clause : sig
type store
val create : unit -> store
type t
val size : t -> int
val get : t -> int -> atom
val iter : f:(atom -> unit) -> t -> unit
val pp : t Fmt.printer
val of_list : store -> atom list -> t
val of_iter : store -> atom Iter.t -> t
end
type clause = Clause.t
module Checker : sig
type t
val create : Clause.store -> t
val add_clause : t -> Clause.t -> unit
val is_valid_drup : t -> Clause.t -> bool
val del_clause : t -> Clause.t -> unit
end
end
module Make() : S = struct
(** Boolean atoms *)
module Atom = struct
type t = int
type atom = t
let hash = CCHash.int
let equal : t -> t -> bool = (=)
let compare : t -> t -> int = compare
let[@inline] neg x = x lxor 1
let[@inline] of_int_dimacs x =
if x=0 then invalid_arg "Atom.of_int_dimacs: 0 is not acceptable";
let v = abs x lsl 1 in
if x < 0 then neg v else v
let[@inline] sign x = (x land 1) = 0
let[@inline] to_int x = (if sign x then 1 else -1) * (x lsr 1)
let pp out x =
Fmt.fprintf out "%s%d" (if sign x then "+" else "-") (x lsr 1)
let[@inline] of_int_unsafe i = i
let dummy = 0
module Assign = struct
type t = Bitvec.t
let create = Bitvec.create
let ensure_size = Bitvec.ensure_size
let is_true = Bitvec.get
let[@inline] is_false self (a:atom) : bool =
is_true self (neg a)
let[@inline] is_unassigned self a =
not (is_true self a) && not (is_false self a)
let set = Bitvec.set
end
module Set = CCSet.Make(CCInt)
module Map = struct
type 'a t = 'a Vec.t
let create () = Vec.create ()
let[@inline] ensure_has (self:_ t) a mk : unit =
(* size: 2+atom, because: 1+atom makes atom valid, and if it's positive,
2+atom is (¬atom)+1 *)
Vec.ensure_size_with self mk (2+(a:atom:>int))
let get = Vec.get
let set = Vec.set
end
module Stack = struct
include VecI32
let create()=create()
end
end
type atom = Atom.t
(** Boolean clauses *)
module Clause : sig
type store
val create : unit -> store
type t
val size : t -> int
val id : t -> int
val get : t -> int -> atom
val iter : f:(atom -> unit) -> t -> unit
val watches: t -> atom * atom
val set_watches : t -> atom * atom -> unit
val pp : t Fmt.printer
val of_list : store -> atom list -> t
val of_iter : store -> atom Iter.t -> t
module Set : CCSet.S with type elt = t
module Tbl : CCHashtbl.S with type key = t
end = struct
type t = {
id: int;
atoms: atom array;
mutable watches: atom * atom;
}
type store = {
mutable n: int;
}
let create(): store =
{ n=0; }
let[@inline] id self = self.id
let[@inline] size self = Array.length self.atoms
let[@inline] get self i = Array.get self.atoms i
let[@inline] watches self = self.watches
let[@inline] set_watches self w = self.watches <- w
let[@inline] iter ~f self =
for i=0 to Array.length self.atoms-1 do
f (Array.unsafe_get self.atoms i)
done
let pp out (self:t) =
let pp_watches out = function
| (p,q) when p=Atom.dummy || q=Atom.dummy -> ()
| (p,q) -> Fmt.fprintf out "@ :watches (%a,%a)" Atom.pp p Atom.pp q in
Fmt.fprintf out "(@[cl[%d]@ %a%a])"
self.id (Fmt.Dump.array Atom.pp) self.atoms pp_watches self.watches
let of_iter self (atoms:atom Iter.t) : t =
(* normalize + find in table *)
let atoms = Atom.Set.of_iter atoms |> Atom.Set.to_iter |> Iter.to_array in
let id = self.n in
self.n <- 1 + self.n;
let c = {atoms; id; watches=Atom.dummy, Atom.dummy} in
c
let of_list self atoms : t = of_iter self (Iter.of_list atoms)
module As_key = struct
type nonrec t=t
let[@inline] hash a = CCHash.int a.id
let[@inline] equal a b = a.id = b.id
let[@inline] compare a b = compare a.id b.id
end
module Set = CCSet.Make(As_key)
module Tbl = CCHashtbl.Make(As_key)
end
type clause = Clause.t
(** Forward proof checker.
Each event is checked by reverse-unit propagation on previous events. *)
module Checker : sig
type t
val create : Clause.store -> t
val add_clause : t -> Clause.t -> unit
val is_valid_drup : t -> Clause.t -> bool
val del_clause : t -> Clause.t -> unit
end = struct
type t = {
cstore: Clause.store;
assign: Atom.Assign.t; (* atom -> is_true(atom) *)
trail: Atom.Stack.t; (* current assignment *)
mutable trail_ptr : int; (* offset in trail for propagation *)
active_clauses: unit Clause.Tbl.t;
watches: Clause.t Vec.t Atom.Map.t; (* atom -> clauses it watches *)
}
let create cstore : t =
{ trail=Atom.Stack.create();
trail_ptr = 0;
cstore;
active_clauses=Clause.Tbl.create 32;
assign=Atom.Assign.create();
watches=Atom.Map.create();
}
(* ensure data structures are big enough to handle [a] *)
let ensure_atom_ self (a:atom) =
Atom.Assign.ensure_size self.assign a;
(* size: 2+atom, because: 1+atom makes atom valid, and if it's positive,
2+atom is (¬atom)+1 *)
Atom.Map.ensure_has self.watches a (fun _ -> Vec.create ());
()
let[@inline] is_true self (a:atom) : bool =
Atom.Assign.is_true self.assign a
let[@inline] is_false self (a:atom) : bool =
Atom.Assign.is_false self.assign a
let[@inline] is_unassigned self a =
Atom.Assign.is_unassigned self.assign a
let add_watch_ self (a:atom) (c:clause) =
Vec.push (Atom.Map.get self.watches a) c
let remove_watch_ self (a:atom) idx =
let v = Atom.Map.get self.watches a in
Vec.fast_remove v idx
exception Conflict
let raise_conflict_ self a =
Log.debugf 5 (fun k->k"conflict on atom %a" Atom.pp a);
raise Conflict
(* set atom to true *)
let[@inline] set_atom_true (self:t) (a:atom) : unit =
if is_true self a then ()
else if is_false self a then raise_conflict_ self a
else (
Atom.Assign.set self.assign a true;
Atom.Stack.push self.trail a
)
(* print the trail *)
let pp_trail_ out self =
Fmt.fprintf out "(@[%a@])" (Fmt.iter Atom.pp) (Atom.Stack.to_iter self.trail)
exception Found_watch of atom
exception Is_sat
exception Is_undecided
(* check if [c] is false in current trail *)
let c_is_false_ self c =
try Clause.iter c ~f:(fun a -> if not (is_false self a) then raise Exit); true
with Exit -> false
type propagation_res =
| Keep
| Remove
(* do boolean propagation in [c], which is watched by the true literal [a] *)
let propagate_in_clause_ (self:t) (a:atom) (c:clause) : propagation_res =
assert (is_true self a);
let a1, a2 = Clause.watches c in
let na = Atom.neg a in
(* [q] is the other literal in [c] such that [¬q] watches [c]. *)
let q = if Atom.equal a1 na then a2 else (assert(a2==na); a1) in
try
if is_true self q then Keep (* clause is satisfied *)
else (
let n_unassigned = ref 0 in
let unassigned_a = ref a in (* an unassigned atom, if [!n_unassigned > 0] *)
if not (is_false self q) then unassigned_a := q;
begin
try
Clause.iter c
~f:(fun ai ->
if is_true self ai then raise Is_sat (* no watch update *)
else if is_unassigned self ai then (
incr n_unassigned;
if q <> ai then unassigned_a := ai;
if !n_unassigned >= 2 then raise Is_undecided; (* early exit *)
);
)
with Is_undecided -> ()
end;
if !n_unassigned = 0 then (
(* if we reach this point it means no literal is true, and none is
unassigned. So they're all false and we have a conflict. *)
assert (is_false self q);
raise_conflict_ self a;
) else if !n_unassigned = 1 then (
(* no lit is true, only one is unassigned: propagate it.
no need to update the watches as the clause is satisfied. *)
assert (is_unassigned self !unassigned_a);
let p = !unassigned_a in
Log.debugf 30 (fun k->k"(@[propagate@ :atom %a@ :reason %a@])" Atom.pp p Clause.pp c);
set_atom_true self p;
Keep
) else (
(* at least 2 unassigned, just update the watch literal to [¬p] *)
let p = !unassigned_a in
assert (p <> q);
Clause.set_watches c (q, p);
add_watch_ self (Atom.neg p) c;
Remove
);
)
with
| Is_sat -> Keep
let propagate_atom_ self (a:atom) : unit =
let v = Atom.Map.get self.watches a in
let i = ref 0 in
while !i < Vec.size v do
match propagate_in_clause_ self a (Vec.get v !i) with
| Keep -> incr i;
| Remove ->
remove_watch_ self a !i
done
(* perform boolean propagation in a fixpoint
@raise Conflict if a clause is false *)
let bcp_fixpoint_ (self:t) : unit =
Profile.with_ "bcp-fixpoint" @@ fun() ->
while self.trail_ptr < Atom.Stack.size self.trail do
let a = Atom.Stack.get self.trail self.trail_ptr in
Log.debugf 50 (fun k->k"(@[bcp@ :atom %a@])" Atom.pp a);
self.trail_ptr <- 1 + self.trail_ptr;
propagate_atom_ self a;
done
(* calls [f] and then restore trail to what it was *)
let with_restore_trail_ self f =
let trail_size0 = Atom.Stack.size self.trail in
let ptr0 = self.trail_ptr in
let restore () =
(* unassign new literals *)
for i=trail_size0 to Atom.Stack.size self.trail - 1 do
let a = Atom.Stack.get self.trail i in
assert (is_true self a);
Atom.Assign.set self.assign a false;
done;
(* remove literals from trail *)
Atom.Stack.shrink self.trail trail_size0;
self.trail_ptr <- ptr0
in
CCFun.finally ~h:restore ~f
(* add clause to the state *)
let add_clause (self:t) (c:Clause.t) =
Log.debugf 50 (fun k->k"(@[add-clause@ %a@])" Clause.pp c);
Clause.iter c ~f:(ensure_atom_ self);
Clause.Tbl.add self.active_clauses c ();
begin match Clause.size c with
| 0 -> ()
| 1 ->
set_atom_true self (Clause.get c 0);
| _ ->
let c0 = Clause.get c 0 in
let c1 = Clause.get c 1 in
assert (c0 <> c1);
Clause.set_watches c (c0,c1);
(* make sure watches are valid *)
if is_false self c0 then (
match propagate_in_clause_ self (Atom.neg c0) c with
| Keep -> add_watch_ self (Atom.neg c0) c;
| Remove -> ()
) else (
add_watch_ self (Atom.neg c0) c
);
if is_false self c1 then (
match propagate_in_clause_ self (Atom.neg c1) c with
| Keep -> add_watch_ self (Atom.neg c1) c;
| Remove -> ()
) else (
add_watch_ self (Atom.neg c1) c
)
end;
()
let is_valid_drup (self:t) (c:Clause.t) : bool =
(* negate [c], pushing each atom on trail, and see if we get [Conflict]
by pure propagation *)
try
with_restore_trail_ self @@ fun () ->
Clause.iter c
~f:(fun a ->
if is_true self a then raise_notrace Conflict; (* tautology *)
let a' = Atom.neg a in
if is_true self a' then () else (
set_atom_true self a'
));
bcp_fixpoint_ self;
(*
(* slow sanity check *)
Clause.Tbl.iter
(fun c () ->
if c_is_false_ self c then
Log.debugf 0 (fun k->k"clause is false: %a" Clause.pp c))
self.active_clauses;
*)
false
with Conflict ->
true
let del_clause (_self:t) (_c:Clause.t) : unit =
() (* TODO *)
end
end

40
src/lit/Sidekick_lit.ml Normal file
View file

@ -0,0 +1,40 @@
(** Implementation of literals from terms *)
module Make(T : Sidekick_core.TERM)
: Sidekick_core.LIT with module T = T
= struct
module T = T
type term = T.Term.t
type t = {
lit_term: term;
lit_sign : bool
}
let[@inline] neg l = {l with lit_sign=not l.lit_sign}
let[@inline] sign t = t.lit_sign
let[@inline] abs t = {t with lit_sign=true}
let[@inline] term (t:t): term = t.lit_term
let[@inline] signed_term t = term t, sign t
let make ~sign t = {lit_sign=sign; lit_term=t}
let atom tst ?(sign=true) (t:term) : t =
let t, sign' = T.Term.abs tst t in
let sign = if not sign' then not sign else sign in
make ~sign t
let equal a b =
a.lit_sign = b.lit_sign &&
T.Term.equal a.lit_term b.lit_term
let hash a =
let sign = a.lit_sign in
CCHash.combine3 2 (CCHash.bool sign) (T.Term.hash a.lit_term)
let pp out l =
if l.lit_sign then T.Term.pp out l.lit_term
else Format.fprintf out "(@[@<1>¬@ %a@])" T.Term.pp l.lit_term
let norm_sign l = if l.lit_sign then l, true else neg l, false
end

7
src/lit/dune Normal file
View file

@ -0,0 +1,7 @@
(library
(name sidekick_lit)
(public_name sidekick.lit)
(synopsis "Implementation of literals for Sidekick")
(libraries containers sidekick.core sidekick.util)
(flags :standard -warn-error -a+8 -open Sidekick_util))

98
src/lra/sidekick_arith_lra.ml
View file

@ -60,9 +60,7 @@ module type ARG = sig
val has_ty_real : term -> bool
(** Does this term have the type [Real] *)
(** TODO: more accurate certificates *)
val proof_lra : S.P.lit Iter.t -> S.P.t
val proof_lra_l : S.P.lit list -> S.P.t
val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit
module Gensym : sig
type t
@ -235,23 +233,18 @@ module Make(A : ARG) : S with module A = A = struct
);
proxy
let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits =
let pr = A.lemma_lra (Iter.of_list lits) in
PA.add_clause lits pr
(* preprocess linear expressions away *)
let preproc_lra (self:state) si ~mk_lit ~add_clause
(t:T.t) : (T.t * _) option =
Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
(t:T.t) : T.t option =
Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
let tst = SI.tst si in
let sub_proofs_ = ref [] in
(* preprocess subterm *)
let preproc_t t =
let u, p_t_eq_u = SI.preprocess_term ~add_clause si t in
if t != u then (
(* add [|- t=u] to hyps *)
sub_proofs_ := (t,u,p_t_eq_u) :: !sub_proofs_;
);
u
in
let preproc_t t = SI.preprocess_term si (module PA) t in
(* tell the CC this term exists *)
let declare_term_to_cc t =
@ -270,13 +263,13 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.encoded_eqs t ();
(* encode [t <=> (u1 /\ u2)] *)
let lit_t = mk_lit t in
let lit_u1 = mk_lit u1 in
let lit_u2 = mk_lit u2 in
add_clause [SI.Lit.neg lit_t; lit_u1] A.S.P.(A.proof_lra_l [lit_na t; lit_a u1]) ;
add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [lit_na t; lit_a u2]);
add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]
A.S.P.(A.proof_lra_l [lit_a t; lit_na u1; lit_na u2]);
let lit_t = PA.mk_lit t in
let lit_u1 = PA.mk_lit u1 in
let lit_u2 = PA.mk_lit u2 in
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
add_clause_lra_ (module PA)
[SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
);
None
@ -305,15 +298,14 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
begin
let lit = mk_lit new_t in
let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
(* FIXME: by def proxy + LRA *)
let proof = A.S.P.sorry in
Some (new_t, proof)
(* FIXME: emit proof: by def proxy + LRA *)
Some new_t
| Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@ -332,14 +324,14 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
begin
let lit = mk_lit new_t in
let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk v op q in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
let proof = A.S.P.sorry in (* TODO: some sort of equality + def? *)
Some (new_t, proof)
(* FIXME: preprocess proof *)
Some new_t
end
| LRA_op _ | LRA_mult _ ->
@ -352,10 +344,8 @@ module Make(A : ARG) : S with module A = A = struct
let proxy = var_encoding_comb self ~pre:"_le" le_comb in
declare_term_to_cc proxy;
(* TODO: proof by def of proxy *)
let proof = A.S.P.sorry in
Some (proxy, proof)
(* FIXME: proof by def of proxy *)
Some proxy
) else (
(* a bit more complicated: we cannot just define [proxy := le_comb]
because of the coefficient.
@ -378,28 +368,29 @@ module Make(A : ARG) : S with module A = A = struct
declare_term_to_cc proxy;
declare_term_to_cc proxy2;
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
PA.add_clause [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
PA.add_clause [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
(* FIXME: actual proof *)
let proof = A.S.P.sorry in
Some (proxy, proof)
Some proxy
)
| LRA_other t when A.has_ty_real t -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
None
let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof) option =
let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
match A.view_as_lra t with
| LRA_op _ | LRA_mult _ ->
let le = as_linexp_id t in
if LE.is_const le then (
let c = LE.const le in
Some (A.mk_lra self.tst (LRA_const c), A.S.P.sorry)
(* FIXME: proof *)
Some (A.mk_lra self.tst (LRA_const c))
) else None
| LRA_pred (pred, l1, l2) ->
let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@ -413,16 +404,13 @@ module Make(A : ARG) : S with module A = A = struct
| Eq -> A.Q.(c = zero)
| Neq -> A.Q.(c <> zero)
in
Some (A.mk_bool self.tst is_true, A.S.P.sorry)
(* FIXME: proof *)
Some (A.mk_bool self.tst is_true)
) else None
| _ -> None
module Q_map = CCMap.Make(A.Q)
let plit_of_lit lit =
let t, sign = Lit.signed_term lit in
A.S.P.lit_mk sign t
(* raise conflict from certificate *)
let fail_with_cert si acts cert : 'a =
Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert;
@ -431,9 +419,7 @@ module Make(A : ARG) : S with module A = A = struct
|> CCList.flat_map (Tag.to_lits si)
|> List.rev_map SI.Lit.neg
in
(* TODO: more detailed proof certificate *)
let pr =
A.(proof_lra (Iter.of_list confl |> Iter.map plit_of_lit)) in
let pr = A.lemma_lra (Iter.of_list confl) in
SI.raise_conflict si acts confl pr
let on_propagate_ si acts lit ~reason =
@ -443,8 +429,8 @@ module Make(A : ARG) : S with module A = A = struct
SI.propagate si acts lit
~reason:(fun() ->
let lits = CCList.flat_map (Tag.to_lits si) reason in
let proof = A.proof_lra Iter.(cons lit (of_list lits) |> map plit_of_lit) in
CCList.flat_map (Tag.to_lits si) reason, proof)
let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in
CCList.flat_map (Tag.to_lits si) reason, pr)
| _ -> ()
let check_simplex_ self si acts : SimpSolver.Subst.t =
@ -592,7 +578,7 @@ module Make(A : ARG) : S with module A = A = struct
);
()
let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
let final_check_ (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
Log.debug 5 "(th-lra.final-check)";
Profile.with_ "lra.final-check" @@ fun () ->

22
src/lra/tests/dune
View file

@ -1,25 +1,15 @@
(executable
(name run_tests)
(modules run_tests test_simplex2)
(libraries containers sidekick.arith-lra
sidekick.zarith zarith iter alcotest qcheck)
(flags :standard -warn-error -a+8 -color always))
(alias
(name runtest)
(locks /test)
(package sidekick)
(action
(progn
(run ./run_tests.exe alcotest) ; run regressions first
(run ./run_tests.exe qcheck --verbose))))
(library
(name sidekick_test_simplex2)
(libraries zarith sidekick.arith-lra sidekick.util sidekick.zarith
qcheck alcotest))
(rule
(targets test_simplex2.ml)
(targets sidekick_test_simplex2.ml)
(enabled_if (>= %{ocaml_version} 4.08.0))
(action (copy test_simplex2.real.ml %{targets})))
(rule
(targets test_simplex2.ml)
(targets sidekick_test_simplex2.ml)
(enabled_if (< %{ocaml_version} 4.08.0))
(action (with-stdout-to %{targets} (echo "let props=[];; let tests=\"simplex2\",[]"))))

7
src/main/dune
View file

@ -4,9 +4,11 @@
(name main)
(public_name sidekick)
(package sidekick-bin)
(modes native)
(libraries containers iter result sidekick.sat sidekick.core sidekick-base
sidekick.msat-solver sidekick-bin.smtlib sidekick.tef
sidekick.memtrace)
sidekick.smt-solver sidekick-bin.smtlib sidekick.tef
sidekick.drup
sidekick.memtrace sidekick-bin.lib)
(flags :standard -safe-string -color always -open Sidekick_util))
(rule
@ -17,4 +19,3 @@
(with-stdout-to %{targets}
(echo "let version = {git|%{version:sidekick}|git}"))))
(ocamllex (modules Dimacs_lexer))

58
src/main/main.ml
View file

@ -19,7 +19,6 @@ exception Out_of_space
let file = ref ""
let p_cnf = ref false
let p_dot_proof = ref ""
let p_proof = ref false
let p_model = ref false
let check = ref false
@ -32,8 +31,6 @@ let p_gc_stat = ref false
let p_progress = ref false
let proof_file = ref ""
let hyps : Term.t list ref = ref []
(* Arguments parsing *)
let int_arg r arg =
let l = String.length arg in
@ -69,7 +66,6 @@ let argspec = Arg.align [
"--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";
"--proof", Arg.Set p_proof, " print proof";
"--no-proof", Arg.Clear p_proof, " do not print proof";
@ -97,8 +93,13 @@ let check_limits () =
else if s > !size_limit then
raise Out_of_space
let main_smt ~dot_proof () : _ result =
let main_smt () : _ result =
let module Proof = Sidekick_smtlib.Proof in
let tst = Term.create ~size:4_096 () in
(* FIXME: use this to enable/disable actual proof
let store_proof = !check || !p_proof || !proof_file <> "" in
*)
let proof = Proof.create() in
let solver =
let theories =
(* TODO: probes, to load only required theories *)
@ -108,8 +109,7 @@ let main_smt ~dot_proof () : _ result =
Process.th_lra;
]
in
let store_proof = !check || !p_proof || !proof_file <> "" in
Process.Solver.create ~store_proof ~theories tst () ()
Process.Solver.create ~proof ~theories tst () ()
in
let proof_file = if !proof_file ="" then None else Some !proof_file in
if !check then (
@ -123,13 +123,12 @@ let main_smt ~dot_proof () : _ result =
(* process statements *)
let res =
try
let hyps = Vec.create() in
E.fold_l
(fun () ->
Process.process_stmt
~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file
~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file
~time:!time_limit ~memory:!size_limit
?dot_proof ~pp_model:!p_model
~pp_model:!p_model
~check:!check ~progress:!p_progress
solver)
() input
@ -142,23 +141,32 @@ let main_smt ~dot_proof () : _ result =
res
let main_cnf () : _ result =
let n_decision = ref 0 in
let n_confl = ref 0 in
let n_atoms = ref 0 in
let solver =
Pure_sat_solver.SAT.create
~on_conflict:(fun _ -> incr n_confl)
~on_decision:(fun _ -> incr n_decision)
~on_new_atom:(fun _ -> incr n_atoms)
~size:`Big ()
let module Proof = Pure_sat_solver.Proof in
let module S = Pure_sat_solver in
let proof, in_memory_proof =
if !check then (
let pr, inmp = Proof.create_in_memory () in
pr, Some inmp
) else if !proof_file <> "" then (
Proof.create_to_file !proof_file, None
) else (
Proof.dummy, None
)
in
Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
let r = Pure_sat_solver.solve ~check:!check solver in
let stat = Stat.create () in
let solver = S.SAT.create ~size:`Big ~proof ~stat () in
S.Dimacs.parse_file solver !file >>= fun () ->
let r = S.solve ~check:!check ?in_memory_proof solver in
(* FIXME: if in memory proof and !proof_file<>"",
then dump proof into file now *)
Proof.close proof;
if !p_stat then (
Fmt.printf "; n-atoms: %d n-conflicts: %d n-decisions: %d@."
!n_atoms !n_confl !n_decision;
Fmt.printf "%a@." Stat.pp_all (Stat.all stat);
);
r
@ -176,8 +184,6 @@ let main () =
Arg.usage argspec usage;
exit 2
);
let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
let al = Gc.create_alarm check_limits in
Util.setup_gc();
let is_cnf = Filename.check_suffix !file ".cnf" in
@ -185,7 +191,7 @@ let main () =
if is_cnf then (
main_cnf ()
) else (
main_smt ~dot_proof ()
main_smt ()
)
in
if !p_gc_stat then (

190
src/main/pure_sat_solver.ml
View file

@ -4,43 +4,185 @@
module E = CCResult
module SS = Sidekick_sat
module Lit = struct
type t = int
let norm_sign t = if t>0 then t, true else -t, false
let abs = abs
let sign t = t>0
let equal = CCInt.equal
let hash = CCHash.int
let neg x = -x
let pp = Fmt.int
end
(* TODO: on the fly compression *)
module Proof : sig
include Sidekick_sat.PROOF with type lit = Lit.t
type in_memory
val dummy : t
val create_in_memory : unit -> t * in_memory
val to_string : in_memory -> string
val to_chan : out_channel -> in_memory -> unit
val create_to_file : string -> t
val close : t -> unit
type event = Sidekick_bin_lib.Drup_parser.event =
| Input of int list
| Add of int list
| Delete of int list
val iter_events : in_memory -> event Iter.t
end = struct
let bpf = Printf.bprintf
let fpf = Printf.fprintf
type lit = Lit.t
type in_memory = Buffer.t
type t =
| Dummy
| Inner of in_memory
| Out of {
oc: out_channel;
close: (unit -> unit);
}
type dproof = t -> unit
let[@inline] with_proof pr f = match pr with
| Dummy -> ()
| Inner _ | Out _ -> f pr
let[@inline] emit_lits_buf_ buf lits =
lits (fun i -> bpf buf "%d " i)
let[@inline] emit_lits_out_ oc lits =
lits (fun i -> fpf oc "%d " i)
let emit_input_clause lits self =
match self with
| Dummy -> ()
| Inner buf ->
bpf buf "i "; emit_lits_buf_ buf lits; bpf buf "0\n"
| Out {oc;_} ->
fpf oc "i "; emit_lits_out_ oc lits; fpf oc "0\n"
let emit_redundant_clause lits self =
match self with
| Dummy -> ()
| Inner buf ->
bpf buf "r "; emit_lits_buf_ buf lits; bpf buf "0\n"
| Out {oc;_} -> fpf oc "r "; emit_lits_out_ oc lits; fpf oc "0\n"
let del_clause lits self =
match self with
| Dummy -> ()
| Inner buf ->
bpf buf "d "; emit_lits_buf_ buf lits; bpf buf "0\n"
| Out {oc; _}->
fpf oc "d "; emit_lits_out_ oc lits; fpf oc "0\n"
(* lifetime *)
let dummy : t = Dummy
let create_in_memory () : t * in_memory =
let buf = Buffer.create 1_024 in
Inner buf, buf
let create_to_file file =
let oc, close =
match Filename.extension file with
| ".gz" ->
let cmd = Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file) in
Log.debugf 1 (fun k->k"proof file: command is %s" cmd);
let oc = Unix.open_process_out cmd in
oc, (fun () -> ignore (Unix.close_process_out oc: Unix.process_status))
| ".drup" ->
let oc = open_out_bin file in
oc, (fun () -> close_out_noerr oc)
| s -> Error.errorf "unknown file extension '%s'" s
in
Out {oc; close}
let close = function
| Dummy | Inner _ -> ()
| Out {close; oc} -> flush oc; close()
let to_string = Buffer.contents
let to_chan = Buffer.output_buffer
module DP = Sidekick_bin_lib.Drup_parser
type event = DP.event =
| Input of int list
| Add of int list
| Delete of int list
(* parse the proof back *)
let iter_events (self:in_memory) : DP.event Iter.t =
let dp = DP.create_string (to_string self) in
DP.iter dp
end
module Arg = struct
module Formula = struct
type t = int
let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated
let abs = abs
let sign t = t>0
let equal = CCInt.equal
let hash = CCHash.int
let neg x = -x
let pp = Fmt.int
end
type proof=unit
module Lit = Lit
type lit = Lit.t
module Proof = Proof
type proof = Proof.t
end
module SAT = Sidekick_sat.Make_pure_sat(Arg)
module Dimacs = struct
open Sidekick_base
module BL = Sidekick_bin_lib
module T = Term
let parse_file (solver:SAT.t) (file:string) : (unit, string) result =
let get_lit i : SAT.atom = SAT.make_atom solver i in
try
CCIO.with_in file
(fun ic ->
let p = Dimacs_parser.create ic in
Dimacs_parser.iter p
(fun c ->
let atoms = List.rev_map get_lit c in
SAT.add_clause solver atoms ());
let p = BL.Dimacs_parser.create ic in
BL.Dimacs_parser.iter p
(fun c -> SAT.add_input_clause solver c);
Ok ())
with e ->
E.of_exn_trace e
end
let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
let check_proof (proof:Proof.in_memory) : bool =
Profile.with_ "pure-sat.check-proof" @@ fun () ->
let module SDRUP = Sidekick_drup.Make() in
let store = SDRUP.Clause.create() in
let checker = SDRUP.Checker.create store in
let ok = ref true in
let tr_clause c =
let c = List.rev_map SDRUP.Atom.of_int_dimacs c in
SDRUP.Clause.of_list store c
in
Proof.iter_events proof
(function
| Proof.Input c ->
let c = tr_clause c in
SDRUP.Checker.add_clause checker c
| Proof.Add c ->
let c = tr_clause c in
if not (SDRUP.Checker.is_valid_drup checker c) then (
ok := false;
);
SDRUP.Checker.add_clause checker c;
| Proof.Delete c ->
let c = tr_clause c in
SDRUP.Checker.del_clause checker c;
);
!ok
let solve ?(check=false) ?in_memory_proof (solver:SAT.t) : (unit, string) result =
let res =
Profile.with_ "solve" (fun () -> SAT.solve solver)
in
@ -53,8 +195,14 @@ let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
| SAT.Unsat (module US) ->
if check then (
let pr = US.get_proof() in
SAT.Proof.check pr;
match in_memory_proof with
| None ->
Error.errorf "Cannot validate proof, no in-memory proof provided"
| Some proof ->
let ok = check_proof proof in
if not ok then (
Error.errorf "Proof validation failed"
);
);
let t3 = Sys.time () -. t2 in

11
src/mini-cc/tests/dune
View file

@ -1,7 +1,4 @@
(tests
(names tests)
(libraries sidekick.mini-cc sidekick-base alcotest)
(package sidekick-base)
(flags :standard -warn-error -a+8 -safe-string -color always)
(locks /test)
(modes native))
(library
(name sidekick_test_minicc)
(libraries sidekick.mini-cc sidekick-base alcotest)
(flags :standard -warn-error -a+8))

7
src/mini-cc/tests/tests.ml → src/mini-cc/tests/sidekick_test_minicc.ml
View file

@ -2,7 +2,7 @@ open Sidekick_base
module A = Alcotest
module CC = Sidekick_mini_cc.Make(struct
module T = Sidekick_base.Arg
module T = Sidekick_base.Solver_arg
let cc_view = Term.cc_view
end)
@ -40,7 +40,7 @@ module Setup() = struct
let p t1 = app_l fun_p [t1]
end
let l = ref []
let l : unit Alcotest.test_case list ref = ref []
let mk_test name f =
l := (name, `Quick, f) :: !l
@ -165,5 +165,4 @@ let () = mk_test "test_reg_1" @@ fun () ->
A.(check bool) "is-unsat" (CC.check_sat cc) false;
()
(* run alcotest *)
let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]
let tests = "mini-cc", List.rev !l

6
src/msat-solver/dune
View file

@ -1,6 +0,0 @@
(library
(name Sidekick_msat_solver)
(public_name sidekick.msat-solver)
(libraries containers iter sidekick.core sidekick.util
sidekick.cc sidekick.sat sidekick.backend)
(flags :standard -open Sidekick_util))

6
src/base/Proof.ml → src/proof/Proof.ml
View file

@ -1,4 +1,5 @@
(*
open Base_types
module T = Term
@ -40,6 +41,7 @@ type t =
| CC_lemma of clause
| Assertion of term
| Assertion_c of clause
| Drup_res of clause
| Hres of t * hres_step list
| Res of term * t * t
| Res1 of t * t
@ -136,6 +138,7 @@ let bool_eq a b : t = Bool_eq (a,b)
let bool_c name c : t = Bool_c (name, c)
let nn c : t = Nn c
let drup_res c : t = Drup_res c
let hres_l p l : t =
let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
if l=[] then p else Hres (p,l)
@ -159,6 +162,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
| CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u
| CC_lemma c | Assertion_c c -> f_clause c
| Assertion t -> f_t t
| Drup_res c -> f_clause c
| Hres (i, l) ->
f_p i;
List.iter
@ -402,6 +406,7 @@ module Quip = struct
| Nn p -> l[a"nn";pp_rec p]
| Assertion t -> l[a"assert";pp_t t]
| Assertion_c c -> l[a"assert-c";pp_cl c]
| Drup_res c -> l[a"drup";pp_cl c]
| Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)]
| Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
| Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]
@ -528,3 +533,4 @@ let pp_debug ~sharing out p =
in
let module M = Quip.Make(Out) in
M.pp_debug ~sharing p out
*)

3
src/base/Proof.mli → src/proof/Proof.mli
View file

@ -1,3 +1,5 @@
(*
(** Proofs of unsatisfiability
Proofs are used in sidekick when the problem is found {b unsatisfiable}.
@ -26,3 +28,4 @@ val ite_false : term -> t
val lra : lit Iter.t -> t
val lra_l : lit list -> t
*)

120
src/sat/Heap.ml
View file

@ -4,16 +4,19 @@ module type RANKED = Heap_intf.RANKED
module type S = Heap_intf.S
module Make(Elt : RANKED) = struct
type elt_store = Elt.store
type elt = Elt.t
type t = {
heap : elt Vec.t;
} [@@unboxed]
store : elt_store;
heap : VecI32.t; (* vec of elements *)
}
let _absent_index = -1
let create () =
{ heap = Vec.create(); }
let create store : t =
{ store;
heap = VecI32.create(); }
let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@ -21,92 +24,96 @@ module Make(Elt : RANKED) = struct
(*
let rec heap_property cmp ({heap=heap} as s) i =
i >= (Vec.size heap) ||
i >= (VecI32.size heap) ||
((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
&& heap_property cmp s (left i) && heap_property cmp s (right i))
let heap_property cmp s = heap_property cmp s 1
*)
let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecI32.get self.heap i)
let[@inline] set_elt_ self i elt = VecI32.set self.heap i (elt:Elt.t:>int)
(* [elt] is above or at its expected position. Move it up the heap
(towards high indices) to restore the heap property *)
let percolate_up {heap} (elt:Elt.t) : unit =
let pi = ref (parent (Elt.idx elt)) in
let i = ref (Elt.idx elt) in
while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do
Vec.set heap !i (Vec.get heap !pi);
Elt.set_idx (Vec.get heap !i) !i;
let percolate_up (self:t) (elt:Elt.t) : unit =
let pi = ref (parent (Elt.heap_idx self.store elt)) in
let i = ref (Elt.heap_idx self.store elt) in
while !i <> 0 && Elt.cmp self.store elt (get_elt_ self !pi) do
set_elt_ self !i (get_elt_ self !pi);
Elt.set_heap_idx self.store (get_elt_ self !i) !i;
i := !pi;
pi := parent !i
done;
Vec.set heap !i elt;
Elt.set_idx elt !i
set_elt_ self !i elt;
Elt.set_heap_idx self.store elt !i
let percolate_down {heap} (elt:Elt.t): unit =
let sz = Vec.size heap in
let li = ref (left (Elt.idx elt)) in
let ri = ref (right (Elt.idx elt)) in
let i = ref (Elt.idx elt) in
let percolate_down (self:t) (elt:Elt.t): unit =
let sz = VecI32.size self.heap in
let li = ref (left (Elt.heap_idx self.store elt)) in
let ri = ref (right (Elt.heap_idx self.store elt)) in
let i = ref (Elt.heap_idx self.store elt) in
begin
try
while !li < sz do
let child =
if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li)
if !ri < sz &&
Elt.cmp self.store (get_elt_ self !ri) (get_elt_ self !li)
then !ri
else !li
in
if not (Elt.cmp (Vec.get heap child) elt) then raise Exit;
Vec.set heap !i (Vec.get heap child);
Elt.set_idx (Vec.get heap !i) !i;
if not (Elt.cmp self.store (get_elt_ self child) elt) then raise_notrace Exit;
set_elt_ self !i (get_elt_ self child);
Elt.set_heap_idx self.store (get_elt_ self !i) !i;
i := child;
li := left !i;
ri := right !i
done;
with Exit -> ()
end;
Vec.set heap !i elt;
Elt.set_idx elt !i
set_elt_ self !i elt;
Elt.set_heap_idx self.store elt !i
let[@inline] in_heap x = Elt.idx x >= 0
let[@inline] in_heap self x = Elt.heap_idx self.store x >= 0
let[@inline] decrease s x = assert (in_heap x); percolate_up s x
let[@inline] decrease self x = assert (in_heap self x); percolate_up self x
(*
let increase cmp s n =
assert (in_heap s n); percolate_down cmp s (V.get s.indices n)
*)
let filter s filt =
let filter (self:t) filt : unit =
let j = ref 0 in
let lim = Vec.size s.heap in
let lim = VecI32.size self.heap in
for i = 0 to lim - 1 do
if filt (Vec.get s.heap i) then (
Vec.set s.heap !j (Vec.get s.heap i);
Elt.set_idx (Vec.get s.heap i) !j;
if filt (get_elt_ self i) then (
set_elt_ self !j (get_elt_ self i);
Elt.set_heap_idx self.store (get_elt_ self i) !j;
incr j;
) else (
Elt.set_idx (Vec.get s.heap i) _absent_index;
Elt.set_heap_idx self.store (get_elt_ self i) _absent_index;
);
done;
Vec.shrink s.heap (lim - !j);
VecI32.shrink self.heap (lim - !j);
for i = (lim / 2) - 1 downto 0 do
percolate_down s (Vec.get s.heap i)
percolate_down self (get_elt_ self i)
done
let size s = Vec.size s.heap
let[@inline] size s = VecI32.size s.heap
let[@inline] is_empty s = VecI32.is_empty s.heap
let is_empty s = Vec.is_empty s.heap
let clear {heap} =
Vec.iter (fun e -> Elt.set_idx e _absent_index) heap;
Vec.clear heap;
let clear self : unit =
VecI32.iter self.heap
~f:(fun e -> Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index);
VecI32.clear self.heap;
()
let insert s elt =
if not (in_heap elt) then (
Elt.set_idx elt (Vec.size s.heap);
Vec.push s.heap elt;
percolate_up s elt;
let insert self elt =
if not (in_heap self elt) then (
Elt.set_heap_idx self.store elt (VecI32.size self.heap);
VecI32.push self.heap (elt:Elt.t:>int);
percolate_up self elt;
)
(*
@ -123,23 +130,22 @@ module Make(Elt : RANKED) = struct
assert (heap_property cmp s)
*)
let remove_min ({heap} as s) =
match Vec.size heap with
let remove_min self =
match VecI32.size self.heap with
| 0 -> raise Not_found
| 1 ->
let x = Vec.pop heap in
Elt.set_idx x _absent_index;
let x = Elt.of_int_unsafe (VecI32.pop self.heap) in
Elt.set_heap_idx self.store x _absent_index;
x
| _ ->
let x = Vec.get heap 0 in
let new_hd = Vec.pop heap in (* heap.last() *)
Vec.set heap 0 new_hd;
Elt.set_idx x _absent_index;
Elt.set_idx new_hd 0;
let x = get_elt_ self 0 in
let new_hd = Elt.of_int_unsafe (VecI32.pop self.heap) in (* heap.last() *)
set_elt_ self 0 new_hd;
Elt.set_heap_idx self.store x _absent_index;
Elt.set_heap_idx self.store new_hd 0;
(* enforce heap property again *)
if Vec.size heap > 1 then (
percolate_down s new_hd;
if VecI32.size self.heap > 1 then (
percolate_down self new_hd;
);
x
end [@@inline]

3
src/sat/Heap.mli
View file

@ -2,4 +2,5 @@ module type RANKED = Heap_intf.RANKED
module type S = Heap_intf.S
module Make(X : RANKED) : S with type elt = X.t
module Make(X : RANKED) :
S with type elt = X.t and type elt_store = X.store

18
src/sat/Heap_intf.ml
View file

@ -1,17 +1,23 @@
module type RANKED = sig
type t
type store
type t = private int
val idx: t -> int
val heap_idx : store -> t -> int
(** Index in heap. return -1 if never set *)
val set_idx : t -> int -> unit
val set_heap_idx : store -> t -> int -> unit
(** Update index in heap *)
val cmp : t -> t -> bool
val cmp : store -> t -> t -> bool
val of_int_unsafe : int -> t
(** turn an integer back into an element *)
end
module type S = sig
type elt_store
type elt
(** Type of elements *)
@ -19,13 +25,13 @@ module type S = sig
(** Heap of {!elt}, whose priority is increased or decreased
incrementally (see {!decrease} for instance) *)
val create : unit -> t
val create : elt_store -> t
(** Create a heap *)
val decrease : t -> elt -> unit
(** [decrease h x] decreases the value associated to [x] within [h] *)
val in_heap : elt -> bool
val in_heap : t -> elt -> bool
(*val increase : (int -> int -> bool) -> t -> int -> unit*)

15
src/sat/Sidekick_sat.ml
View file

@ -4,7 +4,7 @@
module Solver_intf = Solver_intf
module type S = Solver_intf.S
module type FORMULA = Solver_intf.FORMULA
module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PROOF = Solver_intf.PROOF
@ -13,18 +13,13 @@ type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state
type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
module type ACTS = Solver_intf.ACTS
type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts
type ('lit, 'proof) acts = ('lit, 'proof) Solver_intf.acts
type negated = Solver_intf.negated = Negated | Same_sign
(** Print {!negated} values *)
let pp_negated out = function
| Negated -> Format.fprintf out "negated"
| Same_sign -> Format.fprintf out "same-sign"
type negated = bool
(** Print {!lbool} values *)
let pp_lbool out = function

2276
src/sat/Solver.ml
View file

File diff suppressed because it is too large Load diff

12
src/sat/Solver.mli
View file

@ -3,11 +3,15 @@ module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
: S with module Formula = Th.Formula
and type lemma = Th.proof
: S with type lit = Th.lit
and module Lit = Th.Lit
and type proof = Th.proof
and module Proof = Th.Proof
and type theory = unit
module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
: S with module Formula = Th.Formula
and type lemma = Th.proof
: S with type lit = Th.lit
and module Lit = Th.Lit
and type proof = Th.proof
and module Proof = Th.Proof
and type theory = Th.t

345
src/sat/Solver_intf.ml
View file

@ -14,60 +14,54 @@ Copyright 2016 Simon Cruanes
type 'a printer = Format.formatter -> 'a -> unit
module type SAT_STATE = sig
type formula
type lit
(** Literals (signed boolean atoms) *)
val eval : formula -> bool
(** Returns the valuation of a formula in the current state
val eval : lit -> bool
(** Returns the valuation of a lit in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
val eval_level : formula -> bool * int
val eval_level : lit -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
the literal to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
val iter_trail : (formula -> unit) -> unit
(** Iter through the formulas in order of decision/propagation
val iter_trail : (lit -> unit) -> unit
(** Iter through the lits in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
end
type 'form sat_state = (module SAT_STATE with type formula = 'form)
type 'form sat_state = (module SAT_STATE with type lit = 'form)
(** The type of values returned when the solver reaches a SAT state. *)
module type UNSAT_STATE = sig
type atom
type lit
type clause
type proof
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val get_proof : unit -> proof
(** returns a persistent proof of the empty clause from the Unsat result. *)
val unsat_assumptions: unit -> atom list
val unsat_assumptions : unit -> lit Iter.t
(** Subset of assumptions responsible for "unsat" *)
end
type ('atom, 'clause, 'proof) unsat_state =
(module UNSAT_STATE with type atom = 'atom
and type clause = 'clause
and type proof = 'proof)
type ('lit, 'clause) unsat_state =
(module UNSAT_STATE with type lit = 'lit
and type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *)
type negated =
| Negated (** changed sign *)
| Same_sign (** kept sign *)
(** This type is used during the normalisation of formulas.
See {!val:Expr_intf.S.norm} for more details. *)
type same_sign = bool
(** This type is used during the normalisation of lits.
[true] means the literal stayed the same, [false] that its sign was flipped. *)
(** The type of reasons for propagations of a formula [f]. *)
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
(** The type of reasons for propagations of a lit [f]. *)
type ('lit, 'proof) reason =
| Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
(** [Consequence (l, p)] means that the lits in [l] imply the propagated
lit [f]. The proof should be a proof of the clause "[l] implies [f]".
invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
the current trail.
@ -89,60 +83,60 @@ type lbool = L_true | L_false | L_undefined
(** Valuation of an atom *)
module type ACTS = sig
type formula
type lit
type proof
type dproof = proof -> unit
val iter_assumptions: (formula -> unit) -> unit
val iter_assumptions: (lit -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
val eval_lit: formula -> lbool
val eval_lit: lit -> lbool
(** Obtain current value of the given literal *)
val mk_lit: ?default_pol:bool -> formula -> unit
(** Map the given formula to a literal, which will be decided by the
val add_lit: ?default_pol:bool -> lit -> unit
(** Map the given lit to an internal atom, which will be decided by the
SAT solver. *)
val add_clause: ?keep:bool -> formula list -> proof -> unit
val add_clause: ?keep:bool -> lit list -> dproof -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
*)
val raise_conflict: formula list -> proof -> 'b
val raise_conflict: lit list -> dproof -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
val propagate: formula -> (formula, proof) reason -> unit
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
val propagate: lit -> (lit, dproof) reason -> unit
(** Propagate a lit, i.e. the theory can evaluate the lit to be true
(see the definition of {!type:eval_res} *)
val add_decision_lit: formula -> bool -> unit
(** Ask the SAT solver to decide on the given formula with given sign
val add_decision_lit: lit -> bool -> unit
(** Ask the SAT solver to decide on the given lit with given sign
before it can answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. This will be undone on backtracking. *)
end
(* TODO: find a way to use atoms instead of formulas here *)
type ('formula, 'proof) acts =
(module ACTS with type formula = 'formula
type ('lit, 'proof) acts =
(module ACTS with type lit = 'lit
and type proof = 'proof)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
module type FORMULA = sig
(** formulas *)
module type LIT = sig
(** lits *)
type t
(** The type of atomic formulas over terms. *)
(** The type of atomic lits over terms. *)
val equal : t -> t -> bool
(** Equality over formulas. *)
(** Equality over lits. *)
val hash : t -> int
(** Hashing function for formulas. Should be such that two formulas equal according
(** Hashing function for lits. Should be such that two lits equal according
to {!val:Expr_intf.S.equal} have the same hash. *)
val pp : t printer
@ -151,21 +145,29 @@ module type FORMULA = sig
val neg : t -> t
(** Formula negation *)
val norm : t -> t * negated
(** Returns a 'normalized' form of the formula, possibly negated
(in which case return [Negated]).
[norm] must be so that [a] and [neg a] normalise to the same formula,
but one returns [Negated] and the other [Same_sign]. *)
val norm_sign : t -> t * same_sign
(** Returns a 'normalized' form of the lit, possibly same_sign
(in which case return [false]).
[norm] must be so that [a] and [neg a] normalise to the same lit,
but one returns [false] and the other [true]. *)
end
module type PROOF = Sidekick_core.SAT_PROOF
(** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig
type t
(** The plugin state itself *)
module Formula : FORMULA
type lit
module Lit : LIT with type t = lit
type proof
(** Proof storage/recording *)
module Proof : PROOF
with type t = proof
and type lit = lit
val push_level : t -> unit
(** Create a new backtrack level *)
@ -173,12 +175,12 @@ module type PLUGIN_CDCL_T = sig
val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *)
val partial_check : t -> (Formula.t, proof) acts -> unit
(** Assume the formulas in the slice, possibly using the [slice]
to push new formulas to be propagated or to raising a conflict or to add
val partial_check : t -> (lit, proof) acts -> unit
(** Assume the lits in the slice, possibly using the [slice]
to push new lits to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> (Formula.t, proof) acts -> unit
val final_check : t -> (lit, proof) acts -> unit
(** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed;
@ -187,117 +189,11 @@ end
(** Signature for pure SAT solvers *)
module type PLUGIN_SAT = sig
module Formula : FORMULA
type lit
module Lit : LIT with type t = lit
type proof
end
module type PROOF = sig
(** Signature for a module handling proof by resolution from sat solving traces *)
(** {3 Type declarations} *)
exception Resolution_error of string
(** Raised when resolution failed. *)
type formula
type atom
type lemma
type clause
(** Abstract types for atoms, clauses and theory-specific lemmas *)
type t
(** Lazy type for proof trees. Proofs are persistent objects, and can be
extended to proof nodes using functions defined later. *)
and proof_node = {
conclusion : clause; (** The conclusion of the proof *)
step : step; (** The reasoning step used to prove the conclusion *)
}
(** A proof can be expanded into a proof node, which show the first step of the proof. *)
(** The type of reasoning steps allowed in a proof. *)
and step =
| Hypothesis of lemma
(** The conclusion is a user-provided hypothesis *)
| Assumption
(** The conclusion has been locally assumed by the user *)
| Lemma of lemma
(** The conclusion is a tautology provided by the theory, with associated proof *)
| Duplicate of t * atom list
(** The conclusion is obtained by eliminating multiple occurences of the atom in
the conclusion of the provided proof. *)
| Hyper_res of hyper_res_step
and hyper_res_step = {
hr_init: t;
hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
}
(** {3 Proof building functions} *)
val prove : clause -> t
(** Given a clause, return a proof of that clause.
@raise Resolution_error if it does not succeed. *)
val prove_unsat : clause -> t
(** Given a conflict clause [c], returns a proof of the empty clause.
@raise Resolution_error if it does not succeed. *)
val prove_atom : atom -> t option
(** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
val res_of_hyper_res : hyper_res_step -> t * t * atom
(** Turn an hyper resolution step into a resolution step.
The conclusion can be deduced by performing a resolution between the conclusions
of the two given proofs.
The atom on which to perform the resolution is also given. *)
(** {3 Proof Nodes} *)
val parents : step -> t list
(** Returns the parents of a proof node. *)
val is_leaf : step -> bool
(** Returns wether the the proof node is a leaf, i.e. an hypothesis,
an assumption, or a lemma.
[true] if and only if {!parents} returns the empty list. *)
val expl : step -> string
(** Returns a short string description for the proof step; for instance
["hypothesis"] for a [Hypothesis]
(it currently returns the variant name in lowercase). *)
(** {3 Proof Manipulation} *)
val expand : t -> proof_node
(** Return the proof step at the root of a given proof. *)
val conclusion : t -> clause
(** What is proved at the root of the clause *)
val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a
(** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
[f] is executed exactly once on each proof node in the tree, and that the execution of
[f] on a proof node happens after the execution on the parents of the nodes. *)
val unsat_core : t -> clause list
(** Returns the unsat_core of the given proof, i.e the lists of conclusions
of all leafs of the proof.
More efficient than using the [fold] function since it has
access to the internal representation of proofs *)
(** {3 Misc} *)
val check_empty_conclusion : t -> unit
(** Check that the proof's conclusion is the empty clause,
@raise Resolution_error otherwise *)
val check : t -> unit
(** Check the contents of a proof. Mainly for internal use. *)
module Tbl : Hashtbl.S with type key = t
module Proof : PROOF with type t = proof and type lit = lit
end
(** The external interface implemented by safe solvers, such as the one
@ -307,85 +203,91 @@ module type S = sig
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
module Formula : FORMULA
type lit (** literals *)
type formula = Formula.t (** user formulas *)
type atom
(** The type of atoms given by the module argument for formulas.
An atom is a user-defined atomic formula whose truth value is
picked by Msat. *)
module Lit : LIT with type t = lit
type clause
type theory
type lemma
(** A theory lemma or an input axiom *)
type proof
(** A representation of a full proof *)
type dproof = proof -> unit
type solver
(** The main solver type. *)
(* TODO: keep this internal *)
module Atom : sig
type t = atom
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val neg : t -> t
val sign : t -> bool
val abs : t -> t
val formula : t -> formula
val pp : t printer
end
type store
(** Stores atoms, clauses, etc. *)
module Clause : sig
type t = clause
val atoms : t -> atom array
val atoms_l : t -> atom list
val equal : t -> t -> bool
val short_name : t -> string
val pp : t printer
module Tbl : Hashtbl.S with type key = t
val pp : store -> t printer
(** Print the clause *)
val short_name : store -> t -> string
(** Short name for a clause. Unspecified *)
val n_atoms : store -> t -> int
val lits_iter : store -> t -> lit Iter.t
(** Literals of a clause *)
val lits_a : store -> t -> lit array
(** Atoms of a clause *)
val lits_l : store -> t -> lit list
(** List of atoms of a clause *)
end
module Proof : PROOF
with type clause = clause
and type atom = atom
and type formula = formula
and type lemma = lemma
with type lit = lit
and type t = proof
(** A module to manipulate proofs. *)
type t = solver
(** Main solver type, containing all state for solving. *)
val create :
?on_conflict:(atom array -> unit) ->
?on_decision:(atom -> unit) ->
?on_new_atom:(atom -> unit) ->
?store_proof:bool ->
?on_conflict:(t -> Clause.t -> unit) ->
?on_decision:(t -> lit -> unit) ->
?on_learnt:(t -> Clause.t -> unit) ->
?on_gc:(t -> lit array -> unit) ->
?stat:Stat.t ->
?size:[`Tiny|`Small|`Big] ->
proof:Proof.t ->
theory ->
t
(** Create new solver
@param theory the theory
@param store_proof if true, stores proof (default [true]). Otherwise
the functions that return proofs will fail with [No_proof]
@param the proof
@param size the initial size of internal data structures. The bigger,
the faster, but also the more RAM it uses. *)
val theory : t -> theory
(** Access the theory state *)
val store : t -> store
(** Store for the solver *)
val stat : t -> Stat.t
(** Statistics *)
val proof : t -> proof
(** Access the inner proof *)
(** {2 Types} *)
(** Result type for the solver *)
type res =
| Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
| Sat of lit sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (lit,clause) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
@ -393,34 +295,45 @@ module type S = sig
(** {2 Base operations} *)
val assume : t -> formula list list -> lemma -> unit
val assume : t -> lit list list -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *)
val add_clause : t -> atom list -> lemma -> unit
val add_clause : t -> lit list -> dproof -> unit
(** Lower level addition of clauses *)
val add_clause_a : t -> atom array -> lemma -> unit
val add_input_clause : t -> lit list -> unit
(** Like {!add_clause} but with the justification of being an input clause *)
val add_clause_a : t -> lit array -> dproof -> unit
(** Lower level addition of clauses *)
val add_input_clause_a : t -> lit array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *)
(* TODO: API to push/pop/clear assumptions from an inner vector *)
val solve :
?assumptions:atom list ->
?assumptions:lit list ->
t -> res
(** Try and solves the current set of clauses.
@param assumptions additional atomic assumptions to be temporarily added.
The assumptions are just used for this call to [solve], they are
not saved in the solver's state. *)
val make_atom : t -> formula -> atom
(** Add a new atom (i.e propositional formula) to the solver.
This formula will be decided on at some point during solving,
wether it appears in clauses or not. *)
val add_lit : t -> ?default_pol:bool -> lit -> unit
(** Ensure the SAT solver handles this particular literal, ie add
a boolean variable for it if it's not already there. *)
val true_at_level0 : t -> atom -> bool
val set_default_pol : t -> lit -> bool -> unit
(** Set default polarity for the given boolean variable.
Sign of the literal is ignored. *)
val true_at_level0 : t -> lit -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *)
val eval_atom : t -> atom -> lbool
val eval_lit : t -> lit -> lbool
(** Evaluate atom in current state *)
end

4
src/sat/dune
View file

@ -2,9 +2,9 @@
(library
(name sidekick_sat)
(public_name sidekick.sat)
(libraries iter sidekick.util)
(libraries iter sidekick.util sidekick.core)
(synopsis "Pure OCaml SAT solver implementation for sidekick")
(flags :standard -open Sidekick_util)
(flags :standard -warn-error -a+8 -open Sidekick_util)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

0
src/msat-solver/DESIGN.md → src/smt-solver/DESIGN.md
View file

642
src/msat-solver/Sidekick_msat_solver.ml → src/smt-solver/Sidekick_smt_solver.ml
View file

@ -11,7 +11,12 @@
module type ARG = sig
open Sidekick_core
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
type proof
module P : PROOF
with type term = T.Term.t
and type t = proof
and type lit = Lit.t
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
@ -26,71 +31,42 @@ module type S = Sidekick_core.SOLVER
module Make(A : ARG)
: S
with module T = A.T
and type proof = A.proof
and module Lit = A.Lit
and module P = A.P
= struct
module T = A.T
module P = A.P
module Ty = T.Ty
module Term = T.Term
module Lit = A.Lit
type term = Term.t
type ty = Ty.t
type proof = P.t
type proof = A.proof
type dproof = proof -> unit
type lit = Lit.t
module Lit_ = struct
module T = T
type t = {
lit_term: term;
lit_sign : bool
}
let[@inline] neg l = {l with lit_sign=not l.lit_sign}
let[@inline] sign t = t.lit_sign
let[@inline] abs t = {t with lit_sign=true}
let[@inline] term (t:t): term = t.lit_term
let[@inline] signed_term t = term t, sign t
let make ~sign t = {lit_sign=sign; lit_term=t}
let atom tst ?(sign=true) (t:term) : t =
let t, sign' = Term.abs tst t in
let sign = if not sign' then not sign else sign in
make ~sign t
let equal a b =
a.lit_sign = b.lit_sign &&
Term.equal a.lit_term b.lit_term
let hash a =
let sign = a.lit_sign in
CCHash.combine3 2 (CCHash.bool sign) (Term.hash a.lit_term)
let pp out l =
if l.lit_sign then Term.pp out l.lit_term
else Format.fprintf out "(@[@<1>¬@ %a@])" Term.pp l.lit_term
let norm_sign l = if l.lit_sign then l, true else neg l, false
end
type lit = Lit_.t
(* actions from msat *)
type msat_acts = (lit, P.t) Sidekick_sat.acts
(* actions from the sat solver *)
type sat_acts = (lit, proof) Sidekick_sat.acts
(* the full argument to the congruence closure *)
module CC_actions = struct
module T = T
module P = P
module Lit = Lit_
module Lit = Lit
type nonrec proof = proof
let cc_view = A.cc_view
module Actions = struct
module T = T
module P = P
module Lit = Lit
type t = msat_acts
let[@inline] raise_conflict (a:t) lits pr =
type nonrec proof = proof
type dproof = proof -> unit
type t = sat_acts
let[@inline] raise_conflict (a:t) lits (dp:dproof) =
let (module A) = a in
A.raise_conflict lits pr
A.raise_conflict lits dp
let[@inline] propagate (a:t) lit ~reason =
let (module A) = a in
let reason = Sidekick_sat.Consequence reason in
@ -106,9 +82,12 @@ module Make(A : ARG)
module Solver_internal = struct
module T = T
module P = P
module Lit = Lit_
module Lit = Lit
module CC = CC
module N = CC.N
type formula = Lit.t
type nonrec proof = proof
type dproof = proof -> unit
type term = Term.t
type ty = Ty.t
type lit = Lit.t
@ -124,27 +103,28 @@ module Make(A : ARG)
next: th_states;
} -> th_states
type actions = msat_acts
type theory_actions = sat_acts
module Simplify = struct
type t = {
tst: term_store;
ty_st: ty_store;
proof: proof;
mutable hooks: hook list;
cache: Term.t Term.Tbl.t;
}
and hook = t -> term -> (term * P.t) option
and hook = t -> term -> term option
let create tst ty_st ~proof : t =
{tst; ty_st; proof; hooks=[]; cache=Term.Tbl.create 32;}
let create tst ty_st : t =
{tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;}
let[@inline] tst self = self.tst
let[@inline] ty_st self = self.ty_st
let[@inline] with_proof self f = P.with_proof self.proof f
let add_hook self f = self.hooks <- f :: self.hooks
let clear self = Term.Tbl.clear self.cache
let normalize (self:t) (t:Term.t) : (Term.t * P.t) option =
let sub_proofs_ = ref [] in
let normalize (self:t) (t:Term.t) : Term.t option =
(* compute and cache normal form of [t] *)
let rec aux t : Term.t =
match Term.Tbl.find self.cache t with
@ -161,30 +141,36 @@ module Make(A : ARG)
| h :: hooks_tl ->
match h self t with
| None -> aux_rec t hooks_tl
| Some (u, _) when Term.equal t u -> aux_rec t hooks_tl
| Some (u, pr_t_u) ->
sub_proofs_ := pr_t_u :: !sub_proofs_;
aux u
| Some u when Term.equal t u -> aux_rec t hooks_tl
| Some u -> aux u (* fixpoint *)
in
let u = aux t in
if Term.equal t u then None
else (
(* proof: [sub_proofs |- t=u] by CC *)
let pr = P.cc_imply_l !sub_proofs_ t u in
Some (u, pr)
(* proof: [sub_proofs |- t=u] by CC + subproof *)
P.with_proof self.proof (P.lemma_preprocess t u);
Some u
)
let normalize_t self t =
match normalize self t with
| None -> t, P.refl t
| Some (u,pr) -> u, pr
| Some u -> u
| None -> t
end
type simplify_hook = Simplify.hook
module type PREPROCESS_ACTS = sig
val mk_lit : ?sign:bool -> term -> lit
val add_clause : lit list -> dproof -> unit
val add_lit : ?default_pol:bool -> lit -> unit
end
type preprocess_actions = (module PREPROCESS_ACTS)
type t = {
tst: Term.store; (** state for managing terms *)
ty_st: Ty.store;
cc: CC.t lazy_t; (** congruence closure *)
proof: proof; (** proof logger *)
stat: Stat.t;
count_axiom: int Stat.counter;
count_preprocess_clause: int Stat.counter;
@ -194,19 +180,18 @@ module Make(A : ARG)
simp: Simplify.t;
mutable preprocess: preprocess_hook list;
mutable mk_model: model_hook list;
preprocess_cache: (Term.t * P.t list) Term.Tbl.t;
preprocess_cache: Term.t Term.Tbl.t;
mutable t_defs : (term*term) list; (* term definitions *)
mutable th_states : th_states; (** Set of theories *)
mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable level: int;
}
and preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> P.t -> unit) ->
term -> (term * P.t) option
preprocess_actions ->
term -> term option
and model_hook =
recurse:(t -> CC.N.t -> term) ->
@ -214,20 +199,14 @@ module Make(A : ARG)
type solver = t
module Formula = struct
include Lit
let norm lit =
let lit', sign = norm_sign lit in
lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated
end
module Eq_class = CC.N
module Expl = CC.Expl
type proof = P.t
module Proof = P
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] ty_st t = t.ty_st
let[@inline] with_proof self f = Proof.with_proof self.proof f
let stats t = t.stat
let define_const (self:t) ~const ~rhs : unit =
@ -235,24 +214,24 @@ module Make(A : ARG)
let simplifier self = self.simp
let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
let simp_t self (t:Term.t) : Term.t * P.t = Simplify.normalize_t self.simp t
let simp_t self (t:Term.t) : Term.t = Simplify.normalize_t self.simp t
let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
let on_preprocess self f = self.preprocess <- f :: self.preprocess
let on_model_gen self f = self.mk_model <- f :: self.mk_model
let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
let push_decision (_self:t) (acts:theory_actions) (lit:lit) : unit =
let (module A) = acts in
let sign = Lit.sign lit in
A.add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self (acts:actions) c proof : 'a =
let[@inline] raise_conflict self (acts:theory_actions) c proof : 'a =
let (module A) = acts in
Stat.incr self.count_conflict;
A.raise_conflict c proof
let[@inline] propagate self (acts:actions) p ~reason : unit =
let[@inline] propagate self (acts:theory_actions) p ~reason : unit =
let (module A) = acts in
Stat.incr self.count_propagate;
A.propagate p (Sidekick_sat.Consequence reason)
@ -260,133 +239,178 @@ module Make(A : ARG)
let[@inline] propagate_l self acts p cs proof : unit =
propagate self acts p ~reason:(fun()->cs,proof)
let add_sat_clause_ self (acts:actions) ~keep lits (proof:P.t) : unit =
let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit =
let (module A) = acts in
Stat.incr self.count_axiom;
A.add_clause ~keep lits proof
let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
let add_sat_lit self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
let (module A) = acts in
A.add_lit ?default_pol lit
(* actual preprocessing logic, acting on terms.
this calls all the preprocessing hooks on subterms, ensuring
a fixpoint. *)
let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term =
let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
(* compute and cache normal form [u] of [t].
Also cache a list of proofs [ps] such
that [ps |- t=u] by CC. *)
let rec aux t : term * proof list =
match Term.Tbl.find self.preprocess_cache t with
| u, ps ->
u, ps
| exception Not_found ->
let sub_p: P.t list ref = ref [] in
Also cache a list of proofs [ps] such that [ps |- t=u] by CC.
It is important that we cache the proofs here, because
next time we preprocess [t], we will have to re-emit the same
proofs, even though we will not do any actual preprocessing work.
*)
let rec preproc_rec t : term =
match Term.Tbl.find self.preprocess_cache t with
| u -> u
| exception Not_found ->
(* try rewrite at root *)
let t1 = aux_rec ~sub_p t self.preprocess in
let t1 = preproc_with_hooks t self.preprocess in
(* map subterms *)
let t2 =
Term.map_shallow self.tst
(fun t_sub ->
let u_sub, ps_t = aux t_sub in
if not (Term.equal t_sub u_sub) then (
sub_p := List.rev_append ps_t !sub_p;
);
u_sub)
t1
in
let t2 = Term.map_shallow self.tst preproc_rec t1 in
let u =
if not (Term.equal t t2) then (
(* fixpoint *)
let v, ps_t2_v = aux t2 in
if not (Term.equal t2 v) then (
sub_p := List.rev_append ps_t2_v !sub_p
);
v
preproc_rec t2 (* fixpoint *)
) else (
t2
)
in
(* signal boolean subterms, so as to decide them
in the SAT solver *)
if Ty.is_bool (Term.ty u) then (
Log.debugf 5
(fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp u);
(* make a literal (already preprocessed) *)
let lit = mk_lit_nopreproc u in
(* ensure that SAT solver has a boolean atom for [u] *)
A0.add_lit lit;
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
CC.set_as_lit cc (CC.add_term cc u) lit;
);
if t != u then (
Log.debugf 5
(fun k->k "(@[msat-solver.preprocess.term@ :from %a@ :to %a@])"
(fun k->k "(@[smt-solver.preprocess.term@ :from %a@ :to %a@])"
Term.pp t Term.pp u);
);
Term.Tbl.add self.preprocess_cache t (u,!sub_p);
u, !sub_p
Term.Tbl.add self.preprocess_cache t u;
u
(* try each function in [hooks] successively *)
and aux_rec ~sub_p t hooks : term =
and preproc_with_hooks t hooks : term =
match hooks with
| [] -> t
| h :: hooks_tl ->
match h self ~mk_lit ~add_clause t with
| None -> aux_rec ~sub_p t hooks_tl
| Some (u, ps_t_u) ->
sub_p := ps_t_u :: !sub_p;
let v, ps_u_v = aux u in
if t != v then (
sub_p := List.rev_append ps_u_v !sub_p;
);
v
in
(* call hook, using [pacts] which will ensure all new
literals and clauses are also preprocessed *)
match h self (Lazy.force pacts) t with
| None -> preproc_with_hooks t hooks_tl
| Some u -> preproc_rec u
let t1, p_t_t1 = simp_t self t in
(* create literal and preprocess it with [pacts], which uses [A0]
for the base operations, and preprocesses new literals and clauses
recursively. *)
and mk_lit ?sign t =
let u = preproc_rec t in
if not (Term.equal t u) then (
Log.debugf 10
(fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
Term.pp t Term.pp u);
);
Lit.atom self.tst ?sign u
let u, ps_t1_u = aux t1 in
and preprocess_lit (lit:lit) : lit =
let t = Lit.term lit in
let sign = Lit.sign lit in
mk_lit ~sign t
let pr_t_u =
if t != u then (
let hyps =
if t == t1 then ps_t1_u
else p_t_t1 :: ps_t1_u in
P.cc_imply_l hyps t u
) else P.refl u
in
(* wrap [A0] so that all operations go throught preprocessing *)
and pacts = lazy (
(module struct
let add_lit ?default_pol lit =
let lit = preprocess_lit lit in
A0.add_lit lit
let add_clause c pr =
Stat.incr self.count_preprocess_clause;
let c = CCList.map preprocess_lit c in
A0.add_clause c pr
let mk_lit = mk_lit
end : PREPROCESS_ACTS)
) in
u, pr_t_u
P.begin_subproof self.proof;
(* return preprocessed lit + proof they are equal *)
let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * proof =
let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
(* simplify the term *)
let t1 = simp_t self t in
if not (Lit.equal lit lit') then (
Log.debugf 10
(fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])"
Lit.pp lit Lit.pp lit' (P.pp_debug ~sharing:false) p);
(* preprocess *)
let u = preproc_rec t1 in
(* emit [|- t=u] *)
if not (Term.equal t u) then (
P.with_proof self.proof (P.lemma_preprocess t u);
);
lit', p
P.end_subproof self.proof;
u
(* return preprocessed lit *)
let preprocess_lit_ (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
let t = Lit.term lit in
let sign = Lit.sign lit in
let u = preprocess_term_ self pacts t in
Lit.atom self.tst ~sign u
(* add a clause using [acts] *)
let add_clause_ self acts lits (proof:P.t) : unit =
Stat.incr self.count_preprocess_clause;
let add_clause_ self acts lits (proof:dproof) : unit =
add_sat_clause_ self acts ~keep:true lits proof
(* FIXME: should we store the proof somewhere? *)
let mk_lit self acts ?sign t : Lit.t =
let add_clause = add_clause_ self acts in
let lit, _p =
preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
in
lit
let[@inline] preprocess_term self ~add_clause (t:term) : term * proof =
preprocess_term_ self ~add_clause t
let[@inline] add_clause_temp self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:false lits proof
let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:true lits proof
let[@inline] add_lit _self (acts:actions) lit : unit =
let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
let (module A) = acts in
A.mk_lit lit
A.add_lit ?default_pol lit
let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
(module struct
let mk_lit ?sign t = Lit.atom self.tst ?sign t
let add_clause = add_clause_ self acts
let add_lit = add_lit self acts
end)
let preprocess_clause_ (self:t) (acts:theory_actions) (c:lit list) : lit list =
let pacts = preprocess_acts_of_acts self acts in
let c = CCList.map (preprocess_lit_ self pacts) c in
c
(* make literal and preprocess it *)
let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
let lit = Lit.atom self.tst ?sign t in
preprocess_lit_ self pacts lit
let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term =
preprocess_term_ self pacts t
let[@inline] add_clause_temp self acts c (proof:dproof) : unit =
let c = preprocess_clause_ self acts c in
add_sat_clause_ self acts ~keep:false c proof
let[@inline] add_clause_permanent self acts c (proof:dproof) : unit =
let c = preprocess_clause_ self acts c in
add_sat_clause_ self acts ~keep:true c proof
let[@inline] mk_lit (self:t) (acts:theory_actions) ?sign t : lit =
let pacts = preprocess_acts_of_acts self acts in
mk_plit self pacts ?sign t
let add_lit_t self acts ?sign t =
let lit = mk_lit self acts ?sign t in
let pacts = preprocess_acts_of_acts self acts in
let lit = mk_plit self pacts ?sign t in
add_lit self acts lit
let on_final_check self f = self.on_final_check <- f :: self.on_final_check
@ -434,9 +458,9 @@ module Make(A : ARG)
exception E_loop_exit
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit =
Log.debugf 2
(fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])"
(fun k->k "(@[<hv1>@{<green>smt-solver.assume_lits@}%s[lvl=%d]@ %a@])"
(if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
(* transmit to CC *)
let cc = cc self in
@ -462,16 +486,16 @@ module Make(A : ARG)
);
()
let[@inline] iter_atoms_ (acts:actions) : _ Iter.t =
let[@inline] iter_atoms_ (acts:theory_actions) : _ Iter.t =
fun f ->
let (module A) = acts in
A.iter_assumptions f
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
let check_ ~final (self:t) (acts: sat_acts) =
let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
let iter = iter_atoms_ acts in
Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
Log.debugf 5 (fun k->k "(smt-solver.assume :len %d)" (Iter.length iter));
self.on_progress();
assert_lits_ ~final self acts iter;
Profile.exit pb
@ -484,7 +508,7 @@ module Make(A : ARG)
let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
check_ ~final:true self acts
let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t =
let create ~stat ~proof (tst:Term.store) (ty_st:Ty.store) () : t =
let rec self = {
tst;
ty_st;
@ -492,9 +516,10 @@ module Make(A : ARG)
(* lazily tie the knot *)
CC.create ~size:`Big self.tst;
);
proof;
th_states=Ths_nil;
stat;
simp=Simplify.create tst ty_st;
simp=Simplify.create tst ty_st ~proof;
on_progress=(fun () -> ());
preprocess=[];
mk_model=[];
@ -511,145 +536,16 @@ module Make(A : ARG)
ignore (Lazy.force @@ self.cc : CC.t);
self
end
module Lit = Solver_internal.Lit
(** the parametrized SAT Solver *)
module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
module Atom = Sat_solver.Atom
module Pre_proof = struct
module SP = Sat_solver.Proof
module SC = Sat_solver.Clause
type t = {
msat: Sat_solver.Proof.t;
tdefs: (term*term) list; (* term definitions *)
p: P.t lazy_t;
}
let to_proof (self:t) : P.t = Lazy.force self.p
let pp_dot =
let module Dot =
Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
let pp out self = Dot.pp out self.msat in
Some pp
(* export to proof {!P.t}, translating Msat-level proof ising:
- [stepc name cl proof] to bind [name] to given clause and proof
- [deft name t] to define [name] as a shortcut for [t] (tseitin, etc.).
Checker will always expand these. (TODO)
- [steps <defc>+] for a structure proof with definitions, returning last one
- [subproof (assms <lit>* ) (proof)] which uses [proof] to get
clause [c] under given assumptions (each assm is a lit),
and return [-a1 \/ … \/ -an \/ c], discharging assumptions
*)
let conv_proof (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
let assms = ref [] in
let steps = ref [] in
let n_step = ref 0 in
let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *)
(* name of an already processed proof node *)
let find_proof_name (p:Sat_solver.Proof.t) : string =
try SC.Tbl.find n_tbl_ (SP.conclusion p)
with Not_found ->
Error.errorf
"msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a"
SC.pp (SP.conclusion p)
in
let add_step s = steps := s :: !steps in
(* convert [n_init] into a proof step and adds it to [steps] *)
let tr_node_to_step () (n_init:SP.proof_node) : unit =
let {SP.conclusion=c; step} = n_init in
if SC.Tbl.mem n_tbl_ c then ()
else (
let name = Printf.sprintf "c%d" !n_step in
incr n_step;
SC.Tbl.add n_tbl_ c name;
(* build conclusion of proof step *)
let tr_atom a : P.lit =
let sign = Sat_solver.Atom.sign a in
let t = Lit.term (Sat_solver.Atom.formula a) in
P.lit_mk sign t
in
let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in
(* proof for the node *)
let pr_step : P.t =
match step with
| SP.Hypothesis pr -> pr (* FIXME: should this have a special rule? *)
| SP.Assumption ->
(* push into assumptions and introduce a name for it *)
let name = Printf.sprintf "a%d" !n_step in
let lit = match concl with
| [l] -> l
| _ -> Error.errorf "assumption with non-unit clause %a" SC.pp c
in
incr n_step;
assms := (name, lit) :: !assms;
P.ref_by_name name
| Lemma pr -> pr
| Duplicate (c, _) ->
let n = find_proof_name c in
let p = P.ref_by_name n in
(* NOTE: we do not represent this form of transformation for now.
Quip should be able to process clauses as sets. *)
p
| Hyper_res { hr_init=init; hr_steps=steps } ->
let proof_init = P.ref_by_name @@ find_proof_name init in
let tr_step (pivot,p') : P.hres_step =
(* unit resolution? *)
let is_r1_step = Array.length (SC.atoms (SP.conclusion p')) = 1 in
let proof_p' = P.ref_by_name @@ find_proof_name p' in
if is_r1_step then (
P.r1 proof_p'
) else (
let pivot = Lit.term (Sat_solver.Atom.formula pivot) in
P.r proof_p' ~pivot
)
in
P.hres_iter proof_init
(Iter.of_list steps |> Iter.map tr_step)
in
let step = P.stepc ~name concl pr_step in
add_step step;
)
in
(* this should traverse from the leaves, so that order of [steps] is correct *)
Sat_solver.Proof.fold tr_node_to_step () msat;
let assms = !assms in
(* gather all term definitions *)
let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
let make (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
{ msat; tdefs; p=lazy (conv_proof msat tdefs) }
let check self = SP.check self.msat
let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self)
let output oc (self:t) = P.Quip.output oc (to_proof self)
end
(* main solver state *)
type t = {
si: Solver_internal.t;
solver: Sat_solver.t;
stat: Stat.t;
proof: P.t;
count_clause: int Stat.counter;
count_solve: int Stat.counter;
(* config: Config.t *)
@ -672,7 +568,7 @@ module Make(A : ARG)
let add_theory_p (type a) (self:t) (th:a theory_p) : a =
let (module Th) = th in
Log.debugf 2
(fun k-> k "(@[msat-solver.add-theory@ :name %S@])" Th.name);
(fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name);
let st = Th.create_and_setup self.si in
(* add push/pop to the internal solver *)
begin
@ -693,12 +589,12 @@ module Make(A : ARG)
let add_theory_l self = List.iter (add_theory self)
(* create a new solver *)
let create ?(stat=Stat.global) ?size ?store_proof ~theories tst ty_st () : t =
Log.debug 5 "msat-solver.create";
let si = Solver_internal.create ~stat tst ty_st () in
let create ?(stat=Stat.global) ?size ~proof ~theories tst ty_st () : t =
Log.debug 5 "smt-solver.create";
let si = Solver_internal.create ~stat ~proof tst ty_st () in
let self = {
si;
solver=Sat_solver.create ?store_proof ?size si;
si; proof;
solver=Sat_solver.create ~proof ?size ~stat si;
stat;
count_clause=Stat.mk_int stat "solver.add-clause";
count_solve=Stat.mk_int stat "solver.solve";
@ -707,9 +603,10 @@ module Make(A : ARG)
(* assert [true] and [not false] *)
begin
let tst = Solver_internal.tst self.si in
Sat_solver.assume self.solver [
[Lit.atom tst @@ Term.bool tst true];
] P.true_is_true
let t_true = Term.bool tst true in
Sat_solver.add_clause self.solver
[Lit.atom tst t_true]
(P.lemma_true t_true)
end;
self
@ -719,67 +616,25 @@ module Make(A : ARG)
let[@inline] tst self = Solver_internal.tst self.si
let[@inline] ty_st self = Solver_internal.ty_st self.si
let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit
let preprocess_acts_of_solver_
(self:t) : (module Solver_internal.PREPROCESS_ACTS) =
(module struct
let mk_lit ?sign t = Lit.atom ?sign self.si.tst t
let add_lit ?default_pol lit =
Sat_solver.add_lit self.solver ?default_pol lit
let add_clause c pr =
Sat_solver.add_clause self.solver c pr
end)
let mk_atom_t_ self t : Atom.t =
let lit = Lit.atom (tst self) t in
mk_atom_lit_ self lit
(* preprocess literal *)
let preprocess_lit_ (self:t) (lit:lit) : lit =
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.preprocess_lit_ self.si pacts lit
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:Term.t) : unit =
Term.iter_dag t
|> Iter.filter (fun t -> Ty.is_bool @@ Term.ty t)
|> Iter.filter
(fun t -> match A.cc_view t with
| Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.filter (fun t -> A.is_valid_literal t)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp sub);
(* ensure that msat has a boolean atom for [sub] *)
let atom = mk_atom_t_ self sub in
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula atom);
())
let rec mk_atom_lit self lit : Atom.t * P.t =
let lit, proof = preprocess_lit_ self lit in
add_bool_subterms_ self (Lit.term lit);
Sat_solver.make_atom self.solver lit, proof
and preprocess_lit_ self lit : Lit.t * P.t =
Solver_internal.preprocess_lit_
~add_clause:(fun lits proof ->
(* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause;
let pr_l = ref [] in
let atoms =
List.map
(fun lit ->
let a, pr = mk_atom_lit self lit in
if not (P.is_trivial_refl pr) then (
pr_l := pr :: !pr_l;
);
a)
lits
in
(* do paramodulation if needed *)
let proof =
if !pr_l=[] then proof
else P.(hres_l proof (List.rev_map p1 !pr_l))
in
let proof = P.nn proof in (* normalize lits *)
Sat_solver.add_clause self.solver atoms proof)
self.si lit
let[@inline] mk_atom_t self ?sign t : Atom.t * P.t =
let lit = Lit.atom (tst self) ?sign t in
mk_atom_lit self lit
let mk_atom_t' self ?sign t = mk_atom_t self ?sign t |> fst
let mk_atom_lit' self lit = mk_atom_lit self lit |> fst
(* make a literal from a term, ensuring it is properly preprocessed *)
let mk_lit_t (self:t) ?sign (t:term) : lit =
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.mk_plit self.si pacts ?sign t
(** {2 Result} *)
@ -820,8 +675,7 @@ module Make(A : ARG)
type res =
| Sat of Model.t
| Unsat of {
proof: Pre_proof.t option lazy_t;
unsat_core: Atom.t list lazy_t;
unsat_core: unit -> lit Iter.t;
}
| Unknown of Unknown.t
(** Result of solving for the current set of clauses *)
@ -831,26 +685,30 @@ module Make(A : ARG)
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit =
let add_clause (self:t) (c:lit IArray.t) (proof:dproof) : unit =
Stat.incr self.count_clause;
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])"
(Util.pp_iarray Atom.pp) c (P.pp_debug ~sharing:false) proof);
Log.debugf 50 (fun k->
k "(@[solver.add-clause@ %a@])"
(Util.pp_iarray Lit.pp) c);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
Sat_solver.add_clause_a self.solver (c:> lit array) proof;
Profile.exit pb
let add_clause_l self c p = add_clause self (IArray.of_list c) p
let assert_terms self c =
let p = P.assertion_c_l (List.map P.lit_a c) in
let c = CCList.map (mk_atom_t' self) c in
add_clause_l self c p
let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
let c = CCList.map (preprocess_lit_ self) c in
(* TODO: if c != c0 then P.emit_redundant_clause c
because we jsut preprocessed it away? *)
let dp = P.emit_input_clause (Iter.of_list c) in
add_clause_l self c dp
let assert_term self t = assert_terms self [t]
let mk_model (self:t) (lits:lit Iter.t) : Model.t =
Log.debug 1 "(smt.solver.mk-model)";
Profile.with_ "msat-solver.mk-model" @@ fun () ->
Profile.with_ "smt-solver.mk-model" @@ fun () ->
let module M = Term.Tbl in
let model = M.create 128 in
let {Solver_internal.tst; cc=lazy cc; mk_model=model_hooks; _} = self.si in
@ -858,7 +716,8 @@ module Make(A : ARG)
(* first, add all literals to the model using the given propositional model
[lits]. *)
lits
(fun {Lit.lit_term=t;lit_sign=sign} ->
(fun lit ->
let t, sign = Lit.signed_term lit in
M.replace model t (Term.bool tst sign));
(* compute a value for [n]. *)
@ -899,41 +758,26 @@ module Make(A : ARG)
let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
~assumptions (self:t) : res =
Profile.with_ "msat-solver.solve" @@ fun () ->
Profile.with_ "smt-solver.solve" @@ fun () ->
let do_on_exit () =
List.iter (fun f->f()) on_exit;
in
self.si.on_progress <- (fun () -> on_progress self);
(* TODO: msat 0.10
let on_conflict =
if Profile.enabled()
then Some (fun _ -> Profile.instant "sat.conflict")
else None
in
let r = Sat_solver.solve ?on_conflict ~assumptions (solver self) in
*)
let r = Sat_solver.solve ~assumptions (solver self) in
Stat.incr self.count_solve;
match r with
| Sat_solver.Sat (module SAT) ->
Log.debug 1 "sidekick.msat-solver: SAT";
Log.debug 1 "sidekick.smt-solver: SAT";
let _lits f = SAT.iter_trail f in
(* TODO: theory combination *)
let m = mk_model self _lits in
do_on_exit ();
Sat m
| Sat_solver.Unsat (module UNSAT) ->
let proof = lazy (
try
let pr = UNSAT.get_proof () in
if check then Sat_solver.Proof.check pr;
Some (Pre_proof.make pr (List.rev self.si.t_defs))
with Sidekick_sat.Solver_intf.No_proof -> None
) in
let unsat_core = lazy (UNSAT.unsat_assumptions ()) in
let unsat_core () = UNSAT.unsat_assumptions () in
do_on_exit ();
Unsat {proof; unsat_core}
Unsat {unsat_core}
let mk_theory (type st)
~name ~create_and_setup

6
src/smt-solver/dune Normal file
View file

@ -0,0 +1,6 @@
(library
(name Sidekick_smt_solver)
(public_name sidekick.smt-solver)
(libraries containers iter sidekick.core sidekick.util
sidekick.cc sidekick.sat)
(flags :standard -warn-error -a+8 -open Sidekick_util))

0
src/msat-solver/th_key.ml.bak → src/smt-solver/th_key.ml.bak
View file

69
src/smtlib/Process.ml
View file

@ -135,12 +135,10 @@ let mk_progress (_s:Solver.t) : _ -> unit =
let solve
?gc:_
?restarts:_
?dot_proof
?(pp_model=false)
?proof_file
?(check=false)
?time:_ ?memory:_ ?(progress=false)
?hyps:_
~assumptions
s : unit =
let t1 = Sys.time() in
@ -168,32 +166,19 @@ let solve
*)
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat {proof;_} ->
let proof_opt =
if check||CCOpt.is_some proof_file then Lazy.force proof
else None
in
| Solver.Unsat _ ->
if check then (
()
(* FIXME: check trace?
match proof_opt with
| Some p ->
Profile.with_ "unsat.check" (fun () -> Solver.Pre_proof.check p);
| _ -> ()
*)
);
begin match dot_proof, proof, Solver.Pre_proof.pp_dot with
| Some file, lazy (Some p), Some pp_dot ->
Profile.with_ "dot.proof" @@ fun () ->
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
pp_dot fmt p;
Format.pp_print_flush fmt (); flush oc)
| _ -> ()
end;
(* FIXME: instead, create a proof if proof file or --check is given
begin match proof_file, proof with
| Some file, lazy (Some p) ->
Profile.with_ "proof.write-file" @@ fun () ->
@ -202,6 +187,7 @@ let solve
(fun oc -> Proof.Quip.output oc p; flush oc)
| _ -> ()
end;
*)
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
@ -212,9 +198,8 @@ let solve
(* process a single statement *)
let process_stmt
?hyps
?gc ?restarts ?(pp_cnf=false)
?dot_proof ?proof_file ?pp_model ?(check=false)
?proof_file ?pp_model ?(check=false)
?time ?memory ?progress
(solver:Solver.t)
(stmt:Statement.t) : unit or_error =
@ -230,6 +215,7 @@ let process_stmt
ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret);
(* TODO: more? *)
in
begin match stmt with
| Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT"|"QF_UFDT") ->
E.return ()
@ -247,15 +233,13 @@ let process_stmt
(* FIXME: how to map [l] to [assumptions] in proof? *)
let assumptions =
List.map
(fun (sign,t) ->
let a, _pr = Solver.mk_atom_t solver ~sign t in
a)
(fun (sign,t) -> Solver.mk_lit_t solver ~sign t)
l
in
solve
?gc ?restarts ?dot_proof ~check ?proof_file ?pp_model
?gc ?restarts ~check ?proof_file ?pp_model
?time ?memory ?progress
~assumptions ?hyps
~assumptions
solver;
E.return()
| Statement.Stmt_ty_decl (id,n) ->
@ -269,34 +253,27 @@ let process_stmt
if pp_cnf then (
Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
);
let atom, pr_atom = Solver.mk_atom_t solver t in
CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
Solver.add_clause solver (IArray.singleton atom)
Proof.(hres_l (assertion t) [p1 pr_atom]);
let lit = Solver.mk_lit_t solver t in
Solver.add_clause solver (IArray.singleton lit)
(Solver.P.emit_input_clause (Iter.singleton lit));
E.return()
| Statement.Stmt_assert_clause c_ts ->
if pp_cnf then (
Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts
);
let pr_l = ref [] in
let c =
List.map
(fun lit ->
let a, pr = Solver.mk_atom_t solver lit in
if not (Proof.is_trivial_refl pr) then pr_l := pr :: !pr_l;
a)
c_ts in
CCOpt.iter (fun h -> Vec.push h c) hyps;
let proof =
let open Proof in
let p = assertion_c (Iter.of_list c_ts |> Iter.map (fun t->lit_a t)) in
(* rewrite with preprocessing proofs *)
if !pr_l = [] then p else hres_l p (List.rev_map p1 !pr_l)
let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in
(* proof of assert-input + preprocessing *)
let emit_proof p =
let module P = Solver.P in
let tst = Solver.tst solver in
P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) p;
P.emit_redundant_clause (Iter.of_list c) p;
in
Solver.add_clause solver (IArray.of_list c) proof ;
Solver.add_clause solver (IArray.of_list c) emit_proof;
E.return()
| Statement.Stmt_data _ ->

5
src/smtlib/Process.mli
View file

@ -3,10 +3,11 @@
open Sidekick_base
module Solver
: Sidekick_msat_solver.S with type T.Term.t = Term.t
: Sidekick_smt_solver.S with type T.Term.t = Term.t
and type T.Term.store = Term.store
and type T.Ty.t = Ty.t
and type T.Ty.store = Ty.store
and type proof = Proof_stub.t
val th_bool : Solver.theory
val th_data : Solver.theory
@ -20,11 +21,9 @@ module Check_cc : sig
end
val process_stmt :
?hyps:Solver.Atom.t list Vec.t ->
?gc:bool ->
?restarts:bool ->
?pp_cnf:bool ->
?dot_proof:string ->
?proof_file:string ->
?pp_model:bool ->
?check:bool ->

1
src/smtlib/Sidekick_smtlib.ml
View file

@ -8,6 +8,7 @@ module Process = Process
module Solver = Process.Solver
module Term = Sidekick_base.Term
module Stmt = Sidekick_base.Statement
module Proof = Sidekick_base.Proof_stub
type 'a or_error = ('a, string) CCResult.t

1
src/smtlib/Sidekick_smtlib.mli
View file

@ -10,6 +10,7 @@ module Term = Sidekick_base.Term
module Stmt = Sidekick_base.Statement
module Process = Process
module Solver = Process.Solver
module Proof = Sidekick_base.Proof_stub (* FIXME: actual DRUP(T) proof *)
val parse : Term.store -> string -> Stmt.t list or_error

3
src/smtlib/dune
View file

@ -3,6 +3,5 @@
(public_name sidekick-bin.smtlib)
(libraries containers zarith sidekick.core sidekick.util
sidekick-base sidekick-base.solver
sidekick.backend smtlib-utils
sidekick.tef)
smtlib-utils sidekick.tef)
(flags :standard -warn-error -a+8 -open Sidekick_util))

10
src/tests/basic.cnf Normal file
View file

@ -0,0 +1,10 @@
p cnf 4 8
1 2 -3 0
-1 -2 3 0
2 3 -4 0
-2 -3 4 0
1 3 4 0
-1 -3 -4 0
-1 2 4 0
1 -2 -4 0

4
src/tests/basic.drup.expected Normal file
View file

@ -0,0 +1,4 @@
-4 -1 0
-1 0
-3 0
0

29
src/tests/dune Normal file
View file

@ -0,0 +1,29 @@
(executable
(name run_tests)
(modules run_tests)
(modes native)
(libraries containers alcotest qcheck sidekick.util
sidekick_test_simplex2 sidekick_test_util sidekick_test_minicc)
(flags :standard -warn-error -a+8 -color always))
(alias
(name runtest)
(locks /test)
(package sidekick)
(action
(progn
(run ./run_tests.exe alcotest) ; run regressions first
(run ./run_tests.exe qcheck --verbose))))
(rule
(targets basic.drup)
(deps (:pb basic.cnf) (:solver ../main/main.exe))
(action (run %{solver} %{pb} -t 2 -o %{targets})))
(alias
(name runtest)
(locks /test)
(package sidekick-bin)
(action
(diff basic.drup basic.drup.expected)))

12
src/lra/tests/run_tests.ml → src/tests/run_tests.ml
View file

@ -1,11 +1,15 @@
let tests : unit Alcotest.test list = [
Test_simplex2.tests;
]
let tests : unit Alcotest.test list =
List.flatten @@ [
[Sidekick_test_simplex2.tests];
[Sidekick_test_minicc.tests];
Sidekick_test_util.tests;
]
let props =
List.flatten
[ Test_simplex2.props;
[ Sidekick_test_simplex2.props;
Sidekick_test_util.props;
]
let () =

245
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -27,18 +27,6 @@ module type ARG = sig
val view_as_bool : term -> (term, term Iter.t) bool_view
(** Project the term into the boolean view. *)
(** [proof_ite_true (ite a b c)] is [a=true |- ite a b c = b] *)
val proof_ite_true : S.T.Term.t -> S.P.t
(** [proof_ite_false (ite a b c)] is [a=false |- ite a b c = c] *)
val proof_ite_false : S.T.Term.t -> S.P.t
(** Basic boolean logic for [|- a=b] *)
val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t
(** Basic boolean logic for a clause [|- c] *)
val proof_bool_c : string -> term list -> S.P.t
val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
(** Make a term from the given boolean view. *)
@ -48,6 +36,22 @@ module type ARG = sig
Only enable if some theories are susceptible to
create boolean formulas during the proof search. *)
val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> unit
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : string -> term list -> S.P.t -> unit
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the rule designated by [name]. *)
val lemma_bool_equiv : term -> term -> S.P.t -> unit
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : a:term -> ite:term -> S.P.t -> unit
(** lemma [a => ite a b c = b] *)
val lemma_ite_false : a:term -> ite:term -> S.P.t -> unit
(** lemma [¬a => ite a b c = c] *)
(** Fresh symbol generator.
The theory needs to be able to create new terms with fresh names,
@ -98,13 +102,11 @@ module Make(A : ARG) : S with module A = A = struct
type state = {
tst: T.store;
ty_st: Ty.store;
cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t;
}
let create tst ty_st : state =
{ tst; ty_st;
cnf=T.Tbl.create 128;
gensym=A.Gensym.create tst;
}
@ -114,9 +116,17 @@ module Make(A : ARG) : S with module A = A = struct
let is_true t = match T.as_bool t with Some true -> true | _ -> false
let is_false t = match T.as_bool t with Some false -> true | _ -> false
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.P.t) option =
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
let tst = self.tst in
let ret u = Some (u, A.proof_bool_eq t u) in
let ret u =
if not (T.equal t u) then (
SI.Simplify.with_proof simp (fun p ->
A.lemma_bool_equiv t u p;
A.S.P.lemma_preprocess t u p;
);
);
Some u
in
match A.view_as_bool t with
| B_bool _ -> None
| B_not u when is_true u -> ret (T.bool tst false)
@ -138,14 +148,14 @@ module Make(A : ARG) : S with module A = A = struct
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a, pr_a = SI.Simplify.normalize_t simp a in
let a = SI.Simplify.normalize_t simp a in
begin match A.view_as_bool a with
| B_bool true ->
let pr = SI.P.(hres_l (A.proof_ite_true t) [r1 pr_a]) in
Some (b, pr)
SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t);
Some b
| B_bool false ->
let pr = SI.P.(hres_l (A.proof_ite_false t) [r1 pr_a]) in
Some (c, pr)
SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t);
Some c
| _ ->
None
end
@ -163,181 +173,164 @@ module Make(A : ARG) : S with module A = A = struct
| B_eq _ | B_neq _ -> None
| B_atom _ -> None
let fresh_term self ~for_ ~pre ty =
let fresh_term self ~for_t ~pre ty =
let u = A.Gensym.fresh_term self.gensym ~pre ty in
Log.debugf 20
(fun k->k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])"
T.pp u T.pp for_);
T.pp u T.pp for_t);
assert (Ty.equal ty (T.ty u));
u
let fresh_lit (self:state) ~for_ ~mk_lit ~pre : T.t * Lit.t =
let proxy = fresh_term ~for_ ~pre self (Ty.bool self.ty_st) in
let fresh_lit (self:state) ~for_t ~mk_lit ~pre : T.t * Lit.t =
let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in
proxy, mk_lit proxy
(* preprocess "ite" away *)
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
match A.view_as_bool t with
| B_ite (a,b,c) ->
let a, pr_a = SI.simp_t si a in
let a = SI.simp_t si a in
begin match A.view_as_bool a with
| B_bool true ->
(* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
let proof = SI.P.(hres_l (A.proof_ite_true t) [p1 pr_a]) in
Some (b, proof)
SI.with_proof si (A.lemma_ite_true ~a ~ite:t);
Some b
| B_bool false ->
(* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
let proof = SI.P.(hres_l (A.proof_ite_false t) [p1 pr_a]) in
Some (c, proof)
SI.with_proof si (A.lemma_ite_false ~a ~ite:t);
Some c
| _ ->
let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in
let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
SI.define_const si ~const:t_ite ~rhs:t;
let lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]
(A.proof_ite_true t);
add_clause [lit_a; mk_lit (eq self.tst t_ite c)]
(A.proof_ite_false t);
Some (t_ite, SI.P.(refl t))
SI.with_proof si (SI.P.define_term t_ite t);
let lit_a = PA.mk_lit a in
PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
(fun p -> A.lemma_ite_true ~a ~ite:t p);
PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
(fun p -> A.lemma_ite_false p ~a ~ite:t);
Some t_ite
end
| _ -> None
let[@inline] pr_def_refl _proxy t = SI.P.(refl t)
(* TODO: polarity? *)
let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t =
let t_abs, t_sign = T.abs self.tst t in
let lit_abs, pr =
match T.Tbl.find self.cnf t_abs with
| lit_pr -> lit_pr (* cached *)
| exception Not_found ->
(* compute and cache *)
let lit, pr = get_lit_uncached si t_abs in
if not (T.equal (Lit.term lit) t_abs) then (
T.Tbl.add self.cnf t_abs (lit, pr);
Log.debugf 20
(fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
Lit.pp lit T.pp t_abs);
);
lit, pr
in
let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
let lit = if t_sign then lit_abs else Lit.neg lit_abs in
lit, pr
let mk_lit = PA.mk_lit in
and equiv_ si ~get_lit ~is_xor ~for_ t_a t_b : Lit.t * SI.P.t =
let a = get_lit t_a in
let b = get_lit t_b in
(* handle boolean equality *)
let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
let a = mk_lit t_a in
let b = mk_lit t_b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
SI.define_const si ~const:t_proxy ~rhs:for_t;
SI.with_proof si (SI.P.define_term t_proxy for_t);
SI.define_const si ~const:t_proxy ~rhs:for_;
let add_clause c pr =
add_clause c pr
PA.add_clause c pr
in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b]
(if is_xor then A.proof_bool_c "xor-e+" [t_proxy]
else A.proof_bool_c "eq-e" [t_proxy; t_a]);
(if is_xor then A.lemma_bool_c "xor-e+" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_a]);
add_clause [Lit.neg proxy; Lit.neg b; a]
(if is_xor then A.proof_bool_c "xor-e-" [t_proxy]
else A.proof_bool_c "eq-e" [t_proxy; t_b]);
(if is_xor then A.lemma_bool_c "xor-e-" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_b]);
add_clause [proxy; a; b]
(if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_a]
else A.proof_bool_c "eq-i+" [t_proxy]);
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a]
else A.lemma_bool_c "eq-i+" [t_proxy]);
add_clause [proxy; Lit.neg a; Lit.neg b]
(if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_b]
else A.proof_bool_c "eq-i-" [t_proxy]);
proxy, pr_def_refl t_proxy for_
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
else A.lemma_bool_c "eq-i-" [t_proxy]);
proxy
in
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
and get_lit_uncached si t : Lit.t * SI.P.t =
let sub_p = ref [] in
let get_lit t =
let lit, pr = get_lit_and_proof_ t in
if Lit.term lit != t then (
sub_p := pr :: !sub_p;
);
lit
in
let rec get_lit_for_term_ t : Lit.t option =
match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t
| B_opaque_bool t -> mk_lit t, SI.P.refl t
| B_opaque_bool _ -> None
| B_bool _ -> None
| B_not u ->
let lit, pr = get_lit_and_proof_ u in
Lit.neg lit, pr
let lit = get_lit_for_term_ u in
CCOpt.map Lit.neg lit
| B_and l ->
let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
let subs = List.map mk_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause
PA.add_clause
[Lit.neg proxy; u]
(A.proof_bool_c "and-e" [t_proxy; t_u]))
(A.lemma_bool_c "and-e" [t_proxy; t_u]))
t_subs subs;
add_clause (proxy :: List.map Lit.neg subs)
(A.proof_bool_c "and-i" [t_proxy]);
proxy, pr_def_refl t_proxy t
PA.add_clause (proxy :: List.map Lit.neg subs)
(A.lemma_bool_c "and-i" [t_proxy]);
Some proxy
| B_or l ->
let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
let subs = List.map mk_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause [Lit.neg u; proxy]
(A.proof_bool_c "or-i" [t_proxy; t_u]))
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "or-i" [t_proxy; t_u]))
t_subs subs;
add_clause (Lit.neg proxy :: subs)
(A.proof_bool_c "or-e" [t_proxy]);
proxy, pr_def_refl t_proxy t
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "or-e" [t_proxy]);
Some proxy
| B_imply (t_args, t_u) ->
(* transform into [¬args \/ u] on the fly *)
let t_args = Iter.to_list t_args in
let args = List.map (fun t -> Lit.neg (get_lit t)) t_args in
let u = get_lit t_u in
let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in
let u = mk_lit t_u in
let subs = u :: args in
(* now the or-encoding *)
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause [Lit.neg u; proxy]
(A.proof_bool_c "imp-i" [t_proxy; t_u]))
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "imp-i" [t_proxy; t_u]))
(t_u::t_args) subs;
add_clause (Lit.neg proxy :: subs)
(A.proof_bool_c "imp-e" [t_proxy]);
proxy, pr_def_refl t_proxy t
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "imp-e" [t_proxy]);
Some proxy
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t
| B_equiv (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:false a b
| B_xor (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:true a b
| B_atom u -> mk_lit u, SI.P.refl u
| B_ite _ | B_eq _ | B_neq _ -> None
| B_equiv (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:false a b)
| B_xor (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:true a b)
| B_atom _ -> None
in
let lit, pr = get_lit_and_proof_ t in
let u = Lit.term lit in
(* put sign back as a "not" *)
let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
if T.equal u t then None else Some (u, pr)
begin match get_lit_for_term_ t with
| None -> None
| Some lit ->
let u = Lit.term lit in
(* put sign back as a "not" *)
let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
if T.equal u t then None else Some u
end
(* check if new terms were added to the congruence closure, that can be turned
into clauses *)
let check_new_terms (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
let check_new_terms (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
let cc_ = SI.cc si in
let all_terms =
let open SI in
@ -346,17 +339,17 @@ module Make(A : ARG) : S with module A = A = struct
|> Iter.map CC.N.term
in
let cnf_of t =
cnf self si t
~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
let pacts = SI.preprocess_acts_of_acts si acts in
cnf self si pacts t
in
begin
all_terms
(fun t -> match cnf_of t with
| None -> ()
| Some (u, pr_t_u) ->
| Some u ->
Log.debugf 5
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])"
T.pp t T.pp u (SI.P.pp_debug ~sharing:false) pr_t_u);
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
T.pp t T.pp u);
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
());
end;

4
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -9,6 +9,7 @@ let name = "th-cstor"
module type ARG = sig
module S : Sidekick_core.SOLVER
val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view
val lemma_cstor : S.proof -> S.Lit.t Iter.t -> unit
end
module type S = sig
@ -52,6 +53,9 @@ module Make(A : ARG) : S with module A = A = struct
(fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])"
name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t);
(* build full explanation of why the constructor terms are equal *)
(* FIXME: add a (fun p -> A.lemma_cstor p …) here.
probably we need [Some a=Some b => a=b] as a lemma for inj,
and [Some a /= None] for Error case. *)
let expl =
Expl.mk_list [
e_n1_n2;

17
src/th-data/Sidekick_th_data.ml
View file

@ -74,9 +74,9 @@ module type ARG = sig
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t
val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t
val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
end
(** Helper to compute the cardinality of types *)
@ -496,7 +496,7 @@ module Make(A : ARG) : S with module A = A = struct
end;
g
let check (self:t) (solver:SI.t) (acts:SI.actions) : unit =
let check (self:t) (solver:SI.t) (acts:SI.theory_actions) : unit =
let cc = SI.cc solver in
(* create graph *)
let g = mk_graph self cc in
@ -574,18 +574,19 @@ module Make(A : ARG) : S with module A = A = struct
|> Iter.to_rev_list
in
SI.add_clause_permanent solver acts c
(A.proof_isa_split (T.ty t) @@ (Iter.of_list c|>Iter.map SI.Lit.term));
(A.lemma_isa_split (Iter.of_list c));
Iter.diagonal_l c
(fun (c1,c2) ->
let proof = A.proof_isa_disj (T.ty t) (SI.Lit.term c1) (SI.Lit.term c2) in
let pr =
A.lemma_isa_disj (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
SI.add_clause_permanent solver acts
[SI.Lit.neg c1; SI.Lit.neg c2] proof);
[SI.Lit.neg c1; SI.Lit.neg c2] pr);
)
(* on final check, check acyclicity,
then make sure we have done case split on all terms that
need it. *)
let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) trail =
let on_final_check (self:t) (solver:SI.t) (acts:SI.theory_actions) trail =
Profile.with_ "data.final-check" @@ fun () ->
check_is_a self solver acts trail;

14
src/th-data/Sidekick_th_data.mli
View file

@ -30,11 +30,11 @@ type ('c, 'ty) data_ty_view =
module type ARG = sig
module S : Sidekick_core.SOLVER
(** Constructor symbols.
(** Constructor symbols.
A constructor is an injective symbol, part of a datatype (or "sum type").
For example, in [type option a = Some a | None],
the constructors are [Some] and [None]. *)
A constructor is an injective symbol, part of a datatype (or "sum type").
For example, in [type option a = Some a | None],
the constructors are [Some] and [None]. *)
module Cstor : sig
type t
(** Constructor *)
@ -74,9 +74,9 @@ module type ARG = sig
(* TODO: should we store this ourself? would be simpler… *)
val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t
val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t
val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
end
module type S = sig

2
src/util/Backtrack_stack.ml
View file

@ -27,7 +27,7 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
let new_lvl = n_levels self - n in
let i = Vec.get self.lvls new_lvl in
while Vec.size self.vec > i do
let x = Vec.pop self.vec in
let x = Vec.pop_exn self.vec in
f x
done;
Vec.shrink self.lvls new_lvl

55
src/util/Bitvec.ml Normal file
View file

@ -0,0 +1,55 @@
type t = {
mutable chunks: bytes; (* TODO: use a in32vec with bigarray *)
}
let create () : t = {
chunks = Bytes.make 32 '\x00';
}
let i2c = Char.chr
let c2i = Char.code
(* from index to offset in bytes *)
let[@inline] idx_bytes_ (i:int) : int = i lsr 3
(* from index to offset in a single char *)
let mask_ = 0b111
(* number of bytes *)
let[@inline] len_ (self:t) : int = Bytes.length self.chunks
let[@inline never] resize_ self idx : unit =
let new_size =
min Sys.max_string_length
(max (idx+2) (let l = len_ self in l + 10 + l / 2))
in
let new_chunks = Bytes.make new_size (i2c 0) in
Bytes.blit self.chunks 0 new_chunks 0 (len_ self);
self.chunks <- new_chunks;
assert (len_ self > idx)
let[@inline] ensure_size self i =
let idx = idx_bytes_ i in
if idx >= len_ self then (
resize_ self idx
)
let[@inline] get self i : bool =
let idx = idx_bytes_ i in
let c = c2i (Bytes.get self.chunks idx) in
(c land (1 lsl (i land mask_))) <> 0
let set self i b : unit =
let idx = idx_bytes_ i in
let c = c2i (Bytes.get self.chunks idx) in
let c =
if b
then c lor (1 lsl (i land mask_))
else c land (lnot (1 lsl (i land mask_)))
in
Bytes.set self.chunks idx (i2c c)
let clear_all self =
Bytes.fill self.chunks 0 (len_ self) '\x00'

15
src/util/Bitvec.mli Normal file
View file

@ -0,0 +1,15 @@
(** Bitvector *)
type t
val create : unit -> t
val ensure_size : t -> int -> unit
(** [ensure_size bv i] ensures that [i] is a valid index in [bv] *)
val get : t -> int -> bool
val set : t -> int -> bool -> unit
val clear_all : t -> unit

12
src/util/Sidekick_util.ml
View file

@ -1,14 +1,20 @@
(* re-exports *)
module Fmt = CCFormat
module Util = Util
module Vec = Vec
module Log = Log
module VecI32 = VecI32
module Vec_float = Vec_float
module Vec_sig = Vec_sig
module Bitvec = Bitvec
module IArray = IArray
module Backtrack_stack = Backtrack_stack
module Backtrackable_tbl = Backtrackable_tbl
module Log = Log
module Error = Error
module IArray = IArray
module Bag = Bag
module Stat = Stat
module Hash = Hash

11
src/util/Util.ml
View file

@ -26,6 +26,17 @@ let pp_iarray ?(sep=" ") pp out a =
let flat_map_l_ia f l =
CCList.flat_map (fun x -> IArray.to_list @@ f x) l
let array_of_list_map f l =
match l with
| [] -> [| |]
| x :: tl ->
let arr = Array.make (List.length tl+1) (f x) in
List.iteri (fun i y -> arr.(i+1) <- f y) tl;
arr
let array_to_list_map f arr =
List.init (Array.length arr) (fun i -> f arr.(i))
let setup_gc () =
let g = Gc.get () in
Gc.set {

5
src/util/Util.mli
View file

@ -16,6 +16,11 @@ val pp_iarray : ?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.print
val flat_map_l_ia : ('a -> 'b IArray.t) -> 'a list -> 'b list
val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
(** [array_of_list_map f l] is the same as [Array.of_list @@ List.map f l] *)
val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
val setup_gc : unit -> unit
(** Change parameters of the GC *)

55
src/util/Vec.ml
View file

@ -15,12 +15,20 @@ let[@inline] shrink t i =
assert (i<=t.sz);
t.sz <- i
let[@inline] pop t =
let[@inline] pop_exn t =
if t.sz = 0 then invalid_arg "vec.pop";
let x = Array.unsafe_get t.data (t.sz - 1) in
t.sz <- t.sz - 1;
x
let[@inline] pop t =
if t.sz = 0 then None
else (
let x = Array.unsafe_get t.data (t.sz - 1) in
t.sz <- t.sz - 1;
Some x
)
let[@inline] size t = t.sz
let[@inline] is_empty t = t.sz = 0
@ -31,17 +39,38 @@ let[@inline] copy t : _ t =
let data = Array.copy t.data in
{t with data}
let resize_ t x size =
let arr' = Array.make size x in
Array.blit t.data 0 arr' 0 t.sz;
t.data <- arr';
()
let ensure_cap_ self x n =
if n > Array.length self.data then (
let new_size = max n (2 * Array.length self.data) in
resize_ self (x()) new_size
)
let ensure_size_with self f n =
ensure_cap_ self f n;
if n > self.sz then (
for i=self.sz to n-1 do
self.data.(i) <- f();
done;
self.sz <- n
)
let ensure_size self x n = ensure_size_with self (fun() -> x) n
(* grow the array *)
let[@inline never] grow_to_double_size t x : unit =
if Array.length t.data = Sys.max_array_length then (
failwith "vec: cannot resize";
);
let size =
let new_size =
min Sys.max_array_length (max 4 (2 * Array.length t.data))
in
let arr' = Array.make size x in
Array.blit t.data 0 arr' 0 (Array.length t.data);
t.data <- arr';
if new_size = t.sz then (
failwith "vec: cannot resize";
);
resize_ t x new_size;
assert (Array.length t.data > t.sz);
()
@ -67,6 +96,16 @@ let[@inline] fast_remove t i =
Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1);
t.sz <- t.sz - 1
let prepend v ~into : unit =
if v.sz = 0 then ()
else (
if v.sz + into.sz > Array.length into.data then (
resize_ into v.data.(0) (v.sz + into.sz);
);
Array.blit into.data 0 into.data v.sz into.sz; (* shift elements *)
Array.blit v.data 0 into.data 0 v.sz;
)
let filter_in_place f vec =
let i = ref 0 in
while !i < size vec do

14
src/util/Vec.mli
View file

@ -28,14 +28,22 @@ val to_seq : 'a t -> 'a Iter.t
val clear : 'a t -> unit
(** Set size to 0, doesn't free elements *)
val ensure_size : 'a t -> 'a -> int -> unit
(** ensure size is at least [n] *)
val ensure_size_with : 'a t -> (unit -> 'a) -> int -> unit
(** ensure size is at least [n] *)
val shrink : 'a t -> int -> unit
(** [shrink vec sz] resets size of [vec] to [sz].
Assumes [sz >=0 && sz <= size vec] *)
val pop : 'a t -> 'a
val pop_exn : 'a t -> 'a
(** Pop last element and return it.
@raise Invalid_argument if the vector is empty *)
val pop : 'a t -> 'a option
val size : 'a t -> int
val is_empty : 'a t -> bool
@ -62,6 +70,10 @@ val fast_remove : 'a t -> int -> unit
(** Remove element at index [i] without preserving order
(swap with last element) *)
val prepend : 'a t -> into:'a t -> unit
(** [prepend v ~into] pushes all elements of [v] into [into],
at the beginning. consumes [v]. *)
val filter_in_place : ('a -> bool) -> 'a t -> unit
(** [filter_in_place f v] removes from [v] the elements that do
not satisfy [f] *)

100
src/util/VecI32.ml Normal file
View file

@ -0,0 +1,100 @@
module A = Bigarray.Array1
type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t
type t = {
mutable data: int32arr;
mutable sz: int;
}
let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz
let create ?(cap=16) () : t =
{ sz=0; data=mk_arr_ cap }
let[@inline] clear self = self.sz <- 0
let[@inline] shrink self n = if n < self.sz then self.sz <- n
let[@inline] size self = self.sz
let[@inline] is_empty self = self.sz = 0
let[@inline] fast_remove t i =
assert (i>= 0 && i < t.sz);
A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
t.sz <- t.sz - 1
let filter_in_place f vec =
let i = ref 0 in
while !i < size vec do
if f (Int32.to_int (A.unsafe_get vec.data !i)) then incr i else fast_remove vec !i
done
(* ensure capacity is [new_cap] *)
let resize_cap_ self new_cap =
assert (A.dim self.data < new_cap);
let new_data = mk_arr_ new_cap in
A.blit self.data (A.sub new_data 0 (A.dim self.data));
self.data <- new_data
let ensure_cap self (n:int) =
if n > A.dim self.data then (
let new_cap = max n (max 4 (A.dim self.data * 2)) in
resize_cap_ self new_cap;
)
let ensure_size self n =
if n > self.sz then (
ensure_cap self n;
self.sz <- n
)
let[@inline] push (self:t) i : unit =
ensure_cap self (self.sz+1);
self.data.{self.sz} <- Int32.of_int i;
self.sz <- 1 + self.sz
let[@inline] push_i32 self i =
ensure_cap self (self.sz+1);
self.data.{self.sz} <- i;
self.sz <- 1 + self.sz
let[@inline] pop self =
if self.sz > 0 then (
let x = Int32.to_int self.data.{self.sz-1} in
self.sz <- self.sz - 1;
x
) else failwith "vecI32.pop: empty"
let[@inline] get self i : int =
assert (i >= 0 && i < self.sz);
Int32.to_int (A.unsafe_get self.data i)
let[@inline] get_i32 self i : int32 =
assert (i >= 0 && i < self.sz);
A.unsafe_get self.data i
let[@inline] set self i x : unit =
assert (i >= 0 && i < self.sz);
A.unsafe_set self.data i (Int32.of_int x)
let[@inline] set_i32 self i x : unit =
assert (i >= 0 && i < self.sz);
A.unsafe_set self.data i x
let[@inline] iter ~f self =
for i=0 to self.sz - 1 do
f (Int32.to_int self.data.{i})
done
let[@inline] iteri ~f self =
for i=0 to self.sz - 1 do
f i (Int32.to_int self.data.{i})
done
let[@inline] to_iter self k = iter ~f:k self
let pp out self =
Format.fprintf out "[@[";
iteri self ~f:(fun i x -> if i>0 then Format.fprintf out ",@ "; Format.pp_print_int out x);
Format.fprintf out "@]]"

15
src/util/VecI32.mli Normal file
View file

@ -0,0 +1,15 @@
(** Vectors of int32 integers
These vectors are more optimized than {!Vec}. *)
include Vec_sig.S with type elt := int
val ensure_size : t -> int -> unit
val push_i32 : t -> int32 -> unit
val get_i32 : t -> int -> int32
val set_i32 : t -> int -> int32 -> unit

88
src/util/Vec_float.ml Normal file
View file

@ -0,0 +1,88 @@
module A = Bigarray.Array1
type float_arr = (float, Bigarray.float64_elt, Bigarray.c_layout) A.t
type t = {
mutable data: float_arr;
mutable sz: int;
}
let mk_arr_ sz : float_arr = A.create Bigarray.float64 Bigarray.c_layout sz
let create ?(cap=16) () : t =
{ sz=0; data=mk_arr_ cap }
let[@inline] clear self = self.sz <- 0
let[@inline] shrink self n = if n < self.sz then self.sz <- n
let[@inline] size self = self.sz
let[@inline] is_empty self = self.sz = 0
let[@inline] fast_remove t i =
assert (i>= 0 && i < t.sz);
A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
t.sz <- t.sz - 1
let filter_in_place f vec =
let i = ref 0 in
while !i < size vec do
if f (A.unsafe_get vec.data !i) then incr i else fast_remove vec !i
done
(* ensure capacity is [new_cap] *)
let resize_cap_ self new_cap =
assert (A.dim self.data < new_cap);
let new_data = mk_arr_ new_cap in
A.blit self.data (A.sub new_data 0 (A.dim self.data));
self.data <- new_data
let ensure_cap self (n:int) =
if n > A.dim self.data then (
let new_cap = max n (A.dim self.data * 2 + 10) in
resize_cap_ self new_cap;
)
let ensure_size self n =
if n > self.sz then (
ensure_cap self n;
self.sz <- n
)
let[@inline] push (self:t) x : unit =
ensure_cap self (self.sz+1);
self.data.{self.sz} <- x;
self.sz <- 1 + self.sz
let[@inline] pop self =
if self.sz > 0 then (
let x = self.data.{self.sz-1} in
self.sz <- self.sz - 1;
x
) else failwith "vec_float.pop: empty"
let[@inline] get self i : float =
assert (i >= 0 && i < self.sz);
A.unsafe_get self.data i
let[@inline] set self i x : unit =
assert (i >= 0 && i < self.sz);
A.unsafe_set self.data i x
let[@inline] iter ~f self =
for i=0 to self.sz - 1 do
f self.data.{i}
done
let[@inline] iteri ~f self =
for i=0 to self.sz - 1 do
f i self.data.{i}
done
let[@inline] to_iter self k = iter ~f:k self
let pp out self =
Format.fprintf out "[@[";
iteri self
~f:(fun i x -> if i>0 then Format.fprintf out ",@ "; Format.fprintf out "%.3f" x);
Format.fprintf out "@]]"

8
src/util/Vec_float.mli Normal file
View file

@ -0,0 +1,8 @@
(** Vectors of floats
These vectors are more optimized than {!Vec}. *)
include Vec_sig.S with type elt := float
val ensure_size : t -> int -> unit

36
src/util/Vec_sig.ml Normal file
View file

@ -0,0 +1,36 @@
module type S = sig
type elt
type t
val create : ?cap:int -> unit -> t
val size : t -> int
val clear : t -> unit
val is_empty : t -> bool
val push : t -> elt -> unit
val fast_remove : t -> int -> unit
(** Remove element at index [i] without preserving order
(swap with last element) *)
val filter_in_place : (elt -> bool) -> t -> unit
val pop : t -> elt
val get : t -> int -> elt
val set : t -> int -> elt -> unit
val shrink : t -> int -> unit
val iter : f:(elt -> unit) -> t -> unit
val iteri : f:(int -> elt -> unit) -> t -> unit
val to_iter : t -> elt Iter.t
val pp : t CCFormat.printer
end

3
src/util/dune
View file

@ -1,4 +1,5 @@
(library
(name sidekick_util)
(public_name sidekick.util)
(libraries containers iter sidekick.sigs))
(flags :standard -warn-error -a+8)
(libraries containers iter sidekick.sigs bigarray))

5
src/util/tests/dune Normal file
View file

@ -0,0 +1,5 @@
(library
(name sidekick_test_util)
(flags :standard -warn-error -a+8 -open Sidekick_util)
(libraries qcheck alcotest sidekick.util))

5
src/util/tests/sidekick_test_util.ml Normal file
View file

@ -0,0 +1,5 @@
let tests = [Test_bitvec.tests]
let props = [
]

30
src/util/tests/test_bitvec.ml Normal file
View file

@ -0,0 +1,30 @@
module A = Alcotest
let spf = Printf.sprintf
let msgline line = spf "test at line %d" line
let alco_mk name f = name, `Quick, f
module BV = Bitvec
let t1 = alco_mk "mkgetset" @@ fun () ->
let bv = BV.create() in
BV.ensure_size bv 200;
A.(check bool) (msgline __LINE__) false (BV.get bv 0);
A.(check bool) (msgline __LINE__) false (BV.get bv 1);
for i=30 to 150 do
A.(check bool) (msgline __LINE__) false (BV.get bv i);
done;
BV.set bv 25 true;
BV.set bv 1 true;
BV.set bv 127 true;
BV.set bv 126 true;
BV.set bv 126 false;
for i=0 to 150 do
A.(check bool) (msgline __LINE__) (i=1||i=25||i=127) (BV.get bv i);
done;
()
let tests = "bitvec", [t1]

8
tests/benchpress.sexp
View file

@ -20,6 +20,14 @@
(timeout 10)
(dirs $cur_dir/sat $cur_dir/unsat $cur_dir/pigeon))))
(task
(name sidekick-smt-local)
(action
(run_provers
(provers sidekick-dev z3)
(timeout 10)
(dirs $cur_dir/))))
(task
(name sidekick-smt-nodir)
(action

2
tests/bf/README Normal file
View file

@ -0,0 +1,2 @@
Source: http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/BF/bf.tar.gz
Description: http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/BF/descr.html

3681
tests/bf/bf0432-007.cnf Normal file
View file

File diff suppressed because it is too large Load diff

6791
tests/bf/bf1355-075.cnf Normal file
View file

File diff suppressed because it is too large Load diff

6781
tests/bf/bf1355-638.cnf Normal file
View file

File diff suppressed because it is too large Load diff

3447
tests/bf/bf2670-001.cnf Normal file
View file

File diff suppressed because it is too large Load diff

2
tests/dubois/README Normal file
View file

@ -0,0 +1,2 @@
Source: http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/DUBOIS/dubois.tar.gz
Description: http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/DUBOIS/descr.html

813
tests/dubois/dubois100.cnf Normal file
View file

@ -0,0 +1,813 @@
c FILE: dubois100.cnf
c
c SOURCE: Olivier Dubois (dubois@laforia.ibp.fr)
c
c DESCRIPTION: Instance from generator gensathard.c
c
c NOTE: Not satisfiable
c
c d = 100
c n = 300
c p = 800
c r = 3
p cnf 300 800
199 200 1 0
-199 -200 1 0
199 -200 -1 0
-199 200 -1 0
1 201 2 0
-1 -201 2 0
1 -201 -2 0
-1 201 -2 0
2 202 3 0
-2 -202 3 0
2 -202 -3 0
-2 202 -3 0
3 203 4 0
-3 -203 4 0
3 -203 -4 0
-3 203 -4 0
4 204 5 0
-4 -204 5 0
4 -204 -5 0
-4 204 -5 0
5 205 6 0
-5 -205 6 0
5 -205 -6 0
-5 205 -6 0
6 206 7 0
-6 -206 7 0
6 -206 -7 0
-6 206 -7 0
7 207 8 0
-7 -207 8 0
7 -207 -8 0
-7 207 -8 0
8 208 9 0
-8 -208 9 0
8 -208 -9 0
-8 208 -9 0
9 209 10 0
-9 -209 10 0
9 -209 -10 0
-9 209 -10 0
10 210 11 0
-10 -210 11 0
10 -210 -11 0
-10 210 -11 0
11 211 12 0
-11 -211 12 0
11 -211 -12 0
-11 211 -12 0
12 212 13 0
-12 -212 13 0
12 -212 -13 0
-12 212 -13 0
13 213 14 0
-13 -213 14 0
13 -213 -14 0
-13 213 -14 0
14 214 15 0
-14 -214 15 0
14 -214 -15 0
-14 214 -15 0
15 215 16 0
-15 -215 16 0
15 -215 -16 0
-15 215 -16 0
16 216 17 0
-16 -216 17 0
16 -216 -17 0
-16 216 -17 0
17 217 18 0
-17 -217 18 0
17 -217 -18 0
-17 217 -18 0
18 218 19 0
-18 -218 19 0
18 -218 -19 0
-18 218 -19 0
19 219 20 0
-19 -219 20 0
19 -219 -20 0
-19 219 -20 0
20 220 21 0
-20 -220 21 0
20 -220 -21 0
-20 220 -21 0
21 221 22 0
-21 -221 22 0
21 -221 -22 0
-21 221 -22 0
22 222 23 0
-22 -222 23 0
22 -222 -23 0
-22 222 -23 0
23 223 24 0
-23 -223 24 0
23 -223 -24 0
-23 223 -24 0
24 224 25 0
-24 -224 25 0
24 -224 -25 0
-24 224 -25 0
25 225 26 0
-25 -225 26 0
25 -225 -26 0
-25 225 -26 0
26 226 27 0
-26 -226 27 0
26 -226 -27 0
-26 226 -27 0
27 227 28 0
-27 -227 28 0
27 -227 -28 0
-27 227 -28 0
28 228 29 0
-28 -228 29 0
28 -228 -29 0
-28 228 -29 0
29 229 30 0
-29 -229 30 0
29 -229 -30 0
-29 229 -30 0
30 230 31 0
-30 -230 31 0
30 -230 -31 0
-30 230 -31 0
31 231 32 0
-31 -231 32 0
31 -231 -32 0
-31 231 -32 0
32 232 33 0
-32 -232 33 0
32 -232 -33 0
-32 232 -33 0
33 233 34 0
-33 -233 34 0
33 -233 -34 0
-33 233 -34 0
34 234 35 0
-34 -234 35 0
34 -234 -35 0
-34 234 -35 0
35 235 36 0
-35 -235 36 0
35 -235 -36 0
-35 235 -36 0
36 236 37 0
-36 -236 37 0
36 -236 -37 0
-36 236 -37 0
37 237 38 0
-37 -237 38 0
37 -237 -38 0
-37 237 -38 0
38 238 39 0
-38 -238 39 0
38 -238 -39 0
-38 238 -39 0
39 239 40 0
-39 -239 40 0
39 -239 -40 0
-39 239 -40 0
40 240 41 0
-40 -240 41 0
40 -240 -41 0
-40 240 -41 0
41 241 42 0
-41 -241 42 0
41 -241 -42 0
-41 241 -42 0
42 242 43 0
-42 -242 43 0
42 -242 -43 0
-42 242 -43 0
43 243 44 0
-43 -243 44 0
43 -243 -44 0
-43 243 -44 0
44 244 45 0
-44 -244 45 0
44 -244 -45 0
-44 244 -45 0
45 245 46 0
-45 -245 46 0
45 -245 -46 0
-45 245 -46 0
46 246 47 0
-46 -246 47 0
46 -246 -47 0
-46 246 -47 0
47 247 48 0
-47 -247 48 0
47 -247 -48 0
-47 247 -48 0
48 248 49 0
-48 -248 49 0
48 -248 -49 0
-48 248 -49 0
49 249 50 0
-49 -249 50 0
49 -249 -50 0
-49 249 -50 0
50 250 51 0
-50 -250 51 0
50 -250 -51 0
-50 250 -51 0
51 251 52 0
-51 -251 52 0
51 -251 -52 0
-51 251 -52 0
52 252 53 0
-52 -252 53 0
52 -252 -53 0
-52 252 -53 0
53 253 54 0
-53 -253 54 0
53 -253 -54 0
-53 253 -54 0
54 254 55 0
-54 -254 55 0
54 -254 -55 0
-54 254 -55 0
55 255 56 0
-55 -255 56 0
55 -255 -56 0
-55 255 -56 0
56 256 57 0
-56 -256 57 0
56 -256 -57 0
-56 256 -57 0
57 257 58 0
-57 -257 58 0
57 -257 -58 0
-57 257 -58 0
58 258 59 0
-58 -258 59 0
58 -258 -59 0
-58 258 -59 0
59 259 60 0
-59 -259 60 0
59 -259 -60 0
-59 259 -60 0
60 260 61 0
-60 -260 61 0
60 -260 -61 0
-60 260 -61 0
61 261 62 0
-61 -261 62 0
61 -261 -62 0
-61 261 -62 0
62 262 63 0
-62 -262 63 0
62 -262 -63 0
-62 262 -63 0
63 263 64 0
-63 -263 64 0
63 -263 -64 0
-63 263 -64 0
64 264 65 0
-64 -264 65 0
64 -264 -65 0
-64 264 -65 0
65 265 66 0
-65 -265 66 0
65 -265 -66 0
-65 265 -66 0
66 266 67 0
-66 -266 67 0
66 -266 -67 0
-66 266 -67 0
67 267 68 0
-67 -267 68 0
67 -267 -68 0
-67 267 -68 0
68 268 69 0
-68 -268 69 0
68 -268 -69 0
-68 268 -69 0
69 269 70 0
-69 -269 70 0
69 -269 -70 0
-69 269 -70 0
70 270 71 0
-70 -270 71 0
70 -270 -71 0
-70 270 -71 0
71 271 72 0
-71 -271 72 0
71 -271 -72 0
-71 271 -72 0
72 272 73 0
-72 -272 73 0
72 -272 -73 0
-72 272 -73 0
73 273 74 0
-73 -273 74 0
73 -273 -74 0
-73 273 -74 0
74 274 75 0
-74 -274 75 0
74 -274 -75 0
-74 274 -75 0
75 275 76 0
-75 -275 76 0
75 -275 -76 0
-75 275 -76 0
76 276 77 0
-76 -276 77 0
76 -276 -77 0
-76 276 -77 0
77 277 78 0
-77 -277 78 0
77 -277 -78 0
-77 277 -78 0
78 278 79 0
-78 -278 79 0
78 -278 -79 0
-78 278 -79 0
79 279 80 0
-79 -279 80 0
79 -279 -80 0
-79 279 -80 0
80 280 81 0
-80 -280 81 0
80 -280 -81 0
-80 280 -81 0
81 281 82 0
-81 -281 82 0
81 -281 -82 0
-81 281 -82 0
82 282 83 0
-82 -282 83 0
82 -282 -83 0
-82 282 -83 0
83 283 84 0
-83 -283 84 0
83 -283 -84 0
-83 283 -84 0
84 284 85 0
-84 -284 85 0
84 -284 -85 0
-84 284 -85 0
85 285 86 0
-85 -285 86 0
85 -285 -86 0
-85 285 -86 0
86 286 87 0
-86 -286 87 0
86 -286 -87 0
-86 286 -87 0
87 287 88 0
-87 -287 88 0
87 -287 -88 0
-87 287 -88 0
88 288 89 0
-88 -288 89 0
88 -288 -89 0
-88 288 -89 0
89 289 90 0
-89 -289 90 0
89 -289 -90 0
-89 289 -90 0
90 290 91 0
-90 -290 91 0
90 -290 -91 0
-90 290 -91 0
91 291 92 0
-91 -291 92 0
91 -291 -92 0
-91 291 -92 0
92 292 93 0
-92 -292 93 0
92 -292 -93 0
-92 292 -93 0
93 293 94 0
-93 -293 94 0
93 -293 -94 0
-93 293 -94 0
94 294 95 0
-94 -294 95 0
94 -294 -95 0
-94 294 -95 0
95 295 96 0
-95 -295 96 0
95 -295 -96 0
-95 295 -96 0
96 296 97 0
-96 -296 97 0
96 -296 -97 0
-96 296 -97 0
97 297 98 0
-97 -297 98 0
97 -297 -98 0
-97 297 -98 0
98 298 99 0
-98 -298 99 0
98 -298 -99 0
-98 298 -99 0
99 299 300 0
-99 -299 300 0
99 -299 -300 0
-99 299 -300 0
100 299 300 0
-100 -299 300 0
100 -299 -300 0
-100 299 -300 0
101 298 100 0
-101 -298 100 0
101 -298 -100 0
-101 298 -100 0
102 297 101 0
-102 -297 101 0
102 -297 -101 0
-102 297 -101 0
103 296 102 0
-103 -296 102 0
103 -296 -102 0
-103 296 -102 0
104 295 103 0
-104 -295 103 0
104 -295 -103 0
-104 295 -103 0
105 294 104 0
-105 -294 104 0
105 -294 -104 0
-105 294 -104 0
106 293 105 0
-106 -293 105 0
106 -293 -105 0
-106 293 -105 0
107 292 106 0
-107 -292 106 0
107 -292 -106 0
-107 292 -106 0
108 291 107 0
-108 -291 107 0
108 -291 -107 0
-108 291 -107 0
109 290 108 0
-109 -290 108 0
109 -290 -108 0
-109 290 -108 0
110 289 109 0
-110 -289 109 0
110 -289 -109 0
-110 289 -109 0
111 288 110 0
-111 -288 110 0
111 -288 -110 0
-111 288 -110 0
112 287 111 0
-112 -287 111 0
112 -287 -111 0
-112 287 -111 0
113 286 112 0
-113 -286 112 0
113 -286 -112 0
-113 286 -112 0
114 285 113 0
-114 -285 113 0
114 -285 -113 0
-114 285 -113 0
115 284 114 0
-115 -284 114 0
115 -284 -114 0
-115 284 -114 0
116 283 115 0
-116 -283 115 0
116 -283 -115 0
-116 283 -115 0
117 282 116 0
-117 -282 116 0
117 -282 -116 0
-117 282 -116 0
118 281 117 0
-118 -281 117 0
118 -281 -117 0
-118 281 -117 0
119 280 118 0
-119 -280 118 0
119 -280 -118 0
-119 280 -118 0
120 279 119 0
-120 -279 119 0
120 -279 -119 0
-120 279 -119 0
121 278 120 0
-121 -278 120 0
121 -278 -120 0
-121 278 -120 0
122 277 121 0
-122 -277 121 0
122 -277 -121 0
-122 277 -121 0
123 276 122 0
-123 -276 122 0
123 -276 -122 0
-123 276 -122 0
124 275 123 0
-124 -275 123 0
124 -275 -123 0
-124 275 -123 0
125 274 124 0
-125 -274 124 0
125 -274 -124 0
-125 274 -124 0
126 273 125 0
-126 -273 125 0
126 -273 -125 0
-126 273 -125 0
127 272 126 0
-127 -272 126 0
127 -272 -126 0
-127 272 -126 0
128 271 127 0
-128 -271 127 0
128 -271 -127 0
-128 271 -127 0
129 270 128 0
-129 -270 128 0
129 -270 -128 0
-129 270 -128 0
130 269 129 0
-130 -269 129 0
130 -269 -129 0
-130 269 -129 0
131 268 130 0
-131 -268 130 0
131 -268 -130 0
-131 268 -130 0
132 267 131 0
-132 -267 131 0
132 -267 -131 0
-132 267 -131 0
133 266 132 0
-133 -266 132 0
133 -266 -132 0
-133 266 -132 0
134 265 133 0
-134 -265 133 0
134 -265 -133 0
-134 265 -133 0
135 264 134 0
-135 -264 134 0
135 -264 -134 0
-135 264 -134 0
136 263 135 0
-136 -263 135 0
136 -263 -135 0
-136 263 -135 0
137 262 136 0
-137 -262 136 0
137 -262 -136 0
-137 262 -136 0
138 261 137 0
-138 -261 137 0
138 -261 -137 0
-138 261 -137 0
139 260 138 0
-139 -260 138 0
139 -260 -138 0
-139 260 -138 0
140 259 139 0
-140 -259 139 0
140 -259 -139 0
-140 259 -139 0
141 258 140 0
-141 -258 140 0
141 -258 -140 0
-141 258 -140 0
142 257 141 0
-142 -257 141 0
142 -257 -141 0
-142 257 -141 0
143 256 142 0
-143 -256 142 0
143 -256 -142 0
-143 256 -142 0
144 255 143 0
-144 -255 143 0
144 -255 -143 0
-144 255 -143 0
145 254 144 0
-145 -254 144 0
145 -254 -144 0
-145 254 -144 0
146 253 145 0
-146 -253 145 0
146 -253 -145 0
-146 253 -145 0
147 252 146 0
-147 -252 146 0
147 -252 -146 0
-147 252 -146 0
148 251 147 0
-148 -251 147 0
148 -251 -147 0
-148 251 -147 0
149 250 148 0
-149 -250 148 0
149 -250 -148 0
-149 250 -148 0
150 249 149 0
-150 -249 149 0
150 -249 -149 0
-150 249 -149 0
151 248 150 0
-151 -248 150 0
151 -248 -150 0
-151 248 -150 0
152 247 151 0
-152 -247 151 0
152 -247 -151 0
-152 247 -151 0
153 246 152 0
-153 -246 152 0
153 -246 -152 0
-153 246 -152 0
154 245 153 0
-154 -245 153 0
154 -245 -153 0
-154 245 -153 0
155 244 154 0
-155 -244 154 0
155 -244 -154 0
-155 244 -154 0
156 243 155 0
-156 -243 155 0
156 -243 -155 0
-156 243 -155 0
157 242 156 0
-157 -242 156 0
157 -242 -156 0
-157 242 -156 0
158 241 157 0
-158 -241 157 0
158 -241 -157 0
-158 241 -157 0
159 240 158 0
-159 -240 158 0
159 -240 -158 0
-159 240 -158 0
160 239 159 0
-160 -239 159 0
160 -239 -159 0
-160 239 -159 0
161 238 160 0
-161 -238 160 0
161 -238 -160 0
-161 238 -160 0
162 237 161 0
-162 -237 161 0
162 -237 -161 0
-162 237 -161 0
163 236 162 0
-163 -236 162 0
163 -236 -162 0
-163 236 -162 0
164 235 163 0
-164 -235 163 0
164 -235 -163 0
-164 235 -163 0
165 234 164 0
-165 -234 164 0
165 -234 -164 0
-165 234 -164 0
166 233 165 0
-166 -233 165 0
166 -233 -165 0
-166 233 -165 0
167 232 166 0
-167 -232 166 0
167 -232 -166 0
-167 232 -166 0
168 231 167 0
-168 -231 167 0
168 -231 -167 0
-168 231 -167 0
169 230 168 0
-169 -230 168 0
169 -230 -168 0
-169 230 -168 0
170 229 169 0
-170 -229 169 0
170 -229 -169 0
-170 229 -169 0
171 228 170 0
-171 -228 170 0
171 -228 -170 0
-171 228 -170 0
172 227 171 0
-172 -227 171 0
172 -227 -171 0
-172 227 -171 0
173 226 172 0
-173 -226 172 0
173 -226 -172 0
-173 226 -172 0
174 225 173 0
-174 -225 173 0
174 -225 -173 0
-174 225 -173 0
175 224 174 0
-175 -224 174 0
175 -224 -174 0
-175 224 -174 0
176 223 175 0
-176 -223 175 0
176 -223 -175 0
-176 223 -175 0
177 222 176 0
-177 -222 176 0
177 -222 -176 0
-177 222 -176 0
178 221 177 0
-178 -221 177 0
178 -221 -177 0
-178 221 -177 0
179 220 178 0
-179 -220 178 0
179 -220 -178 0
-179 220 -178 0
180 219 179 0
-180 -219 179 0
180 -219 -179 0
-180 219 -179 0
181 218 180 0
-181 -218 180 0
181 -218 -180 0
-181 218 -180 0
182 217 181 0
-182 -217 181 0
182 -217 -181 0
-182 217 -181 0
183 216 182 0
-183 -216 182 0
183 -216 -182 0
-183 216 -182 0
184 215 183 0
-184 -215 183 0
184 -215 -183 0
-184 215 -183 0
185 214 184 0
-185 -214 184 0
185 -214 -184 0
-185 214 -184 0
186 213 185 0
-186 -213 185 0
186 -213 -185 0
-186 213 -185 0
187 212 186 0
-187 -212 186 0
187 -212 -186 0
-187 212 -186 0
188 211 187 0
-188 -211 187 0
188 -211 -187 0
-188 211 -187 0
189 210 188 0
-189 -210 188 0
189 -210 -188 0
-189 210 -188 0
190 209 189 0
-190 -209 189 0
190 -209 -189 0
-190 209 -189 0
191 208 190 0
-191 -208 190 0
191 -208 -190 0
-191 208 -190 0
192 207 191 0
-192 -207 191 0
192 -207 -191 0
-192 207 -191 0
193 206 192 0
-193 -206 192 0
193 -206 -192 0
-193 206 -192 0
194 205 193 0
-194 -205 193 0
194 -205 -193 0
-194 205 -193 0
195 204 194 0
-195 -204 194 0
195 -204 -194 0
-195 204 -194 0
196 203 195 0
-196 -203 195 0
196 -203 -195 0
-196 203 -195 0
197 202 196 0
-197 -202 196 0
197 -202 -196 0
-197 202 -196 0
198 201 197 0
-198 -201 197 0
198 -201 -197 0
-198 201 -197 0
199 200 -198 0
-199 -200 -198 0
199 -200 198 0
-199 200 198 0

173
tests/dubois/dubois20.cnf Normal file
View file

@ -0,0 +1,173 @@
c FILE: dubois20.cnf
c
c SOURCE: Olivier Dubois (dubois@laforia.ibp.fr)
c
c DESCRIPTION: Instance from generator gensathard.c
c
c NOTE: Not satisfiable
c
c d = 20
c n = 60
c p = 160
c r = 3
p cnf 60 160
39 40 1 0
-39 -40 1 0
39 -40 -1 0
-39 40 -1 0
1 41 2 0
-1 -41 2 0
1 -41 -2 0
-1 41 -2 0
2 42 3 0
-2 -42 3 0
2 -42 -3 0
-2 42 -3 0
3 43 4 0
-3 -43 4 0
3 -43 -4 0
-3 43 -4 0
4 44 5 0
-4 -44 5 0
4 -44 -5 0
-4 44 -5 0
5 45 6 0
-5 -45 6 0
5 -45 -6 0
-5 45 -6 0
6 46 7 0
-6 -46 7 0
6 -46 -7 0
-6 46 -7 0
7 47 8 0
-7 -47 8 0
7 -47 -8 0
-7 47 -8 0
8 48 9 0
-8 -48 9 0
8 -48 -9 0
-8 48 -9 0
9 49 10 0
-9 -49 10 0
9 -49 -10 0
-9 49 -10 0
10 50 11 0
-10 -50 11 0
10 -50 -11 0
-10 50 -11 0
11 51 12 0
-11 -51 12 0
11 -51 -12 0
-11 51 -12 0
12 52 13 0
-12 -52 13 0
12 -52 -13 0
-12 52 -13 0
13 53 14 0
-13 -53 14 0
13 -53 -14 0
-13 53 -14 0
14 54 15 0
-14 -54 15 0
14 -54 -15 0
-14 54 -15 0
15 55 16 0
-15 -55 16 0
15 -55 -16 0
-15 55 -16 0
16 56 17 0
-16 -56 17 0
16 -56 -17 0
-16 56 -17 0
17 57 18 0
-17 -57 18 0
17 -57 -18 0
-17 57 -18 0
18 58 19 0
-18 -58 19 0
18 -58 -19 0
-18 58 -19 0
19 59 60 0
-19 -59 60 0
19 -59 -60 0
-19 59 -60 0
20 59 60 0
-20 -59 60 0
20 -59 -60 0
-20 59 -60 0
21 58 20 0
-21 -58 20 0
21 -58 -20 0
-21 58 -20 0
22 57 21 0
-22 -57 21 0
22 -57 -21 0
-22 57 -21 0
23 56 22 0
-23 -56 22 0
23 -56 -22 0
-23 56 -22 0
24 55 23 0
-24 -55 23 0
24 -55 -23 0
-24 55 -23 0
25 54 24 0
-25 -54 24 0
25 -54 -24 0
-25 54 -24 0
26 53 25 0
-26 -53 25 0
26 -53 -25 0
-26 53 -25 0
27 52 26 0
-27 -52 26 0
27 -52 -26 0
-27 52 -26 0
28 51 27 0
-28 -51 27 0
28 -51 -27 0
-28 51 -27 0
29 50 28 0
-29 -50 28 0
29 -50 -28 0
-29 50 -28 0
30 49 29 0
-30 -49 29 0
30 -49 -29 0
-30 49 -29 0
31 48 30 0
-31 -48 30 0
31 -48 -30 0
-31 48 -30 0
32 47 31 0
-32 -47 31 0
32 -47 -31 0
-32 47 -31 0
33 46 32 0
-33 -46 32 0
33 -46 -32 0
-33 46 -32 0
34 45 33 0
-34 -45 33 0
34 -45 -33 0
-34 45 -33 0
35 44 34 0
-35 -44 34 0
35 -44 -34 0
-35 44 -34 0
36 43 35 0
-36 -43 35 0
36 -43 -35 0
-36 43 -35 0
37 42 36 0
-37 -42 36 0
37 -42 -36 0
-37 42 -36 0
38 41 37 0
-38 -41 37 0
38 -41 -37 0
-38 41 -37 0
39 40 -38 0
-39 -40 -38 0
39 -40 38 0
-39 40 38 0

181
tests/dubois/dubois21.cnf Normal file
View file

@ -0,0 +1,181 @@
c FILE: dubois21.cnf
c
c SOURCE: Olivier Dubois (dubois@laforia.ibp.fr)
c
c DESCRIPTION: Instance from generator gensathard.c
c
c NOTE: Not satisfiable
c
c d = 21
c n = 63
c p = 168
c r = 3
p cnf 63 168
41 42 1 0
-41 -42 1 0
41 -42 -1 0
-41 42 -1 0
1 43 2 0
-1 -43 2 0
1 -43 -2 0
-1 43 -2 0
2 44 3 0
-2 -44 3 0
2 -44 -3 0
-2 44 -3 0
3 45 4 0
-3 -45 4 0
3 -45 -4 0
-3 45 -4 0
4 46 5 0
-4 -46 5 0
4 -46 -5 0
-4 46 -5 0
5 47 6 0
-5 -47 6 0
5 -47 -6 0
-5 47 -6 0
6 48 7 0
-6 -48 7 0
6 -48 -7 0
-6 48 -7 0
7 49 8 0
-7 -49 8 0
7 -49 -8 0
-7 49 -8 0
8 50 9 0
-8 -50 9 0
8 -50 -9 0
-8 50 -9 0
9 51 10 0
-9 -51 10 0
9 -51 -10 0
-9 51 -10 0
10 52 11 0
-10 -52 11 0
10 -52 -11 0
-10 52 -11 0
11 53 12 0
-11 -53 12 0
11 -53 -12 0
-11 53 -12 0
12 54 13 0
-12 -54 13 0
12 -54 -13 0
-12 54 -13 0
13 55 14 0
-13 -55 14 0
13 -55 -14 0
-13 55 -14 0
14 56 15 0
-14 -56 15 0
14 -56 -15 0
-14 56 -15 0
15 57 16 0
-15 -57 16 0
15 -57 -16 0
-15 57 -16 0
16 58 17 0
-16 -58 17 0
16 -58 -17 0
-16 58 -17 0
17 59 18 0
-17 -59 18 0
17 -59 -18 0
-17 59 -18 0
18 60 19 0
-18 -60 19 0
18 -60 -19 0
-18 60 -19 0
19 61 20 0
-19 -61 20 0
19 -61 -20 0
-19 61 -20 0
20 62 63 0
-20 -62 63 0
20 -62 -63 0
-20 62 -63 0
21 62 63 0
-21 -62 63 0
21 -62 -63 0
-21 62 -63 0
22 61 21 0
-22 -61 21 0
22 -61 -21 0
-22 61 -21 0
23 60 22 0
-23 -60 22 0
23 -60 -22 0
-23 60 -22 0
24 59 23 0
-24 -59 23 0
24 -59 -23 0
-24 59 -23 0
25 58 24 0
-25 -58 24 0
25 -58 -24 0
-25 58 -24 0
26 57 25 0
-26 -57 25 0
26 -57 -25 0
-26 57 -25 0
27 56 26 0
-27 -56 26 0
27 -56 -26 0
-27 56 -26 0
28 55 27 0
-28 -55 27 0
28 -55 -27 0
-28 55 -27 0
29 54 28 0
-29 -54 28 0
29 -54 -28 0
-29 54 -28 0
30 53 29 0
-30 -53 29 0
30 -53 -29 0
-30 53 -29 0
31 52 30 0
-31 -52 30 0
31 -52 -30 0
-31 52 -30 0
32 51 31 0
-32 -51 31 0
32 -51 -31 0
-32 51 -31 0
33 50 32 0
-33 -50 32 0
33 -50 -32 0
-33 50 -32 0
34 49 33 0
-34 -49 33 0
34 -49 -33 0
-34 49 -33 0
35 48 34 0
-35 -48 34 0
35 -48 -34 0
-35 48 -34 0
36 47 35 0
-36 -47 35 0
36 -47 -35 0
-36 47 -35 0
37 46 36 0
-37 -46 36 0
37 -46 -36 0
-37 46 -36 0
38 45 37 0
-38 -45 37 0
38 -45 -37 0
-38 45 -37 0
39 44 38 0
-39 -44 38 0
39 -44 -38 0
-39 44 -38 0
40 43 39 0
-40 -43 39 0
40 -43 -39 0
-40 43 -39 0
41 42 -40 0
-41 -42 -40 0
41 -42 40 0
-41 42 40 0

189
tests/dubois/dubois22.cnf Normal file
View file

@ -0,0 +1,189 @@
c FILE: dubois22.cnf
c
c SOURCE: Olivier Dubois (dubois@laforia.ibp.fr)
c
c DESCRIPTION: Instance from generator gensathard.c
c
c NOTE: Not satisfiable
c
c d = 22
c n = 66
c p = 176
c r = 3
p cnf 66 176
43 44 1 0
-43 -44 1 0
43 -44 -1 0
-43 44 -1 0
1 45 2 0
-1 -45 2 0
1 -45 -2 0
-1 45 -2 0
2 46 3 0
-2 -46 3 0
2 -46 -3 0
-2 46 -3 0
3 47 4 0
-3 -47 4 0
3 -47 -4 0
-3 47 -4 0
4 48 5 0
-4 -48 5 0
4 -48 -5 0
-4 48 -5 0
5 49 6 0
-5 -49 6 0
5 -49 -6 0
-5 49 -6 0
6 50 7 0
-6 -50 7 0
6 -50 -7 0
-6 50 -7 0
7 51 8 0
-7 -51 8 0
7 -51 -8 0
-7 51 -8 0
8 52 9 0
-8 -52 9 0
8 -52 -9 0
-8 52 -9 0
9 53 10 0
-9 -53 10 0
9 -53 -10 0
-9 53 -10 0
10 54 11 0
-10 -54 11 0
10 -54 -11 0
-10 54 -11 0
11 55 12 0
-11 -55 12 0
11 -55 -12 0
-11 55 -12 0
12 56 13 0
-12 -56 13 0
12 -56 -13 0
-12 56 -13 0
13 57 14 0
-13 -57 14 0
13 -57 -14 0
-13 57 -14 0
14 58 15 0
-14 -58 15 0
14 -58 -15 0
-14 58 -15 0
15 59 16 0
-15 -59 16 0
15 -59 -16 0
-15 59 -16 0
16 60 17 0
-16 -60 17 0
16 -60 -17 0
-16 60 -17 0
17 61 18 0
-17 -61 18 0
17 -61 -18 0
-17 61 -18 0
18 62 19 0
-18 -62 19 0
18 -62 -19 0
-18 62 -19 0
19 63 20 0
-19 -63 20 0
19 -63 -20 0
-19 63 -20 0
20 64 21 0
-20 -64 21 0
20 -64 -21 0
-20 64 -21 0
21 65 66 0
-21 -65 66 0
21 -65 -66 0
-21 65 -66 0
22 65 66 0
-22 -65 66 0
22 -65 -66 0
-22 65 -66 0
23 64 22 0
-23 -64 22 0
23 -64 -22 0
-23 64 -22 0
24 63 23 0
-24 -63 23 0
24 -63 -23 0
-24 63 -23 0
25 62 24 0
-25 -62 24 0
25 -62 -24 0
-25 62 -24 0
26 61 25 0
-26 -61 25 0
26 -61 -25 0
-26 61 -25 0
27 60 26 0
-27 -60 26 0
27 -60 -26 0
-27 60 -26 0
28 59 27 0
-28 -59 27 0
28 -59 -27 0
-28 59 -27 0
29 58 28 0
-29 -58 28 0
29 -58 -28 0
-29 58 -28 0
30 57 29 0
-30 -57 29 0
30 -57 -29 0
-30 57 -29 0
31 56 30 0
-31 -56 30 0
31 -56 -30 0
-31 56 -30 0
32 55 31 0
-32 -55 31 0
32 -55 -31 0
-32 55 -31 0
33 54 32 0
-33 -54 32 0
33 -54 -32 0
-33 54 -32 0
34 53 33 0
-34 -53 33 0
34 -53 -33 0
-34 53 -33 0
35 52 34 0
-35 -52 34 0
35 -52 -34 0
-35 52 -34 0
36 51 35 0
-36 -51 35 0
36 -51 -35 0
-36 51 -35 0
37 50 36 0
-37 -50 36 0
37 -50 -36 0
-37 50 -36 0
38 49 37 0
-38 -49 37 0
38 -49 -37 0
-38 49 -37 0
39 48 38 0
-39 -48 38 0
39 -48 -38 0
-39 48 -38 0
40 47 39 0
-40 -47 39 0
40 -47 -39 0
-40 47 -39 0
41 46 40 0
-41 -46 40 0
41 -46 -40 0
-41 46 -40 0
42 45 41 0
-42 -45 41 0
42 -45 -41 0
-42 45 -41 0
43 44 -42 0
-43 -44 -42 0
43 -44 42 0
-43 44 42 0

197
tests/dubois/dubois23.cnf Normal file
View file

@ -0,0 +1,197 @@
c FILE: dubois23.cnf
c
c SOURCE: Olivier Dubois (dubois@laforia.ibp.fr)
c
c DESCRIPTION: Instance from generator gensathard.c
c
c NOTE: Not satisfiable
c
c d = 23
c n = 69
c p = 184
c r = 3
p cnf 69 184
45 46 1 0
-45 -46 1 0
45 -46 -1 0
-45 46 -1 0
1 47 2 0
-1 -47 2 0
1 -47 -2 0
-1 47 -2 0
2 48 3 0
-2 -48 3 0
2 -48 -3 0
-2 48 -3 0
3 49 4 0
-3 -49 4 0
3 -49 -4 0
-3 49 -4 0
4 50 5 0
-4 -50 5 0
4 -50 -5 0
-4 50 -5 0
5 51 6 0
-5 -51 6 0
5 -51 -6 0
-5 51 -6 0
6 52 7 0
-6 -52 7 0
6 -52 -7 0
-6 52 -7 0
7 53 8 0
-7 -53 8 0
7 -53 -8 0
-7 53 -8 0
8 54 9 0
-8 -54 9 0
8 -54 -9 0
-8 54 -9 0
9 55 10 0
-9 -55 10 0
9 -55 -10 0
-9 55 -10 0
10 56 11 0
-10 -56 11 0
10 -56 -11 0
-10 56 -11 0
11 57 12 0
-11 -57 12 0
11 -57 -12 0
-11 57 -12 0
12 58 13 0
-12 -58 13 0
12 -58 -13 0
-12 58 -13 0
13 59 14 0
-13 -59 14 0
13 -59 -14 0
-13 59 -14 0
14 60 15 0
-14 -60 15 0
14 -60 -15 0
-14 60 -15 0
15 61 16 0
-15 -61 16 0
15 -61 -16 0
-15 61 -16 0
16 62 17 0
-16 -62 17 0
16 -62 -17 0
-16 62 -17 0
17 63 18 0
-17 -63 18 0
17 -63 -18 0
-17 63 -18 0
18 64 19 0
-18 -64 19 0
18 -64 -19 0
-18 64 -19 0
19 65 20 0
-19 -65 20 0
19 -65 -20 0
-19 65 -20 0
20 66 21 0
-20 -66 21 0
20 -66 -21 0
-20 66 -21 0
21 67 22 0
-21 -67 22 0
21 -67 -22 0
-21 67 -22 0
22 68 69 0
-22 -68 69 0
22 -68 -69 0
-22 68 -69 0
23 68 69 0
-23 -68 69 0
23 -68 -69 0
-23 68 -69 0
24 67 23 0
-24 -67 23 0
24 -67 -23 0
-24 67 -23 0
25 66 24 0
-25 -66 24 0
25 -66 -24 0
-25 66 -24 0
26 65 25 0
-26 -65 25 0
26 -65 -25 0
-26 65 -25 0
27 64 26 0
-27 -64 26 0
27 -64 -26 0
-27 64 -26 0
28 63 27 0
-28 -63 27 0
28 -63 -27 0
-28 63 -27 0
29 62 28 0
-29 -62 28 0
29 -62 -28 0
-29 62 -28 0
30 61 29 0
-30 -61 29 0
30 -61 -29 0
-30 61 -29 0
31 60 30 0
-31 -60 30 0
31 -60 -30 0
-31 60 -30 0
32 59 31 0
-32 -59 31 0
32 -59 -31 0
-32 59 -31 0
33 58 32 0
-33 -58 32 0
33 -58 -32 0
-33 58 -32 0
34 57 33 0
-34 -57 33 0
34 -57 -33 0
-34 57 -33 0
35 56 34 0
-35 -56 34 0
35 -56 -34 0
-35 56 -34 0
36 55 35 0
-36 -55 35 0
36 -55 -35 0
-36 55 -35 0
37 54 36 0
-37 -54 36 0
37 -54 -36 0
-37 54 -36 0
38 53 37 0
-38 -53 37 0
38 -53 -37 0
-38 53 -37 0
39 52 38 0
-39 -52 38 0
39 -52 -38 0
-39 52 -38 0
40 51 39 0
-40 -51 39 0
40 -51 -39 0
-40 51 -39 0
41 50 40 0
-41 -50 40 0
41 -50 -40 0
-41 50 -40 0
42 49 41 0
-42 -49 41 0
42 -49 -41 0
-42 49 -41 0
43 48 42 0
-43 -48 42 0
43 -48 -42 0
-43 48 -42 0
44 47 43 0
-44 -47 43 0
44 -47 -43 0
-44 47 -43 0
45 46 -44 0
-45 -46 -44 0
45 -46 44 0
-45 46 44 0

Some files were not shown because too many files have changed in this diff Show more