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

make it compile! with stubs for conversion parse ast -> ast -> term

Browse source
This commit is contained in:
Simon Cruanes 2018-02-08 22:19:32 -06:00
parent f52883f059
commit 7b44146102
22 changed files with 886 additions and 889 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/main/main.ml
View file

@ -10,6 +10,7 @@ module E = CCResult
module Fmt = CCFormat
module Term = Dagon_smt.Term
module Ast = Dagon_smt.Ast
module Solver = Dagon_smt.Solver
type 'a or_error = ('a, string) E.t
@ -30,12 +31,10 @@ let p_stat = ref false
let p_gc_stat = ref false
let p_progress = ref false
(* FIXME
module Dot = CDCL_backend.Dot.Make(CDCL_backend.Dot.Default(Sat))
*)
let hyps : Ast.term list ref = ref []
module Dot = Dagon_backend.Dot.Make(Solver.Sat_solver.Proof)(Dagon_backend.Dot.Default(Solver.Sat_solver.Proof))
let check_model _state =
let check_clause _c =
true
@ -138,7 +137,7 @@ let main () =
try
E.fold_l
(fun () ->
Dagon_smtlib.process_stmt
Dagon_smt.Process.process_stmt
~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
~time:!time_limit ~memory:!size_limit
?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress

2
src/sat/Solver.ml
View file

@ -87,7 +87,7 @@ module Make
let[@inline] add_clause st c : unit =
cleanup_ st;
S.add_clause st c
S.assume st [c]
let solve (st:t) ?(assumptions=[]) () =
cleanup_ st;

2
src/sat/Solver_intf.ml
View file

@ -88,7 +88,7 @@ module type S = sig
Modifies the sat solver state in place. *)
(* TODO: provide a local, backtrackable version *)
val add_clause : t -> clause -> unit
val add_clause : t -> atom list -> unit
(** Lower level addition of clauses *)
val solve : t -> ?assumptions:atom list -> unit -> res

8
src/smt/Ast.ml
View file

@ -139,7 +139,7 @@ and term_cell =
| Let of (var * term) list * term
| Not of term
| Op of op * term list
| Asserting of term * term
| Asserting of {t: term; guard: term}
| Undefined_value
| Bool of bool
@ -232,8 +232,8 @@ let pp_term =
| Arith (op, l) ->
Fmt.fprintf out "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp) l
| Undefined_value -> Fmt.string out "<undefined>"
| Asserting (t, g) ->
Fmt.fprintf out "(@[asserting@ %a@ %a@])" pp t pp g
| Asserting {t;guard} ->
Fmt.fprintf out "(@[asserting@ %a@ %a@])" pp t pp guard
and pp_vbs out l =
let pp_vb out (v,t) = Fmt.fprintf out "(@[%a@ %a@])" Var.pp v pp t in
@ -267,7 +267,7 @@ let asserting t g =
if not (Ty.equal Ty.prop g.ty) then (
Ty.ill_typed "asserting: test must have type prop, not `@[%a@]`" Ty.pp g.ty;
);
mk_ (Asserting (t,g)) t.ty
mk_ (Asserting {t;guard=g}) t.ty
let var v = mk_ (Var v) (Var.ty v)
let const id ty = mk_ (Const id) ty

2
src/smt/Ast.mli
View file

@ -106,7 +106,7 @@ and term_cell =
| Let of (var * term) list * term
| Not of term
| Op of op * term list
| Asserting of term * term
| Asserting of {t: term; guard: term}
| Undefined_value
| Bool of bool

6
src/smt/Model.ml
View file

@ -141,8 +141,8 @@ let apply_subst (subst:subst) t =
A.bind ~ty:(A.ty t) b x' (aux subst' body)
| A.Not f -> A.not_ (aux subst f)
| A.Op (op,l) -> A.op op (List.map (aux subst) l)
| A.Asserting (t,g) ->
A.asserting (aux subst t)(aux subst g)
| A.Asserting {t;guard} ->
A.asserting (aux subst t) (aux subst guard)
| A.Arith (op,l) ->
let ty = A.ty t in
A.arith ty op (List.map (aux subst) l)
@ -287,7 +287,7 @@ and eval_whnf_rec m st subst t = match A.term_view t with
| A.Bool false -> A.true_
| _ -> A.not_ f
end
| A.Asserting (u, g) ->
| A.Asserting {t=u; guard=g} ->
let g' = eval_whnf m st subst g in
begin match A.term_view g' with
| A.Bool true -> eval_whnf m st subst u

689
src/smt/Process.ml Normal file
View file

@ -0,0 +1,689 @@
(** {2 Conversion into {!Term.t}} *)
type 'a or_error = ('a, string) CCResult.t
module E = CCResult
module A = Ast
module Fmt = CCFormat
module Subst = struct
type 'a t = 'a ID.Map.t
let empty = ID.Map.empty
let mem subst v = ID.Map.mem (A.Var.id v) subst
let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out
let add subst v t =
if mem subst v then (
Util.errorf "%a already bound" A.Var.pp v;
);
ID.Map.add (A.Var.id v) t subst
let find subst v = ID.Map.get (A.Var.id v) subst
let find_exn subst v = ID.Map.find (A.Var.id v) subst
end
module Conv = struct
let conv_ty (ty:A.Ty.t) : Ty.t =
let mk_ty id = Ty.atomic id Ty.Uninterpreted ~card:(lazy Ty_card.infinite) in
(* convert a type *)
let rec aux_ty (ty:A.Ty.t) : Ty.t = match ty with
| A.Ty.Prop -> Ty.prop
(* | A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat *)
| A.Ty.App (id, []) -> mk_ty id
| A.Ty.App (_, _) ->
Util.errorf "cannot convert parametrized type %a" A.Ty.pp ty
| A.Ty.Arrow _ ->
Util.errorf "cannot convert arrow type `%a`" A.Ty.pp ty
in
aux_ty ty
let conv_term (tst:Term.state) (t:A.term): Term.t =
(* polymorphic equality *)
let mk_eq t u = Term.eq tst t u in
let mk_app f l = Term.app_cst tst f (IArray.of_list l) in
let mk_const = Term.const tst in
(*
let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in
let mk_lra_eq t u = mk_lra_pred Mc2_lra.Eq0 (RLE.diff t u) |> Term.Bool.pa in
let side_clauses : atom list list ref = ref [] in
(* introduce intermediate variable for LRA sub-expression *)
let mk_lra_expr (e:RLE.t): term = match RLE.as_const e, RLE.as_singleton e with
| Some n, _ -> Reg.find_exn reg Mc2_lra.k_make_const n
| None, Some (n,t) when Q.equal n Q.one -> t
| _ ->
let id = mk_lra_id() in
Log.debugf 30
(fun k->k"(@[smtlib.name_lra@ %a@ :as %a@])" RLE.pp e ID.pp id);
decl id [] (Reg.find_exn reg Mc2_lra.k_rat);
let t = mk_const id in
side_clauses := [mk_lra_eq (RLE.singleton1 t) e] :: !side_clauses;
t
in
(* adaptative equality *)
let mk_eq_t_tf (t:term) (u:term_or_form) : F.t = match u with
| F u -> F.equiv (F.atom (Term.Bool.pa t)) u
| T u when Term.is_bool u ->
F.equiv (F.atom (Term.Bool.pa t)) (F.atom (Term.Bool.pa u))
| T u -> mk_eq t u |> F.atom
| Rat u -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
and mk_eq_tf_tf (t:term_or_form) (u:term_or_form) = match t, u with
| T t, T u -> mk_eq t u |> F.atom
| T t, Rat u | Rat u, T t -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
| Rat t, Rat u -> mk_lra_eq t u |> F.atom
| F t, F u -> F.equiv t u
| _ -> assert false
in
*)
(* convert term.
@param subst used to expand let-bindings on the fly *)
let rec aux (subst:Term.t Subst.t) (t:A.term) : Term.t =
let ty = A.ty t |> conv_ty in
begin match A.term_view t with
| A.Var v ->
begin match Subst.find subst v with
| None -> Util.errorf "variable %a not bound" A.Var.pp v
| Some t -> t
end
| A.Const id ->
mk_const (Cst.make_undef id ty)
| A.App (f, l) ->
let l = List.map (aux subst) l in
begin match A.term_view f with
| A.Const id ->
(* TODO: lookup definition of [f] *)
mk_app (Cst.make_undef id (A.ty f |> conv_ty)) l
| _ -> Util.errorf "cannot process HO application %a" A.pp_term t
end
| A.If (a,b,c) ->
let a = aux subst a in
let b = aux subst b in
let c = aux subst c in
Term.if_ tst a b c
| A.Let (vbs,u) ->
let subst =
List.fold_left
(fun s (v,t) -> Subst.add s v (aux subst t))
subst vbs
in
aux subst u
| A.Op (A.And, l) -> Term.and_l tst (List.map (aux subst) l)
| A.Op (A.Or, l) -> Term.or_l tst (List.map (aux subst) l)
| A.Op (A.Imply, l) ->
let l = List.map (aux subst) l in
begin match List.rev l with
| [] -> Term.true_ tst
| ret :: hyps ->
Term.imply tst hyps ret
end
| A.Op (A.Eq, l) ->
let l = List.map (aux subst) l in
let rec curry_eq = function
| [] | [_] -> assert false
| [a;b] -> [mk_eq a b]
| a :: b :: tail ->
mk_eq a b :: curry_eq (b::tail)
in
Term.and_l tst (curry_eq l)
| A.Op (A.Distinct, l) ->
Term.distinct tst @@ List.map (aux subst) l
| A.Not f -> Term.not_ tst (aux subst f)
| A.Bool true -> Term.true_ tst
| A.Bool false -> Term.false_ tst
| A.Num_q _n -> assert false (* TODO Mc2_lra.LE.const n |> ret_rat *)
| A.Num_z _n -> assert false (* TODO Mc2_lra.LE.const (Q.of_bigint n) |> ret_rat *)
| A.Arith (_op, _l) ->
assert false
(* TODO
let l = List.map (aux_rat subst) l in
begin match op, l with
| A.Minus, [a] -> RLE.neg a |> ret_rat
| _, [] | _, [_] ->
Util.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t
| A.Leq, [a;b] ->
let e = RLE.diff a b in
mk_lra_pred Mc2_lra.Leq0 e |> ret_any
| A.Geq, [a;b] ->
let e = RLE.diff b a in
mk_lra_pred Mc2_lra.Leq0 e |> ret_any
| A.Lt, [a;b] ->
let e = RLE.diff a b in
mk_lra_pred Mc2_lra.Lt0 e |> ret_any
| A.Gt, [a;b] ->
let e = RLE.diff b a in
mk_lra_pred Mc2_lra.Lt0 e |> ret_any
| (A.Leq | A.Lt | A.Geq | A.Gt), _ ->
Util.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t
| A.Add, _ ->
let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in
mk_lra_expr e |> ret_t
| A.Minus, a::tail ->
let e =
List.fold_left
(fun n t -> RLE.diff n t)
a tail
in
mk_lra_expr e |> ret_t
| A.Mult, _::_::_ ->
let coeffs, terms =
CCList.partition_map
(fun t -> match RLE.as_const t with
| None -> `Right t
| Some c -> `Left c)
l
in
begin match coeffs, terms with
| c::c_tail, [] ->
List.fold_right RLE.mult c_tail (RLE.const c) |> ret_rat
| _, [t] ->
List.fold_right RLE.mult coeffs t |> ret_rat
| _ ->
Util.errorf "non-linear expr:@ `%a`" A.pp_term t
end
| A.Div, (first::l) ->
(* support t/a/b/c where only [t] is a rational *)
let coeffs =
List.map
(fun c -> match RLE.as_const c with
| None ->
Util.errorf "non-linear expr:@ `%a`" A.pp_term t
| Some c -> Q.inv c)
l
in
List.fold_right RLE.mult coeffs first |> ret_rat
end
*)
| A.Select _ -> assert false (* TODO *)
| A.Match _ -> assert false (* TODO *)
| A.Bind _ -> assert false (* TODO *)
| A.Undefined_value -> assert false (* TODO *)
| A.Asserting _ -> assert false (* TODO *)
end
in
aux Subst.empty t
end
let conv_ty = Conv.conv_ty
let conv_term = Conv.conv_term
(* call the solver to check-sat *)
let solve
?gc:_
?restarts:_
?dot_proof:_
?(pp_model=false)
?(check=false)
?time:_ ?memory:_ ?progress:_
~assumptions s : unit =
let t1 = Sys.time() in
let res =
Solver.solve ~assumptions s
(* ?gc ?restarts ?time ?memory ?progress s *)
in
let t2 = Sys.time () in
begin match res with
| Solver.Sat m ->
if pp_model then (
Format.printf "(@[<hv1>model@ %a@])@." Model.pp m
);
if check then (
(* TODO
if not (check_model m) then (
Util.error "invalid model"
)
*)
);
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat _pr ->
(*
if check then (
Solver.Proof.check p;
begin match dot_proof with
| None -> ()
| Some file ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.print fmt p;
Format.pp_print_flush fmt (); flush oc)
end
);
*)
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unknown reas ->
Format.printf "Unknown (:reason %a)" Solver.pp_unknown reas
end
(* process a single statement *)
let process_stmt
?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
?time ?memory ?progress
(solver:Solver.t)
(stmt:Ast.statement) : unit or_error =
Log.debugf 5
(fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt);
let tst = Solver.tst solver in
let decl_sort _ _ : unit = assert false in (* TODO *)
let decl _id _args _ret : unit = assert false in (* TODO *)
begin match stmt with
| A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return ()
| A.SetLogic s ->
Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
E.return ()
| A.SetOption l ->
Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l);
E.return ()
| A.SetInfo _ -> E.return ()
| A.Exit ->
Log.debug 1 "exit";
raise Exit
| A.CheckSat ->
solve ?gc ?restarts ?dot_proof ?check ?pp_model ?time ?memory ?progress
solver ~assumptions:[];
E.return()
| A.TyDecl (id,n) ->
decl_sort id n;
E.return ()
| A.Decl (f,ty) ->
let ty_args, ty_ret = A.Ty.unfold ty in
let ty_args = List.map conv_ty ty_args in
let ty_ret = conv_ty ty_ret in
decl f ty_args ty_ret;
E.return ()
| A.Assert t ->
let t = conv_term tst t in
if pp_cnf then (
Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
);
(* TODO
hyps := clauses @ !hyps;
*)
Solver.assume solver (Clause.make [Lit.atom t]);
E.return()
| A.Goal (_, _) ->
Util.errorf "cannot deal with goals yet"
| A.Data _ ->
Util.errorf "cannot deal with datatypes yet"
| A.Define _ ->
Util.errorf "cannot deal with definitions yet"
end
(* FIXME: merge this
module Conv : sig
val add_statement : Ast.statement -> unit
val add_statement_l : Ast.statement list -> unit
val ty_to_ast: Ty.t -> Ast.Ty.t
val term_to_ast: term -> Ast.term
end = struct
(* for converting Ast.Ty into Ty *)
let ty_tbl_ : Ty.t lazy_t ID.Tbl.t = ID.Tbl.create 16
(* for converting constants *)
let decl_ty_ : cst lazy_t ID.Tbl.t = ID.Tbl.create 16
(* environment for variables *)
type conv_env = {
let_bound: (term * int) ID.Map.t;
(* let-bound variables, to be replaced. int=depth at binding position *)
bound: (int * Ty.t) ID.Map.t;
(* set of bound variables. int=depth at binding position *)
depth: int;
}
let empty_env : conv_env =
{let_bound=ID.Map.empty; bound=ID.Map.empty; depth=0}
let rec conv_ty (ty:Ast.Ty.t): Ty.t = match ty with
| Ast.Ty.Prop -> Ty.prop
| Ast.Ty.Const id ->
begin try ID.Tbl.find ty_tbl_ id |> Lazy.force
with Not_found -> Util.errorf "type %a not in ty_tbl" ID.pp id
end
| Ast.Ty.Arrow (a,b) -> Ty.arrow (conv_ty a) (conv_ty b)
let add_bound env v =
let ty = Ast.Var.ty v |> conv_ty in
{ env with
depth=env.depth+1;
bound=ID.Map.add (Ast.Var.id v) (env.depth,ty) env.bound; }
(* add [v := t] to bindings. Depth is not incremented
(there will be no binders) *)
let add_let_bound env v t =
{ env with
let_bound=ID.Map.add (Ast.Var.id v) (t,env.depth) env.let_bound }
let find_env env v =
let id = Ast.Var.id v in
ID.Map.get id env.let_bound, ID.Map.get id env.bound
let rec conv_term_rec
(env: conv_env)
(t:Ast.term): term = match Ast.term_view t with
| Ast.Bool true -> Term.true_
| Ast.Bool false -> Term.false_
| Ast.Unknown _ -> assert false
| Ast.Const id ->
begin
try ID.Tbl.find decl_ty_ id |> Lazy.force |> Term.const
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
end
| Ast.App (f, l) ->
begin match Ast.term_view f with
| Ast.Const id ->
let f =
try ID.Tbl.find decl_ty_ id |> Lazy.force
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
in
let l = List.map (conv_term_rec env) l in
if List.length l = fst (Ty.unfold_n (Cst.ty f))
then Term.app_cst f (IArray.of_list l) (* fully applied *)
else Term.app (Term.const f) l
| _ ->
let f = conv_term_rec env f in
let l = List.map (conv_term_rec env) l in
Term.app f l
end
| Ast.Var v ->
(* look whether [v] must be replaced by some term *)
begin match AstVarMap.get v env.subst with
| Some t -> t
| None ->
(* lookup as bound variable *)
begin match CCList.find_idx (Ast.Var.equal v) env.bound with
| None -> errorf "could not find var `%a`" Ast.Var.pp v
| Some (i,_) ->
let ty = Ast.Var.ty v |> conv_ty in
Term.db (DB.make i ty)
end
end
| Ast.Bind (Ast.Fun,v,body) ->
let body = conv_term_rec {env with bound=v::env.bound} body in
let ty = Ast.Var.ty v |> conv_ty in
Term.fun_ ty body
| Ast.Bind ((Ast.Forall | Ast.Exists),_, _) ->
errorf "quantifiers not supported"
| Ast.Bind (Ast.Mu,v,body) ->
let env' = add_bound env v in
let body = conv_term_rec env' body in
Term.mu body
| Ast.Select _ -> assert false (* TODO *)
| Ast.Match (u,m) ->
let any_rhs_depends_vars = ref false in (* some RHS depends on matched arg? *)
let m =
ID.Map.map
(fun (vars,rhs) ->
let n_vars = List.length vars in
let env', tys =
CCList.fold_map
(fun env v -> add_bound env v, Ast.Var.ty v |> conv_ty)
env vars
in
let rhs = conv_term_rec env' rhs in
let depends_on_vars =
Term.to_seq_depth rhs
|> Sequence.exists
(fun (t,k) -> match t.term_cell with
| DB db ->
DB.level db < n_vars + k (* [k]: number of intermediate binders *)
| _ -> false)
in
if depends_on_vars then any_rhs_depends_vars := true;
tys, rhs)
m
in
(* optim: check whether all branches return the same term, that
does not depend on matched variables *)
(* TODO: do the closedness check during conversion, above *)
let rhs_l =
ID.Map.values m
|> Sequence.map snd
|> Sequence.sort_uniq ~cmp:Term.compare
|> Sequence.to_rev_list
in
begin match rhs_l with
| [x] when not (!any_rhs_depends_vars) ->
(* every branch yields the same [x], which does not depend
on the argument: remove the match and return [x] instead *)
x
| _ ->
let u = conv_term_rec env u in
Term.match_ u m
end
| Ast.Switch _ ->
errorf "cannot convert switch %a" Ast.pp_term t
| Ast.Let (v,t,u) ->
(* substitute on the fly *)
let t = conv_term_rec env t in
let env' = add_let_bound env v t in
conv_term_rec env' u
| Ast.If (a,b,c) ->
let b = conv_term_rec env b in
let c = conv_term_rec env c in
(* optim: [if _ b b --> b] *)
if Term.equal b c
then b
else Term.if_ (conv_term_rec env a) b c
| Ast.Not t -> Term.not_ (conv_term_rec env t)
| Ast.Binop (op,a,b) ->
let a = conv_term_rec env a in
let b = conv_term_rec env b in
begin match op with
| Ast.And -> Term.and_ a b
| Ast.Or -> Term.or_ a b
| Ast.Imply -> Term.imply a b
| Ast.Eq -> Term.eq a b
end
| Ast.Undefined_value ->
Term.undefined_value (conv_ty t.Ast.ty) Undef_absolute
| Ast.Asserting (t, g) ->
(* [t asserting g] becomes [if g t fail] *)
let t = conv_term_rec env t in
let g = conv_term_rec env g in
Term.if_ g t (Term.undefined_value t.term_ty Undef_absolute)
let add_statement st =
Log.debugf 2
(fun k->k "(@[add_statement@ @[%a@]@])" Ast.pp_statement st);
model_env_ := Ast.env_add_statement !model_env_ st;
begin match st with
| Ast.Assert t ->
let t = conv_term_rec empty_env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.Goal (vars, t) ->
(* skolemize *)
let env, consts =
CCList.fold_map
(fun env v ->
let ty = Ast.Var.ty v |> conv_ty in
let c = Cst.make_undef (Ast.Var.id v) ty in
{env with subst=AstVarMap.add v (Term.const c) env.subst}, c)
empty_env
vars
in
(* model should contain values of [consts] *)
List.iter add_cst_support_ consts;
let t = conv_term_rec env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.TyDecl id ->
let ty = Ty.atomic id Uninterpreted ~card:(Lazy.from_val Infinite) in
add_ty_support_ ty;
ID.Tbl.add ty_tbl_ id (Lazy.from_val ty)
| Ast.Decl (id, ty) ->
assert (not (ID.Tbl.mem decl_ty_ id));
let ty = conv_ty ty in
let cst = Cst.make_undef id ty in
add_cst_support_ cst; (* need it in model *)
ID.Tbl.add decl_ty_ id (Lazy.from_val cst)
| Ast.Data l ->
(* the datatypes in [l]. Used for computing cardinalities *)
let in_same_block : ID.Set.t =
List.map (fun {Ast.Ty.data_id; _} -> data_id) l |> ID.Set.of_list
in
(* declare the type, and all the constructors *)
List.iter
(fun {Ast.Ty.data_id; data_cstors} ->
let ty = lazy (
let card_ : ty_card ref = ref Finite in
let cstors = lazy (
data_cstors
|> ID.Map.map
(fun c ->
let c_id = c.Ast.Ty.cstor_id in
let ty_c = conv_ty c.Ast.Ty.cstor_ty in
let ty_args, ty_ret = Ty.unfold ty_c in
(* add cardinality of [c] to the cardinality of [data_id].
(product of cardinalities of args) *)
let cstor_card =
ty_args
|> List.map
(fun ty_arg -> match ty_arg.ty_cell with
| Atomic (id, _) when ID.Set.mem id in_same_block ->
Infinite
| _ -> Lazy.force ty_arg.ty_card)
|> Ty_card.product
in
card_ := Ty_card.( !card_ + cstor_card );
let rec cst = lazy (
Cst.make_cstor c_id ty_c cstor
) and cstor = lazy (
let cstor_proj = lazy (
let n = ref 0 in
List.map2
(fun id ty_arg ->
let ty_proj = Ty.arrow ty_ret ty_arg in
let i = !n in
incr n;
Cst.make_proj id ty_proj cstor i)
c.Ast.Ty.cstor_proj ty_args
|> IArray.of_list
) in
let cstor_test = lazy (
let ty_test = Ty.arrow ty_ret Ty.prop in
Cst.make_tester c.Ast.Ty.cstor_test ty_test cstor
) in
{ cstor_ty=ty_c; cstor_cst=Lazy.force cst;
cstor_args=IArray.of_list ty_args;
cstor_proj; cstor_test; cstor_card; }
) in
ID.Tbl.add decl_ty_ c_id cst; (* declare *)
Lazy.force cstor)
)
in
let data = { data_cstors=cstors; } in
let card = lazy (
ignore (Lazy.force cstors);
let r = !card_ in
Log.debugf 5
(fun k->k "(@[card_of@ %a@ %a@])" ID.pp data_id Ty_card.pp r);
r
) in
Ty.atomic data_id (Data data) ~card
) in
ID.Tbl.add ty_tbl_ data_id ty;
)
l;
(* force evaluation *)
List.iter
(fun {Ast.Ty.data_id; _} ->
let lazy ty = ID.Tbl.find ty_tbl_ data_id in
ignore (Lazy.force ty.ty_card);
begin match ty.ty_cell with
| Atomic (_, Data {data_cstors=lazy _; _}) -> ()
| _ -> assert false
end)
l
| Ast.Define (k,l) ->
(* declare the mutually recursive functions *)
List.iter
(fun (id,ty,rhs) ->
let ty = conv_ty ty in
let rhs = lazy (conv_term_rec empty_env rhs) in
let k = match k with
| Ast.Recursive -> Cst_recursive
| Ast.Non_recursive -> Cst_non_recursive
in
let cst = lazy (
Cst.make_defined id ty rhs k
) in
ID.Tbl.add decl_ty_ id cst)
l;
(* force thunks *)
List.iter
(fun (id,_,_) -> ignore (ID.Tbl.find decl_ty_ id |> Lazy.force))
l
end
let add_statement_l = List.iter add_statement
module A = Ast
let rec ty_to_ast (t:Ty.t): A.Ty.t = match t.ty_cell with
| Prop -> A.Ty.Prop
| Atomic (id,_) -> A.Ty.const id
| Arrow (a,b) -> A.Ty.arrow (ty_to_ast a) (ty_to_ast b)
let fresh_var =
let n = ref 0 in
fun ty ->
let id = ID.makef "x%d" !n in
incr n;
A.Var.make id (ty_to_ast ty)
let with_var ty env ~f =
let v = fresh_var ty in
let env = DB_env.push (A.var v) env in
f v env
let term_to_ast (t:term): Ast.term =
let rec aux env t = match t.term_cell with
| True -> A.true_
| False -> A.false_
| DB d ->
begin match DB_env.get d env with
| Some t' -> t'
| None -> errorf "cannot find DB %a in env" Term.pp t
end
| App_cst (f, args) when IArray.is_empty args ->
A.const f.cst_id (ty_to_ast t.term_ty)
| App_cst (f, args) ->
let f = A.const f.cst_id (ty_to_ast (Cst.ty f)) in
let args = IArray.map (aux env) args in
A.app f (IArray.to_list args)
| App_ho (f,l) -> A.app (aux env f) (List.map (aux env) l)
| Fun (ty,bod) ->
with_var ty env
~f:(fun v env -> A.fun_ v (aux env bod))
| Mu _ -> assert false
| If (a,b,c) -> A.if_ (aux env a)(aux env b) (aux env c)
| Case (u,m) ->
let u = aux env u in
let m =
ID.Map.mapi
(fun _c_id _rhs ->
assert false (* TODO: fetch cstor; bind variables; convert rhs *)
(*
with_vars tys env ~f:(fun vars env -> vars, aux env rhs)
*)
)
m
in
A.match_ u m
| Builtin b ->
begin match b with
| B_not t -> A.not_ (aux env t)
| B_and (a,b) -> A.and_ (aux env a) (aux env b)
| B_or (a,b) -> A.or_ (aux env a) (aux env b)
| B_eq (a,b) -> A.eq (aux env a) (aux env b)
| B_imply (a,b) -> A.imply (aux env a) (aux env b)
end
in aux DB_env.empty t
end
*)

24
src/smt/Process.mli Normal file
View file

@ -0,0 +1,24 @@
(** {1 Process Statements} *)
type 'a or_error = ('a, string) CCResult.t
(* TODO: record type for config *)
val conv_ty : Ast.Ty.t -> Ty.t
val conv_term : Term.state -> Ast.term -> Term.t
val process_stmt :
?gc:bool ->
?restarts:bool ->
?pp_cnf:bool ->
?dot_proof:string ->
?pp_model:bool ->
?check:bool ->
?time:float ->
?memory:float ->
?progress:bool ->
Solver.t ->
Ast.statement ->
unit or_error

476
src/smt/Solver.ml
View file

@ -5,16 +5,6 @@
open Solver_types
type term = Term.t
type cst = Cst.t
type ty = Ty.t
type ty_def = Solver_types.ty_def
type ty_cell = Solver_types.ty_cell =
| Prop
| Atomic of ID.t * ty_def
| Arrow of ty * ty
let get_time : unit -> float = Sys.time
(** {2 The Main Solver} *)
@ -23,6 +13,37 @@ type level = int
module Sat_solver = Dagon_sat.Make(Theory_combine)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t =
Sat_solver.Clause.atoms_l c |> Clause.make
module Proof = struct
type t = Sat_solver.Proof.proof
let pp out (p:t) : unit =
let pp_step_res out p =
let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
let conclusion = clause_of_mclause conclusion in
Clause.pp out conclusion
in
let pp_step out = function
| Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
| Sat_solver.Proof.Resolution (p1, p2, _) ->
Format.fprintf out "(@[<1>resolution@ %a@ %a@])"
pp_step_res p1 pp_step_res p2
| _ -> Fmt.string out "<other>"
in
Format.fprintf out "(@[<v>";
Sat_solver.Proof.fold
(fun () {Sat_solver.Proof.conclusion; step } ->
let conclusion = clause_of_mclause conclusion in
Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
Clause.pp conclusion pp_step step)
() p;
Format.fprintf out "@])";
()
end
(* main solver state *)
type t = {
solver: Sat_solver.t;
@ -34,6 +55,7 @@ let solver self = self.solver
let th_combine (self:t) : Theory_combine.t = Sat_solver.theory self.solver
let add_theory self th = Theory_combine.add_theory (th_combine self) th
let stats self = self.stat
let tst self = Theory_combine.tst (th_combine self)
let create ?size ?(config=Config.empty) ~theories () : t =
let self = {
@ -116,383 +138,6 @@ let add_cst_support_ (c:cst): unit =
let add_ty_support_ (_ty:Ty.t): unit = ()
(* FIXME: do this in another module, perhaps?
module Conv : sig
val add_statement : Ast.statement -> unit
val add_statement_l : Ast.statement list -> unit
val ty_to_ast: Ty.t -> Ast.Ty.t
val term_to_ast: term -> Ast.term
end = struct
(* for converting Ast.Ty into Ty *)
let ty_tbl_ : Ty.t lazy_t ID.Tbl.t = ID.Tbl.create 16
(* for converting constants *)
let decl_ty_ : cst lazy_t ID.Tbl.t = ID.Tbl.create 16
(* environment for variables *)
type conv_env = {
let_bound: (term * int) ID.Map.t;
(* let-bound variables, to be replaced. int=depth at binding position *)
bound: (int * Ty.t) ID.Map.t;
(* set of bound variables. int=depth at binding position *)
depth: int;
}
let empty_env : conv_env =
{let_bound=ID.Map.empty; bound=ID.Map.empty; depth=0}
let rec conv_ty (ty:Ast.Ty.t): Ty.t = match ty with
| Ast.Ty.Prop -> Ty.prop
| Ast.Ty.Const id ->
begin try ID.Tbl.find ty_tbl_ id |> Lazy.force
with Not_found -> Util.errorf "type %a not in ty_tbl" ID.pp id
end
| Ast.Ty.Arrow (a,b) -> Ty.arrow (conv_ty a) (conv_ty b)
let add_bound env v =
let ty = Ast.Var.ty v |> conv_ty in
{ env with
depth=env.depth+1;
bound=ID.Map.add (Ast.Var.id v) (env.depth,ty) env.bound; }
(* add [v := t] to bindings. Depth is not incremented
(there will be no binders) *)
let add_let_bound env v t =
{ env with
let_bound=ID.Map.add (Ast.Var.id v) (t,env.depth) env.let_bound }
let find_env env v =
let id = Ast.Var.id v in
ID.Map.get id env.let_bound, ID.Map.get id env.bound
let rec conv_term_rec
(env: conv_env)
(t:Ast.term): term = match Ast.term_view t with
| Ast.Bool true -> Term.true_
| Ast.Bool false -> Term.false_
| Ast.Unknown _ -> assert false
| Ast.Const id ->
begin
try ID.Tbl.find decl_ty_ id |> Lazy.force |> Term.const
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
end
| Ast.App (f, l) ->
begin match Ast.term_view f with
| Ast.Const id ->
let f =
try ID.Tbl.find decl_ty_ id |> Lazy.force
with Not_found ->
errorf "could not find constant `%a`" ID.pp id
in
let l = List.map (conv_term_rec env) l in
if List.length l = fst (Ty.unfold_n (Cst.ty f))
then Term.app_cst f (IArray.of_list l) (* fully applied *)
else Term.app (Term.const f) l
| _ ->
let f = conv_term_rec env f in
let l = List.map (conv_term_rec env) l in
Term.app f l
end
| Ast.Var v ->
(* look whether [v] must be replaced by some term *)
begin match AstVarMap.get v env.subst with
| Some t -> t
| None ->
(* lookup as bound variable *)
begin match CCList.find_idx (Ast.Var.equal v) env.bound with
| None -> errorf "could not find var `%a`" Ast.Var.pp v
| Some (i,_) ->
let ty = Ast.Var.ty v |> conv_ty in
Term.db (DB.make i ty)
end
end
| Ast.Bind (Ast.Fun,v,body) ->
let body = conv_term_rec {env with bound=v::env.bound} body in
let ty = Ast.Var.ty v |> conv_ty in
Term.fun_ ty body
| Ast.Bind ((Ast.Forall | Ast.Exists),_, _) ->
errorf "quantifiers not supported"
| Ast.Bind (Ast.Mu,v,body) ->
let env' = add_bound env v in
let body = conv_term_rec env' body in
Term.mu body
| Ast.Select _ -> assert false (* TODO *)
| Ast.Match (u,m) ->
let any_rhs_depends_vars = ref false in (* some RHS depends on matched arg? *)
let m =
ID.Map.map
(fun (vars,rhs) ->
let n_vars = List.length vars in
let env', tys =
CCList.fold_map
(fun env v -> add_bound env v, Ast.Var.ty v |> conv_ty)
env vars
in
let rhs = conv_term_rec env' rhs in
let depends_on_vars =
Term.to_seq_depth rhs
|> Sequence.exists
(fun (t,k) -> match t.term_cell with
| DB db ->
DB.level db < n_vars + k (* [k]: number of intermediate binders *)
| _ -> false)
in
if depends_on_vars then any_rhs_depends_vars := true;
tys, rhs)
m
in
(* optim: check whether all branches return the same term, that
does not depend on matched variables *)
(* TODO: do the closedness check during conversion, above *)
let rhs_l =
ID.Map.values m
|> Sequence.map snd
|> Sequence.sort_uniq ~cmp:Term.compare
|> Sequence.to_rev_list
in
begin match rhs_l with
| [x] when not (!any_rhs_depends_vars) ->
(* every branch yields the same [x], which does not depend
on the argument: remove the match and return [x] instead *)
x
| _ ->
let u = conv_term_rec env u in
Term.match_ u m
end
| Ast.Switch _ ->
errorf "cannot convert switch %a" Ast.pp_term t
| Ast.Let (v,t,u) ->
(* substitute on the fly *)
let t = conv_term_rec env t in
let env' = add_let_bound env v t in
conv_term_rec env' u
| Ast.If (a,b,c) ->
let b = conv_term_rec env b in
let c = conv_term_rec env c in
(* optim: [if _ b b --> b] *)
if Term.equal b c
then b
else Term.if_ (conv_term_rec env a) b c
| Ast.Not t -> Term.not_ (conv_term_rec env t)
| Ast.Binop (op,a,b) ->
let a = conv_term_rec env a in
let b = conv_term_rec env b in
begin match op with
| Ast.And -> Term.and_ a b
| Ast.Or -> Term.or_ a b
| Ast.Imply -> Term.imply a b
| Ast.Eq -> Term.eq a b
end
| Ast.Undefined_value ->
Term.undefined_value (conv_ty t.Ast.ty) Undef_absolute
| Ast.Asserting (t, g) ->
(* [t asserting g] becomes [if g t fail] *)
let t = conv_term_rec env t in
let g = conv_term_rec env g in
Term.if_ g t (Term.undefined_value t.term_ty Undef_absolute)
let add_statement st =
Log.debugf 2
(fun k->k "(@[add_statement@ @[%a@]@])" Ast.pp_statement st);
model_env_ := Ast.env_add_statement !model_env_ st;
begin match st with
| Ast.Assert t ->
let t = conv_term_rec empty_env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.Goal (vars, t) ->
(* skolemize *)
let env, consts =
CCList.fold_map
(fun env v ->
let ty = Ast.Var.ty v |> conv_ty in
let c = Cst.make_undef (Ast.Var.id v) ty in
{env with subst=AstVarMap.add v (Term.const c) env.subst}, c)
empty_env
vars
in
(* model should contain values of [consts] *)
List.iter add_cst_support_ consts;
let t = conv_term_rec env t in
Top_goals.push t;
push_clause (Clause.make [Lit.atom t])
| Ast.TyDecl id ->
let ty = Ty.atomic id Uninterpreted ~card:(Lazy.from_val Infinite) in
add_ty_support_ ty;
ID.Tbl.add ty_tbl_ id (Lazy.from_val ty)
| Ast.Decl (id, ty) ->
assert (not (ID.Tbl.mem decl_ty_ id));
let ty = conv_ty ty in
let cst = Cst.make_undef id ty in
add_cst_support_ cst; (* need it in model *)
ID.Tbl.add decl_ty_ id (Lazy.from_val cst)
| Ast.Data l ->
(* the datatypes in [l]. Used for computing cardinalities *)
let in_same_block : ID.Set.t =
List.map (fun {Ast.Ty.data_id; _} -> data_id) l |> ID.Set.of_list
in
(* declare the type, and all the constructors *)
List.iter
(fun {Ast.Ty.data_id; data_cstors} ->
let ty = lazy (
let card_ : ty_card ref = ref Finite in
let cstors = lazy (
data_cstors
|> ID.Map.map
(fun c ->
let c_id = c.Ast.Ty.cstor_id in
let ty_c = conv_ty c.Ast.Ty.cstor_ty in
let ty_args, ty_ret = Ty.unfold ty_c in
(* add cardinality of [c] to the cardinality of [data_id].
(product of cardinalities of args) *)
let cstor_card =
ty_args
|> List.map
(fun ty_arg -> match ty_arg.ty_cell with
| Atomic (id, _) when ID.Set.mem id in_same_block ->
Infinite
| _ -> Lazy.force ty_arg.ty_card)
|> Ty_card.product
in
card_ := Ty_card.( !card_ + cstor_card );
let rec cst = lazy (
Cst.make_cstor c_id ty_c cstor
) and cstor = lazy (
let cstor_proj = lazy (
let n = ref 0 in
List.map2
(fun id ty_arg ->
let ty_proj = Ty.arrow ty_ret ty_arg in
let i = !n in
incr n;
Cst.make_proj id ty_proj cstor i)
c.Ast.Ty.cstor_proj ty_args
|> IArray.of_list
) in
let cstor_test = lazy (
let ty_test = Ty.arrow ty_ret Ty.prop in
Cst.make_tester c.Ast.Ty.cstor_test ty_test cstor
) in
{ cstor_ty=ty_c; cstor_cst=Lazy.force cst;
cstor_args=IArray.of_list ty_args;
cstor_proj; cstor_test; cstor_card; }
) in
ID.Tbl.add decl_ty_ c_id cst; (* declare *)
Lazy.force cstor)
)
in
let data = { data_cstors=cstors; } in
let card = lazy (
ignore (Lazy.force cstors);
let r = !card_ in
Log.debugf 5
(fun k->k "(@[card_of@ %a@ %a@])" ID.pp data_id Ty_card.pp r);
r
) in
Ty.atomic data_id (Data data) ~card
) in
ID.Tbl.add ty_tbl_ data_id ty;
)
l;
(* force evaluation *)
List.iter
(fun {Ast.Ty.data_id; _} ->
let lazy ty = ID.Tbl.find ty_tbl_ data_id in
ignore (Lazy.force ty.ty_card);
begin match ty.ty_cell with
| Atomic (_, Data {data_cstors=lazy _; _}) -> ()
| _ -> assert false
end)
l
| Ast.Define (k,l) ->
(* declare the mutually recursive functions *)
List.iter
(fun (id,ty,rhs) ->
let ty = conv_ty ty in
let rhs = lazy (conv_term_rec empty_env rhs) in
let k = match k with
| Ast.Recursive -> Cst_recursive
| Ast.Non_recursive -> Cst_non_recursive
in
let cst = lazy (
Cst.make_defined id ty rhs k
) in
ID.Tbl.add decl_ty_ id cst)
l;
(* force thunks *)
List.iter
(fun (id,_,_) -> ignore (ID.Tbl.find decl_ty_ id |> Lazy.force))
l
end
let add_statement_l = List.iter add_statement
module A = Ast
let rec ty_to_ast (t:Ty.t): A.Ty.t = match t.ty_cell with
| Prop -> A.Ty.Prop
| Atomic (id,_) -> A.Ty.const id
| Arrow (a,b) -> A.Ty.arrow (ty_to_ast a) (ty_to_ast b)
let fresh_var =
let n = ref 0 in
fun ty ->
let id = ID.makef "x%d" !n in
incr n;
A.Var.make id (ty_to_ast ty)
let with_var ty env ~f =
let v = fresh_var ty in
let env = DB_env.push (A.var v) env in
f v env
let term_to_ast (t:term): Ast.term =
let rec aux env t = match t.term_cell with
| True -> A.true_
| False -> A.false_
| DB d ->
begin match DB_env.get d env with
| Some t' -> t'
| None -> errorf "cannot find DB %a in env" Term.pp t
end
| App_cst (f, args) when IArray.is_empty args ->
A.const f.cst_id (ty_to_ast t.term_ty)
| App_cst (f, args) ->
let f = A.const f.cst_id (ty_to_ast (Cst.ty f)) in
let args = IArray.map (aux env) args in
A.app f (IArray.to_list args)
| App_ho (f,l) -> A.app (aux env f) (List.map (aux env) l)
| Fun (ty,bod) ->
with_var ty env
~f:(fun v env -> A.fun_ v (aux env bod))
| Mu _ -> assert false
| If (a,b,c) -> A.if_ (aux env a)(aux env b) (aux env c)
| Case (u,m) ->
let u = aux env u in
let m =
ID.Map.mapi
(fun _c_id _rhs ->
assert false (* TODO: fetch cstor; bind variables; convert rhs *)
(*
with_vars tys env ~f:(fun vars env -> vars, aux env rhs)
*)
)
m
in
A.match_ u m
| Builtin b ->
begin match b with
| B_not t -> A.not_ (aux env t)
| B_and (a,b) -> A.and_ (aux env a) (aux env b)
| B_or (a,b) -> A.or_ (aux env a) (aux env b)
| B_eq (a,b) -> A.eq (aux env a) (aux env b)
| B_imply (a,b) -> A.imply (aux env a) (aux env b)
end
in aux DB_env.empty t
end
*)
(** {2 Result} *)
type unknown =
@ -500,12 +145,17 @@ type unknown =
| U_max_depth
| U_incomplete
let pp_unknown out = function
| U_timeout -> Fmt.string out "timeout"
| U_max_depth -> Fmt.string out "max depth reached"
| U_incomplete -> Fmt.string out "incomplete fragment"
type model = Model.t
let pp_model = Model.pp
type res =
| Sat of model
| Unsat (* TODO: proof *)
| Unsat of Proof.t
| Unknown of unknown
(* FIXME: repair this and output a nice model.
@ -708,9 +358,6 @@ end
(** {2 Main} *)
let[@inline] clause_of_mclause (c:Sat_solver.clause): Clause.t =
Sat_solver.Clause.atoms_l c |> Clause.make
(* convert unsat-core *)
let clauses_of_unsat_core (core:Sat_solver.clause list): Clause.t Sequence.t =
Sequence.of_list core
@ -741,34 +388,8 @@ let do_on_exit ~on_exit =
List.iter (fun f->f()) on_exit;
()
let add_statement_l (_:t) _ = ()
(* FIXME
Conv.add_statement_l
*)
(* TODO: move this into submodule *)
let pp_proof out p =
let pp_step_res out p =
let {Sat_solver.Proof.conclusion; _ } = Sat_solver.Proof.expand p in
let conclusion = clause_of_mclause conclusion in
Clause.pp out conclusion
in
let pp_step out = function
| Sat_solver.Proof.Lemma _ -> Format.fprintf out "(@[<1>lemma@ ()@])"
| Sat_solver.Proof.Resolution (p1, p2, _) ->
Format.fprintf out "(@[<1>resolution@ %a@ %a@])"
pp_step_res p1 pp_step_res p2
| _ -> Fmt.string out "<other>"
in
Format.fprintf out "(@[<v>";
Sat_solver.Proof.fold
(fun () {Sat_solver.Proof.conclusion; step } ->
let conclusion = clause_of_mclause conclusion in
Format.fprintf out "(@[<hv1>step@ %a@ @[<1>from:@ %a@]@])@,"
Clause.pp conclusion pp_step step)
() p;
Format.fprintf out "@])";
()
let assume (self:t) (c:Clause.t) : unit =
Sat_solver.add_clause (solver self) (Clause.lits c)
(*
type unsat_core = Sat.clause list
@ -776,10 +397,21 @@ type unsat_core = Sat.clause list
(* TODO: main loop with iterative deepening of the unrolling limit
(not the value depth limit) *)
let solve ?on_exit:(_=[]) ?check:(_=true) (_self:t) : res =
Unknown U_incomplete
let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res =
let r = Sat_solver.solve ~assumptions (solver self) () in
match r with
| Sat_solver.Sat (Dagon_sat.Sat_state _st) ->
Log.debugf 0 (fun k->k "SAT");
Unknown U_incomplete (* TODO *)
(*
let env = Ast.env_empty in
let m = Model.make ~env
Sat m *)
| Sat_solver.Unsat (Dagon_sat.Unsat_state us) ->
let pr = us.get_proof () in
Unsat pr
(* FIXME
(* FIXME:
(* TODO: max_depth should actually correspond to the maximum depth
of un-expanded terms (expand in body of t --> depth = depth(t)+1),
so it corresponds to unfolding call graph to some depth *)

23
src/smt/Solver.mli
View file

@ -5,10 +5,21 @@
The solving algorithm, based on MCSat *)
module Sat_solver : Dagon_sat.S
with type formula = Lit.t
and type theory = Theory_combine.t
and type Proof.lemma = Theory_combine.proof
(** {2 Result} *)
type model = Model.t
module Proof : sig
type t = Sat_solver.Proof.proof
val pp : t CCFormat.printer
end
type unknown =
| U_timeout
| U_max_depth
@ -16,14 +27,9 @@ type unknown =
type res =
| Sat of Model.t
| Unsat (* TODO: proof *)
| Unsat of Proof.t
| Unknown of unknown
module Sat_solver : Dagon_sat.S
with type formula = Lit.t
and type theory = Theory_combine.t
and type Proof.lemma = Theory_combine.proof
(** {2 Main} *)
type t
@ -39,12 +45,14 @@ val solver : t -> Sat_solver.t
val th_combine : t -> Theory_combine.t
val add_theory : t -> Theory.t -> unit
val stats : t -> Stat.t
val tst : t -> Term.state
val add_statement_l : t -> Ast.statement list -> unit
val assume : t -> Clause.t -> unit
val solve :
?on_exit:(unit -> unit) list ->
?check:bool ->
assumptions:Lit.t list ->
t ->
res
(** [solve s] checks the satisfiability of the statement added so far to [s]
@ -53,3 +61,4 @@ val solve :
val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer
val pp_unknown : unknown CCFormat.printer

3
src/smt/Solver_types.ml
View file

@ -32,6 +32,7 @@ and 'a builtin =
| B_and of 'a list
| B_or of 'a list
| B_imply of 'a list * 'a
| B_distinct of 'a list
(** Methods on the custom term view whose leaves are ['a].
Terms must be comparable, hashable, printable, and provide
@ -310,6 +311,8 @@ let pp_term_top ~ids out t =
Fmt.fprintf out "(@[<hv1>=>@ %a@ %a@])" (Util.pp_list pp) a pp b
| Builtin (B_eq (a,b)) ->
Fmt.fprintf out "(@[<hv1>=@ %a@ %a@])" pp a pp b
| Builtin (B_distinct l) ->
Fmt.fprintf out "(@[<hv1>distinct@ %a@])" (Util.pp_list pp) l
| Custom {view; tc} -> tc.tc_t_pp pp out view
and pp_id =
if ids then ID.pp else ID.pp_name

16
src/smt/Term.ml
View file

@ -72,10 +72,15 @@ let or_l st = function
| l -> make st (Term_cell.or_ l)
let and_ st a b = and_l st [a;b]
let or_ st a b = and_l st [a;b]
let imply st a b = match a with [] -> b | _ -> make st (Term_cell.imply a b)
let or_ st a b = or_l st [a;b]
let imply st a b = match a, b.term_cell with
| [], _ -> b
| _::_, Builtin (B_imply (a',b')) ->
make st (Term_cell.imply (CCList.append a a') b')
| _ -> make st (Term_cell.imply a b)
let eq st a b = make st (Term_cell.eq a b)
let neq st a b = not_ st (eq st a b)
let distinct st l = make st (Term_cell.distinct l)
let neq st a b = make st (Term_cell.neq a b)
let builtin st b = make st (Term_cell.builtin b)
(* "eager" and, evaluating [a] first *)
@ -109,6 +114,9 @@ let fold_map_builtin
| B_eq (a,b) ->
let acc, a, b = fold_binary acc a b in
acc, B_eq (a, b)
| B_distinct l ->
let acc, l = CCList.fold_map f acc l in
acc, B_distinct l
| B_imply (a,b) ->
let acc, a = CCList.fold_map f acc a in
let acc, b = f acc b in
@ -135,7 +143,7 @@ let map_builtin f b =
let builtin_to_seq b yield = match b with
| B_not t -> yield t
| B_or l | B_and l -> List.iter yield l
| B_or l | B_and l | B_distinct l -> List.iter yield l
| B_imply (a,b) -> List.iter yield a; yield b
| B_eq (a,b) -> yield a; yield b

1
src/smt/Term.mli
View file

@ -27,6 +27,7 @@ val not_ : state -> t -> t
val imply : state -> t list -> t -> t
val eq : state -> t -> t -> t
val neq : state -> t -> t -> t
val distinct : state -> t list -> t
val and_eager : state -> t -> t -> t (* evaluate left argument first *)
val cstor_test : state -> data_cstor -> term -> t

9
src/smt/Term_cell.ml
View file

@ -30,6 +30,7 @@ module Make_eq(A : ARG) = struct
| Builtin (B_or l) -> Hash.combine2 22 (Hash.list sub_hash l)
| Builtin (B_imply (l1,t2)) -> Hash.combine3 23 (Hash.list sub_hash l1) (sub_hash t2)
| Builtin (B_eq (t1,t2)) -> Hash.combine3 24 (sub_hash t1) (sub_hash t2)
| Builtin (B_distinct l) -> Hash.combine2 26 (Hash.list sub_hash l)
| Custom {view;tc} -> tc.tc_t_hash sub_hash view
(* equality that relies on physical equality of subterms *)
@ -53,10 +54,12 @@ module Make_eq(A : ARG) = struct
| B_not a1, B_not a2 -> sub_eq a1 a2
| B_and l1, B_and l2
| B_or l1, B_or l2 -> CCEqual.list sub_eq l1 l2
| B_distinct l1, B_distinct l2 -> CCEqual.list sub_eq l1 l2
| B_eq (a1,b1), B_eq (a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2
| B_imply (a1,b1), B_imply (a2,b2) -> CCEqual.list sub_eq a1 a2 && sub_eq b1 b2
| B_not _, _ | B_and _, _ | B_eq _, _
| B_or _, _ | B_imply _, _ -> false
| B_or _, _ | B_imply _, _ | B_distinct _, _
-> false
end
| Custom r1, Custom r2 ->
r1.tc.tc_t_equal sub_eq r1.view r2.view
@ -110,6 +113,10 @@ let and_ l = builtin (B_and l)
let or_ l = builtin (B_or l)
let imply a b = builtin (B_imply (a,b))
let eq a b = builtin (B_eq (a,b))
let distinct = function
| [] | [_] -> true_
| l -> builtin (B_distinct l)
let neq a b = distinct [a;b]
let custom ~tc view = Custom {view;tc}

2
src/smt/Term_cell.mli
View file

@ -19,6 +19,8 @@ val or_ : term list -> t
val not_ : term -> t
val imply : term list -> term -> t
val eq : term -> term -> t
val neq : term -> term -> t
val distinct : term list -> t
val custom : tc:term_view_tc -> term term_view_custom -> t
val ty : t -> Ty.t

8
src/smt/Theory.ml
View file

@ -56,3 +56,11 @@ type t = {
make: Term.state -> actions -> state;
}
let make ~name ~make () : t = {name;make}
let make_st
?(on_merge=fun _ _ _ -> ())
?(on_assert=fun _ -> ())
~final_check
() : state =
{ on_merge; on_assert; final_check }

24
src/smt/Ty.ml
View file

@ -2,8 +2,28 @@
open Solver_types
type t = ty
type cell = ty_cell
type def = ty_def
and cell = Solver_types.ty_cell =
| Prop
| Atomic of ID.t * ty_def
| Arrow of ty * ty
type def = Solver_types.ty_def =
| Uninterpreted
| Data of datatype
and datatype = Solver_types.datatype = {
data_cstors: data_cstor ID.Map.t lazy_t;
}
(* a constructor *)
and data_cstor = Solver_types.data_cstor = {
cstor_ty: ty;
cstor_args: ty IArray.t; (* argument types *)
cstor_proj: cst IArray.t lazy_t; (* projectors *)
cstor_test: cst lazy_t; (* tester *)
cstor_cst: cst; (* the cstor itself *)
cstor_card: ty_card; (* cardinality of the constructor('s args) *)
}
let view t = t.ty_cell

26
src/smt/Ty.mli
View file

@ -1,9 +1,31 @@
(** {1 Hashconsed Types} *)
open Solver_types
type t = Solver_types.ty
type cell = Solver_types.ty_cell
type def = Solver_types.ty_def
type cell = Solver_types.ty_cell =
| Prop
| Atomic of ID.t * ty_def
| Arrow of ty * ty
type def = Solver_types.ty_def =
| Uninterpreted
| Data of datatype
and datatype = Solver_types.datatype = {
data_cstors: data_cstor ID.Map.t lazy_t;
}
(* a constructor *)
and data_cstor = Solver_types.data_cstor = {
cstor_ty: ty;
cstor_args: ty IArray.t; (* argument types *)
cstor_proj: cst IArray.t lazy_t; (* projectors *)
cstor_test: cst lazy_t; (* tester *)
cstor_cst: cst; (* the cstor itself *)
cstor_card: ty_card; (* cardinality of the constructor('s args) *)
}
val view : t -> cell

420
src/smtlib/Dagon_smtlib.ml
View file

@ -1,11 +1,8 @@
(** {1 Process Statements} *)
open Dagon_smt
module Fmt = CCFormat
module A = Ast
module PA = Parse_ast
module Ast = Dagon_smt.Ast
module E = CCResult
module Loc = Locations
@ -21,7 +18,7 @@ module Parse = struct
try Result.Ok (parse_chan_exn ?filename ic)
with e -> Result.Error (Printexc.to_string e)
let parse_file_exn file : PA.statement list =
let parse_file_exn file : Parse_ast.statement list =
CCIO.with_in file (parse_chan_exn ~filename:file)
let parse_file file =
@ -31,426 +28,21 @@ module Parse = struct
let parse_file_exn ctx file : Ast.statement list =
(* delegate parsing to [Tip_parser] *)
parse_file_exn file
|> CCList.flat_map (Convert.conv_statement ctx)
|> CCList.flat_map (Typecheck.conv_statement ctx)
let parse file =
let ctx = Convert.Ctx.create () in
let ctx = Typecheck.Ctx.create () in
try Result.Ok (parse_file_exn ctx file)
with e -> Result.Error (Printexc.to_string e)
let parse_stdin () =
let ctx = Convert.Ctx.create () in
let ctx = Typecheck.Ctx.create () in
try
parse_chan_exn ~filename:"<stdin>" stdin
|> CCList.flat_map (Convert.conv_statement ctx)
|> CCList.flat_map (Typecheck.conv_statement ctx)
|> CCResult.return
with e -> Result.Error (Printexc.to_string e)
end
let parse = Parse.parse
let parse_stdin = Parse.parse_stdin
(** {2 Conversion into {!Term.t}} *)
module Subst = struct
type 'a t = 'a ID.Map.t
let empty = ID.Map.empty
let mem subst v = ID.Map.mem (A.Var.id v) subst
let pp pp_x out = ID.Map.pp ~arrow:"→" ID.pp pp_x out
let add subst v t =
if mem subst v then (
Util.errorf "%a already bound" A.Var.pp v;
);
ID.Map.add (A.Var.id v) t subst
let find subst v = ID.Map.get (A.Var.id v) subst
let find_exn subst v = ID.Map.find (A.Var.id v) subst
end
let mk_ite_id =
let n = ref 0 in
fun () -> ID.makef "ite_%d" (CCRef.incr_then_get n)
let mk_sub_form =
let n = ref 0 in
fun () -> ID.makef "sub_form_%d" (CCRef.incr_then_get n)
let mk_lra_id =
let n = ref 0 in
fun () -> ID.makef "lra_%d" (CCRef.incr_then_get n)
type term_or_form =
| T of A.term
| Rat of RLE.t (* rational linear expression *)
let[@inline] ret_t t = T t
let[@inline] ret_f f = F f
let[@inline] ret_rat t = Rat t
let[@inline] ret_any t = if Term.is_bool t then F (F.atom (Term.Bool.pa t)) else T t
let conv_ty (reg:Reg.t) (ty:A.Ty.t) : Type.t =
let mk_ty = Reg.find_exn reg Mc2_unin_sort.k_make in
(* convert a type *)
let rec aux_ty (ty:A.Ty.t) : Type.t = match ty with
| A.Ty.Ty_bool -> Type.bool
| A.Ty.Rat -> Reg.find_exn reg Mc2_lra.k_rat
| A.Ty.Atomic (id, args) -> mk_ty id (List.map aux_ty args)
| A.Ty.Arrow _ ->
Util.errorf "cannot convert arrow type `%a`" A.Ty.pp ty
in
aux_ty ty
let conv_bool_term (reg:Reg.t) (t:A.term): atom list list =
let decl = Reg.find_exn reg Mc2_uf.k_decl in
(* polymorphic equality *)
let[@inline] mk_eq_ t u = Term.mk_eq t u in
let mk_app = Reg.find_exn reg Mc2_uf.k_app in
let mk_const = Reg.find_exn reg Mc2_uf.k_const in
let fresh = Reg.find_exn reg Mc2_propositional.k_fresh in
let mk_eq t u = Term.Bool.pa (mk_eq_ t u) in
let mk_neq t u = Term.Bool.na (mk_eq_ t u) in
let mk_lra_pred = Reg.find_exn reg Mc2_lra.k_make_pred in
let mk_lra_eq t u = mk_lra_pred Mc2_lra.Eq0 (RLE.diff t u) |> Term.Bool.pa in
let side_clauses : atom list list ref = ref [] in
(* introduce intermediate variable for LRA sub-expression *)
let mk_lra_expr (e:RLE.t): term = match RLE.as_const e, RLE.as_singleton e with
| Some n, _ -> Reg.find_exn reg Mc2_lra.k_make_const n
| None, Some (n,t) when Q.equal n Q.one -> t
| _ ->
let id = mk_lra_id() in
Log.debugf 30
(fun k->k"(@[smtlib.name_lra@ %a@ :as %a@])" RLE.pp e ID.pp id);
decl id [] (Reg.find_exn reg Mc2_lra.k_rat);
let t = mk_const id in
side_clauses := [mk_lra_eq (RLE.singleton1 t) e] :: !side_clauses;
t
in
(* adaptative equality *)
let mk_eq_t_tf (t:term) (u:term_or_form) : F.t = match u with
| F u -> F.equiv (F.atom (Term.Bool.pa t)) u
| T u when Term.is_bool u ->
F.equiv (F.atom (Term.Bool.pa t)) (F.atom (Term.Bool.pa u))
| T u -> mk_eq t u |> F.atom
| Rat u -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
and mk_eq_tf_tf (t:term_or_form) (u:term_or_form) = match t, u with
| T t, T u -> mk_eq t u |> F.atom
| T t, Rat u | Rat u, T t -> mk_lra_eq (RLE.singleton1 t) u |> F.atom
| Rat t, Rat u -> mk_lra_eq t u |> F.atom
| F t, F u -> F.equiv t u
| _ -> assert false
in
(* convert term *)
let rec aux (subst:term_or_form Subst.t) (t:A.term) : term_or_form =
begin match A.term_view t with
| A.Var v ->
begin match Subst.find subst v with
| None -> Util.errorf "variable %a not bound" A.Var.pp v
| Some t -> t
end
| A.Const id -> mk_const id |> ret_any
| A.App (f, l) ->
let l = List.map (aux_t subst) l in
begin match A.term_view f with
| A.Const id -> mk_app id l |> ret_any
| _ -> Util.errorf "cannot process HO application %a" A.pp_term t
end
| A.If (a,b,c) ->
let a = aux_form subst a in
let b = aux subst b in
let c = aux subst c in
let ty_b = match b with
| F _ -> Type.bool
| T t -> Term.ty t
| Rat _ -> Reg.find_exn reg Mc2_lra.k_rat
in
let placeholder_id = mk_ite_id () in
Log.debugf 30
(fun k->k"(@[smtlib.name_term@ %a@ :as %a@])" A.pp_term t ID.pp placeholder_id);
decl placeholder_id [] ty_b;
let placeholder = mk_const placeholder_id in
(* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *)
let form =
F.and_
[ F.imply a (mk_eq_t_tf placeholder b);
F.imply (F.not_ a) (mk_eq_t_tf placeholder c);
]
in
side_clauses := List.rev_append (mk_cnf form) !side_clauses;
ret_t placeholder
| A.Let (v,t,u) ->
let subst = Subst.add subst v (aux subst t) in
aux subst u
| A.Op (A.And, l) -> F.and_ (List.map (aux_form subst) l) |> ret_f
| A.Op (A.Or, l) -> F.or_ (List.map (aux_form subst) l) |> ret_f
| A.Op (A.Imply, l) ->
let rec curry_imply_ = function
| [] -> assert false
| [a] -> aux_form subst a
| a :: b -> F.imply (aux_form subst a) (curry_imply_ b)
in
curry_imply_ l |> ret_f
| A.Op (A.Eq, l) ->
let l = List.map (aux subst) l in
let rec curry_eq = function
| [] | [_] -> assert false
| [a;b] -> [mk_eq_tf_tf a b]
| a :: b :: tail ->
mk_eq_tf_tf a b :: curry_eq (b::tail)
in
F.and_ (curry_eq l) |> ret_f
| A.Op (A.Distinct, l) ->
(* TODO: more efficient "distinct"? *)
List.map (aux_t subst) l
|> CCList.diagonal
|> List.map (fun (t,u) -> mk_neq t u |> F.atom)
|> F.and_ |> ret_f
| A.Not f -> F.not_ (aux_form subst f) |> ret_f
| A.Bool_term true -> ret_f F.true_
| A.Bool_term false -> ret_f F.false_
| A.Num_q n -> Mc2_lra.LE.const n |> ret_rat
| A.Num_z n -> Mc2_lra.LE.const (Q.of_bigint n) |> ret_rat
| A.Arith (op, l) ->
let l = List.map (aux_rat subst) l in
begin match op, l with
| A.Minus, [a] -> RLE.neg a |> ret_rat
| _, [] | _, [_] ->
Util.errorf "ill-formed arith expr:@ %a@ (need ≥ 2 args)" A.pp_term t
| A.Leq, [a;b] ->
let e = RLE.diff a b in
mk_lra_pred Mc2_lra.Leq0 e |> ret_any
| A.Geq, [a;b] ->
let e = RLE.diff b a in
mk_lra_pred Mc2_lra.Leq0 e |> ret_any
| A.Lt, [a;b] ->
let e = RLE.diff a b in
mk_lra_pred Mc2_lra.Lt0 e |> ret_any
| A.Gt, [a;b] ->
let e = RLE.diff b a in
mk_lra_pred Mc2_lra.Lt0 e |> ret_any
| (A.Leq | A.Lt | A.Geq | A.Gt), _ ->
Util.errorf "ill-formed arith expr:@ %a@ (binary operator)" A.pp_term t
| A.Add, _ ->
let e = List.fold_left (fun n t -> RLE.add t n) RLE.empty l in
mk_lra_expr e |> ret_t
| A.Minus, a::tail ->
let e =
List.fold_left
(fun n t -> RLE.diff n t)
a tail
in
mk_lra_expr e |> ret_t
| A.Mult, _::_::_ ->
let coeffs, terms =
CCList.partition_map
(fun t -> match RLE.as_const t with
| None -> `Right t
| Some c -> `Left c)
l
in
begin match coeffs, terms with
| c::c_tail, [] ->
List.fold_right RLE.mult c_tail (RLE.const c) |> ret_rat
| _, [t] ->
List.fold_right RLE.mult coeffs t |> ret_rat
| _ ->
Util.errorf "non-linear expr:@ `%a`" A.pp_term t
end
| A.Div, (first::l) ->
(* support t/a/b/c where only [t] is a rational *)
let coeffs =
List.map
(fun c -> match RLE.as_const c with
| None ->
Util.errorf "non-linear expr:@ `%a`" A.pp_term t
| Some c -> Q.inv c)
l
in
List.fold_right RLE.mult coeffs first |> ret_rat
end
| A.Select _ -> assert false (* TODO *)
| A.Match _ -> assert false (* TODO *)
| A.Bind _ -> assert false (* TODO *)
end
(* expect a term *)
and aux_t subst (t:A.term) : term = match aux subst t with
| T t -> t
| Rat e -> mk_lra_expr e
| F (F.Lit a) when Atom.is_pos a -> Atom.term a
| F f ->
(* name the sub-formula and add CNF *)
let placeholder_id = mk_sub_form() in
decl placeholder_id [] Type.bool;
let placeholder = mk_const placeholder_id in
(* add [f_a => placeholder=b] and [¬f_a => placeholder=c] *)
let form = F.equiv (F.atom (Term.Bool.pa placeholder)) f in
side_clauses := List.rev_append (mk_cnf form) !side_clauses;
placeholder
(* convert formula *)
and aux_form subst (t:A.term): F.t = match aux subst t with
| T t -> F.atom (Term.Bool.pa t)
| F f -> f
| Rat _ -> Util.errorf "expected proposition,@ got %a" A.pp_term t
(* expect a rational expr *)
and aux_rat subst (t:A.term) : RLE.t = match aux subst t with
| Rat e -> e
| T t -> RLE.singleton1 t
| F _ -> assert false
and mk_cnf (f:F.t) : atom list list =
F.cnf ~fresh f
in
let cs = aux_form Subst.empty t |> mk_cnf in
List.rev_append !side_clauses cs
(** {2 Processing Statements} *)
(* list of (local) hypothesis *)
let hyps = ref []
let check_model state : bool =
Log.debug 4 "checking model";
let check_clause c =
Log.debugf 15
(fun k -> k "(@[check.clause@ %a@])" Clause.debug_atoms c);
let ok =
List.exists (fun t -> Solver.Sat_state.eval_opt state t = Some true) c
in
if not ok then (
Log.debugf 0
(fun k->k "(@[check.fail:@ clause %a@ not satisfied in model@])" Clause.debug_atoms c);
);
ok
in
Solver.Sat_state.check_model state &&
List.for_all check_clause !hyps
module Dot = Mc2_backend.Dot.Make(Mc2_backend.Dot.Default)
(* call the solver to check-sat *)
let solve
?gc ?restarts ?dot_proof
?(pp_model=false) ?(check=false) ?time ?memory ?progress
~assumptions s : unit =
let t1 = Sys.time() in
let res = Solver.solve ?gc ?restarts ?time ?memory ?progress s ~assumptions in
let t2 = Sys.time () in
begin match res with
| Solver.Sat state ->
if pp_model then (
let pp_t out = function
| A_bool (t,b) -> Fmt.fprintf out "(@[%a@ %B@])" Term.pp t b
| A_semantic (t,v) -> Fmt.fprintf out "(@[%a@ %a@])" Term.pp t Value.pp v
in
Format.printf "(@[<hv1>model@ %a@])@."
(Util.pp_list pp_t) (Solver.Sat_state.model state)
);
if check then (
if not (check_model state) then (
Util.error "invalid model"
)
);
let t3 = Sys.time () -. t2 in
Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
| Solver.Unsat state ->
if check then (
let p = Solver.Unsat_state.get_proof state in
Proof.check p;
begin match dot_proof with
| None -> ()
| Some file ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Dot.print fmt p;
Format.pp_print_flush fmt (); flush oc)
end
);
let t3 = Sys.time () -. t2 in
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
end
(* process a single statement *)
let process_stmt
?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
?time ?memory ?progress
(solver:Solver.t)
(stmt:Ast.statement) : unit or_error =
Log.debugf 5
(fun k->k "(@[<2>process statement@ %a@])" A.pp_statement stmt);
let decl_sort = Solver.get_service_exn solver Mc2_unin_sort.k_decl_sort in
let decl = Solver.get_service_exn solver Mc2_uf.k_decl in
let conv_ty = conv_ty (Solver.services solver) in
begin match stmt with
| A.SetLogic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> E.return ()
| A.SetLogic s ->
Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
E.return ()
| A.SetOption l ->
Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l);
E.return ()
| A.SetInfo _ -> E.return ()
| A.Exit ->
Log.debug 1 "exit";
raise Exit
| A.CheckSat ->
solve ?gc ?restarts ?dot_proof ?check ?pp_model ?time ?memory ?progress
solver ~assumptions:[];
E.return()
| A.TyDecl (id,n) ->
decl_sort id n;
E.return ()
| A.Decl (f,ty) ->
let ty_args, ty_ret = A.Ty.unfold ty in
let ty_args = List.map conv_ty ty_args in
let ty_ret = conv_ty ty_ret in
decl f ty_args ty_ret;
E.return ()
| A.Assert t ->
let clauses =
conv_bool_term (Solver.services solver) t
in
if pp_cnf then (
Format.printf "(@[<hv1>assert@ %a@])@."
(Util.pp_list Clause.pp_atoms) clauses;
);
hyps := clauses @ !hyps;
Solver.assume solver clauses;
E.return()
| A.Goal (_, _) ->
Util.errorf "cannot deal with goals yet"
(*
| Dolmen.Statement.Def (id, t) -> T.def id t
| Dolmen.Statement.Decl (id, t) -> T.decl id t
| Dolmen.Statement.Consequent t ->
let cnf = T.consequent t in
pp_cnf solver cnf;
hyps := cnf @ !hyps;
S.assume s cnf
| Dolmen.Statement.Antecedent t ->
let cnf = T.antecedent t in
pp_cnf cnf;
hyps := cnf @ !hyps;
S.assume cnf
| Dolmen.Statement.Pack [
{ Dolmen.Statement.descr = Dolmen.Statement.Push 1; _ };
{ Dolmen.Statement.descr = Dolmen.Statement.Antecedent f; _ };
{ Dolmen.Statement.descr = Dolmen.Statement.Prove; _ };
{ Dolmen.Statement.descr = Dolmen.Statement.Pop 1; _ };
] ->
let assumptions = T.assumptions f in
prove solver ~assumptions
| Dolmen.Statement.Prove ->
prove solver ~assumptions:[]
| Dolmen.Statement.Set_info _
| Dolmen.Statement.Set_logic _ -> ()
| Dolmen.Statement.Exit -> exit 0
| _ ->
Format.printf "Command not supported:@\n%a@."
Dolmen.Statement.print s
*)
end

25
src/smtlib/Dagon_smtlib.mli
View file

@ -7,28 +7,9 @@
type 'a or_error = ('a, string) CCResult.t
module Ast = Ast
module Ast = Dagon_smt.Ast
val parse : string -> Dagon_smt.Ast.statement list or_error
val parse : string -> Ast.statement list or_error
val parse_stdin : unit -> Dagon_smt.Ast.statement list or_error
val parse_stdin : unit -> Ast.statement list or_error
val conv_bool_term : Dagon_smt.Term.state -> Dagon_smt.Ast.term -> Dagon_smt.Lit.t list list
(** Convert a boolean term into CNF *)
val process_stmt :
?gc:bool ->
?restarts:bool ->
?pp_cnf:bool ->
?dot_proof:string ->
?pp_model:bool ->
?check:bool ->
?time:float ->
?memory:float ->
?progress:bool ->
Dagon_smt.Solver.t ->
Dagon_smt.Ast.statement ->
unit or_error
(** Process the given statement.
@raise Incorrect_model if model is not correct
*)

0
src/smtlib/Convert.ml → src/smtlib/Typecheck.ml
View file

0
src/smtlib/Convert.mli → src/smtlib/Typecheck.mli
View file