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

Merge branch 'wip-lra-simplex'

Browse source
This commit is contained in:
Simon Cruanes 2021-02-22 17:13:39 -05:00
commit 04615e4e3d
57 changed files with 15864 additions and 707 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6,15 +6,24 @@ jobs:
runs-on: ${{ matrix.operating-system }}
strategy:
matrix:
operating-system: [macos-latest, ubuntu-latest, windows-latest]
ocaml-version: [ '4.05.0' ]
#operating-system: [macos-latest, ubuntu-latest, windows-latest]
operating-system: [ubuntu-latest]
ocaml-version: [ '4.08.0' ]
steps:
- uses: actions/checkout@master
- uses: avsm/setup-ocaml@master
with:
ocaml-version: ${{ matrix.ocaml-version }}
#- name: cache opam
# id: cache-opam
# uses: actions/cache@v2
# with:
# path: _opam
# key: opam-${{matrix.operating-system}}-${{matrix.ocaml-version}}
- run: opam pin -n .
- run: opam depext -yt sidekick-bin
#if: steps.cache-opam.outputs.cache-hit != 'true'
- run: opam install -t . --deps-only
#if: steps.cache-opam.outputs.cache-hit != 'true'
- run: opam exec -- dune build
- run: opam exec -- dune runtest

6
Makefile
View file

@ -41,6 +41,12 @@ $(TESTTOOL)-smt-QF_UF: snapshots
$(TESTTOOL)-smt-QF_DT: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_DT-$(DATE).csv --task sidekick-smt-nodir tests/QF_DT
$(TESTTOOL)-smt-QF_LRA: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_LRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_LRA
$(TESTTOOL)-smt-QF_UFLRA: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_UFLRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_UFLRA
install: build-install
@dune install

1
dune Normal file
View file

@ -0,0 +1 @@
(data_only_dirs tests)

3
dune-project
View file

@ -1,3 +1,2 @@
(lang dune 1.1)
(lang dune 1.6)
(using menhir 1.0)
(using fmt 1.1)

3
sidekick-arith.opam
View file

@ -15,8 +15,9 @@ depends: [
"containers" { >= "3.0" & < "4.0" }
"iter" { >= "1.0" & < "2.0" }
"ocaml" { >= "4.03" }
"zarith"
"zarith" { >= "1.8" } # for infix ops
"alcotest" {with-test}
"qcheck" {with-test & >= "0.16" }
]
tags: [ "sat" "smt" ]
homepage: "https://github.com/c-cube/sidekick"

4
sidekick-bin.opam
View file

@ -15,10 +15,10 @@ depends: [
"containers" { >= "3.0" & < "4.0" }
"iter"
"zarith"
"smtlib-utils" { >= "0.1" & < "0.2" }
"smtlib-utils" { >= "0.1" & < "0.3" }
"sidekick" { = version }
"menhir"
"msat" { >= "0.8" < "0.9" }
"mtime"
"ocaml" { >= "4.03" }
]
tags: [ "sat" "smt" ]

5
sidekick.opam
View file

@ -14,10 +14,13 @@ depends: [
"dune" { >= "1.1" }
"containers" { >= "3.0" & < "4.0" }
"iter" { >= "1.0" & < "2.0" }
"msat" { >= "0.8.3" < "0.9" }
"msat" { >= "0.9" < "0.10" }
"ocaml" { >= "4.03" }
"alcotest" {with-test}
]
depopts: [
"mtime" # for profiling stuff
]
tags: [ "sat" "smt" ]
homepage: "https://github.com/c-cube/sidekick"
dev-repo: "git+https://github.com/c-cube/sidekick.git"

34
src/arith/base-term/Base_types.ml
View file

@ -4,7 +4,7 @@ module Fmt = CCFormat
module CC_view = Sidekick_core.CC_view
type lra_pred = Sidekick_arith_lra.FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type lra_op = Sidekick_arith_lra.op = Plus | Minus
type 'a lra_view = 'a Sidekick_arith_lra.lra_view =
@ -12,6 +12,8 @@ type 'a lra_view = 'a Sidekick_arith_lra.lra_view =
| LRA_op of lra_op * 'a * 'a
| LRA_mult of Q.t * 'a
| LRA_const of Q.t
| LRA_simplex_var of 'a
| LRA_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * Q.t
| LRA_other of 'a
(* main term cell. *)
@ -209,7 +211,7 @@ let string_of_lra_pred = function
| Leq -> "<="
| Neq -> "!="
| Eq -> "="
| Gt-> ">"
| Gt -> ">"
| Geq -> ">="
let pp_pred out p = Fmt.string out (string_of_lra_pred p)
@ -238,6 +240,10 @@ let pp_term_view_gen ~pp_id ~pp_t out = function
| LRA_mult (n, x) ->
Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
| LRA_const q -> Q.pp_print out q
| LRA_simplex_var v -> pp_t out v
| LRA_simplex_pred (v, op, q) ->
Fmt.fprintf out "(@[%a@ %s %a@])"
pp_t v (Sidekick_arith_lra.S_op.to_string op) Q.pp_print q
| LRA_other x -> pp_t out x
end
@ -593,6 +599,8 @@ end = struct
let sub_hash = A.hash
let sub_eq = A.equal
let hash_q q = Hash.string (Q.to_string q)
let hash (t:A.t view) : int = match t with
| Bool b -> Hash.bool b
| App_fun (f,l) ->
@ -607,8 +615,11 @@ end = struct
| LRA_op (p, a, b) ->
Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
| LRA_mult (n, x) ->
Hash.combine3 83 (Hash.string @@ Q.to_string n) (sub_hash x)
| LRA_const q -> Hash.combine2 84 (Hash.string @@ Q.to_string q)
Hash.combine3 83 (hash_q n) (sub_hash x)
| LRA_const q -> Hash.combine2 84 (hash_q q)
| LRA_simplex_var v -> Hash.combine2 99 (sub_hash v)
| LRA_simplex_pred (v,op,q) ->
Hash.combine4 120 (sub_hash v) (Hash.poly op) (hash_q q)
| LRA_other x -> sub_hash x
end
@ -630,8 +641,11 @@ end = struct
| LRA_const a1, LRA_const a2 -> Q.equal a1 a2
| LRA_mult (n1,x1), LRA_mult (n2,x2) -> Q.equal n1 n2 && sub_eq x1 x2
| LRA_other x1, LRA_other x2 -> sub_eq x1 x2
| (LRA_pred _ | LRA_op _ | LRA_const _
| LRA_mult _ | LRA_other _), _ -> false
| LRA_simplex_var v1, LRA_simplex_var v2 -> sub_eq v1 v2
| LRA_simplex_pred (v1,op1,q1), LRA_simplex_pred (v2,op2,q2) ->
sub_eq v1 v2 && (op1==op2) && Q.equal q1 q2
| (LRA_pred _ | LRA_op _ | LRA_const _ | LRA_simplex_var _
| LRA_mult _ | LRA_other _ | LRA_simplex_pred _), _ -> false
end
| (Bool _ | App_fun _ | Eq _ | Not _ | Ite _ | LRA _), _
-> false
@ -700,8 +714,8 @@ end = struct
end
| LRA l ->
begin match l with
| LRA_pred _ -> Ty.bool
| LRA_op _ | LRA_const _ | LRA_mult _ -> Ty.real
| LRA_pred _ | LRA_simplex_pred _ -> Ty.bool
| LRA_op _ | LRA_const _ | LRA_mult _ | LRA_simplex_var _ -> Ty.real
| LRA_other x -> x.term_ty
end
@ -716,6 +730,8 @@ end = struct
begin match l with
| LRA_pred (_, a, b)|LRA_op (_, a, b) -> f a; f b
| LRA_mult (_,x) | LRA_other x -> f x
| LRA_simplex_var x -> f x
| LRA_simplex_pred (x,_,_) -> f x
| LRA_const _ -> ()
end
@ -914,6 +930,8 @@ end = struct
| Eq (a,b) -> C.Eq (a, b)
| Not u -> C.Not u
| Ite (a,b,c) -> C.If (a,b,c)
| LRA (LRA_pred (Eq, a, b)) ->
C.Eq (a,b) (* need congruence closure on this one, for theory combination *)
| LRA _ -> C.Opaque t (* no congruence here *)
module As_key = struct

280
src/arith/lra/Sidekick_arith_lra.ml
View file

@ -1,280 +0,0 @@
(** {1 Linear Rational Arithmetic} *)
(* Reference:
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LRA *)
open Sidekick_core
module FM = Fourier_motzkin
type pred = FM.Pred.t = Lt | Leq | Geq | Gt | Neq | Eq
type op = Plus | Minus
type 'a lra_view =
| LRA_pred of pred * 'a * 'a
| LRA_op of op * 'a * 'a
| LRA_mult of Q.t * 'a
| LRA_const of Q.t
| LRA_other of 'a
let map_view f (l:_ lra_view) : _ lra_view =
begin match l with
| LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
| LRA_op (p, a, b) -> LRA_op (p, f a, f b)
| LRA_mult (n,a) -> LRA_mult (n, f a)
| LRA_const q -> LRA_const q
| LRA_other x -> LRA_other (f x)
end
module type ARG = sig
module S : Sidekick_core.SOLVER
type term = S.T.Term.t
val view_as_lra : term -> term lra_view
(** Project the term into the theory view *)
val mk_lra : S.T.Term.state -> term lra_view -> term
(** Make a term from the given theory view *)
module Gensym : sig
type t
val create : S.T.Term.state -> t
val fresh_term : t -> pre:string -> S.T.Ty.t -> term
(** Make a fresh term of the given type *)
end
end
module type S = sig
module A : ARG
type state
val create : A.S.T.Term.state -> state
val theory : A.S.theory
end
module Make(A : ARG) : S with module A = A = struct
module A = A
module Ty = A.S.T.Ty
module T = A.S.T.Term
module Lit = A.S.Solver_internal.Lit
module SI = A.S.Solver_internal
(* the fourier motzkin module *)
module FM_A = FM.Make(struct
module T = T
type tag = Lit.t
end)
(* linear expressions *)
module LE = FM_A.LE
type state = {
tst: T.state;
simps: T.t T.Tbl.t; (* cache *)
gensym: A.Gensym.t;
neq_encoded: unit T.Tbl.t;
(* if [a != b] asserted and not in this table, add clause [a = b \/ a<b \/ a>b] *)
mutable t_defs: (T.t * LE.t) list; (* term definitions *)
pred_defs: (pred * LE.t * LE.t) T.Tbl.t; (* predicate definitions *)
}
let create tst : state =
{ tst;
simps=T.Tbl.create 128;
gensym=A.Gensym.create tst;
neq_encoded=T.Tbl.create 16;
t_defs=[];
pred_defs=T.Tbl.create 16;
}
(* FIXME
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
let tst = self.tst in
match A.view_as_bool t with
| B_bool _ -> None
| B_not u when is_true u -> Some (T.bool tst false)
| B_not u when is_false u -> Some (T.bool tst true)
| B_not _ -> None
| B_opaque_bool _ -> None
| B_and a ->
if IArray.exists is_false a then Some (T.bool tst false)
else if IArray.for_all is_true a then Some (T.bool tst true)
else None
| B_or a ->
if IArray.exists is_true a then Some (T.bool tst true)
else if IArray.for_all is_false a then Some (T.bool tst false)
else None
| B_imply (args, u) ->
(* turn into a disjunction *)
let u =
or_a tst @@
IArray.append (IArray.map (not_ tst) args) (IArray.singleton u)
in
Some u
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a = SI.Simplify.normalize simp a in
begin match A.view_as_bool a with
| B_bool true -> Some b
| B_bool false -> Some c
| _ ->
None
end
| B_equiv (a,b) when is_true a -> Some b
| B_equiv (a,b) when is_false a -> Some (not_ tst b)
| B_equiv (a,b) when is_true b -> Some a
| B_equiv (a,b) when is_false b -> Some (not_ tst a)
| B_equiv _ -> None
| B_eq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_eq _ -> None
| B_atom _ -> None
*)
let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
let fresh_lit (self:state) ~mk_lit ~pre : Lit.t =
let t = fresh_term ~pre self Ty.bool in
mk_lit t
(* turn the term into a linear expression *)
let rec as_linexp (t:T.t) : LE.t =
let open LE.Infix in
match A.view_as_lra t with
| LRA_other _ -> LE.var t
| LRA_pred _ ->
Error.errorf "type error: in linexp, LRA predicate %a" T.pp t
| LRA_op (op, t1, t2) ->
let t1 = as_linexp t1 in
let t2 = as_linexp t2 in
begin match op with
| Plus -> t1 + t2
| Minus -> t1 - t2
end
| LRA_mult (n, x) ->
let t = as_linexp x in
LE.( n * t )
| LRA_const q -> LE.const q
(* TODO: keep the linexps until they're asserted;
TODO: but use simplification in preprocess
*)
(* preprocess linear expressions away *)
let preproc_lra self si ~mk_lit:_ ~add_clause:_ (t:T.t) : T.t option =
Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
let _tst = SI.tst si in
match A.view_as_lra t with
| LRA_pred (pred, t1, t2) ->
(* TODO: map preproc on [l1] and [l2] *)
let l1 = as_linexp t1 in
let l2 = as_linexp t2 in
let proxy = fresh_term self ~pre:"_pred_lra_" Ty.bool in
T.Tbl.add self.pred_defs proxy (pred, l1, l2);
Log.debugf 5 (fun k->k"lra.preprocess.step %a :into %a" T.pp t T.pp proxy);
Some proxy
| LRA_op _ | LRA_mult _ ->
let le = as_linexp t in
(* TODO: map preproc on [le] *)
let proxy = fresh_term self ~pre:"_e_lra_" (T.ty t) in
self.t_defs <- (proxy, le) :: self.t_defs;
Log.debugf 5 (fun k->k"lra.preprocess.step %a :into %a" T.pp t T.pp proxy);
Some proxy
| LRA_const _ | LRA_other _ -> None
(* partial check: just ensure [a != b] triggers the clause
[a=b \/ a<b \/ a>b] *)
let partial_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
let tst = self.tst in
begin
trail
|> Iter.filter (fun lit -> not (Lit.sign lit))
|> Iter.filter_map
(fun lit ->
let t = Lit.term lit in
match A.view_as_lra t with
| LRA_pred (Eq, a, b) when not (T.Tbl.mem self.neq_encoded t) ->
Some (lit, a,b)
| _ -> None)
|> Iter.iter
(fun (lit,a,b) ->
let c = [
Lit.abs lit;
SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, a, b)));
SI.mk_lit si acts (A.mk_lra tst (LRA_pred (Lt, b, a)));
] in
SI.add_clause_permanent si acts c;
T.Tbl.add self.neq_encoded (Lit.term lit) ();
)
end
let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit =
Log.debug 5 "(th-lra.final-check)";
let fm = FM_A.create() in
(* first, add definitions *)
begin
List.iter
(fun (t,le) ->
let open LE.Infix in
let le = le - LE.var t in
let c = FM_A.Constr.mk ?tag:None Eq (LE.var t) le in
FM_A.assert_c fm c)
self.t_defs
end;
(* add trail *)
begin
trail
|> Iter.iter
(fun lit ->
let sign = Lit.sign lit in
let t = Lit.term lit in
begin match T.Tbl.find self.pred_defs t with
| exception Not_found -> ()
| (pred, a, b) ->
let pred = if sign then pred else FM.Pred.neg pred in
if pred = Neq then (
Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
) else (
let c = FM_A.Constr.mk ~tag:lit pred a b in
FM_A.assert_c fm c;
)
end)
end;
Log.debug 5 "lra: call arith solver";
begin match FM_A.solve fm with
| FM_A.Sat ->
Log.debug 5 "lra: solver returns SAT";
() (* TODO: get a model + model combination *)
| FM_A.Unsat lits ->
(* we tagged assertions with their lit, so the certificate being an
unsat core translates directly into a conflict clause *)
Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
(Fmt.Dump.list Lit.pp) lits);
let confl = List.rev_map Lit.neg lits in
(* TODO: produce and store a proper LRA resolution proof *)
SI.raise_conflict si acts confl SI.P.default
end;
()
let create_and_setup si =
Log.debug 2 "(th-lra.setup)";
let st = create (SI.tst si) in
(* TODO SI.add_simplifier si (simplify st); *)
SI.add_preprocess si (preproc_lra st);
SI.on_partial_check si (partial_check_ st);
SI.on_final_check si (final_check_ st);
(* SI.add_preprocess si (cnf st); *)
(* TODO: theory combination *)
st
let theory =
A.S.mk_theory
~name:"th-lra"
~create_and_setup
()
end

1
src/arith/lra/dune
View file

@ -2,6 +2,5 @@
(library
(name sidekick_arith_lra)
(public_name sidekick-arith.lra)
(optional) ; only if deps present
(flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)
(libraries containers sidekick.core zarith))

378
src/arith/lra/fourier_motzkin.ml
View file

@ -1,378 +0,0 @@
module type ARG = sig
(** terms *)
module T : sig
type t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val pp : t Fmt.printer
end
type tag
end
module Pred : sig
type t = Lt | Leq | Geq | Gt | Neq | Eq
val neg : t -> t
val pp : t Fmt.printer
val to_string : t -> string
end = struct
type t = Lt | Leq | Geq | Gt | Neq | Eq
let to_string = function
| Lt -> "<"
| Leq -> "<="
| Eq -> "="
| Neq -> "!="
| Gt -> ">"
| Geq -> ">="
let neg = function
| Leq -> Gt
| Lt -> Geq
| Eq -> Neq
| Neq -> Eq
| Geq -> Lt
| Gt -> Leq
let pp out p = Fmt.string out (to_string p)
end
module type S = sig
module A : ARG
type t
type term = A.T.t
module LE : sig
type t
val const : Q.t -> t
val zero : t
val var : term -> t
val neg : t -> t
val find_exn : term -> t -> Q.t
val find : term -> t -> Q.t option
module Infix : sig
val (+) : t -> t -> t
val (-) : t -> t -> t
val ( * ) : Q.t -> t -> t
end
include module type of Infix
val pp : t Fmt.printer
end
(** {3 Arithmetic constraint} *)
module Constr : sig
type t
val pp : t Fmt.printer
val mk : ?tag:A.tag -> Pred.t -> LE.t -> LE.t -> t
val is_absurd : t -> bool
end
val create : unit -> t
val assert_c : t -> Constr.t -> unit
type res =
| Sat
| Unsat of A.tag list
val solve : t -> res
end
module Make(A : ARG)
: S with module A = A
= struct
module A = A
module T = A.T
module T_set = CCSet.Make(A.T)
module T_map = CCMap.Make(A.T)
type term = A.T.t
module LE = struct
module M = T_map
type t = {
le: Q.t M.t;
const: Q.t;
}
let const x : t = {const=x; le=M.empty}
let zero = const Q.zero
let var x : t = {const=Q.zero; le=M.singleton x Q.one}
let find_exn v le = M.find v le.le
let find v le = M.get v le.le
let remove v le : t = {le with le=M.remove v le.le}
let neg a : t =
{const=Q.neg a.const;
le=M.map Q.neg a.le; }
let (+) a b : t =
{const = Q.(a.const + b.const);
le=M.merge_safe a.le b.le
~f:(fun _ -> function
| `Left x | `Right x -> Some x
| `Both (x,y) ->
let z = Q.(x + y) in
if Q.sign z = 0 then None else Some z)
}
let (-) a b : t =
{const = Q.(a.const - b.const);
le=M.merge_safe a.le b.le
~f:(fun _ -> function
| `Left x -> Some x
| `Right x -> Some (Q.neg x)
| `Both (x,y) ->
let z = Q.(x - y) in
if Q.sign z = 0 then None else Some z)
}
let ( * ) x a : t =
if Q.sign x = 0 then const Q.zero
else (
{const=Q.( a.const * x );
le=M.map (fun y -> Q.(x * y)) a.le
}
)
let max_var self : T.t option =
M.keys self.le |> Iter.max ~lt:(fun a b -> T.compare a b < 0)
(* ensure coeff of [v] is 1 *)
let normalize_wrt (v:T.t) le : t =
let q = find_exn v le in
Q.inv q * le
module Infix = struct
let (+) = (+)
let (-) = (-)
let ( * ) = ( * )
end
let vars self = T_map.keys self.le
let pp out (self:t) : unit =
let pp_pair out (e,q) =
if Q.equal Q.one q then T.pp out e
else Fmt.fprintf out "%a * %a" Q.pp_print q T.pp e
in
Fmt.fprintf out "(@[%a@ + %a@])"
Q.pp_print self.const (Util.pp_iter ~sep:" + " pp_pair) (M.to_iter self.le)
end
module Constr = struct
type t = {
pred: Pred.t;
le: LE.t;
tag: A.tag list;
}
let pp out (c:t) : unit =
Fmt.fprintf out "(@[constr@ :le %a@ :pred %s 0@])"
LE.pp c.le (Pred.to_string c.pred)
let mk_ ~tag pred le : t = {pred; tag; le; }
let mk ?tag pred l1 l2 : t =
mk_ ~tag:(CCOpt.to_list tag) pred LE.(l1 - l2)
let is_absurd (self:t) : bool =
T_map.is_empty self.le.le &&
let c = self.le.const in
begin match self.pred with
| Leq -> Q.compare c Q.zero > 0
| Lt -> Q.compare c Q.zero >= 0
| Geq -> Q.compare c Q.zero < 0
| Gt -> Q.compare c Q.zero <= 0
| Eq -> Q.compare c Q.zero <> 0
| Neq -> Q.compare c Q.zero = 0
end
let is_trivial (self:t) : bool =
T_map.is_empty self.le.le && not (is_absurd self)
(* nornalize and return maximum variable *)
let normalize (self:t) : t =
match self.pred with
| Geq -> mk_ ~tag:self.tag Lt (LE.neg self.le)
| Gt -> mk_ ~tag:self.tag Leq (LE.neg self.le)
| _ -> self
let find_max (self:t) : T.t option * bool =
match LE.max_var self.le with
| None -> None, true
| Some t -> Some t, Q.sign (T_map.find t self.le.le) > 0
end
(** constraints for a variable (where the variable is maximal) *)
type c_for_var = {
occ_pos: Constr.t list;
occ_eq: Constr.t list;
occ_neg: Constr.t list;
}
type system = {
empties: Constr.t list; (* no variables, check first *)
idx: c_for_var T_map.t;
(* map [t] to [c1,c2] where [c1] are normalized constraints whose
maximum term is [t], with positive sign for [c1]
and negative for [c2] respectively. *)
}
type t = {
mutable cs: Constr.t list;
mutable sys: system;
}
let empty_sys : system = {empties=[]; idx=T_map.empty}
let empty_c_for_v : c_for_var =
{ occ_pos=[]; occ_neg=[]; occ_eq=[] }
let create () : t = {
cs=[];
sys=empty_sys;
}
let add_sys (sys:system) (c:Constr.t) : system =
assert (match c.pred with Eq|Leq|Lt -> true | _ -> false);
if Constr.is_trivial c then (
Log.debugf 10 (fun k->k"(@[FM.drop-trivial@ %a@])" Constr.pp c);
sys
) else (
match Constr.find_max c with
| None, _ -> {sys with empties=c :: sys.empties}
| Some v, occ_pos ->
Log.debugf 30 (fun k->k "(@[FM.add-sys %a@ :max_var %a@ :occurs-pos %B@])"
Constr.pp c T.pp v occ_pos);
let cs = T_map.get_or ~default:empty_c_for_v v sys.idx in
let cs =
if c.pred = Eq then {cs with occ_eq = c :: cs.occ_eq}
else if occ_pos then {cs with occ_pos = c :: cs.occ_pos}
else {cs with occ_neg = c :: cs.occ_neg }
in
let idx = T_map.add v cs sys.idx in
{sys with idx}
)
let assert_c (self:t) c0 : unit =
Log.debugf 10 (fun k->k "(@[FM.add-constr@ %a@])" Constr.pp c0);
let c = Constr.normalize c0 in
if c.pred <> c0.pred then (
Log.debugf 30 (fun k->k "(@[FM.normalized %a@])" Constr.pp c);
);
assert (match c.pred with Eq | Leq | Lt -> true | _ -> false);
self.cs <- c :: self.cs;
self.sys <- add_sys self.sys c;
()
let pp_system out (self:system) : unit =
let pp_idxkv out (t,{occ_eq; occ_pos; occ_neg}) =
Fmt.fprintf out "(@[for-var %a@ :occ-eq %a@ :occ-pos %a@ :occ-neg %a@])"
T.pp t
(Fmt.Dump.list Constr.pp) occ_eq
(Fmt.Dump.list Constr.pp) occ_pos
(Fmt.Dump.list Constr.pp) occ_neg
in
Fmt.fprintf out "(@[:empties %a@ :idx (@[%a@])@])"
(Fmt.Dump.list Constr.pp) self.empties
(Util.pp_iter pp_idxkv) (T_map.to_iter self.idx)
(* TODO: be able to provide a model for SAT *)
type res =
| Sat
| Unsat of A.tag list
(* replace [x] with [by] inside [le] *)
let subst_le (x:T.t) (le:LE.t) ~by:(le1:LE.t) : LE.t =
let q = LE.find_exn x le in
let le = LE.remove x le in
LE.( le + q * le1 )
let subst_constr x c ~by : Constr.t =
let c = {c with Constr.le=subst_le x ~by c.Constr.le} in
Constr.normalize c
let rec solve_ (self:system) : res =
Log.debugf 50
(fun k->k "(@[FM.solve-rec@ :sys %a@])" pp_system self);
begin match List.find Constr.is_absurd self.empties with
| c ->
Log.debugf 10 (fun k->k"(@[FM.unsat@ :by-absurd %a@])" Constr.pp c);
Unsat c.tag
| exception Not_found ->
(* need to process biggest variable first *)
match T_map.max_binding_opt self.idx with
| None -> Sat
| Some (v, {occ_eq=c0 :: ceq'; occ_pos; occ_neg}) ->
(* remove [v] from [idx] *)
let sys = {self with idx=T_map.remove v self.idx} in
(* substitute using [c0] in the other constraints containing [v] *)
assert (c0.pred = Eq);
let c0 = LE.normalize_wrt v c0.le in
(* build [v = rhs] *)
let rhs = LE.neg @@ LE.remove v c0 in
Log.debugf 50
(fun k->k "(@[FM.subst-from-eq@ :v %a@ :rhs %a@])"
T.pp v LE.pp rhs);
(* perform substitution *)
let new_sys =
[Iter.of_list ceq'; Iter.of_list occ_pos; Iter.of_list occ_neg]
|> Iter.of_list
|> Iter.flatten
|> Iter.map (subst_constr v ~by:rhs)
|> Iter.fold add_sys sys
in
solve_ new_sys
| Some (v, {occ_eq=[]; occ_pos=l1; occ_neg=l2}) ->
Log.debugf 10
(fun k->k "(@[@{<yellow>FM.pivot@}@ :v %a@ :lpos %a@ :lneg %a@])"
T.pp v (Fmt.Dump.list Constr.pp) l1
(Fmt.Dump.list Constr.pp) l2);
(* remove [v] *)
let sys = {self with idx=T_map.remove v self.idx} in
let new_sys =
Iter.product (Iter.of_list l1) (Iter.of_list l2)
|> Iter.map
(fun (c1,c2) ->
let q1 = LE.find_exn v c1.Constr.le in
let le = LE.( c1.Constr.le + (Q.inv q1 * c2.Constr.le) ) in
let pred = match c1.Constr.pred, c2.Constr.pred with
| Eq, Eq -> Pred.Eq
| Lt, _ | _, Lt -> Pred.Lt
| Leq, _ | _, Leq -> Pred.Leq
| _ -> assert false
in
let c = Constr.mk_ ~tag:(c1.tag @ c2.tag) pred le in
Log.debugf 50 (fun k->k "(@[FM.resolve@ %a@ %a@ :yields@ %a@])"
Constr.pp c1 Constr.pp c2 Constr.pp c);
c)
|> Iter.fold add_sys sys
in
solve_ new_sys
end
let solve (self:t) : res =
Log.debugf 5
(fun k->k"(@[<hv>@{<Green>FM.solve@}@ %a@])" (Util.pp_list Constr.pp) self.cs);
solve_ self.sys
end

196
src/arith/lra/linear_expr.ml Normal file
View file

@ -0,0 +1,196 @@
(*
copyright (c) 2014-2018, Guillaume Bury, Simon Cruanes
*)
module type COEFF = Linear_expr_intf.COEFF
module type VAR = Linear_expr_intf.VAR
module type S = Linear_expr_intf.S
type bool_op = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq
module Make(C : COEFF)(Var : VAR) = struct
module C = C
module Var_map = CCMap.Make(Var)
module Var = Var
type var = Var.t
type subst = C.t Var_map.t
(** Linear combination of variables. *)
module Comb = struct
(* A map from variables to their coefficient in the linear combination. *)
type t = C.t Var_map.t
let compare = Var_map.compare C.compare
let empty = Var_map.empty
let is_empty = Var_map.is_empty
let monomial c x =
if C.equal c C.zero then empty else Var_map.singleton x c
let monomial1 x = Var_map.singleton x C.one
let as_singleton m =
if is_empty m then None
else (
let x, c = Var_map.choose m in
if is_empty (Var_map.remove x m) then Some (c, x) else None
)
let add c x e =
let c' = Var_map.get_or ~default:C.zero x e in
let c' = C.(c + c') in
if C.equal C.zero c' then Var_map.remove x e else Var_map.add x c' e
let[@inline] map2 ~fr ~f a b =
Var_map.merge_safe
~f:(fun _ rhs -> match rhs with
| `Left x -> Some x
| `Right x -> Some (fr x)
| `Both (x,y) -> f x y)
a b
let[@inline] some_if_nzero x =
if C.equal C.zero x then None else Some x
let filter_map ~f m =
Var_map.fold
(fun x y m -> match f y with
| None -> m
| Some z -> Var_map.add x z m)
m Var_map.empty
module Infix = struct
let (+) = map2 ~fr:(fun x->x) ~f:(fun a b -> some_if_nzero C.(a + b))
let (-) = map2 ~fr:C.neg ~f:(fun a b -> some_if_nzero C.(a - b))
let ( * ) q = filter_map ~f:(fun x -> some_if_nzero C.(x * q))
end
include Infix
let iter = Var_map.iter
let of_list l = List.fold_left (fun e (c,x) -> add c x e) empty l
let to_list e = Var_map.bindings e |> List.rev_map CCPair.swap
let to_map e = e
let of_map e = Var_map.filter (fun _ c -> not (C.equal C.zero c)) e
let pp_pair =
Fmt.(pair ~sep:(return "@ * ") C.pp Var.pp)
let pp out (e:t) =
Fmt.(hovbox @@ list ~sep:(return "@ + ") pp_pair) out (to_list e)
let eval (subst : subst) (e:t) : C.t =
Var_map.fold
(fun x c acc -> C.(acc + c * (Var_map.find x subst)))
e C.zero
end
(** A linear arithmetic expression, composed of a combination of variables
with coefficients and a constant offset. *)
module Expr = struct
type t = {
const : C.t;
comb : Comb.t
}
let[@inline] const e = e.const
let[@inline] comb e = e.comb
let compare e e' =
CCOrd.(C.compare e.const e'.const
<?> (Comb.compare, e.comb, e'.comb))
let pp fmt e =
Format.fprintf fmt "@[<hov>%a@ + %a" Comb.pp e.comb C.pp e.const
let[@inline] make comb const : t = { comb; const; }
let of_const = make Comb.empty
let of_comb c = make c C.zero
let monomial c x = of_comb (Comb.monomial c x)
let monomial1 x = of_comb (Comb.monomial1 x)
let of_list c l = make (Comb.of_list l) c
let zero = of_const C.zero
let is_zero e = C.equal C.zero e.const && Comb.is_empty e.comb
let map2 f g e e' = make (f e.comb e'.comb) (g e.const e'.const)
module Infix = struct
let (+) = map2 Comb.(+) C.(+)
let (-) = map2 Comb.(-) C.(-)
let ( * ) c e =
if C.equal C.zero c
then zero
else make Comb.(c * e.comb) C.(c * e.const)
end
include Infix
let eval subst e = C.(e.const + Comb.eval subst e.comb)
end
module Constr = struct
type op = bool_op = Leq | Geq | Lt | Gt | Eq | Neq
(** Constraints are expressions implicitly compared to zero. *)
type t = {
expr: Expr.t;
op: op;
}
let compare c c' =
CCOrd.(compare c.op c'.op
<?> (Expr.compare, c.expr, c'.expr))
let pp_op out o =
Fmt.string out (match o with
| Leq -> "=<" | Geq -> ">=" | Lt -> "<"
| Gt -> ">" | Eq -> "=" | Neq -> "!=")
let pp out c =
Format.fprintf out "(@[%a@ %a 0@])"
Expr.pp c.expr pp_op c.op
let op t = t.op
let expr t = t.expr
let[@inline] of_expr expr op = { expr; op; }
let make comb op const = of_expr (Expr.make comb (C.neg const)) op
let geq e c = make e Geq c
let leq e c = make e Leq c
let gt e c = make e Gt c
let lt e c = make e Lt c
let eq e c = make e Eq c
let neq e c = make e Neq c
let geq0 e = of_expr e Geq
let leq0 e = of_expr e Leq
let gt0 e = of_expr e Gt
let lt0 e = of_expr e Lt
let eq0 e = of_expr e Eq
let neq0 e = of_expr e Neq
let[@inline] split {expr = {Expr.const; comb}; op} =
comb, op, C.neg const
let eval subst c =
let v = Expr.eval subst c.expr in
begin match c.op with
| Leq -> C.compare v C.zero <= 0
| Geq -> C.compare v C.zero >= 0
| Lt -> C.compare v C.zero < 0
| Gt -> C.compare v C.zero > 0
| Eq -> C.compare v C.zero = 0
| Neq -> C.compare v C.zero <> 0
end
end
end[@@inline]

18
src/arith/lra/linear_expr.mli Normal file
View file

@ -0,0 +1,18 @@
(*
copyright (c) 2014-2018, Guillaume Bury, Simon Cruanes
*)
(** Arithmetic expressions *)
module type COEFF = Linear_expr_intf.COEFF
module type VAR = Linear_expr_intf.VAR
module type S = Linear_expr_intf.S
type nonrec bool_op = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq
module Make(C : COEFF)(Var : VAR)
: S with module C = C
and module Var = Var
and module Var_map = CCMap.Make(Var)

265
src/arith/lra/linear_expr_intf.ml Normal file
View file

@ -0,0 +1,265 @@
(*
copyright (c) 2014-2018, Guillaume Bury, Simon Cruanes
*)
(** {1 Linear expressions interface} *)
(** {2 Coefficients}
Coefficients are used in expressions. They usually
are either rationals, or integers.
*)
module type COEFF = sig
type t
val equal : t -> t -> bool
(** Equality on coefficients. *)
val compare : t -> t -> int
(** Comparison on coefficients. *)
val pp : t Fmt.printer
(** Printer for coefficients. *)
val zero : t
(** The zero coefficient. *)
val one : t
(** The one coefficient (to rule them all, :p). *)
val neg : t -> t
(** Unary negation *)
val (+) : t -> t -> t
val (-) : t -> t -> t
val ( * ) : t -> t -> t
(** Standard operations on coefficients. *)
end
(** {2 Variable interface}
Standard interface for variables that are meant to be used
in expressions.
*)
module type VAR = sig
type t
(** Variable type. *)
val compare : t -> t -> int
(** Standard comparison function on variables. *)
val pp : t Fmt.printer
(** Printer for variables. *)
type lit
val pp_lit : lit Fmt.printer
end
type bool_op = Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
(** {2 Linear expressions & formulas} *)
(** Linear expressions & formulas.
This modules defines linear expressions (which are linear
combinations of variables), and linear constraints, where
the value of a linear expressions is constrained.
*)
module type S = sig
module C : COEFF
(** Coeficients used. Can be integers as well as rationals. *)
module Var : VAR
(** Variables used in expressions. *)
type var = Var.t
(** The type of variables appearing in expressions. *)
module Var_map : CCMap.S with type key = var
(** Maps from variables, used for expressions as well as substitutions. *)
type subst = C.t Var_map.t
(** Type for substitutions. *)
(** Combinations.
This module defines linear combnations as mapping from variables
to coefficients. This allows for very fast computations.
*)
module Comb : sig
type t
(** The type of linear combinations. *)
val compare : t -> t -> int
(** Comparisons on linear combinations. *)
val pp : t Fmt.printer
(** Printer for linear combinations. *)
val is_empty : t -> bool
(** Is the given expression empty ?*)
(** {5 Creation} *)
val empty : t
(** The empty linear combination. *)
val monomial : C.t -> var -> t
(** [monome n v] creates the linear combination [n * v] *)
val monomial1 : var -> t
(** [monome1 v] creates the linear combination [1 * v] *)
val as_singleton : t -> (C.t * var) option
(** [as_singleton l] returns [Some (c,x)] if [l = c * x], [None] otherwise *)
val add : C.t -> var -> t -> t
(** [add n v t] adds the monome [n * v] to the combination [t]. *)
(** Infix operations on combinations
This module defines usual operations on linear combinations,
as infix operators to ease reading of complex computations. *)
module Infix : sig
val (+) : t -> t -> t
(** Addition between combinations. *)
val (-) : t -> t -> t
(** Substraction between combinations. *)
val ( * ) : C.t -> t -> t
(** Multiplication by a constant. *)
end
include module type of Infix
(** Include the previous module. *)
val iter : (var -> C.t -> unit) -> t -> unit
val of_list : (C.t * var) list -> t
val to_list : t -> (C.t * var) list
(** Converters to and from lists of monomes. *)
val of_map : C.t Var_map.t -> t
val to_map : t -> C.t Var_map.t
(** {5 Semantics} *)
val eval : subst -> t -> C.t
(** Evaluate a linear combination given a substitution for its variables.
TODO: document potential exceptions raised ?*)
end
(** {2 Linear expressions.} *)
(** Linear expressions represent linear arithmetic expressions as
a linear combination and a constant. *)
module Expr : sig
type t
(** The type of linear expressions. *)
val comb : t -> Comb.t
val const : t -> C.t
val is_zero : t -> bool
val compare : t -> t -> int
(** Standard comparison function on expressions. *)
val pp : t Fmt.printer
(** Standard printing function on expressions. *)
val zero : t
(** The expression [2]. *)
val of_const : C.t -> t
(** The constant expression. *)
val of_comb : Comb.t -> t
(** Combination without constant *)
val of_list : C.t -> (C.t * Var.t) list -> t
val make : Comb.t -> C.t -> t
(** [make c n] makes the linear expression [c + n]. *)
val monomial : C.t -> var -> t
val monomial1 : var -> t
(** Infix operations on expressions
This module defines usual operations on linear expressions,
as infix operators to ease reading of complex computations. *)
module Infix : sig
val (+) : t -> t -> t
(** Addition between expressions. *)
val (-) : t -> t -> t
(** Substraction between expressions. *)
val ( * ) : C.t -> t -> t
(** Multiplication by a constant. *)
end
include module type of Infix
(** Include the previous module. *)
(** {5 Semantics} *)
val eval : subst -> t -> C.t
(** Evaluate a linear expression given a substitution for its variables.
TODO: document potential exceptions raised ?*)
end
(** {2 Linear constraints.}
Represents constraints on linear expressions. *)
module Constr : sig
type op = bool_op
(** Arithmetic comparison operators. *)
type t = {
expr: Expr.t;
op: op;
}
(** Linear constraints. Expressions are implicitly compared to zero. *)
val compare : t -> t -> int
(** Standard comparison function. *)
val pp : t Fmt.printer
(** Standard printing function. *)
val of_expr : Expr.t -> bool_op -> t
val make : Comb.t -> bool_op -> C.t -> t
(** Create a constraint from a linear expression/combination and a constant. *)
val geq : Comb.t -> C.t -> t
val leq : Comb.t -> C.t -> t
val gt: Comb.t -> C.t -> t
val lt : Comb.t -> C.t -> t
val eq : Comb.t -> C.t -> t
val neq : Comb.t -> C.t -> t
val geq0 : Expr.t -> t
val leq0 : Expr.t -> t
val gt0 : Expr.t -> t
val lt0 : Expr.t -> t
val eq0 : Expr.t -> t
val neq0 : Expr.t -> t
val op : t -> bool_op
val expr : t -> Expr.t
(** Extract the given part from a constraint. *)
val split : t -> Comb.t * bool_op * C.t
(** Split the linear combinations from the constant *)
val eval : subst -> t -> bool
(** Evaluate the given constraint under a substitution. *)
end
end

25
src/arith/lra/predicate.ml Normal file
View file

@ -0,0 +1,25 @@
type t = Leq | Geq | Lt | Gt | Eq | Neq
let neg = function
| Leq -> Gt
| Lt -> Geq
| Eq -> Neq
| Neq -> Eq
| Geq -> Lt
| Gt -> Leq
let neg_sign = function
| Leq -> Geq
| Lt -> Gt
| Geq -> Leq
| Gt -> Lt
| Neq -> Neq
| Eq -> Eq
let to_string = function
| Leq -> "=<" | Geq -> ">=" | Lt -> "<"
| Gt -> ">" | Eq -> "=" | Neq -> "!="
let pp out (self:t) = Fmt.string out (to_string self)

532
src/arith/lra/sidekick_arith_lra.ml Normal file
View file

@ -0,0 +1,532 @@
(** {1 Linear Rational Arithmetic} *)
(* Reference:
http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LRA *)
open Sidekick_core
module Simplex2 = Simplex2
module Predicate = Predicate
module Linear_expr = Linear_expr
module S_op = Simplex2.Op
type pred = Linear_expr_intf.bool_op = Leq | Geq | Lt | Gt | Eq | Neq
type op = Plus | Minus
type 'a lra_view =
| LRA_pred of pred * 'a * 'a
| LRA_op of op * 'a * 'a
| LRA_mult of Q.t * 'a
| LRA_const of Q.t
| LRA_simplex_var of 'a (* an opaque variable *)
| LRA_simplex_pred of 'a * S_op.t * Q.t (* an atomic constraint *)
| LRA_other of 'a
let map_view f (l:_ lra_view) : _ lra_view =
begin match l with
| LRA_pred (p, a, b) -> LRA_pred (p, f a, f b)
| LRA_op (p, a, b) -> LRA_op (p, f a, f b)
| LRA_mult (n,a) -> LRA_mult (n, f a)
| LRA_const q -> LRA_const q
| LRA_simplex_var v -> LRA_simplex_var (f v)
| LRA_simplex_pred (v, op, q) -> LRA_simplex_pred (f v, op, q)
| LRA_other x -> LRA_other (f x)
end
module type ARG = sig
module S : Sidekick_core.SOLVER
type term = S.T.Term.t
type ty = S.T.Ty.t
val view_as_lra : term -> term lra_view
(** Project the term into the theory view *)
val mk_lra : S.T.Term.state -> term lra_view -> term
(** Make a term from the given theory view *)
val ty_lra : S.T.Term.state -> ty
val mk_eq : S.T.Term.state -> term -> term -> term
(** syntactic equality *)
val has_ty_real : term -> bool
(** Does this term have the type [Real] *)
module Gensym : sig
type t
val create : S.T.Term.state -> t
val tst : t -> S.T.Term.state
val copy : t -> t
val fresh_term : t -> pre:string -> S.T.Ty.t -> term
(** Make a fresh term of the given type *)
end
end
module type S = sig
module A : ARG
type state
val create : ?stat:Stat.t -> A.S.T.Term.state -> state
val theory : A.S.theory
end
module Make(A : ARG) : S with module A = A = struct
module A = A
module Ty = A.S.T.Ty
module T = A.S.T.Term
module Lit = A.S.Solver_internal.Lit
module SI = A.S.Solver_internal
module N = A.S.Solver_internal.CC.N
module Tag = struct
type t =
| By_def
| Lit of Lit.t
| CC_eq of N.t * N.t
let pp out = function
| By_def -> Fmt.string out "by-def"
| Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l
| CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2
let to_lits si = function
| By_def -> []
| Lit l -> [l]
| CC_eq (n1,n2) ->
SI.CC.explain_eq (SI.cc si) n1 n2
end
module SimpVar
: Linear_expr.VAR
with type t = A.term
and type lit = Tag.t
= struct
type t = A.term
let pp = A.S.T.Term.pp
let compare = A.S.T.Term.compare
type lit = Tag.t
let pp_lit = Tag.pp
end
module LE_ = Linear_expr.Make(struct include Q let pp=pp_print end)(SimpVar)
module LE = LE_.Expr
module SimpSolver = Simplex2.Make(SimpVar)
module LConstr = SimpSolver.Constraint
module Subst = SimpSolver.Subst
module Comb_map = CCMap.Make(LE_.Comb)
type state = {
tst: T.state;
simps: T.t T.Tbl.t; (* cache *)
gensym: A.Gensym.t;
encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
needs_th_combination: unit T.Tbl.t; (* terms that require theory combination *)
mutable encoded_le: T.t Comb_map.t; (* [le] -> var encoding [le] *)
local_eqs: (N.t * N.t) Backtrack_stack.t; (* inferred by the congruence closure *)
simplex: SimpSolver.t;
}
let create ?stat tst : state =
{ tst;
simps=T.Tbl.create 128;
gensym=A.Gensym.create tst;
encoded_eqs=T.Tbl.create 8;
needs_th_combination=T.Tbl.create 8;
encoded_le=Comb_map.empty;
local_eqs = Backtrack_stack.create();
simplex=SimpSolver.create ?stat ();
}
let push_level self =
SimpSolver.push_level self.simplex;
Backtrack_stack.push_level self.local_eqs;
()
let pop_levels self n =
SimpSolver.pop_levels self.simplex n;
Backtrack_stack.pop_levels self.local_eqs n ~f:(fun _ -> ());
()
let fresh_term self ~pre ty = A.Gensym.fresh_term self.gensym ~pre ty
let fresh_lit (self:state) ~mk_lit ~pre : Lit.t =
let t = fresh_term ~pre self Ty.bool in
mk_lit t
let pp_pred_def out (p,l1,l2) : unit =
Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2
(* turn the term into a linear expression. Apply [f] on leaves. *)
let rec as_linexp ~f (t:T.t) : LE.t =
let open LE.Infix in
match A.view_as_lra t with
| LRA_other _ -> LE.monomial1 (f t)
| LRA_pred _ | LRA_simplex_pred _ ->
Error.errorf "type error: in linexp, LRA predicate %a" T.pp t
| LRA_op (op, t1, t2) ->
let t1 = as_linexp ~f t1 in
let t2 = as_linexp ~f t2 in
begin match op with
| Plus -> t1 + t2
| Minus -> t1 - t2
end
| LRA_mult (n, x) ->
let t = as_linexp ~f x in
LE.( n * t )
| LRA_simplex_var v -> LE.monomial1 v
| LRA_const q -> LE.of_const q
let as_linexp_id = as_linexp ~f:CCFun.id
(* return a variable that is equal to [le_comb] in the simplex. *)
let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t =
match LE_.Comb.as_singleton le_comb with
| Some (c, x) when Q.(c = one) -> x (* trivial linexp *)
| _ ->
match Comb_map.find le_comb self.encoded_le with
| x -> x (* already encoded that *)
| exception Not_found ->
(* new variable to represent [le_comb] *)
let proxy = fresh_term self ~pre (A.ty_lra self.tst) in
self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
Log.debugf 50
(fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy);
(* it's actually 0 *)
if LE_.Comb.is_empty le_comb then (
Log.debug 50 "(lra.encode-le.is-trivially-0)";
SimpSolver.add_constraint self.simplex
(SimpSolver.Constraint.leq proxy Q.zero) Tag.By_def;
SimpSolver.add_constraint self.simplex
(SimpSolver.Constraint.geq proxy Q.zero) Tag.By_def;
) else (
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb);
);
proxy
(* preprocess linear expressions away *)
let preproc_lra (self:state) si ~recurse ~mk_lit ~add_clause (t:T.t) : T.t option =
Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
let tst = SI.tst si in
(* tell the CC this term exists *)
let declare_term_to_cc t =
Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t);
ignore (SI.CC.add_term (SI.cc si) t : SI.CC.N.t);
in
match A.view_as_lra t with
| LRA_pred ((Eq | Neq), t1, t2) ->
(* the equality side. *)
let t, _ = T.abs tst t in
if not (T.Tbl.mem self.encoded_eqs t) then (
let u1 = A.mk_lra tst (LRA_pred (Leq, t1, t2)) in
let u2 = A.mk_lra tst (LRA_pred (Geq, t1, t2)) in
T.Tbl.add self.encoded_eqs t ();
(* encode [t <=> (u1 /\ u2)] *)
let lit_t = mk_lit t in
let lit_u1 = mk_lit (recurse u1) in
let lit_u2 = mk_lit (recurse u2) in
add_clause [SI.Lit.neg lit_t; lit_u1];
add_clause [SI.Lit.neg lit_t; lit_u2];
add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
);
None
| LRA_pred (pred, t1, t2) ->
let l1 = as_linexp ~f:recurse t1 in
let l2 = as_linexp ~f:recurse t2 in
let le = LE.(l1 - l2) in
let le_comb, le_const = LE.comb le, LE.const le in
let le_const = Q.neg le_const in
(* now we have [le_comb <pred> le_const] *)
begin match LE_.Comb.as_singleton le_comb, pred with
| None, _ ->
(* non trivial linexp, give it a fresh name in the simplex *)
let proxy = var_encoding_comb self ~pre:"_le" le_comb in
declare_term_to_cc proxy;
let op =
match pred with
| Eq | Neq -> assert false (* unreachable *)
| Leq -> S_op.Leq
| Lt -> S_op.Lt
| Geq -> S_op.Geq
| Gt -> S_op.Gt
in
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
Some new_t
| Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
let q = Q.div le_const coeff in
declare_term_to_cc v;
let op = match pred with
| Leq -> S_op.Leq
| Lt -> S_op.Lt
| Geq -> S_op.Geq
| Gt -> S_op.Gt
| Eq | Neq -> assert false
in
(* make sure to swap sides if multiplying with a negative coeff *)
let op = if Q.(coeff < zero) then S_op.neg_sign op else op in
let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
Some new_t
end
| LRA_op _ | LRA_mult _ ->
let le = as_linexp ~f:recurse t in
let le_comb, le_const = LE.comb le, LE.const le in
if Q.(le_const = zero) then (
(* if there is no constant, define [proxy] as [proxy := le_comb] and
return [proxy] *)
let proxy = var_encoding_comb self ~pre:"_le" le_comb in
declare_term_to_cc proxy;
Some proxy
) else (
(* a bit more complicated: we cannot just define [proxy := le_comb]
because of the coefficient.
Instead we assert [proxy - le_comb = le_const] using a secondary
variable [proxy2 := le_comb - proxy]
and asserting [proxy2 = -le_const] *)
let proxy = fresh_term self ~pre:"_le" (T.ty t) in
let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
SimpSolver.add_var self.simplex proxy;
LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
SimpSolver.define self.simplex proxy2
((Q.minus_one, proxy) :: LE_.Comb.to_list le_comb);
Log.debugf 50
(fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])"
LE_.Comb.pp le_comb T.pp proxy T.pp proxy2);
declare_term_to_cc proxy;
declare_term_to_cc proxy2;
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, Q.neg le_const)))
];
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, Q.neg le_const)))
];
Some proxy
)
| LRA_other t when A.has_ty_real t -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
module Q_map = CCMap.Make(Q)
(* raise conflict from certificate *)
let fail_with_cert si acts cert : 'a =
Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert;
let confl =
SimpSolver.Unsat_cert.lits cert
|> CCList.flat_map (Tag.to_lits si)
|> List.rev_map SI.Lit.neg
in
SI.raise_conflict si acts confl SI.P.default
let check_simplex_ self si acts : SimpSolver.Subst.t =
Log.debug 5 "lra: call arith solver";
let res = Profile.with1 "simplex.solve" SimpSolver.check self.simplex in
begin match res with
| SimpSolver.Sat m -> m
| SimpSolver.Unsat cert ->
Log.debugf 10
(fun k->k "(@[lra.check.unsat@ :cert %a@])"
SimpSolver.Unsat_cert.pp cert);
fail_with_cert si acts cert
end
(* TODO: trivial propagations *)
let add_local_eq (self:state) si acts n1 n2 : unit =
Log.debugf 20 (fun k->k "(@[lra.add-local-eq@ %a@ %a@])" N.pp n1 N.pp n2);
let t1 = N.term n1 in
let t2 = N.term n2 in
let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in
let le = LE.(as_linexp_id t1 - as_linexp_id t2) in
let le_comb, le_const = LE.comb le, LE.const le in
let le_const = Q.neg le_const in
let v = var_encoding_comb ~pre:"le_local_eq" self le_comb in
let lit = Tag.CC_eq (n1,n2) in
begin
try
let c1 = SimpSolver.Constraint.geq v le_const in
SimpSolver.add_constraint self.simplex c1 lit;
let c2 = SimpSolver.Constraint.leq v le_const in
SimpSolver.add_constraint self.simplex c2 lit;
with SimpSolver.E_unsat cert ->
fail_with_cert si acts cert
end;
()
(* theory combination: add decisions [t=u] whenever [t] and [u]
have the same value in [subst] and both occur under function symbols *)
let do_th_combination (self:state) si acts (subst:Subst.t) : unit =
let n_th_comb = T.Tbl.keys self.needs_th_combination |> Iter.length in
if n_th_comb > 0 then (
Log.debugf 5
(fun k->k "(@[LRA.needs-th-combination@ :n-lits %d@])" n_th_comb);
Log.debugf 50
(fun k->k "(@[LRA.needs-th-combination@ :terms [@[%a@]]@])"
(Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination));
);
(* theory combination: for [t1,t2] terms in [self.needs_th_combination]
that have same value, but are not provably equal, push
decision [t1=t2] into the SAT solver. *)
begin
let by_val: T.t list Q_map.t =
T.Tbl.keys self.needs_th_combination
|> Iter.map (fun t -> Subst.eval subst t, t)
|> Iter.fold
(fun m (q,t) ->
let l = Q_map.get_or ~default:[] q m in
Q_map.add q (t::l) m)
Q_map.empty
in
Q_map.iter
(fun _q ts ->
begin match ts with
| [] | [_] -> ()
| ts ->
(* several terms! see if they are already equal *)
CCList.diagonal ts
|> List.iter
(fun (t1,t2) ->
Log.debugf 50
(fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])"
Q.pp_print _q T.pp t1 T.pp t2);
assert(SI.cc_mem_term si t1);
assert(SI.cc_mem_term si t2);
(* if both [t1] and [t2] are relevant to the congruence
closure, and are not equal in it yet, add [t1=t2] as
the next decision to do *)
if not (SI.cc_are_equal si t1 t2) then (
Log.debug 50 "LRA.th-comb.must-decide-equal";
let t = A.mk_eq (SI.tst si) t1 t2 in
let lit = SI.mk_lit si acts t in
SI.push_decision si acts lit
)
)
end)
by_val;
()
end;
()
(* partial checks is where we add literals from the trail to the
simplex. *)
let partial_check_ self si acts trail : unit =
Profile.with_ "lra.partial-check" @@ fun () ->
let changed = ref false in
trail
(fun lit ->
let sign = SI.Lit.sign lit in
let lit_t = SI.Lit.term lit in
match A.view_as_lra lit_t with
| LRA_simplex_pred (v, op, q) ->
(* need to account for the literal's sign *)
let op = if sign then op else S_op.not_ op in
(* assert new constraint to Simplex *)
let constr = SimpSolver.Constraint.mk v op q in
Log.debugf 10
(fun k->k "(@[lra.partial-check.assert@ %a@])"
SimpSolver.Constraint.pp constr);
begin
changed := true;
try
SimpSolver.add_var self.simplex v;
SimpSolver.add_constraint self.simplex constr (Tag.Lit lit)
with SimpSolver.E_unsat cert ->
Log.debugf 10
(fun k->k "(@[lra.partial-check.unsat@ :cert %a@])"
SimpSolver.Unsat_cert.pp cert);
fail_with_cert si acts cert
end
| _ -> ());
(* incremental check *)
if !changed then (
ignore (check_simplex_ self si acts : SimpSolver.Subst.t);
);
()
let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
Log.debug 5 "(th-lra.final-check)";
Profile.with_ "lra.final-check" @@ fun () ->
(* add congruence closure equalities *)
Backtrack_stack.iter self.local_eqs
~f:(fun (n1,n2) -> add_local_eq self si acts n1 n2);
Log.debug 5 "(th-lra: call arith solver)";
let model = check_simplex_ self si acts in
Log.debugf 20 (fun k->k "(@[lra.model@ %a@])" SimpSolver.Subst.pp model);
Log.debug 5 "lra: solver returns SAT";
do_th_combination self si acts model;
()
(* look for subterms of type Real, for they will need theory combination *)
let on_subterm (self:state) _ (t:T.t) : unit =
Log.debugf 50 (fun k->k "lra: cc-on-subterm %a" T.pp t);
if A.has_ty_real t &&
not (T.Tbl.mem self.needs_th_combination t) then (
Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t);
T.Tbl.add self.needs_th_combination t ()
)
let create_and_setup si =
Log.debug 2 "(th-lra.setup)";
let stat = SI.stats si in
let st = create ~stat (SI.tst si) in
(* TODO SI.add_simplifier si (simplify st); *)
SI.add_preprocess si (preproc_lra st);
SI.on_final_check si (final_check_ st);
SI.on_partial_check si (partial_check_ st);
SI.on_cc_is_subterm si (on_subterm st);
SI.on_cc_post_merge si
(fun _ _ n1 n2 ->
if A.has_ty_real (N.term n1) then (
Backtrack_stack.push st.local_eqs (n1, n2)
));
st
let theory =
A.S.mk_theory
~name:"th-lra"
~create_and_setup ~push_level ~pop_levels
()
end

1035
src/arith/lra/simplex2.ml Normal file
View file

File diff suppressed because it is too large Load diff

123
src/arith/lra/simplex_intf.ml Normal file
View file

@ -0,0 +1,123 @@
(*
copyright (c) 2014-2018, Guillaume Bury, Simon Cruanes
*)
(** {1 Modular and incremental implementation of the general simplex}. *)
(** The simplex is used as a decision procedure for linear rational arithmetic
problems.
More information can be found on the particular flavor of this
implementation at https://gbury.eu/public/papers/stage-m2.pdf
*)
module type S = sig
(** The given type of the variables *)
type var
(** A map on variables *)
module Var_map : CCMap.S with type key = var
(** Parameter required at the creation of the simplex *)
type param
type lit
(** The type of a (possibly not solved) linear system *)
type t
(** An unsatisfiability explanation is a couple [(x, expr)]. If [expr] is the
empty list, then there is a contradiction between two given bounds of [x].
Else, the explanation is an equality [x = expr] that is valid
(it can be derived from the original equations of the system) from which a
bound can be deduced which contradicts an already given bound of the
system. *)
type cert = {
cert_var: var;
cert_expr: (Q.t * var) list;
}
(** Generic type returned when solving the simplex. A solution is a list of
bindings that satisfies all the constraints inside the system. If the
system is unsatisfiable, an explanation of type ['cert] is returned. *)
type res =
| Solution of Q.t Var_map.t
| Unsatisfiable of cert
(** {3 Simplex construction} *)
(** The empty system.
@param fresh the state for generating fresh variables on demand. *)
val create : param -> t
(** [add_eq s (x, eq)] adds the equation [x=eq] to [s] *)
val add_eq : t -> var * (Q.t * var) list -> unit
(** [add_bounds (x, lower, upper)] adds to [s]
the bounds [lower] and [upper] for the given variable [x].
If the bound is loose on one side
(no upper bounds for instance), the values [Q.inf] and
[Q.minus_inf] can be used. By default, in a system, all variables
have no bounds, i.e have lower bound [Q.minus_inf] and upper bound
[Q.inf].
Optional parameters allow to make the the bounds strict. Defaults to false,
so that bounds are large by default. *)
val add_bounds : t ->
?strict_lower:bool -> ?strict_upper:bool ->
?lower_reason:lit -> ?upper_reason:lit ->
var * Q.t * Q.t -> unit
val add_lower_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
val add_upper_bound : t -> ?strict:bool -> reason:lit -> var -> Q.t -> unit
(** {3 Simplex solving} *)
(** [solve s] solves the system [s] and returns a solution, if one exists.
This function may change the internal representation of the system to
that of an equivalent one
(permutation of basic and non basic variables and pivot operation
on the tableaux).
*)
val solve : t -> res
val check_cert :
t ->
cert ->
[`Ok of lit list | `Bad_bounds of string * string | `Diff_not_0 of Q.t Var_map.t]
(** checks that the certificat indeed yields to a contradiction
in the current state of the simplex.
@return [`Ok unsat_core] if the certificate is valid. *)
(* TODO: push/pop? at least on bounds *)
val pp_cert : cert CCFormat.printer
val pp_full_state : t CCFormat.printer
(**/**)
val check_invariants : t -> bool (* check that all invariants hold *)
val matrix_pp_width : int ref (* horizontal filling when we print the matrix *)
(**/**)
end
(* TODO: benchmark
- copy current implem;
- move random generator somewhere shared;
- compare cur & old implem;
- optimize (remove find_expr?))
*)
module type S_FULL = sig
include S
module L : Linear_expr_intf.S
with type C.t = Q.t and type Var.t = var and type Var.lit = lit
type op = Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
type constr = L.Constr.t
val add_constr : t -> constr -> lit -> unit
(** Add a constraint to a simplex state. *)
end

13
src/arith/tests/dune Normal file
View file

@ -0,0 +1,13 @@
(executable
(name run_tests)
(libraries containers sidekick-arith.lra zarith iter alcotest qcheck)
(flags :standard -warn-error -a+8 -color always))
(alias
(name runtest)
(locks /test)
(package sidekick-arith)
(action
(progn
(run ./run_tests.exe alcotest) ; run regressions first
(run ./run_tests.exe qcheck --verbose))))

21
src/arith/tests/run_tests.ml Normal file
View file

@ -0,0 +1,21 @@
let tests : unit Alcotest.test list = [
Test_simplex2.tests;
]
let props =
List.flatten
[ Test_simplex2.props;
]
let () =
match Array.to_list Sys.argv with
| a0::"alcotest"::tl ->
Sidekick_util.Log.set_debug 50;
let argv= Array.of_list (a0::tl) in
Alcotest.run ~argv ~and_exit:true "arith tests" tests;
| a0::"qcheck"::tl ->
let argv= Array.of_list (a0::tl) in
CCFormat.set_color_default true;
QCheck_runner.run_tests_main ~argv props
| _ -> failwith "expected (qcheck|alcotest) as first arg"

502
src/arith/tests/test_simplex2.ml Normal file
View file

@ -0,0 +1,502 @@
open CCMonomorphic
module Fmt = CCFormat
module QC = QCheck
module Log = Sidekick_util.Log
let spf = Printf.sprintf
module Var = struct
include CCInt
let pp out x = Format.fprintf out "X_%d" x
let rand n : t QC.arbitrary = QC.make ~print:(Fmt.to_string pp) @@ QC.Gen.(0--n)
type lit = int
let pp_lit = Fmt.int
end
module Spl = Sidekick_arith_lra.Simplex2.Make(Var)
let rand_n low n : Z.t QC.arbitrary =
QC.map ~rev:Z.to_int Z.of_int QC.(low -- n)
let rand_q_with u l : Q.t QC.arbitrary =
let n1 = rand_n (~- u) u in
let n2 = rand_n 1 l in
let qc =
QC.map ~rev:(fun q -> Q.num q, Q.den q)
(fun (x,y) -> Q.make x y)
(QC.pair n1 n2)
in
(* avoid [undef] when shrinking *)
let shrink q yield =
CCOpt.get_exn qc.QC.shrink q (fun x -> if Q.is_real x then yield x)
in
QC.set_shrink shrink qc
let rand_q = rand_q_with 200_000 40_000
module Step = struct
module G = QC.Gen
type t =
| S_new_var of Var.t
| S_define of Var.t * (Q.t * Var.t) list
| S_leq of Var.t * Q.t
| S_lt of Var.t * Q.t
| S_geq of Var.t * Q.t
| S_gt of Var.t * Q.t
let pp_le out le =
let pp_pair out (n,x) =
if Q.equal Q.one n then Var.pp out x
else Fmt.fprintf out "%a . %a" Q.pp_print n Var.pp x in
Fmt.fprintf out "(@[%a@])"
Fmt.(list ~sep:(return " +@ ") pp_pair) le
let pp_ out = function
| S_new_var v -> Fmt.fprintf out "(@[new-var %a@])" Var.pp v
| S_define (v,le) -> Fmt.fprintf out "(@[define %a@ := %a@])" Var.pp v pp_le le
| S_leq (x,n) -> Fmt.fprintf out "(@[upper %a <= %a@])" Var.pp x Q.pp_print n
| S_lt (x,n) -> Fmt.fprintf out "(@[upper %a < %a@])" Var.pp x Q.pp_print n
| S_geq (x,n) -> Fmt.fprintf out "(@[lower %a >= %a@])" Var.pp x Q.pp_print n
| S_gt (x,n) -> Fmt.fprintf out "(@[lower %a > %a@])" Var.pp x Q.pp_print n
(* check that a sequence is well formed *)
let well_formed (l:t list) : bool =
let rec aux vars = function
| [] -> true
| S_new_var v :: tl ->
not (List.mem v vars) && aux (v::vars) tl
| (S_leq (x,_) | S_lt (x,_) | S_geq (x,_) | S_gt (x,_)) :: tl ->
List.mem x vars && aux vars tl
| S_define (x,le) :: tl->
not (List.mem x vars) &&
List.for_all (fun (_,y) -> List.mem y vars) le &&
aux (x::vars) tl
in
aux [] l
let shrink_step self =
let module S = QC.Shrink in
match self with
| S_new_var _
| S_leq _ | S_lt _ | S_geq _ | S_gt _ -> QC.Iter.empty
| S_define (x, le) ->
let open QC.Iter in
let* le = S.list le in
if List.length le >= 2 then return (S_define (x,le)) else empty
let rand_steps (n:int) : t list QC.Gen.t =
let open G in
let rec aux n vars acc =
if n<=0 then return (List.rev acc)
else (
let* vars, step =
frequency @@ List.flatten [
(* add a bound *)
(match vars with
| [] -> []
| vs ->
let gen =
let+ x = oneofl vs
and+ kind = oneofl [`Leq;`Lt;`Geq;`Gt]
and+ n = rand_q.QC.gen in
vars, (match kind with
| `Lt -> S_lt(x,n)
| `Leq -> S_leq(x,n)
| `Gt -> S_gt(x,n)
| `Geq -> S_geq(x,n))
in
[6, gen]);
(* make a new non-basic var *)
(let gen =
let v = List.length vars in
return ((v::vars), S_new_var v)
in
[2, gen]);
(* make a definition *)
(if List.length vars>2
then (
let v = List.length vars in
let gen =
let* vars' = G.shuffle_l vars in
let* n = 1 -- 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 le = List.combine coeffs vars' in
return (v::vars, S_define (v, le))
in
[5, gen]
) else []);
]
in
aux (n-1) vars (step::acc)
)
in
aux n [] []
(* shrink a list but keep it well formed *)
let shrink : t list QC.Shrink.t =
QC.Shrink.(filter well_formed @@ list ~shrink:shrink_step)
let gen_for n1 n2 =
let open G in
assert (n1 < n2);
let* n = n1 -- n2 in
rand_steps n
let rand_for n1 n2 : t list QC.arbitrary =
let print = Fmt.to_string (Fmt.Dump.list pp_) in
QC.make ~shrink ~print (gen_for n1 n2)
let rand : t list QC.arbitrary = rand_for 1 100
end
(* add a single step to the simplexe *)
let add_step simplex (s:Step.t) : unit =
begin match s with
| Step.S_new_var v -> Spl.add_var simplex v
| Step.S_leq (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.leq v n) 0
| Step.S_lt (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.lt v n) 0
| Step.S_geq (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.geq v n) 0
| Step.S_gt (v,n) ->
Spl.add_constraint simplex (Spl.Constraint.gt v n) 0
| Step.S_define (x,le) ->
Spl.define simplex x le
end
let add_steps ?(f=fun()->()) (simplex:Spl.t) l : unit =
f();
List.iter
(fun s -> add_step simplex s; f())
l
(* is this simplex's state sat? *)
let check_simplex_is_sat simplex : bool =
(try Spl.check_exn simplex; true
with Spl.E_unsat _ -> false)
(* is this problem sat? *)
let check_pb_is_sat pb : bool =
let simplex = Spl.create() in
(try add_steps simplex pb; Spl.check_exn simplex; true
with Spl.E_unsat _ -> false)
let check_steps l : bool =
let simplex = Spl.create () in
try add_steps simplex l; Spl.check_exn simplex; true
with _ -> false
(* basic debug printer for Q.t *)
let q_dbg q = Fmt.asprintf "%.3f" (Q.to_float q)
let prop_sound ?(inv=false) pb =
let simplex = Spl.create () in
begin match
add_steps simplex pb;
Spl.check simplex
with
| Sat subst ->
let get_val v =
try Spl.V_map.find v subst
with Not_found -> assert false
in
let check_step s =
(try
if inv then Spl._check_invariants simplex;
match s with
| Step.S_new_var _ -> ()
| Step.S_define (x, le) ->
let v_x = get_val x in
let v_le =
List.fold_left (fun s (n,y) -> Q.(s + n * get_val y)) Q.zero le
in
if Q.(v_x <> v_le) then (
failwith (spf "bad def (X_%d): val(x)=%s, val(expr)=%s" x (q_dbg v_x)(q_dbg v_le))
);
| Step.S_lt (x, n) ->
let v_x = get_val x in
if Q.(v_x >= n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n))
| Step.S_leq (x, n) ->
let v_x = get_val x in
if Q.(v_x > n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n))
| Step.S_gt (x, n) ->
let v_x = get_val x in
if Q.(v_x <= n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n))
| Step.S_geq (x, n) ->
let v_x = get_val x in
if Q.(v_x < n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n))
with e ->
QC.Test.fail_reportf "step failed: %a@.exn:@.%s@."
Step.pp_ s (Printexc.to_string e)
);
if inv then Spl._check_invariants simplex;
true
in
List.for_all check_step pb
| Spl.Unsat cert ->
Spl._check_cert cert;
true
| exception Spl.E_unsat _cert ->
true (* TODO : check certificate *)
end
(* a bunch of useful stats for a problem *)
let steps_stats = [
"n-define", Step.(List.fold_left (fun n -> function S_define _ -> n+1 | _->n) 0);
"n-bnd",
Step.(List.fold_left
(fun n -> function (S_leq _ | S_lt _ | S_geq _ | S_gt _) -> n+1 | _->n) 0);
"n-vars",
Step.(List.fold_left
(fun n -> function S_define _ | S_new_var _ -> n+1 | _ -> n) 0);
]
let enable_stats =
match Sys.getenv_opt "TEST_STAT" with Some("1"|"true") -> true | _ -> false
let set_stats_maybe ar =
if enable_stats then QC.set_stats steps_stats ar else ar
let check_sound =
let ar =
Step.(rand_for 0 300)
|> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
|> set_stats_maybe
in
QC.Test.make ~long_factor:10 ~count:500 ~name:"simplex2_sound" ar prop_sound
let prop_invariants pb =
let simplex = Spl.create () in
(try
add_steps simplex pb ~f:(fun () -> Spl._check_invariants simplex);
Spl.check_exn simplex
with Spl.E_unsat _ -> ());
Spl._check_invariants simplex;
true
let check_invariants =
let ar =
Step.(rand_for 0 300)
|> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
|> set_stats_maybe
in
QC.Test.make
~long_factor:10 ~count:500 ~name:"simplex2_invariants"
ar prop_invariants
let prop_backtrack pb =
let simplex = Spl.create () in
let stack = Stack.create() in
let res = ref true in
begin try
List.iter
(fun s ->
let is_sat = check_simplex_is_sat simplex in
Spl.push_level simplex;
Stack.push is_sat stack;
if not is_sat then (res := false; raise Exit);
(try add_step simplex s
with Spl.E_unsat _ -> res := false; raise Exit);
)
pb;
with Exit -> ()
end;
res := !res && check_simplex_is_sat simplex;
Log.debugf 50 (fun k->k "res=%b, expected=%b" !res (check_pb_is_sat pb));
assert CCBool.(equal !res (check_pb_is_sat pb));
(* now backtrack and check at each level *)
while not (Stack.is_empty stack) do
let res = Stack.pop stack in
Spl.pop_levels simplex 1;
assert CCBool.(equal res (check_simplex_is_sat simplex))
done;
true
let check_backtrack =
let ar =
Step.(rand_for 0 300)
|> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
|> set_stats_maybe
in
QC.Test.make
~long_factor:10 ~count:200 ~name:"simplex2_backtrack"
ar prop_backtrack
let check_scalable =
let prop pb =
let simplex = Spl.create () in
(try
add_steps simplex pb;
Spl.check_exn simplex
with _ -> ());
true
in
let ar =
Step.(rand_for 3_000 5_000)
|> QC.set_collect (fun pb -> if check_steps pb then "sat" else "unsat")
|> set_stats_maybe
in
QC.Test.make ~long_factor:2 ~count:10 ~name:"simplex2_scalable"
ar prop
let props = [
check_invariants;
check_sound;
check_backtrack;
check_scalable;
]
(* regression tests *)
module Reg = struct
let alco_mk name f = name, `Quick, f
let reg_prop_sound ?inv name l =
alco_mk name @@ fun () ->
if not (prop_sound ?inv l) then Alcotest.fail "fail";
()
let reg_prop_invariants name l =
alco_mk name @@ fun () ->
if not (prop_invariants l) then Alcotest.fail "fail";
()
let reg_prop_backtrack name l =
alco_mk name @@ fun () ->
if not (prop_backtrack l) then Alcotest.fail "fail";
()
open Step
let qstr = Q.of_string
(* regression from qcheck *)
let t1 =
let l = [
S_new_var 1;
S_gt (1, qstr "2630/16347");
S_leq (1, qstr "26878/30189");
] in
reg_prop_sound "t1" l
let t2_snd, t2_inv =
let l = [
S_new_var 0; S_new_var 1; S_new_var 2;
S_define (3, [
(qstr "19682/2117", 1);
(qstr "26039/15663", 0);
(qstr "-11221/17868", 2)
]);
] in
reg_prop_sound "t2_snd" l, reg_prop_invariants "t2_inv" l
let t3_snd =
let l = [
S_new_var 0;
S_leq (0, qstr "-4831/8384");
S_new_var 1;
S_new_var 3;
S_define (4, [
qstr "-22841/11339", 0;
qstr "5792/491", 1;
qstr "-48819/5089", 3;
]);
] in
reg_prop_sound "t3" l
let t4_snd_short =
let l = [
S_new_var 0; S_new_var 1; S_new_var 2;
S_define (3, [qstr "76889/9000", 2; qstr "55017/30392", 1]);
S_define (4, [qstr "14217/27439", 3; qstr "14334/25735", 0]);
S_leq (1, qstr "-58451/29068");
] in
reg_prop_sound "t4_short" l
let t4_snd =
let l = [
S_new_var 0;
S_new_var 1;
S_new_var 2;
S_define (3, [
qstr "-86184/12073", 1;
qstr "-67593/25801", 0;
qstr "19113/16768", 2;
]);
S_define (4, [
qstr "-26393/10015", 2;
qstr "-12730/2099", 3
]);
S_new_var 6;
S_define (7, [
qstr "-30739/30520", 6;
qstr "-1840/2773", 4;
qstr "40708/16579", 0;
qstr "-77011/34083", 3;
]);
S_leq (7, qstr "-6555/1838")
] in
reg_prop_sound "t4" l
let t5 =
let l = [
S_new_var 0;
S_lt (0, qstr "-45822/1835");
S_new_var 2;
S_new_var 4;
S_define (5, [qstr "40461/27377", 2; qstr"4292/31193", 0]);
S_define (6, [qstr "-51582/5441", 5; qstr"-88432/27939", 4]);
] in
reg_prop_sound "t5" l
let t6 =
let l = [
S_new_var 0;
S_new_var 1;
S_define (3, [qstr "-21185/6058", 0; qstr "35055/29267", 1]);
S_define (4 , [qstr "4013/2790", 1; qstr "-23314/11713", 3]);
S_define (5 , [qstr "-15503/1523", 1; qstr "49580/15623", 0]);
S_define (13, [qstr "41722/2083", 0; qstr "-20558/8483", 5]);
S_define (15, [qstr "-18908/11213", 4; qstr "-66053/8560", 3]);
S_leq (13, qstr "-5123/16411");
S_lt (15, qstr "-9588/859");
] in
reg_prop_sound ~inv:true "t6" l
let t7 =
let l = [
S_new_var 1;
S_leq (1, qstr "32908/13565");
S_gt (1, qstr "92197/15966");
] in
reg_prop_backtrack "t7" l
(* regression for simplex certificate checking *)
let t8 =
let l = [
S_new_var 0;
S_lt (0, qstr "-8675/8802");
S_new_var 5;
S_define (7, [qstr "95221/14629", 5; qstr "60092/7011", 0]);
S_lt (5, qstr "-80423/7787");
S_geq (7, qstr "-10544/35599");
] in
reg_prop_sound "t8" l
let tests = [
t1; t2_snd; t2_inv; t3_snd; t4_snd_short; t4_snd; t5; t6; t7; t8;
]
end
let tests =
"simplex2", List.flatten [ Reg.tests ]

18
src/cc/Sidekick_cc.ml
View file

@ -260,6 +260,7 @@ module Make (A: CC_ARG)
mutable on_new_term: ev_on_new_term list;
mutable on_conflict: ev_on_conflict list;
mutable on_propagate: ev_on_propagate list;
mutable on_is_subterm : ev_on_is_subterm list;
mutable new_merges: bool;
bitgen: Bits.bitfield_gen;
field_marked_explain: Bits.field; (* used to mark traversed nodes when looking for a common ancestor *)
@ -281,6 +282,7 @@ module Make (A: CC_ARG)
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) -> unit
and ev_on_is_subterm = N.t -> term -> unit
let[@inline] size_ (r:repr) = r.n_size
let[@inline] n_true cc = Lazy.force cc.true_
@ -373,6 +375,7 @@ module Make (A: CC_ARG)
end
let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ =
Profile.instant "cc.conflict";
(* clear tasks queue *)
Vec.clear cc.pending;
Vec.clear cc.combine;
@ -531,6 +534,10 @@ module Make (A: CC_ARG)
begin
let sub_r = find_ sub in
let old_parents = sub_r.n_parents in
if Bag.is_empty old_parents then (
(* first time it has parents: call watchers that this is a subterm *)
List.iter (fun f -> f sub u) self.on_is_subterm;
);
on_backtrack self (fun () -> sub_r.n_parents <- old_parents);
sub_r.n_parents <- Bag.cons n sub_r.n_parents;
end;
@ -557,6 +564,8 @@ module Make (A: CC_ARG)
let[@inline] add_term cc t : node = add_term_rec_ cc t
let mem_term = mem
let set_as_lit cc (n:node) (lit:lit) : unit =
match n.n_as_lit with
| Some _ -> ()
@ -835,14 +844,20 @@ module Make (A: CC_ARG)
let[@inline] merge_t cc t1 t2 expl =
merge cc (add_term cc t1) (add_term cc t2) expl
let explain_eq cc n1 n2 : lit list =
let th = ref true in
explain_pair cc ~th [] n1 n2
let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge
let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict
let on_propagate cc f = cc.on_propagate <- f :: cc.on_propagate
let on_is_subterm cc f = cc.on_is_subterm <- f :: cc.on_is_subterm
let create ?(stat=Stat.global)
?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[]) ?(on_conflict=[]) ?(on_propagate=[])
?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[])
?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[])
?(size=`Big)
(tst:term_state) : t =
let size = match size with `Small -> 128 | `Big -> 2048 in
@ -858,6 +873,7 @@ module Make (A: CC_ARG)
on_new_term;
on_conflict;
on_propagate;
on_is_subterm;
pending=Vec.create();
combine=Vec.create();
undo=Backtrack_stack.create();

39
src/core/Sidekick_core.ml
View file

@ -216,11 +216,15 @@ module type CC_S = sig
(** Add the term to the congruence closure, if not present already.
Will be backtracked. *)
val mem_term : t -> term -> bool
(** Returns [true] if the term is explicitly present in the congruence closure *)
type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit
type ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
type ev_on_new_term = t -> N.t -> term -> unit
type ev_on_conflict = t -> th:bool -> lit list -> unit
type ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
type ev_on_is_subterm = N.t -> term -> unit
val create :
?stat:Stat.t ->
@ -229,6 +233,7 @@ module type CC_S = sig
?on_new_term:ev_on_new_term list ->
?on_conflict:ev_on_conflict list ->
?on_propagate:ev_on_propagate list ->
?on_is_subterm:ev_on_is_subterm list ->
?size:[`Small | `Big] ->
term_state ->
t
@ -258,6 +263,9 @@ module type CC_S = sig
val on_propagate : t -> ev_on_propagate -> unit
(** Called when the congruence closure propagates a literal *)
val on_is_subterm : t -> ev_on_is_subterm -> unit
(** Called on terms that are subterms of function symbols *)
val set_as_lit : t -> N.t -> lit -> unit
(** map the given node to a literal. *)
@ -280,6 +288,10 @@ module type CC_S = sig
val assert_lits : t -> lit Iter.t -> unit
(** Addition of many literals *)
val explain_eq : t -> N.t -> N.t -> lit list
(** Explain why the two nodes are equal.
Fails if they are not, in an unspecified way *)
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
(** Raise a conflict with the given explanation
it must be a theory tautology that [expl ==> absurd].
@ -390,10 +402,19 @@ module type SOLVER_INTERNAL = sig
(** {3 hooks for the theory} *)
val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
(** Propagate a literal for a reason. This is similar to asserting
the clause [reason => lit], but more lightweight, and in a way
that is backtrackable. *)
val raise_conflict : t -> actions -> lit list -> proof -> 'a
(** Give a conflict clause to the solver *)
val push_decision : t -> 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 -> (unit -> lit list) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
@ -429,6 +450,9 @@ module type SOLVER_INTERNAL = sig
val cc_find : t -> CC.N.t -> CC.N.t
(** Find representative of the node *)
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
(** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
@ -442,6 +466,10 @@ module type SOLVER_INTERNAL = sig
(** Add/retrieve congruence closure node for this term.
To be used in theories *)
val cc_mem_term : t -> term -> bool
(** 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
(** Callback for when two classes containing data for this key are merged (called before) *)
@ -452,6 +480,10 @@ module type SOLVER_INTERNAL = sig
(** Callback to add data on terms when they are added to the congruence
closure *)
val on_cc_is_subterm : t -> (CC.N.t -> term -> unit) -> unit
(** Callback for when a term is a subterm of another term in the
congruence closure *)
val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
(** Callback called on every CC conflict *)
@ -481,11 +513,16 @@ module type SOLVER_INTERNAL = sig
type preprocess_hook =
t ->
recurse:(term -> term) ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> unit) ->
term -> term option
(** Given a term, try to preprocess it. Return [None] if it didn't change.
Can also add clauses to define new terms. *)
Can also add clauses to define new terms.
@param recurse call preprocessor on subterms.
@param mk_lit creates a new literal for a boolean term.
@param add_clause pushes a new clause into the SAT solver.
*)
val add_preprocess : t -> preprocess_hook -> unit
end

2
src/main/dune
View file

@ -5,7 +5,7 @@
(public_name sidekick)
(package sidekick-bin)
(libraries containers iter result msat sidekick.core sidekick-arith.base-term
sidekick.msat-solver sidekick-bin.smtlib)
sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
(flags :standard -safe-string -color always -open Sidekick_util))
(rule

3
src/main/main.ml
View file

@ -78,6 +78,7 @@ let argspec = Arg.align [
"--no-p", Arg.Clear p_progress, " no progress bar";
"--size", Arg.String (int_arg size_limit), " <s>[kMGT] sets the size limit for the sat solver";
"--time", Arg.String (int_arg time_limit), " <t>[smhd] sets the time limit for the sat solver";
"-t", Arg.String (int_arg time_limit), " short for --time";
"--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit";
"-d", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
"--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
@ -126,6 +127,8 @@ let check_limits () =
raise Out_of_space
let main () =
Sidekick_tef.setup();
at_exit Sidekick_tef.teardown;
CCFormat.set_color_default true;
(* Administrative duties *)
Arg.parse argspec input_file usage;

10
src/mini-cc/Sidekick_mini_cc.ml
View file

@ -147,13 +147,14 @@ module Make(A: ARG) = struct
self
let clear (self:t) : unit =
let {ok=_; tbl; sig_tbl; pending=_; combine=_; true_; false_} = self in
self.ok <- true;
T_tbl.clear self.tbl;
Sig_tbl.clear self.sig_tbl;
self.pending <- [];
self.combine <- [];
T_tbl.add self.tbl self.true_.n_t self.true_;
T_tbl.add self.tbl self.false_.n_t self.false_;
T_tbl.clear tbl;
Sig_tbl.clear sig_tbl;
T_tbl.add tbl true_.n_t true_;
T_tbl.add tbl false_.n_t false_;
()
let sub_ t k : unit =
@ -317,5 +318,4 @@ module Make(A: ARG) = struct
|> Iter.filter Node.is_root
|> Iter.map
(fun n -> Node.iter_cls n |> Iter.map Node.term)
end

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

@ -2,4 +2,5 @@
(names tests)
(libraries sidekick.mini-cc sidekick-arith.base-term alcotest)
(package sidekick-arith)
(locks /test)
(modes native))

41
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -174,6 +174,7 @@ module Make(A : ARG)
and preprocess_hook =
t ->
recurse:(term -> term) ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> unit) ->
term -> term option
@ -201,6 +202,10 @@ module Make(A : ARG)
let add_preprocess self f = self.preprocess <- f :: self.preprocess
let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
let sign = Lit.sign lit in
acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self acts c : 'a =
Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c P.default
@ -223,23 +228,27 @@ module Make(A : ARG)
match Term.Tbl.find self.preprocess_cache t with
| u -> u
| exception Not_found ->
(* first, map subterms *)
let u = Term.map_shallow self.tst aux t in
(* then rewrite *)
let u = aux_rec u self.preprocess in
(* try rewrite here *)
let u =
match aux_rec t self.preprocess with
| None ->
Term.map_shallow self.tst aux t (* just map subterms *)
| Some u -> u
in
Term.Tbl.add self.preprocess_cache t u;
u
(* try each function in [hooks] successively *)
and aux_rec t hooks = match hooks with
| [] -> t
| [] -> None
| h :: hooks_tl ->
match h self ~mk_lit ~add_clause t with
match h self ~recurse:aux ~mk_lit ~add_clause t with
| None -> aux_rec t hooks_tl
| Some u ->
Log.debugf 30
(fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])"
Term.pp t Term.pp u);
aux u
let u' = aux u in
Some u'
in
let t = Lit.term lit |> simp_t self |> aux in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
@ -271,9 +280,15 @@ module Make(A : ARG)
let on_cc_post_merge self f = CC.on_post_merge (cc self) f
let on_cc_conflict self f = CC.on_conflict (cc self) f
let on_cc_propagate self f = CC.on_propagate (cc self) f
let on_cc_is_subterm self f = CC.on_is_subterm (cc self) f
let cc_add_term self t = CC.add_term (cc self) t
let cc_mem_term self t = CC.mem_term (cc self) t
let cc_find self n = CC.find (cc self) n
let cc_are_equal self t1 t2 =
let n1 = cc_add_term self t1 in
let n2 = cc_add_term self t2 in
N.equal (cc_find self n1) (cc_find self n2)
let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e
let cc_merge_t self acts t1 t2 e =
cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e
@ -340,10 +355,12 @@ module Make(A : ARG)
(* propagation from the bool solver *)
let check_ ~final (self:t) (acts: msat_acts) =
let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
let iter = iter_atoms_ acts in
Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
self.on_progress();
assert_lits_ ~final self acts iter
assert_lits_ ~final self acts iter;
Profile.exit pb
(* propagation from the bool solver *)
let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
@ -573,13 +590,16 @@ module Make(A : ARG)
let add_clause (self:t) (c:Atom.t IArray.t) : unit =
Stat.incr self.count_clause;
Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c);
Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default;
Profile.exit pb
let add_clause_l self c = add_clause self (IArray.of_list c)
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 () ->
let module M = Term.Tbl in
let m = M.create 128 in
let tst = self.si.tst in
@ -601,6 +621,7 @@ module Make(A : ARG)
let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
~assumptions (self:t) : res =
Profile.with_ "msat-solver.solve" @@ fun () ->
let do_on_exit () =
List.iter (fun f->f()) on_exit;
in

1
src/smtlib/Form.ml
View file

@ -134,6 +134,7 @@ let imply_l st xs y = match xs with
| _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs)
let imply st a b = imply_a st (IArray.singleton a) b
let xor st a b = not_ st (equiv st a b)
let distinct_l tst l =
match l with

15
src/smtlib/Process.ml
View file

@ -1,6 +1,7 @@
(** {2 Conversion into {!Term.t}} *)
module BT = Sidekick_base_term
module Profile = Sidekick_util.Profile
open Sidekick_base_term
[@@@ocaml.warning "-32"]
@ -156,8 +157,10 @@ let solve
let on_progress =
if progress then Some (mk_progress s) else None in
let res =
Solver.solve ~assumptions ?on_progress s
Profile.with_ "solve" begin fun () ->
Solver.solve ~assumptions ?on_progress s
(* ?gc ?restarts ?time ?memory ?progress *)
end
in
let t2 = Sys.time () in
Printf.printf "\r"; flush stdout;
@ -179,11 +182,12 @@ let solve
Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
| Solver.Unsat {proof=Some p;_} ->
if check then (
Solver.Proof.check p;
Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
);
begin match dot_proof with
| None -> ()
| Some file ->
Profile.with_ "dot.proof" @@ fun () ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
@ -309,13 +313,18 @@ module Th_lra = Sidekick_arith_lra.Make(struct
module S = Solver
module T = BT.Term
type term = S.T.Term.t
type ty = S.T.Ty.t
let mk_eq = Form.eq
let mk_lra = T.lra
let view_as_lra t = match T.view t with
| T.LRA l -> l
| T.Eq (a,b) when Ty.equal (T.ty a) Ty.real -> LRA_pred (Eq, a, b)
| _ -> LRA_other t
let ty_lra _st = Ty.real
let has_ty_real t = Ty.equal (T.ty t) Ty.real
module Gensym = struct
type t = {
tst: T.state;
@ -323,6 +332,8 @@ module Th_lra = Sidekick_arith_lra.Make(struct
}
let create tst : t = {tst; fresh=0}
let tst self = self.tst
let copy s = {s with tst=s.tst}
let fresh_term (self:t) ~pre (ty:Ty.t) : T.t =
let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in

13
src/smtlib/Typecheck.ml
View file

@ -144,6 +144,10 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
errorf_ctx ctx "expected term, not type; got `%s`" f
end
end
| PA.App ("xor", [a;b]) ->
let a = conv_term ctx a in
let b = conv_term ctx b in
Form.xor ctx.tst a b
| PA.App (f, args) ->
let args = List.map (conv_term ctx) args in
begin match find_id_ ctx f with
@ -280,6 +284,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
| PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b))
| PA.Add, (a::l) ->
List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l
| PA.Minus, [a] ->
begin match t_as_q a with
| Some a -> T.lra ctx.tst (LRA_const (Q.neg a))
| None ->
T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a))
end
| PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b))
| PA.Minus, (a::l) ->
List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l
@ -294,9 +304,8 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
| PA.Div, [a;b] ->
begin match t_as_q a, t_as_q b with
| Some a, Some b -> T.lra ctx.tst (LRA_const (Q.div a b))
| Some a, _ -> T.lra ctx.tst (LRA_mult (Q.inv a, b))
| _, Some b -> T.lra ctx.tst (LRA_mult (Q.inv b, a))
| None, None ->
| _, None ->
errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t
end
| _ ->

3
src/smtlib/dune
View file

@ -3,5 +3,6 @@
(public_name sidekick-bin.smtlib)
(libraries containers zarith msat sidekick.core sidekick.util
sidekick.msat-solver sidekick-arith.base-term sidekick.th-bool-static
sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils)
sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils
sidekick.tef)
(flags :standard -warn-error -a+8 -open Sidekick_util))

74
src/tef/Sidekick_tef.ml Normal file
View file

@ -0,0 +1,74 @@
module P = Sidekick_util.Profile
let active = lazy (
match Sys.getenv "TEF" with
| "1"|"true" -> true | _ -> false
| exception Not_found -> false
)
let program_start = Mtime_clock.now()
module Make()
: P.BACKEND
= struct
let first_ = ref true
let closed_ = ref false
let teardown_ oc =
if not !closed_ then (
closed_ := true;
output_char oc ']'; (* close array *)
flush oc;
close_out_noerr oc
)
(* connection to subprocess writing into the file *)
let oc =
let oc = Unix.open_process_out "gzip - --stdout > trace.json.gz" in
output_char oc '[';
at_exit (fun () -> teardown_ oc);
oc
let get_ts () : float =
let now = Mtime_clock.now() in
Mtime.Span.to_us (Mtime.span program_start now)
let emit_sep_ () =
if !first_ then (
first_ := false;
) else (
output_string oc ",\n";
)
let emit_duration_event ~name ~start ~end_ () : unit =
let dur = end_ -. start in
let ts = start in
let pid = Unix.getpid() in
let tid = Thread.id (Thread.self()) in
emit_sep_();
Printf.fprintf oc
{json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":"%s","ph":"X"}|json}
pid tid dur ts name;
()
let emit_instant_event ~name ~ts () : unit =
let pid = Unix.getpid() in
let tid = Thread.id (Thread.self()) in
emit_sep_();
Printf.fprintf oc
{json|{"pid": %d,"cat":"","tid": %d,"ts": %.2f,"name":"%s","ph":"I"}|json}
pid tid ts name;
()
let teardown () = teardown_ oc
end
let setup_ = lazy (
let lazy active = active in
let b = if active then Some (module Make() : P.BACKEND) else None in
P.Control.setup b
)
let setup () = Lazy.force setup_
let teardown = P.Control.teardown

10
src/tef/Sidekick_tef.mli Normal file
View file

@ -0,0 +1,10 @@
(** {1 Tracing Event Format}
A nice profiling format based on json, useful for visualizing what goes on.
See https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/
*)
val setup : unit -> unit
val teardown : unit -> unit

8
src/tef/dune Normal file
View file

@ -0,0 +1,8 @@
(library
(name sidekick_tef)
(public_name sidekick.tef)
(synopsis "profiling backend based on TEF")
(optional)
(flags :standard -warn-error -a+8)
(libraries sidekick.util unix threads mtime mtime.clock.os))

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

@ -84,7 +84,7 @@ 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 option =
let tst = self.tst in
match A.view_as_bool t with
@ -133,18 +133,26 @@ module Make(A : ARG) : S with module A = A = struct
mk_lit t
(* preprocess "ite" away *)
let preproc_ite self _si ~mk_lit ~add_clause (t:T.t) : T.t option =
let preproc_ite self _si ~recurse ~mk_lit ~add_clause (t:T.t) : T.t option =
match A.view_as_bool t with
| B_ite (a,b,c) ->
let t_a = fresh_term self ~pre:"ite" (T.ty b) in
let lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
add_clause [lit_a; mk_lit (eq self.tst t_a c)];
Some t_a
let a = recurse a in
begin match A.view_as_bool a with
| B_bool true -> Some (recurse b)
| B_bool false -> Some (recurse c)
| _ ->
let t_a = fresh_term self ~pre:"ite" (T.ty b) in
let lit_a = mk_lit a in
let b = recurse b in
let c = recurse c in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
add_clause [lit_a; mk_lit (eq self.tst t_a c)];
Some t_a
end
| _ -> None
(* TODO: polarity? *)
let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
let cnf (self:state) (_si:SI.t) ~recurse:_ ~mk_lit ~add_clause (t:T.t) : T.t option =
let rec get_lit (t:T.t) : Lit.t =
let t_abs, t_sign = T.abs self.tst t in
let lit =
@ -217,6 +225,7 @@ module Make(A : ARG) : S with module A = A = struct
in
let cnf_of t =
cnf self si t
~recurse:(fun t -> t)
~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
in
begin

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

@ -390,7 +390,11 @@ module Make(A : ARG) : S with module A = A = struct
let pp_entry out (n,node) =
Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node
in
Fmt.fprintf out "(@[graph@ %a@])" (Fmt.iter pp_entry) (N_tbl.to_iter g)
if N_tbl.length g = 0 then (
Fmt.string out "(graph ø)"
) else (
Fmt.fprintf out "(@[graph@ %a@])" (Fmt.iter pp_entry) (N_tbl.to_iter g)
)
let mk_graph (self:t) cc : graph =
let g: graph = N_tbl.create ~size:32 () in

2
src/util/Backtrack_stack.ml
View file

@ -34,3 +34,5 @@ let pop_levels (self:_ t) (n:int) ~f : unit =
done;
Vec.shrink self.lvls new_lvl
)
let iter ~f self = Vec.iter f self.vec

2
src/util/Backtrack_stack.mli
View file

@ -19,3 +19,5 @@ val push_level : _ t -> unit
val pop_levels : 'a t -> int -> f:('a -> unit) -> unit
(** [pop_levels st n ~f] removes [n] levels, calling [f] on every removed item *)
val iter : f:('a -> unit) -> 'a t -> unit

102
src/util/Profile.ml Normal file
View file

@ -0,0 +1,102 @@
module type BACKEND = sig
val get_ts : unit -> float
val emit_duration_event :
name : string ->
start : float ->
end_ : float ->
unit ->
unit
val emit_instant_event :
name : string ->
ts : float ->
unit ->
unit
val teardown : unit -> unit
end
type backend = (module BACKEND)
type probe =
| No_probe
| Probe of {
name: string;
start: float;
}
let null_probe = No_probe
(* where to print events *)
let out_ : backend option ref = ref None
let begin_with_ (module B:BACKEND) name : probe =
Probe {name; start=B.get_ts ()}
let[@inline] begin_ name : probe =
match !out_ with
| None -> No_probe
| Some b -> begin_with_ b name
let[@inline] instant name =
match !out_ with
| None -> ()
| Some (module B) ->
let now = B.get_ts() in
B.emit_instant_event ~name ~ts:now ()
(* slow path *)
let exit_full_ (module B : BACKEND) name start =
let now = B.get_ts() in
B.emit_duration_event ~name ~start ~end_:now ()
let exit_with_ b pb =
match pb with
| No_probe -> ()
| Probe {name; start} -> exit_full_ b name start
let[@inline] exit pb =
match pb, !out_ with
| Probe {name;start}, Some b -> exit_full_ b name start
| _ -> ()
let[@inline] with_ name f =
match !out_ with
| None -> f()
| Some b ->
let pb = begin_with_ b name in
try
let x = f() in
exit_with_ b pb;
x
with e ->
exit_with_ b pb;
raise e
let[@inline] with1 name f x =
match !out_ with
| None -> f x
| Some b ->
let pb = begin_with_ b name in
try
let res = f x in
exit_with_ b pb;
res
with e ->
exit_with_ b pb;
raise e
module Control = struct
let setup b =
assert (!out_ = None);
out_ := b
let teardown () =
match !out_ with
| None -> ()
| Some (module B) ->
out_ := None;
B.teardown()
end

43
src/util/Profile.mli Normal file
View file

@ -0,0 +1,43 @@
(** {1 Profiling probes} *)
type probe
val null_probe : probe
val instant : string -> unit
val begin_ : string -> probe
val exit : probe -> unit
val with_ : string -> (unit -> 'a) -> 'a
val with1 : string -> ('a -> 'b) -> 'a -> 'b
module type BACKEND = sig
val get_ts : unit -> float
val emit_duration_event :
name : string ->
start : float ->
end_ : float ->
unit ->
unit
val emit_instant_event :
name : string ->
ts : float ->
unit ->
unit
val teardown : unit -> unit
end
type backend = (module BACKEND)
module Control : sig
val setup : backend option -> unit
val teardown : unit -> unit
end

1
src/util/Sidekick_util.ml
View file

@ -12,3 +12,4 @@ module Intf = Intf
module Bag = Bag
module Stat = Stat
module Hash = Hash
module Profile = Profile

537
tests/sat/broydn.c.i.broydn.pl.t2.fixed.t2.c_Iteration8_Loop_7-phaseTemplate.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

112
tests/sat/cpachecker-induction.1_3.c_false-unreach-call.i.smt2 Normal file
View file

@ -0,0 +1,112 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun |freePtr::ptr@3| () Real)
(declare-fun *signed_int@4 (Real) Real)
(declare-fun |getrr::__CPAchecker_TMP_0@3| () Real)
(declare-fun |getrr::r@2| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun *signed_int@3 (Real) Real)
(declare-fun |__ADDRESS_OF_main::ptr1| () Real)
(declare-fun |malloc#2| () Real)
(declare-fun |__ADDRESS_OF_getPtr::r| () Real)
(declare-fun |freePtr::ptr@2| () Real)
(declare-fun |__ADDRESS_OF_getrr::__CPAchecker_TMP_0| () Real)
(declare-fun |main::ptr1@2| () Real)
(declare-fun *signed_int@2 (Real) Real)
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1| () Real)
(declare-fun |__ADDRESS_OF_getrr::r| () Real)
(declare-fun |getPtr::__retval__@2| () Real)
(declare-fun |main::ptr1@3| () Real)
(declare-fun |getrr::__retval__@2| () Real)
(declare-fun |getPtr::r@3| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real |__ADDRESS_OF_main::ptr1|)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real |main::ptr1@2|)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real |__ADDRESS_OF_getPtr::r|)
(define-fun _15 () Real (__BASE_ADDRESS_OF__ _14))
(define-fun _16 () Bool (= _14 _15))
(define-fun _17 () Bool (and _13 _16))
(define-fun _18 () Real |__ADDRESS_OF_getrr::__CPAchecker_TMP_0|)
(define-fun _19 () Real (__BASE_ADDRESS_OF__ _18))
(define-fun _20 () Bool (= _18 _19))
(define-fun _21 () Bool (and _17 _20))
(define-fun _22 () Real |malloc#2|)
(define-fun _23 () Bool (= _22 _7))
(define-fun _24 () Bool (not _23))
(define-fun _27 () Real |getrr::__CPAchecker_TMP_0@3|)
(define-fun _30 () Real |__ADDRESS_OF_getrr::r|)
(define-fun _31 () Real (__BASE_ADDRESS_OF__ _30))
(define-fun _32 () Bool (= _30 _31))
(define-fun _35 () Real |getrr::r@2|)
(define-fun _36 () Bool (= _27 _35))
(define-fun _40 () Real (*signed_int@2 _35))
(define-fun _41 () Bool (= _40 _7))
(define-fun _43 () Real |getrr::__retval__@2|)
(define-fun _44 () Bool (= _35 _43))
(define-fun _46 () Real |getPtr::r@3|)
(define-fun _47 () Bool (= _43 _46))
(define-fun _49 () Real 1)
(define-fun _50 () Real (*signed_int@3 _46))
(define-fun _51 () Bool (= _50 _49))
(define-fun _59 () Real |getPtr::__retval__@2|)
(define-fun _60 () Bool (= _46 _59))
(define-fun _62 () Real |main::ptr1@3|)
(define-fun _63 () Bool (= _59 _62))
(define-fun _65 () Real |freePtr::ptr@2|)
(define-fun _66 () Bool (= _62 _65))
(define-fun _68 () Real (*signed_int@3 _65))
(define-fun _69 () Bool (= _68 _49))
(define-fun _75 () Real 2)
(define-fun _76 () Real (*signed_int@4 _65))
(define-fun _77 () Bool (= _76 _75))
(define-fun _84 () Real |freePtr::ptr@3|)
(define-fun _85 () Bool (= _62 _84))
(define-fun _87 () Real (*signed_int@4 _84))
(define-fun _88 () Bool (= _87 _49))
(define-fun _91 () Bool (not _88))
(define-fun _161 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#1|)
(define-fun _162 () Real (ite _24 _161 _7))
(define-fun _163 () Bool (= _27 _162))
(define-fun _164 () Bool (and _21 _163))
(define-fun _165 () Bool (<= _161 _7))
(define-fun _166 () Bool (not _165))
(define-fun _167 () Bool (and _32 _166))
(define-fun _168 () Bool (and _36 _167))
(define-fun _169 () Bool (and _164 _168))
(define-fun _170 () Bool (and _41 _169))
(define-fun _171 () Bool (and _44 _170))
(define-fun _172 () Bool (and _47 _171))
(define-fun _173 () Bool (= _46 _161))
(define-fun _174 () Real (*signed_int@3 _161))
(define-fun _175 () Real (*signed_int@2 _161))
(define-fun _176 () Bool (= _174 _175))
(define-fun _177 () Bool (or _173 _176))
(define-fun _178 () Bool (and _51 _177))
(define-fun _179 () Bool (and _172 _178))
(define-fun _180 () Bool (and _60 _179))
(define-fun _181 () Bool (and _63 _180))
(define-fun _182 () Bool (and _66 _181))
(define-fun _183 () Bool (and _69 _182))
(define-fun _184 () Bool (= _65 _161))
(define-fun _185 () Real (*signed_int@4 _161))
(define-fun _186 () Bool (= _174 _185))
(define-fun _187 () Bool (or _184 _186))
(define-fun _188 () Bool (and _77 _187))
(define-fun _189 () Bool (and _183 _188))
(define-fun _190 () Bool (and _85 _189))
(define-fun _191 () Bool (and _91 _190))
(assert _191)
(check-sat)
(exit)

4116
tests/sat/cpachecker-induction.32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--joystick--magellan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2 Normal file
View file

File diff suppressed because it is too large Load diff

1145
tests/sat/cpachecker-induction.minepump_spec1_product33_false-unreach-call.cil.c.smt2 Normal file
View file

File diff suppressed because it is too large Load diff

6135
tests/sat/disj_nightmare.t2.c_Iteration1_Loop_3-pieceTemplate.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

27
tests/sat/polypaver-bench-exp-3d-chunk-0032.smt2 Normal file
View file

@ -0,0 +1,27 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source |
These benchmarks used in the paper:
Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic.
In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
The meti-tarski benchmarks are proof obligations extracted from the
Meti-Tarski project, see:
B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
for real-valued special functions. Journal of Automated Reasoning,
44(3):175-205, 2010.
Submitted by Dejan Jovanovic for SMT-LIB.
|)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun skoZ () Real)
(declare-fun skoY () Real)
(declare-fun skoX () Real)
(assert (let ((?v_0 (* skoX (- 1))) (?v_1 (* skoY (- 1)))) (and (<= (+ ?v_0 ?v_1) skoZ) (and (not (<= skoZ (+ (+ (/ 3 2) ?v_0) ?v_1))) (and (<= skoZ 1) (and (<= skoY 1) (and (<= skoX 1) (and (<= 0 skoZ) (and (<= 0 skoY) (<= 0 skoX))))))))))
(check-sat)
(exit)

203
tests/sat/uart-10.induction.cvc.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

16
tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2 Normal file
View file

@ -0,0 +1,16 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(assert (let ((?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_2 (not (<= (- 1 1) (+ (+ (+ x_5 x_6) (* (* (+ x_7 x_4) 2) (/ 1 999))) (/ 2335 666)))))) (and (and (and (and (and (and (and (and (and (and (and (not (<= x_3 0)) (not (<= x_4 0))) (not (<= x_5 0))) (not (< x_6 (+ x_5 (* (* (+ (* (* x_4 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_7 (- (* (* (- (- x_4 x_6) 1) 999) (/ 1 2)) 1))) (not (< x_7 (* (* (+ (+ (+ x_3 x_5) x_6) (/ 1501 1000)) 1001) (/ 1 999))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (or (or (or ?v_2 ?v_2) ?v_2) ?v_2))))
(check-sat)
(exit)

79
tests/unsat/pb_real_30_0600_10_18.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

95
tests/unsat/pb_real_40_80_60_01.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

36
tests/unsat/reg_lra_fm1.smt2 Normal file
View file

@ -0,0 +1,36 @@
; expect: unsat
; intermediate problem in tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2
(set-logic QF_LRA)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(assert (< (+ (/ 2335 666) x_5 x_6 (* (/ 2 999) x_7) (* (/ 2 999) x_4)) 0))
(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_2) 0))
(assert (<= (+ (/ 999 1000) x_0 (* -1 x_2)) 0))
(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_1) 0))
(assert (<= (+ (/ 999 1000) x_0 (- 0 x_1)) 0))
(assert (= x_0 0))
(assert
(<= (+
(/ 1502501 999000)
(* (/ 1001 999) x_5)
(* (/ 1001 999) x_6)
(* -1 x_7)
(* (/ 1001 999) x_3))
0))
(assert (< (+ (/ 1001 2) (* (/ 999 2) x_6) x_7 (* (/ -999 2) x_4)) 0))
(assert (<= (+ (/ 1001 999) x_5 (* -1 x_6) (* (/ 1001 1998) x_4)) 0))
(assert (< (* -1 x_5) 0))
(assert (< (* -1 x_4) 0))
(assert (< (* -1 x_3) 0))
(check-sat)

6
tests/unsat/reg_uflra.smt2 Normal file
View file

@ -0,0 +1,6 @@
(set-logic QF_UFLRA)
(set-info :status unsat)
(declare-fun f0_2 (Real Real) Real)
(assert (and (not (< (f0_2 (- 0.0 0.0) 0.0) 10)) (< (f0_2 0.0 0.0) 0)))
(check-sat)
(exit)

144
tests/unsat/sc-6.base.cvc.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

27
tests/unsat/simple_example_1-node2318.smt2 Normal file
View file

@ -0,0 +1,27 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source |
These benchmarks used in the paper:
Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic.
In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
The keymaera family contains VCs from Keymaera verification, see:
A. Platzer, J.-D. Quesel, and P. Rummer. Real world verification.
In CADE 2009, pages 485-501. Springer, 2009.
Submitted by Dejan Jovanovic for SMT-LIB.
KeYmaera example: simple_example_1, node 2318 For more info see: No further information available.
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun e () Real)
(declare-fun buscore2dollarskuscore1 () Real)
(declare-fun duscore2dollarskuscore1 () Real)
(declare-fun cuscore2dollarskuscore1 () Real)
(declare-fun auscore2dollarskuscore1 () Real)
(assert (not (=> (and (and (= e 0) (= (* 2 auscore2dollarskuscore1) buscore2dollarskuscore1)) (= cuscore2dollarskuscore1 duscore2dollarskuscore1)) (= (+ cuscore2dollarskuscore1 1) (+ duscore2dollarskuscore1 1)))))
(check-sat)
(exit)

16
tests/unsat/smtlib.624916.smt2 Normal file
View file

@ -0,0 +1,16 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 () Real)
(assert (not (= f1 f2)))
(assert (= (f3 f4) (- 1)))
(assert (not (=> (= f5 f4) (not (= (f3 f5) 1.0)))))
(check-sat)
(exit)