[Quant] Keep the substitution during skolemization

colibrics.opam

@@ -28,3 +28,8 @@ build: [
   ]
 ]
 dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
+pin-depends: [
+  [ "dolmen.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+  [ "dolmen_type.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+  [ "dolmen_loop.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+]

colibrics.opam.template

+pin-depends: [
+  [ "dolmen.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+  [ "dolmen_type.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+  [ "dolmen_loop.0.5~dev" "git+https://github.com/bobot/dolmen.git#for_colibri2" ]
+]

src_colibri2/core/ground.ml

@@ -144,7 +144,7 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
   match t.descr with
   | Var v ->
     begin match Expr.Term.Var.M.find v subst.term with
-      | exception Not_found -> invalid_arg "Not_ground"
+      | exception Not_found -> invalid_arg (Fmt.str "Not_ground: %a" Expr.Term.Var.pp v)
       | n -> n
     end
   | App (f, tyargs, args) ->

src_colibri2/tests/solve/smt_quant/unsat/dune.inc

 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
 (rule (action (with-stdout-to exists.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists.smt2}))))
 (rule (alias runtest) (action (diff oracle exists.smt2.res)))
+(rule (action (with-stdout-to exists2.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:exists2.smt2}))))
+(rule (alias runtest) (action (diff oracle exists2.smt2.res)))
 (rule (action (with-stdout-to forall0.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall0.smt2}))))
 (rule (alias runtest) (action (diff oracle forall0.smt2.res)))
 (rule (action (with-stdout-to forall1.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall1.smt2}))))

src_colibri2/tests/solve/smt_quant/unsat/exists2.smt2

+(set-logic ALL)
+
+(assert (not
+   (forall ((x Real))
+     (=> (= x 1.0) (forall ((y Real)) (= y (* y x)))))))
+
+(check-sat)

src_colibri2/theories/quantifier/quantifier.ml

@@ -159,20 +159,16 @@ let skolemize d (e : Ground.ClosedQuantifier.t) =
   if not (Base.List.is_empty e.ty_vars) then
     invalid_arg "False type quantification";
   let subst_term =
-    List.map
-      (fun v ->
+    List.fold_left
+      (fun acc v ->
         let id = Expr.Term.Const.mk v.Expr.name [] [] v.ty in
         let t = Expr.Term.apply id [] [] in
-        (v, Ground.convert t))
-      e.term_vars
+        Expr.Term.Var.M.add v (Ground.convert t) acc)
+      e.subst.term e.term_vars
   in
   let n =
     Ground.convert
-      ~subst:
-        {
-          Ground.Subst.ty = Expr.Ty.Var.M.empty;
-          term = Expr.Term.Var.M.of_list subst_term;
-        }
+      ~subst:{ Ground.Subst.ty = e.subst.ty; term = subst_term }
       e.body
   in
   Egraph.register d n;

src_common/modulo.mlw

@@ -19,14 +19,7 @@ module Divisible
            let d = a /. m in
            let t = floor d in
            let f = from_int t in
-           assert { f <=. d <. from_int (t + 1) };
-           assert { f <=. d <. f +. 1. };
-           assert { (a /. m) -. 1. <. f <=. a /. m };
-           assert { ((a /. m) -. 1.) *. m <. f *. m <=. (a /. m) *. m };
-           assert { ((a /. m) *. m) -. m <. f *. m };
-           assert { a -. m <. f *. m  <=. a };
-           assert { -. a <=. -. f *. m  <. -. a +. m };
-           assert { 0. <=. a -. f *. m  <. m }
+           assert { f <=. d <. from_int (t + 1) }
 
        predicate ddivisible_using (a b:real) (d:int) =
           a = (from_int d) *. b