diff --git a/src/main/main.ml b/src/main/main.ml index 6122d918..ad3b08e1 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -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 diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index b8a87d01..f122854b 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -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; diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 3a6678a2..32327977 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -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 diff --git a/src/smt/Ast.ml b/src/smt/Ast.ml index 3e34fbc6..26840918 100644 --- a/src/smt/Ast.ml +++ b/src/smt/Ast.ml @@ -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 "(@[%a@ %a@])" pp_arith op (Util.pp_list pp) l | Undefined_value -> Fmt.string out "" - | 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 diff --git a/src/smt/Ast.mli b/src/smt/Ast.mli index fcd4a19c..2abd401f 100644 --- a/src/smt/Ast.mli +++ b/src/smt/Ast.mli @@ -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 diff --git a/src/smt/Model.ml b/src/smt/Model.ml index 9b0aab2f..4b82c068 100644 --- a/src/smt/Model.ml +++ b/src/smt/Model.ml @@ -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 diff --git a/src/smt/Process.ml b/src/smt/Process.ml new file mode 100644 index 00000000..6f3d0abb --- /dev/null +++ b/src/smt/Process.ml @@ -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 "(@[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 "(@[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 + *) diff --git a/src/smt/Process.mli b/src/smt/Process.mli new file mode 100644 index 00000000..e234369b --- /dev/null +++ b/src/smt/Process.mli @@ -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 diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 28d5b73f..29832d4e 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -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 "" + in + Format.fprintf out "(@["; + Sat_solver.Proof.fold + (fun () {Sat_solver.Proof.conclusion; step } -> + let conclusion = clause_of_mclause conclusion in + Format.fprintf out "(@[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 "" - in - Format.fprintf out "(@["; - Sat_solver.Proof.fold - (fun () {Sat_solver.Proof.conclusion; step } -> - let conclusion = clause_of_mclause conclusion in - Format.fprintf out "(@[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 *) diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index fc63402b..72657584 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -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 diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 5de9d809..16175d48 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -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 "(@[=>@ %a@ %a@])" (Util.pp_list pp) a pp b | Builtin (B_eq (a,b)) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b + | Builtin (B_distinct l) -> + Fmt.fprintf out "(@[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 diff --git a/src/smt/Term.ml b/src/smt/Term.ml index f4fbac4c..eaa01804 100644 --- a/src/smt/Term.ml +++ b/src/smt/Term.ml @@ -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 diff --git a/src/smt/Term.mli b/src/smt/Term.mli index c8ae454f..747169b2 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -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 diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml index f4349a36..c04e68e3 100644 --- a/src/smt/Term_cell.ml +++ b/src/smt/Term_cell.ml @@ -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} diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli index 9d5f17a6..5dd09799 100644 --- a/src/smt/Term_cell.mli +++ b/src/smt/Term_cell.mli @@ -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 diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index 2093b892..0d5b122e 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -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 } diff --git a/src/smt/Ty.ml b/src/smt/Ty.ml index 73995cea..b9d4f1a3 100644 --- a/src/smt/Ty.ml +++ b/src/smt/Ty.ml @@ -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 diff --git a/src/smt/Ty.mli b/src/smt/Ty.mli index 39989fa0..79845285 100644 --- a/src/smt/Ty.mli +++ b/src/smt/Ty.mli @@ -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 diff --git a/src/smtlib/Dagon_smtlib.ml b/src/smtlib/Dagon_smtlib.ml index 8095f1ae..888a84c5 100644 --- a/src/smtlib/Dagon_smtlib.ml +++ b/src/smtlib/Dagon_smtlib.ml @@ -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 - |> 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 "(@[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 "(@[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 - diff --git a/src/smtlib/Dagon_smtlib.mli b/src/smtlib/Dagon_smtlib.mli index f6f73029..dac3fea8 100644 --- a/src/smtlib/Dagon_smtlib.mli +++ b/src/smtlib/Dagon_smtlib.mli @@ -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 -*) diff --git a/src/smtlib/Convert.ml b/src/smtlib/Typecheck.ml similarity index 100% rename from src/smtlib/Convert.ml rename to src/smtlib/Typecheck.ml diff --git a/src/smtlib/Convert.mli b/src/smtlib/Typecheck.mli similarity index 100% rename from src/smtlib/Convert.mli rename to src/smtlib/Typecheck.mli