From 53ab8ec24618f7592cc75488e6e081452a8800e5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 21 Jan 2021 19:05:51 +0100
Subject: [PATCH] [Quant] Fix forall in forall
Remains a todo with type substitution
---
.../tests/solve/smt_quant/unsat/dune.inc | 2 +
.../tests/solve/smt_quant/unsat/forall8.smt2 | 12 +++
src_colibri2/theories/LRA/delta.ml | 2 +
.../theories/quantifier/InvertedPath.ml | 10 ++-
.../theories/quantifier/InvertedPath.mli | 5 ++
src_colibri2/theories/quantifier/PN.ml | 10 +++
src_colibri2/theories/quantifier/PN.mli | 3 +
src_colibri2/theories/quantifier/pattern.ml | 26 +++++--
src_colibri2/theories/quantifier/pattern.mli | 7 +-
.../theories/quantifier/quantifier.ml | 73 +++++++++++++------
src_colibri2/theories/quantifier/trigger.ml | 25 ++++++-
11 files changed, 138 insertions(+), 37 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_quant/unsat/forall8.smt2
create mode 100644 src_colibri2/theories/quantifier/PN.ml
create mode 100644 src_colibri2/theories/quantifier/PN.mli
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index 70a69ffb9..63371f6c6 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -19,3 +19,5 @@
(rule (alias runtest) (action (diff oracle forall6.smt2.res)))
(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall7.smt2}))))
(rule (alias runtest) (action (diff oracle forall7.smt2.res)))
+(rule (action (with-stdout-to forall8.smt2.res (run %{bin:colibri2} --max-step 1300 %{dep:forall8.smt2}))))
+(rule (alias runtest) (action (diff oracle forall8.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/forall8.smt2 b/src_colibri2/tests/solve/smt_quant/unsat/forall8.smt2
new file mode 100644
index 000000000..8353a3977
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_quant/unsat/forall8.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun P (S S) Bool)
+
+(assert (forall ((x S)) (=> (P x x) (forall ((y S)) (P x y)))))
+
+(declare-fun a () S)
+(declare-fun b () S)
+(assert (P a a))
+(assert (not (P a b)))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/delta.ml b/src_colibri2/theories/LRA/delta.ml
index dfbcf4303..c5e9c5649 100644
--- a/src_colibri2/theories/LRA/delta.ml
+++ b/src_colibri2/theories/LRA/delta.ml
@@ -57,6 +57,7 @@ let ta = Expr.Term.of_var a
let floor_pattern = (* Other floor functions? *)
Colibri2_theories_quantifiers.Pattern.of_term
+ ~subst:Ground.Subst.empty
(Expr.Term.Real.floor_to_int ta)
(* let ceiling_patterns =
@@ -65,6 +66,7 @@ let floor_pattern = (* Other floor functions? *)
let ceiling_pattern =
Colibri2_theories_quantifiers.Pattern.of_term
+ ~subst:Ground.Subst.empty
(Expr.Term.Int.minus (Expr.Term.Real.floor_to_int (Expr.Term.Real.minus ta)))
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 1b856e01a..a485a4cf2 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -80,6 +80,7 @@ let rec exec d acc substs n ip =
module HPC = Datastructure.Memo (PC)
module HPP = Datastructure.Memo (PP)
module HPT = Datastructure.Memo (F_Pos)
+module HPN = Datastructure.Memo (PN)
(** parent-child, wait for a subterm with the right application *)
let pc_ips = HPC.create Fmt.nop "Quantifier.pc" create
@@ -90,6 +91,9 @@ let pp_ips = HPP.create Fmt.nop "Quantifier.pp" create
(** parent-type, wait for a type to match a variable *)
let pt_ips = HPT.create Fmt.nop "Quantifier.pt" Context.Queue.create
+(** parent-node, wait for a subterm with the right class *)
+let pn_ips = HPN.create Fmt.nop "Quantifier.pn" create
+
let add_pattern pat ip =
Context.Ref.set ip
@@
@@ -142,6 +146,10 @@ let insert_pattern d (trigger : Trigger.t) =
let ip = add_match p ip in
let ips = ip :: ips in
ips
+ | Node n ->
+ let ip = HPN.find pn_ips d PN.{ parent = fp; node = n } in
+ let ips = [ ip ] in
+ ips
and insert_children pp_vars f tytl tl =
List.foldi
(fun acc pos p ->
@@ -153,7 +161,7 @@ let insert_pattern d (trigger : Trigger.t) =
in
let pp_vars = Pattern.get_pps trigger.pat in
match trigger.pat with
- | Var _ -> ()
+ | Var _ | Node _ -> ()
| App (f, tytl, tl) ->
let ips = insert_children pp_vars f tytl tl in
List.iter (add_pattern trigger) ips
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index d53db87e9..a4b64a06d 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -34,3 +34,8 @@ module HPT : Datastructure.Sig3 with type key := F_Pos.t
val pt_ips : (Ty.t * t) Context.Queue.t HPT.t
(** The database of inverted path for each parent-type, needed for polymorphic
variables *)
+
+module HPN : Datastructure.Sig3 with type key := PN.t
+
+val pn_ips : t HPN.t
+(** The database of inverted path for each parent-node pairs *)
diff --git a/src_colibri2/theories/quantifier/PN.ml b/src_colibri2/theories/quantifier/PN.ml
new file mode 100644
index 000000000..608538eee
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PN.ml
@@ -0,0 +1,10 @@
+open Colibri2_popop_lib
+
+module T = struct
+ open! Base
+
+ type t = { parent : F_Pos.t; node : Node.t } [@@deriving show, ord, hash, eq]
+end
+
+include T
+include Popop_stdlib.MkDatatype (T)
diff --git a/src_colibri2/theories/quantifier/PN.mli b/src_colibri2/theories/quantifier/PN.mli
new file mode 100644
index 000000000..d3a676cbf
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PN.mli
@@ -0,0 +1,3 @@
+type t = { parent : F_Pos.t; node : Node.t }
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index c626270a0..5cd7975ca 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -6,7 +6,10 @@ open Common
module T = struct
open Base
- type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
+ type t =
+ | Var of Expr.Term.Var.t
+ | App of F.t * Expr.Ty.t list * t list
+ | Node of Node.t
[@@deriving eq, ord, hash]
let rec pp fmt = function
@@ -17,16 +20,22 @@ module T = struct
tyl
Fmt.(list ~sep:comma pp)
tl
+ | Node n -> Node.pp fmt n
end
include T
include Popop_stdlib.MkDatatype (T)
-let rec of_term (t : Expr.Term.t) =
+let rec of_term ~subst (t : Expr.Term.t) =
match t.descr with
- | Var v -> Var v
- | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term a
- | App (f, tys, tl) -> App (f, tys, List.map of_term tl)
+ | Var v -> (
+ match Expr.Term.Var.M.find v subst.Ground.Subst.term with
+ | exception Not_found -> Var v (* todo type substitution *)
+ | n -> Node n )
+ | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term ~subst a
+ | App (f, tys, tl) ->
+ (* todo type substitution *)
+ App (f, tys, List.map (of_term ~subst) tl)
| _ -> (* absurd *) assert false
let init = Ground.Subst.S.singleton Ground.Subst.empty
@@ -99,6 +108,7 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
in
Ground.Subst.S.union substs acc)
Ground.Subst.S.empty s
+ | Node n' -> if Egraph.is_equal d n n' then substs else Ground.Subst.S.empty
let rec check_ty subst (ty : Ground.Ty.t) (p : Expr.Ty.t) : bool =
match p.descr with
@@ -137,6 +147,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
List.for_all2 (check_ty subst) tyl ptyl
&& List.for_all2 (check_term d subst) args pargs)
s
+ | Node n' -> Egraph.is_equal d n n'
let _ = check_term
@@ -191,6 +202,7 @@ let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
(get_parents 0 parg) pargs
in
if Node.S.is_empty nodes then raise Not_found else nodes
+ | Node n -> Node.S.singleton n
let check_term_exists d (subst : Ground.Subst.t) (p : t) : Node.S.t =
try check_term_exists_exn d subst p with Not_found -> Node.S.empty
@@ -201,10 +213,11 @@ let get_pps pattern =
| Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
| App (f, _, tl) ->
List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
+ | Node _ -> acc
in
let m =
match pattern with
- | Var _ -> Expr.Term.Var.M.empty
+ | Var _ | Node _ -> Expr.Term.Var.M.empty
| App (f, _, tl) ->
List.foldi
(fun acc pos p -> aux acc F_Pos.{ f; pos } p)
@@ -263,3 +276,4 @@ let match_any_term d (p : t) : Ground.Subst.S.t =
Ground.Subst.S.union substs acc)
Ground.Subst.S.empty
(F.EnvApps.find env_ground_by_apps d pf)
+ | Node _ -> Ground.Subst.S.empty
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index bf9565f7d..e68c6ef09 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,10 +1,13 @@
(** Pattern *)
-type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
+type t =
+ | Var of Expr.Term.Var.t
+ | App of F.t * Expr.Ty.t list * t list
+ | Node of Node.t
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
-val of_term : Expr.Term.t -> t
+val of_term : subst:Ground.Subst.t -> Expr.Term.t -> t
val init : Ground.Subst.S.t
(** Singleton set with the empty substitution, can be used as initial value for
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 3616679c3..f0750206a 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -10,14 +10,15 @@ let add_trigger d t =
let substs = Pattern.match_any_term d t.pat in
Ground.Subst.S.iter (Trigger.instantiate d t) substs
-let find_new_event d n (info : Info.t) (info' : Info.t) =
- Debug.dprintf6 debug "Find_new_event %a %a %a" Node.pp n Info.pp info Info.pp
- info';
- let symmetric f acc a b =
- if CCEqual.physical a b then f acc a b else f (f acc a b) b a
+let find_new_event d n (info : Info.t) n' (info' : Info.t) =
+ Debug.dprintf8 debug "Find_new_event %a %a %a %a" Node.pp n Info.pp info
+ Node.pp n' Info.pp info';
+ let symmetric f acc na a nb b =
+ if CCEqual.physical a b && Node.equal na nb then f acc na a nb b
+ else f (f acc na a nb b) nb b na a
in
let do_pp pp ip acc =
- let aux acc info1 info2 =
+ let aux acc _ info1 _ info2 =
match
( F_Pos.M.find_opt pp.PP.parent1 info1.Info.parents,
F_Pos.M.find_opt pp.PP.parent2 info2.Info.parents )
@@ -30,13 +31,13 @@ let find_new_event d n (info : Info.t) (info' : Info.t) =
* acc parents *)
Debug.dprintf4 debug_full "[Quant] PP %a found for %a" PP.pp pp
Node.pp n;
- InvertedPath.exec d acc Pattern.init n ip
+ ip :: acc
| _ -> acc
in
- symmetric aux acc info info'
+ symmetric aux acc n info n' info'
in
let do_pc pc ip acc =
- let aux acc info1 info2 =
+ let aux acc _ info1 _ info2 =
match
( F_Pos.M.find_opt pc.PC.parent info1.Info.parents,
F.M.find_opt pc.PC.child info2.Info.apps )
@@ -49,13 +50,26 @@ let find_new_event d n (info : Info.t) (info' : Info.t) =
* acc parents *)
Debug.dprintf4 debug_full "[Quant] PC %a found for %a" PC.pp pc
Node.pp n;
- InvertedPath.exec d acc Pattern.init n ip
+ ip :: acc
| _ -> acc
in
- symmetric aux acc info info'
+ symmetric aux acc n info n' info'
+ in
+ let do_pn pn ip acc =
+ let aux acc n info1 n' _ =
+ if Egraph.is_equal d n' pn.PN.node then
+ match F_Pos.M.find_opt pn.PN.parent info1.Info.parents with
+ | Some _ ->
+ Debug.dprintf4 debug_full "[Quant] PC %a found for %a" PN.pp pn
+ Node.pp n;
+ ip :: acc
+ | _ -> acc
+ else acc
+ in
+ symmetric aux acc n info n' info'
in
let do_pt f_pos q acc =
- let aux acc info1 info2 =
+ let aux acc _ info1 _ info2 =
match F_Pos.M.find_opt f_pos info1.Info.parents with
| Some _ ->
Context.Queue.fold
@@ -81,16 +95,25 @@ let find_new_event d n (info : Info.t) (info' : Info.t) =
else (
Debug.dprintf6 debug_full "[Quant] PT %a %a found for %a"
F_Pos.pp f_pos Expr.Ty.pp vty Node.pp n;
- InvertedPath.exec d acc Pattern.init n ip ))
+ ip :: acc ))
acc q
| None -> acc
in
- symmetric aux acc info info'
+ symmetric aux acc n info n' info'
in
- let acc = Trigger.M.empty in
+ let acc = [] in
let acc = InvertedPath.HPP.fold do_pp InvertedPath.pp_ips d acc in
let acc = InvertedPath.HPC.fold do_pc InvertedPath.pc_ips d acc in
let acc = InvertedPath.HPT.fold do_pt InvertedPath.pt_ips d acc in
+ let acc = InvertedPath.HPN.fold do_pn InvertedPath.pn_ips d acc in
+ acc
+
+let process_inverted_path d n acc =
+ let acc =
+ List.fold_left
+ (fun acc ip -> InvertedPath.exec d acc Pattern.init n ip)
+ Trigger.M.empty acc
+ in
Trigger.M.iter
(fun tri substs -> Ground.Subst.S.iter (Trigger.instantiate d tri) substs)
acc
@@ -105,7 +128,7 @@ module Delayed_find_new_event = struct
let key =
Events.Dem.create_key
( module struct
- type d = Node.t * Info.t * Info.t
+ type d = Node.t * InvertedPath.t list
type t = unit
@@ -114,12 +137,12 @@ module Delayed_find_new_event = struct
let delay = Events.Delayed_by 10
- type runable = Node.t * Info.t * Info.t [@@deriving show]
+ type runable = Node.t * InvertedPath.t list [@@deriving show]
let print_runable = pp_runable
- let run d (n, info, info') =
- find_new_event d n info info';
+ let run d (n, ips) =
+ process_inverted_path d n ips;
None
end
@@ -151,8 +174,10 @@ let () =
let info = Info.merge d ~other ~repr info0 info1 in
Egraph.set_dom d Info.dom cl0 info;
Egraph.set_dom d Info.dom cl1 info;
- Egraph.register_delayed_event d Delayed_find_new_event.key
- (repr, info0, info1)
+ let ips = find_new_event d cl0 info0 cl1 info1 in
+ if not (List.is_empty ips) then
+ Egraph.register_delayed_event d Delayed_find_new_event.key
+ (repr, ips)
end )
let skolemize d (e : Ground.ClosedQuantifier.t) =
@@ -228,11 +253,11 @@ let add_info_on_ground_terms d thg =
match Egraph.get_dom d Info.dom repr with
| None ->
Egraph.set_dom d Info.dom repr info;
- find_new_event d repr info info
+ process_inverted_path d repr (find_new_event d repr info repr info)
| Some info' ->
Egraph.set_dom d Info.dom repr (Info.merge d ~repr ~other info info');
- find_new_event d repr info info;
- find_new_event d repr info info'
+ process_inverted_path d repr (find_new_event d repr info repr info);
+ process_inverted_path d repr (find_new_event d repr info repr info')
in
let add_pc pos n =
merge_info n
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 84980929a..1b7444353 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -51,11 +51,11 @@ let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
let sty, st =
Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) pat
in
- Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs)
+ Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st)
pats
in
- let pats_full = List.map Pattern.of_term pats_full in
- let pats_partial = List.map Pattern.of_term pats_partial in
+ let pats_full = List.map (Pattern.of_term ~subst:cq'.subst) pats_full in
+ let pats_partial = List.map (Pattern.of_term ~subst:cq'.subst) pats_partial in
let multi_pats =
let rec aux acc other = function
| [] -> acc
@@ -121,7 +121,13 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
List.filter_map
(fun (c, (sty, st)) ->
if Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs then
- Some { pat = Pattern.of_term c; form = cq; eager = true; checks = [] }
+ Some
+ {
+ pat = Pattern.of_term ~subst:cq'.subst c;
+ form = cq;
+ eager = true;
+ checks = [];
+ }
else None)
pats
in
@@ -138,10 +144,21 @@ let add_trigger d t =
match t.pat with
| Var _ -> Datastructure.Queue.push env_vars d t
| App (f, _, _) -> Context.Queue.push (F.EnvApps.find env_tri_by_apps d f) t
+ | Node _ -> ()
let instantiate_aux d tri subst =
let form = Ground.ThClosedQuantifier.sem tri.form in
Debug.incr nb_instantiation;
+ let subst =
+ {
+ Ground.Subst.ty =
+ Expr.Ty.Var.M.union (fun _ _ -> assert false) subst.ty form.subst.ty;
+ Ground.Subst.term =
+ Expr.Term.Var.M.union
+ (fun _ _ -> assert false)
+ subst.Ground.Subst.term form.subst.term;
+ }
+ in
let n = Ground.convert ~subst form.body in
if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
Debug.incr nb_new_instantiation;
--
GitLab