mirror of
https://github.com/c-cube/sidekick.git
synced 2026-05-05 08:54:24 -04:00
Compare commits
2 commits
83cef9e2b9
...
d191317108
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
d191317108 | ||
|
|
3d9b32ad38 |
7 changed files with 24 additions and 15 deletions
6
Makefile
6
Makefile
|
|
@ -27,6 +27,12 @@ clean:
|
|||
test:
|
||||
@dune runtest $(OPTS) --force --no-buffer
|
||||
|
||||
format:
|
||||
@dune build @fmt --auto-promote
|
||||
|
||||
format-check:
|
||||
@dune build @fmt --quiet
|
||||
|
||||
test-promote:
|
||||
@dune runtest $(OPTS) --force --no-buffer --auto-promote
|
||||
|
||||
|
|
|
|||
|
|
@ -124,8 +124,8 @@ module Step = struct
|
|||
| [] -> []
|
||||
| vs ->
|
||||
let gen =
|
||||
let+ x = oneofl vs
|
||||
and+ kind = oneofl [ `Leq; `Lt; `Geq; `Gt ]
|
||||
let+ x = oneof_list vs
|
||||
and+ kind = oneof_list [ `Leq; `Lt; `Geq; `Gt ]
|
||||
and+ n = rand_q.QC.gen in
|
||||
( vars,
|
||||
match kind with
|
||||
|
|
@ -145,11 +145,11 @@ module Step = struct
|
|||
(if List.length vars > 2 then (
|
||||
let v = List.length vars in
|
||||
let gen =
|
||||
let* vars' = G.shuffle_l vars in
|
||||
let* vars' = shuffle_list vars in
|
||||
let* n = 1 -- min 12 (List.length vars') in
|
||||
let vars' = CCList.take n vars' in
|
||||
assert (List.length vars' = n);
|
||||
let* coeffs = list_repeat n rand_q.gen in
|
||||
let* coeffs = list_size (return n) rand_q.gen in
|
||||
let le = List.combine coeffs vars' in
|
||||
return (v :: vars, S_define (v, le))
|
||||
in
|
||||
|
|
|
|||
|
|
@ -2,11 +2,15 @@
|
|||
(name sidekick_bin_lib)
|
||||
(public_name sidekick-bin.lib)
|
||||
(synopsis "Utils for the sidekick binaries")
|
||||
(libraries containers sidekick.util
|
||||
(select trace_setup.ml from
|
||||
(trace-fuchsia -> trace_setup.fuchsia.ml)
|
||||
(trace-tef -> trace_setup.tef.ml)
|
||||
(-> trace_setup.dummy.ml)))
|
||||
(libraries
|
||||
containers
|
||||
sidekick.util
|
||||
(select
|
||||
trace_setup.ml
|
||||
from
|
||||
(trace-fuchsia -> trace_setup.fuchsia.ml)
|
||||
(trace-tef -> trace_setup.tef.ml)
|
||||
(-> trace_setup.dummy.ml)))
|
||||
(flags :standard -warn-error -a+8 -open Sidekick_util))
|
||||
|
||||
(ocamllex
|
||||
|
|
|
|||
|
|
@ -2,6 +2,5 @@
|
|||
(name main)
|
||||
(public_name sidekick-checker)
|
||||
(package sidekick-bin)
|
||||
(libraries containers sidekick-bin.lib sidekick.util
|
||||
sidekick.drup)
|
||||
(libraries containers sidekick-bin.lib sidekick.util sidekick.drup)
|
||||
(flags :standard -warn-error -a+8 -open Sidekick_util))
|
||||
|
|
|
|||
|
|
@ -7,8 +7,8 @@
|
|||
(modules main pure_sat_solver)
|
||||
(modes native)
|
||||
(libraries containers iter result sidekick.sat sidekick.core sidekick-base
|
||||
sidekick.smt-solver sidekick-base.smtlib sidekick.drup
|
||||
sidekick.memtrace sidekick-bin.lib)
|
||||
sidekick.smt-solver sidekick-base.smtlib sidekick.drup sidekick.memtrace
|
||||
sidekick-bin.lib)
|
||||
(flags :standard -safe-string -color always -open Sidekick_util))
|
||||
|
||||
(executable
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ type state = {
|
|||
p_reader: Proof.Trace_reader.t;
|
||||
}
|
||||
|
||||
let show_sat (self : state) ~tag v : unit =
|
||||
let show_sat (_self : state) ~tag v : unit =
|
||||
match tag with
|
||||
| "AssCSat" ->
|
||||
(match
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ module Atom = Store.Atom
|
|||
module Var = Store.Var
|
||||
module Clause = Store.Clause
|
||||
|
||||
module H = Heap.Make [@specialise] (struct
|
||||
module H = Heap.Make (struct
|
||||
type store = Store.t
|
||||
type t = var
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue