diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 9e3fc5993fb6bd4b3aef0703abe1df78bf3d82c6..974c065fd8aae1f400d24630e8cab171ce65d2e9 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -556,6 +556,8 @@ module Interp : sig
val unfold_with :
'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Base.Sequence.Step.t) -> 'c t
+
+ val hd_exn : 'a t -> 'a
end
type check =
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 8559fa075398f2a0606529feb34ab66836e3d6ae..4ddca2101c30f2c41ee20f79f9971fcf1fd02674 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -123,6 +123,8 @@ module SeqLim = struct
d.limitreached := true;
Sequence.take (x (i + 1)) 1)
else x (i + 1)
+
+ let hd_exn s = Sequence.hd_exn (s 1)
end
let check_of_bool = function true -> Right | false -> Wrong
@@ -486,39 +488,41 @@ module Fix_model = struct
end
let pp_gen_ground fmt = function
- | `Ground g -> Ground.Term.pp fmt (Ground.sem g)
- | `ClosedQuantifier g -> Ground.ClosedQuantifier.pp fmt g
- | `NotTotallyApplied g -> Ground.NotTotallyApplied.pp fmt g
+ | `Ground g -> Fmt.pf fmt "ground term %a" Ground.Term.pp (Ground.sem g)
+ | `ClosedQuantifier g ->
+ Fmt.pf fmt "closed quantifier %a" Ground.ClosedQuantifier.pp g
+ | `NotTotallyApplied g ->
+ Fmt.pf fmt "not totally applied function %a" Ground.NotTotallyApplied.pp g
-let ty_gen = function
- | `Ground g -> (Ground.sem g).ty
- | `ClosedQuantifier _ -> Ground.Ty.bool
- | `NotTotallyApplied _ ->
- (* todo *)
- assert false
+let pp_ty_gen fmt = function
+ | `Ground g -> Ground.Ty.pp fmt (Ground.sem g).ty
+ | `ClosedQuantifier _ -> Ground.Ty.pp fmt Ground.Ty.bool
+ | `NotTotallyApplied _ -> ()
let () =
- Exn_printer.register (fun fmt exn ->
+ Caml.Printexc.register_printer (fun exn ->
match exn with
| CantInterpretNode t ->
- Fmt.pf fmt "Can't interpret the node %a." Node.pp t
+ Some (Fmt.str "Can't interpret the node %a." Node.pp t)
| CantCheckGround g ->
- Fmt.pf fmt "Can't check ground term %a of type %a." pp_gen_ground g
- Ground.Ty.pp (ty_gen g)
+ Some
+ (Fmt.str "Can't check %a of type %a." pp_gen_ground g pp_ty_gen g)
| CantComputeGround g ->
- Fmt.pf fmt "Can't compute ground term %a of type %a." pp_gen_ground g
- Ground.Ty.pp (ty_gen g)
+ Some
+ (Fmt.str "Can't compute %a of type %a." pp_gen_ground g pp_ty_gen g)
| CantInterpretTy t ->
- Fmt.pf fmt "Can't interpret the type %a." Ground.Ty.pp t
+ Some (Fmt.str "Can't interpret the type %a." Ground.Ty.pp t)
| GroundTermWithoutValueAfterModelFixing g ->
- Fmt.pf fmt "After model fixing %a of type %a has no value"
- pp_gen_ground g Ground.Ty.pp (ty_gen g)
+ Some
+ (Fmt.str "After model fixing %a of type %a has no value"
+ pp_gen_ground g pp_ty_gen g)
| ArgOfGroundTermWithoutValueAfterModelFixing (g, n) ->
- Fmt.pf fmt
- "After model fixing arguments %a of %a of type %a has no value"
- Node.pp n Ground.Term.pp (Ground.sem g) Ground.Ty.pp
- (Ground.sem g).ty
- | exn -> raise exn)
+ Some
+ (Fmt.str
+ "After model fixing arguments %a of %a of type %a has no value"
+ Node.pp n Ground.Term.pp (Ground.sem g) Ground.Ty.pp
+ (Ground.sem g).ty)
+ | _ -> None)
(** Helpers *)
module WatchArgs = struct
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index 9d55c9d15838d3ebf6ab4de7328dff963c3e3ca3..01211721e12551a00104946115e437a0cd540799 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -42,6 +42,8 @@ module SeqLim : sig
val unfold_with :
'a t -> init:'b -> f:('b -> 'a -> ('c, 'b) Sequence.Step.t) -> 'c t
+
+ val hd_exn : 'a t -> 'a
end
type check = Right | Wrong | NA | Unknown
diff --git a/src_colibri2/popop_lib/exn_printer.ml b/src_colibri2/popop_lib/exn_printer.ml
index 7efec44d2aa2b468fdfae3d6fef937f15467e49a..291ba0bf2fbfb19d50ad2f09d6cca9c58cdf4564 100644
--- a/src_colibri2/popop_lib/exn_printer.ml
+++ b/src_colibri2/popop_lib/exn_printer.ml
@@ -33,9 +33,6 @@ let exn_printer fmt exn =
with Exit_loop -> ()
-let () =
- Printexc.register_printer (fun exn -> Some (Pp.string_of exn_printer exn))
-
(** usual version *)
let exn_printer fmt exn =
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index 89e160d477e264a4b61fee38f0f2d3f60117f413..d9e85ca2a9d59ea32b25f99e8f89d81cf7a8d347 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -85,7 +85,7 @@ let split_input = function
| `Stdin -> (Sys.getcwd (), `Stdin)
| `File f -> (Filename.dirname f, `File (Filename.basename f))
-let print_exn st = function
+let print_exn_and_exit st = function
(* Sigint, potentially wrapped by the typechecker *)
| Pipeline.Sigint
| Dolmen_loop.Typer.T.Typing_error
@@ -175,14 +175,14 @@ let print_exn st = function
command line"
(* Generic catch-all *)
| e ->
- State.error st "@[<hv>Unhandled exception:@ %s@]" (Printexc.to_string e)
+ State.error ~code:Dolmen_loop.Code.bug st "@[<hv>Internal error:@ %s@]"
+ (Printexc.to_string e)
let handle_exn_with_exit st bt exn =
if st.State.debug then (
Printexc.print_raw_backtrace stderr bt;
Format.eprintf "%s@." (Printexc.to_string exn));
- let () = print_exn st exn in
- exit 2
+ print_exn_and_exit st exn
let handle_exn_with_error _ bt exn = Printexc.raise_with_backtrace exn bt
diff --git a/src_colibri2/tests/solve/models/dune.inc b/src_colibri2/tests/solve/models/dune.inc
index 0e2e72b0121a760a25b46721ab67f33c4a0435c9..d381eb29b1999f7ed376e200b80b3818eab53088 100644
--- a/src_colibri2/tests/solve/models/dune.inc
+++ b/src_colibri2/tests/solve/models/dune.inc
@@ -1,4 +1,6 @@
(rule (action (with-stdout-to abs_real.smt2.res (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status colibri2 %{dep:abs_real.smt2}))))
(rule (alias runtest) (action (diff abs_real.smt2.oracle abs_real.smt2.res)))
+(rule (action (with-stdout-to function.smt2.res (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status colibri2 %{dep:function.smt2}))))
+(rule (alias runtest) (action (diff function.smt2.oracle function.smt2.res)))
(rule (action (with-stdout-to get_value.smt2.res (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status colibri2 %{dep:get_value.smt2}))))
(rule (alias runtest) (action (diff get_value.smt2.oracle get_value.smt2.res)))
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index 393b91ecf69bc0311554a432960094792120a9a1..2e6b6b9a88d7287d0bca1ba178081ba58b35352e 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -283,16 +283,28 @@ module UFModel = struct
module Hargs = Context.Hashtbl (Values)
+ type t = { known : Value.t Hargs.t; other : Value.t option Context.Ref.t }
+
let env =
- HConst.create Fmt.nop "Uninterp.UFModel.env" (fun c _ -> Hargs.create c)
+ HConst.create Fmt.nop "Uninterp.UFModel.env" (fun c _ ->
+ { known = Hargs.create c; other = Context.Ref.create c None })
let find d (g : Ground.s) lv =
let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
- Hargs.find_opt h lv
+ Hargs.find_opt h.known lv
let set d (g : Ground.s) lv v =
let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
- Hargs.set h lv v
+ Hargs.set h.known lv v
+
+ let get_other d (g : Ground.s) =
+ let h = HConst.find env d { tc = g.app; ta = g.tyargs } in
+ match Context.Ref.get h.other with
+ | None ->
+ let o = Interp.SeqLim.hd_exn (Interp.ty d g.ty) in
+ Context.Ref.set h.other (Some o);
+ o
+ | Some x -> x
let on_uninterpreted_domain d g =
let check_or_update g d _ _ =
@@ -318,6 +330,20 @@ module UFModel = struct
Interp.WatchArgs.create d on_uninterpreted_domain g
end
+module V' = struct
+ module T = struct
+ type t = { maps : Value.t UFModel.Values.M.t; other : Value.t }
+ [@@deriving ord, eq, hash, show]
+ end
+
+ include T
+ include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
+
+ let name = "fun"
+end
+
+module V = Value.Register (V')
+
module On_uninterpreted_domain = struct
(** For model fixing *)
@@ -336,9 +362,7 @@ module On_uninterpreted_domain = struct
let lv = IArray.map ~f:interp s.args in
match UFModel.find d s lv with
| Some v' -> Value v'
- | None ->
- (* todo error because should be computed? *)
- NA
+ | None -> Value (UFModel.get_other d s)
end
let init_check d =
@@ -358,6 +382,12 @@ let converter d (t : Ground.t) =
let th_register env =
Ground.register_converter env converter;
init_check env;
- init_ty env
+ init_ty env;
+ Interp.Register.compute env (fun d t ->
+ match Ground.sem t with
+ | { app = { builtin = Expr.Base; _ }; args; _ }
+ when IArray.length args >= 1 ->
+ On_uninterpreted_domain.compute d t
+ | _ -> NA)
let () = Init.add_default_theory th_register