From 79b56fe599d486c5247a23112ddee8508feb80e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 12 Nov 2020 11:36:14 +0100
Subject: [PATCH] Add tests for UF and simplify synTerm
---
src_colibri2/core/synTerm.ml | 42 ++---
src_colibri2/core/synTerm.mli | 9 +-
src_colibri2/solver/scheduler.ml | 178 ++++++++----------
src_colibri2/tests/solve/smt_uf/sat/dune | 8 +
src_colibri2/tests/solve/smt_uf/sat/dune.inc | 3 +
src_colibri2/tests/solve/smt_uf/unsat/dune | 8 +
.../tests/solve/smt_uf/unsat/dune.inc | 21 +++
src_colibri2/tests/tests_uf.ml | 141 +++++++-------
src_colibri2/theories/LRA/LRA.ml | 42 ++---
src_colibri2/theories/bool/boolean.ml | 58 +++---
src_colibri2/theories/bool/equality.ml | 18 +-
src_colibri2/theories/bool/uninterp.ml | 13 +-
src_colibri2/theories/bool/uninterp.mli | 10 +-
13 files changed, 282 insertions(+), 269 deletions(-)
create mode 100644 src_colibri2/tests/solve/smt_uf/sat/dune
create mode 100644 src_colibri2/tests/solve/smt_uf/sat/dune.inc
create mode 100644 src_colibri2/tests/solve/smt_uf/unsat/dune
create mode 100644 src_colibri2/tests/solve/smt_uf/unsat/dune.inc
diff --git a/src_colibri2/core/synTerm.ml b/src_colibri2/core/synTerm.ml
index 17550576e..9a053bfc1 100644
--- a/src_colibri2/core/synTerm.ml
+++ b/src_colibri2/core/synTerm.ml
@@ -35,8 +35,7 @@ let node_of_term x = ThTerm.node (ThTerm.index x)
type env = {
- converters: (Egraph.t -> Expr.Term.t -> Node.t option) list;
- decvars: (Expr.Term.t -> Node.t -> Egraph.choice option) list;
+ converters: (Egraph.t -> Expr.Term.t -> Node.t -> unit) list;
}
let converters = Env.Saved.create_key (module struct
@@ -46,11 +45,7 @@ let converters = Env.Saved.create_key (module struct
let register_converter env r =
let e = Egraph.get_env env converters in
- Egraph.set_env env converters {e with converters = r::e.converters}
-
-let register_decvars env r =
- let e = Egraph.get_env env converters in
- Egraph.set_env env converters {e with decvars = r::e.decvars}
+ Egraph.set_env env converters {converters = r::e.converters}
let () = Env.Saved.register (fun _ _ -> ()) converters
@@ -67,24 +62,21 @@ module DaemonConvertTerm = struct
let e = Egraph.get_env d converters in
let thterm = ThTerm.coerce_thterm thterm in
let v = ThTerm.sem thterm in
- begin match v with
- | { descr = App({builtin = Dolmen_std.Expr.Base; _ },_,[]); _ } ->
- let n = ThTerm.node thterm in
- List.iter (fun f ->
- Opt.iter
- (Egraph.register_decision d)
- (f v n)
- ) e.decvars
- | _ -> ()
- end;
- let iter conv =
- match conv d v with
- | None -> ()
- | Some node ->
- Egraph.register d node;
- Egraph.merge d (ThTerm.node thterm) node
+ let rec handle (v:Expr.Term.t) =
+ match v with
+ | { descr = Binder(Letin l,t); _ } ->
+ let subst = List.fold_left
+ (fun acc (v,t) -> Expr.Subst.Var.bind acc v t)
+ Expr.Subst.empty l
+ in
+ (** todo subst with cache for not blowing-up memory *)
+ handle (Expr.Term.subst Expr.Subst.empty subst t)
+ | _ ->
+ let cl = ThTerm.node thterm in
+ let iter conv = conv d v cl in
+ List.iter iter e.converters
in
- List.iter iter e.converters
+ handle v
end with Exit -> () end
| _ -> raise UnwaitedEvent
@@ -93,7 +85,7 @@ end
module RDaemonConvertTerm = Demon.Fast.Register(DaemonConvertTerm)
let init env =
- Egraph.set_env env converters {converters=[]; decvars = []};
+ Egraph.set_env env converters {converters=[]};
RDaemonConvertTerm.init env;
Demon.Fast.attach env
DaemonConvertTerm.key [Demon.Create.EventRegSem(ThTerm.key,())];
diff --git a/src_colibri2/core/synTerm.mli b/src_colibri2/core/synTerm.mli
index 60f4fda96..7645b601a 100644
--- a/src_colibri2/core/synTerm.mli
+++ b/src_colibri2/core/synTerm.mli
@@ -33,13 +33,6 @@ val init: Egraph.t -> unit
val register_converter:
Egraph.t ->
- (Egraph.t -> Expr.Term.t -> Node.t option) ->
+ (Egraph.t -> Expr.Term.t -> Node.t -> unit) ->
unit
(** register converters between syntactic terms *)
-
-
-val register_decvars:
- Egraph.t ->
- (Expr.Term.t -> Node.t -> Egraph.choice option) ->
- unit
-(** register decision adder on variables *)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index f0d3824a9..0c809dcd2 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -41,6 +41,7 @@ let stats_dec = Debug.register_stats_int ~name:"Scheduler.decision" ~init:0
let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
exception NeedStopDelayed
+exception Contradiction
module Att = struct
type t =
@@ -64,22 +65,23 @@ module Att = struct
| Decision (_,choice) -> float_of_int choice.prio
end
-exception Contradiction = Egraph.Contradiction
-
module Prio = Leftistheap.Make(Att)
+type bp_kind =
+ | Choices of (Egraph.t -> unit) list
+ | External
+
type bp =
{ pre_wakeup_daemons : Prio.t;
pre_prev_scheduler_state : bp option;
pre_backtrack_point : Context.bp;
- pre_choices : (Egraph.t -> unit) list;
+ kind : bp_kind;
pre_level : int;
}
type t =
{ mutable wakeup_daemons : Prio.t;
mutable prev_scheduler_state : bp option;
- mutable choices : (Egraph.t -> unit) list;
solver_state : Egraph.Backtrackable.t;
mutable delayed : Egraph.t option;
(* global *)
@@ -113,7 +115,6 @@ let new_solver () =
let context = Context.create () in
{ wakeup_daemons = Prio.empty;
prev_scheduler_state = None;
- choices = [];
solver_state = Egraph.Backtrackable.new_t (Context.creator context);
context;
delayed = None;
@@ -122,23 +123,33 @@ let new_solver () =
level = 0;
}
-let push t =
+let push kind t =
if Debug.test_flag debug_dotgui then
Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
- Debug.dprintf0 debug_pushpop "[Scheduler] push";
+ Debug.dprintf2 debug_pushpop "[Scheduler] push from %a" print_level t;
let prev =
{ pre_wakeup_daemons = t.wakeup_daemons;
pre_prev_scheduler_state = t.prev_scheduler_state;
pre_backtrack_point = Context.bp t.context;
- pre_choices = t.choices;
+ kind;
pre_level = t.level;
} in
- t.choices <- [];
t.level <- t.level + 1;
t.prev_scheduler_state <- Some prev;
ignore (Context.push t.context);
prev
+let pop_to t prev =
+ Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a"
+ print_level t;
+ t.wakeup_daemons <- prev.pre_wakeup_daemons;
+ t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
+ t.level <- prev.pre_level;
+ Context.pop prev.pre_backtrack_point;
+ Egraph.Backtrackable.draw_graph t.solver_state;
+ Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
+ print_level t
+
let update_prio t chogen =
Node.H.change (function
| None -> Some (!(t.var_inc))
@@ -181,28 +192,6 @@ let new_delayed =
conflict_analysis t pexp
*)
-let pop_to t prev =
- Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a"
- print_level t;
- t.wakeup_daemons <- prev.pre_wakeup_daemons;
- t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
- t.choices <- prev.pre_choices;
- t.level <- prev.pre_level;
- Context.pop prev.pre_backtrack_point;
- let d = new_delayed t in
- Egraph.Backtrackable.draw_graph t.solver_state;
- Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
- print_level t;
- d
-
-
-let rec apply_learnt t d =
- try
- run_until_dec t d;
- d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction during apply learnt";
- conflict_analysis t
(*
and conflict_analysis t pexp =
@@ -229,94 +218,82 @@ let rec apply_learnt t d =
pop_to llearnt t prev
*)
-and conflict_analysis t =
+let rec conflict_analysis t =
if Debug.test_flag debug_dotgui then
Egraph.Backtrackable.draw_graph ~force:true t.solver_state;
Debug.incr stats_con;
t.var_inc := !(t.var_inc) *. var_decay;
- (** We look for the level just below the backtrack level *)
- let rewind t prevo =
- match prevo with
+ let rec rewind () =
+ match t.prev_scheduler_state with
| None ->
Debug.dprintf0 debug "[Scheduler] learnt clause false at level 0";
raise Contradiction
| Some prev ->
- let d = pop_to t prev in
- d
+ pop_to t prev;
+ t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
+ match prev.kind with
+ | Choices [] -> rewind ()
+ | Choices (choice::choices) ->
+ make_choice t choice choices
+ | External -> raise Contradiction
in
- let d =
- rewind t t.prev_scheduler_state in
- t.wakeup_daemons <- Prio.reprio t.decprio t.wakeup_daemons;
- apply_learnt t d
+ rewind ()
and try_run_dec:
t -> Egraph.t -> Prio.t -> Egraph.choice -> Egraph.t = fun t d prio choice ->
- (** First we verify its the decision is at this point needed *)
- assert (t.choices = []);
- try
- match choice.choice d with
- | Egraph.DecNo | Egraph.DecTodo [] ->
- t.wakeup_daemons <- prio;
- d (** d can be precised by choose_decision *)
- | Egraph.DecTodo (todo::todos) ->
- (** We remove the decision it is replaced by the todos,
- we can change the interface of choice and in that case
- we want to keep the decision in the current branch *)
- t.wakeup_daemons <- prio;
- Debug.incr stats_dec;
- make_choice t d todo todos
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
-
-and make_choice t d todo todos =
- Egraph.Backtrackable.delayed_stop d;
- t.choices <- todos;
- begin match todos with
- | [] -> ()
- | _ -> ignore (push t)
- end;
+ (** First we verify its the decision is at this point needed *)
+ match choice.choice d with
+ | Egraph.DecNo | Egraph.DecTodo [] ->
+ t.wakeup_daemons <- prio;
+ d (** d can be precised by choose_decision *)
+ | Egraph.DecTodo (todo::todos) ->
+ (** We remove the decision it is replaced by the todos,
+ we can change the interface of choice and in that case
+ we want to keep the decision in the current branch *)
+ t.wakeup_daemons <- prio;
+ Debug.incr stats_dec;
+ Egraph.Backtrackable.delayed_stop d;
+ make_choice t todo todos
+
+and make_choice t todo todos =
+ ignore (push (Choices todos) t);
let d = new_delayed t in
- todo d;
- d
+ try
+ todo d;
+ d
+ with Egraph.Contradiction ->
+ conflict_analysis t
-and run_until_dec t d =
- let act = Prio.min t.wakeup_daemons in
- match act with
- | Some (Att.Daemon (_,att)) -> begin
- let _, prio = Prio.extract_min t.wakeup_daemons in
- Debug.incr stats_propa;
- t.wakeup_daemons <- prio;
- Egraph.Backtrackable.run_daemon d att;
- Egraph.Backtrackable.flush d;
- run_until_dec t d
- end
- | Some (Att.Decision (_,_)) | None -> ()
+(* let rec run_until_dec t d =
+ * let act = Prio.min t.wakeup_daemons in
+ * match act with
+ * | Some (Att.Daemon (_,att)) -> begin
+ * let _, prio = Prio.extract_min t.wakeup_daemons in
+ * Debug.incr stats_propa;
+ * t.wakeup_daemons <- prio;
+ * Egraph.Backtrackable.run_daemon d att;
+ * Egraph.Backtrackable.flush d;
+ * run_until_dec t d
+ * end
+ * | Some (Att.Decision (_,_)) | None -> () *)
let run_one_step t d =
- match t.choices with
- | [] -> begin
- let act, prio = Prio.extract_min t.wakeup_daemons in
- match act with
- | Att.Daemon (_,att) -> begin
- Debug.incr stats_propa;
- t.wakeup_daemons <- prio;
- try
- Egraph.Backtrackable.run_daemon d att; d
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
- end
- | Att.Decision (_,chogen) -> try_run_dec t d prio chogen
+ let act, prio = Prio.extract_min t.wakeup_daemons in
+ match act with
+ | Att.Daemon (_,att) -> begin
+ Debug.incr stats_propa;
+ t.wakeup_daemons <- prio;
+ try
+ Egraph.Backtrackable.run_daemon d att; d
+ with Egraph.Contradiction ->
+ Debug.dprintf0 debug "[Scheduler] Contradiction";
+ conflict_analysis t
end
- | todo::todos ->
- try
- make_choice t d todo todos
- with Egraph.Contradiction ->
- Debug.dprintf0 debug "[Scheduler] Contradiction";
- conflict_analysis t
+ | Att.Decision (_,chogen) ->
+ Debug.dprintf0 debug "[Scheduler] decision";
+ try_run_dec t d prio chogen
let rec flush t d =
try
@@ -428,3 +405,4 @@ let run ?nodec ?limit ~theories f =
`Contradiction
let pop_to st bp = ignore (pop_to st bp)
+let push st = push External st
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune b/src_colibri2/tests/solve/smt_uf/sat/dune
new file mode 100644
index 000000000..47c20f59d
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune
@@ -0,0 +1,8 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
+ (mode promote)
+)
diff --git a/src_colibri2/tests/solve/smt_uf/sat/dune.inc b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
new file mode 100644
index 000000000..0b8d7662a
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_uf/sat/dune.inc
@@ -0,0 +1,3 @@
+(rule (action (with-stdout-to oracle (echo "sat\n"))))
+(rule (action (with-stdout-to bad_conflict.smt2.res (run colibri2 --max-step 1000 bad_conflict.smt2))))
+(rule (alias runtest) (action (diff oracle bad_conflict.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune b/src_colibri2/tests/solve/smt_uf/unsat/dune
new file mode 100644
index 000000000..9ca94f895
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune
@@ -0,0 +1,8 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps (glob_files *.cnf) (glob_files *.smt2))
+ (action (with-stdout-to dune.inc (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote)
+)
diff --git a/src_colibri2/tests/solve/smt_uf/unsat/dune.inc b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
new file mode 100644
index 000000000..0fd7accf3
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_uf/unsat/dune.inc
@@ -0,0 +1,21 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to NEQ004_size4__decide_eq_us.smt2.res (run colibri2 --max-step 1000 NEQ004_size4__decide_eq_us.smt2))))
+(rule (alias runtest) (action (diff oracle NEQ004_size4__decide_eq_us.smt2.res)))
+(rule (action (with-stdout-to deltaed0.smt2.res (run colibri2 --max-step 1000 deltaed0.smt2))))
+(rule (alias runtest) (action (diff oracle deltaed0.smt2.res)))
+(rule (action (with-stdout-to diff_to_value_for_bool.smt2.res (run colibri2 --max-step 1000 diff_to_value_for_bool.smt2))))
+(rule (alias runtest) (action (diff oracle diff_to_value_for_bool.smt2.res)))
+(rule (action (with-stdout-to diff_value_substupfalse.smt2.res (run colibri2 --max-step 1000 diff_value_substupfalse.smt2))))
+(rule (alias runtest) (action (diff oracle diff_value_substupfalse.smt2.res)))
+(rule (action (with-stdout-to distinct.smt2.res (run colibri2 --max-step 1000 distinct.smt2))))
+(rule (alias runtest) (action (diff oracle distinct.smt2.res)))
+(rule (action (with-stdout-to eq_diamond2.smt2.res (run colibri2 --max-step 1000 eq_diamond2.smt2))))
+(rule (alias runtest) (action (diff oracle eq_diamond2.smt2.res)))
+(rule (action (with-stdout-to equality_norm_set.smt2.res (run colibri2 --max-step 1000 equality_norm_set.smt2))))
+(rule (alias runtest) (action (diff oracle equality_norm_set.smt2.res)))
+(rule (action (with-stdout-to many_distinct.smt2.res (run colibri2 --max-step 1000 many_distinct.smt2))))
+(rule (alias runtest) (action (diff oracle many_distinct.smt2.res)))
+(rule (action (with-stdout-to polyeq_genequality_deltaed.smt2.res (run colibri2 --max-step 1000 polyeq_genequality_deltaed.smt2))))
+(rule (alias runtest) (action (diff oracle polyeq_genequality_deltaed.smt2.res)))
+(rule (action (with-stdout-to xor.smt2.res (run colibri2 --max-step 1000 xor.smt2))))
+(rule (alias runtest) (action (diff oracle xor.smt2.res)))
diff --git a/src_colibri2/tests/tests_uf.ml b/src_colibri2/tests/tests_uf.ml
index 1d7005b4d..88774546c 100644
--- a/src_colibri2/tests/tests_uf.ml
+++ b/src_colibri2/tests/tests_uf.ml
@@ -30,9 +30,12 @@ let ($$) f x = f x
open Expr
-let a = fresh Ty.bool "a"
-let b = fresh Ty.bool "b"
-let c = fresh Ty.bool "c"
+let ta = fresht Ty.bool "a"
+let tb = fresht Ty.bool "b"
+let tc = fresht Ty.bool "c"
+let a = SynTerm.node_of_term ta
+let b = SynTerm.node_of_term tb
+let c = SynTerm.node_of_term tc
let empty _ =
let env = run $$ fun env ->
@@ -74,12 +77,13 @@ let noteq _ =
let basic = "Uf.Basic" >::: ["empty" >:: empty; "tauto" >:: tauto;
"trans" >:: trans; "noteq" >:: noteq]
-(*
-let f = Uninterp.fun1 ty "f"
-let fa = f a
-let fb = f b
-let ffa = f (f a)
-let ffb = f (f b)
+
+let f = Expr.Term.Const.mk "f" [] [Ty.bool] Ty.bool
+let f x = Expr.Term.apply f [] [x]
+let fa = SynTerm.node_of_term @@ f ta
+let fb = SynTerm.node_of_term @@ f tb
+let ffa = SynTerm.node_of_term @@ f (f ta)
+let ffb = SynTerm.node_of_term @@ f (f tb)
let refl _ =
let env = run $$ fun env ->
@@ -95,7 +99,7 @@ let empty _ =
let congru _ =
let env = run $$ fun env ->
- Shuffle.seql [
+ Colibri2_stdlib.Shuffle.seql [
(fun () -> register env fa);
(fun () -> register env fb);
(fun () -> register env a);
@@ -108,7 +112,7 @@ let congru _ =
let _2level _ =
let env = run $$ fun env ->
- Shuffle.seql [
+ Colibri2_stdlib.Shuffle.seql [
(fun () -> register env ffa);
(fun () -> register env ffb);
(fun () -> register env a);
@@ -129,36 +133,36 @@ let _2level' _ =
let bigger _ =
- let rec bf n = if n < 1 then a else (f (bf(n-1))) in
- let fa = bf 1 in
- let fffa = bf 3 in
- let fffffa = bf 5 in
+ let rec bf n = if n < 1 then ta else f (bf(n-1)) in
+ let fa = SynTerm.node_of_term @@ bf 1 in
+ let fffa = SynTerm.node_of_term @@ bf 3 in
+ let fffffa = SynTerm.node_of_term @@ bf 5 in
let env = run $$ fun env ->
- Shuffle.seql
+ Colibri2_stdlib.Shuffle.seql
[(fun () -> register env a);
(fun () -> register env fa);
(fun () -> register env fffa);
(fun () -> register env fffffa);
];
- Shuffle.seql
+ Colibri2_stdlib.Shuffle.seql
[(fun () -> merge env a fffa);
(fun () -> merge env fffffa a)];
in
assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
(is_equal env fa a)
-
-
-
-let congru1 = "Uf.Congru 1 arg" >::: ["refl" >:: refl; "congru" >:: congru;
+let congru1 = "Uf.Congru 1 arg" >::: ["refl" >:: refl;"congru" >:: congru;
"2level" >:: _2level; "2level'" >:: _2level';
- "bigger" >:: bigger]
-
-
-let g = Uninterp.fun2 ty "g"
-let gab = g a b
-let gaa = g a a
-let ggabb = g gab b
+ "bigger" >:: bigger]
+let (!!) = SynTerm.node_of_term
+let g = Expr.Term.Const.mk "g" [] [Ty.bool;Ty.bool] Ty.bool
+let g a b = Expr.Term.apply g [] [a;b]
+let gab = g ta tb
+let gaa = g ta ta
+let ggabb = g gab tb
+let gab = !!gab
+let gaa = !!gaa
+let ggabb = !!ggabb
let refl _ =
let env = run $$ fun env -> register env gab in
@@ -166,7 +170,7 @@ let refl _ =
let congru _ =
let env = run $$ fun env ->
- Shuffle.seql [
+ Colibri2_stdlib.Shuffle.seql [
(fun () -> register env gab);
(fun () -> register env gaa);
(fun () -> register env a);
@@ -187,11 +191,11 @@ let notcongru _ =
let _2level _ =
let env = run $$ fun env ->
- Shuffle.seql [
+ Colibri2_stdlib.Shuffle.seql [
(fun () -> register env a);
(fun () -> register env gab);
];
- Shuffle.seql [
+ Colibri2_stdlib.Shuffle.seql [
(fun () -> merge env gab a;);
(fun () -> register env ggabb);
];
@@ -207,75 +211,72 @@ let merge env x y =
register env y;
merge env x y
-let x = Variable.fresh ty "x"
-let y = Variable.fresh ty "y"
+let x = fresht Ty.bool "x"
+let y = fresht Ty.bool "y"
let altergo0 _ =
- let h = Uninterp.fun1 ty "h" in
- let g = Uninterp.fun2 ty "g" in
- let gax = g a x in
+ let h = Expr.Term.Const.mk "h" [] [Ty.bool] Ty.bool in
+ let h x = Expr.Term.apply h [] [x] in
+ let g = Expr.Term.Const.mk "g" [] [Ty.bool;Ty.bool] Ty.bool in
+ let g x y = Expr.Term.apply g [] [x;y] in
+ let gax = g ta x in
let hx = h x in
- let gahx = g a hx in
+ let gahx = g ta hx in
let ggahxx = g gahx x in
let env = run $$ fun env ->
- Shuffle.seql
- [(fun () -> merge env hx x);
- (fun () -> merge env gax a)];
- register env ggahxx
+ Colibri2_stdlib.Shuffle.seql
+ [(fun () -> merge env !!hx !!x);
+ (fun () -> merge env !!gax a)];
+ register env !!ggahxx
in
assert_bool "h(x)=x and g(a,x)=a -> g(g(a,h(x)),x)=a"
- (is_equal env ggahxx a)
+ (is_equal env !!ggahxx a)
let altergo1 _ =
- let h = Uninterp.fun2 ty "h" in
- let rec bf n = if n < 1 then a else f (bf (n-1)) in
+ let h = Expr.Term.Const.mk "h" [] [Ty.bool;Ty.bool] Ty.bool in
+ let h x y = Expr.Term.apply h [] [x;y] in
+ let rec bf n = if n < 1 then ta else f (bf (n-1)) in
let fffa = bf 3 in
let fffffa = bf 5 in
let gxy = g x y in
let ggxyy = g gxy y in
- let hggxyya = h ggxyy a in
- let fa = f a in
+ let hggxyya = h ggxyy ta in
+ let fa = f ta in
let hxfa = h x fa in
let env = run $$ fun env ->
- Shuffle.seql
- [(fun () -> merge env fffa a);
- (fun () -> merge env fffffa a);
- (fun () -> merge env gxy x)];
- register env hggxyya;
- register env hxfa;
+ Colibri2_stdlib.Shuffle.seql
+ [(fun () -> merge env !!fffa a);
+ (fun () -> merge env !!fffffa a);
+ (fun () -> merge env !!gxy !!x)];
+ register env !!hggxyya;
+ register env !!hxfa;
in
assert_bool
"f(f(f(a)))=a and f(f(f(f(f(a)))))=a and g(x,y)=x -> \
h(g(g(x,y),y),a)=h(x,f(a))"
- (is_equal env hggxyya hxfa)
+ (is_equal env !!hggxyya !!hxfa)
let altergo2 _ =
- let h = Uninterp.fun2 ty "h" in
+ let h = Expr.Term.Const.mk "h" [] [Ty.bool;Ty.bool] Ty.bool in
+ let h x y = Expr.Term.apply h [] [x;y] in
let gxy = g x y in
- let fa = f a in
+ let fa = f ta in
let ggxyy = g gxy y in
- let hggxyya = h ggxyy a in
+ let hggxyya = h ggxyy ta in
let hxfa = h x fa in
let env = run $$ fun env ->
- Shuffle.seql
- [(fun () -> merge env fa a);
- (fun () -> merge env gxy x)];
- register env hggxyya;
- register env hxfa;
+ Colibri2_stdlib.Shuffle.seql
+ [(fun () -> merge env !!fa a);
+ (fun () -> merge env !!gxy !!x)];
+ register env !!hggxyya;
+ register env !!hxfa;
in
assert_bool
"f(a) = a -> g(x,y)=x -> h(g(g(x,y),y),a)=h(x,f(a))"
- (is_equal env hggxyya hxfa)
+ (is_equal env !!hggxyya !!hxfa)
let altergo = "Uf.altergo tests" &: [altergo0; altergo1; altergo2]
-let files = []
-
-let altergo2 = TestList (List.map Tests_lib.test_split files)
-*)
-
-
-let tests = OUnit2.test_list [basic;(* congru1;congru2;altergo;altergo2;*)
- ]
+let tests = OUnit2.test_list [basic; congru1;congru2;altergo]
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index f8491a49b..84cdd0fd2 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -491,27 +491,34 @@ let gt cl1 cl2 = lt cl2 cl1
let ge cl1 cl2 = le cl2 cl1
(** {2 Initialization} *)
-let converter d (f:Expr.Term.t) =
+let converter d (f:Expr.Term.t) res =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
+ let reg n =
+ Egraph.register d n;
+ Egraph.merge d res n
+ in
match f with
+ | { descr = App({builtin = Dolmen_std.Expr.Base; _ },_,_); ty }
+ when Expr.Ty.equal ty Expr.Ty.real ->
+ Egraph.register_decision d (ChoLRA.choice res)
| { descr = Expr.App({builtin = Expr.Integer s},[],[]); _ } ->
- Some (cst (Q.of_string s))
+ reg (cst (Q.of_string s))
| { descr = Expr.App({builtin = Expr.Decimal s},[],[]); _ } ->
- Some (cst (Q.of_string_decimal s))
+ reg (cst (Q.of_string_decimal s))
| { descr = Expr.App({builtin = Expr.Rational s},[],[]); _ } ->
- Some (cst (Q.of_string_decimal s))
+ reg (cst (Q.of_string_decimal s))
| { descr = Expr.App({builtin = Expr.Add},[],[a;b]); _ } ->
- Some (add (of_term a) (of_term b))
+ reg (add (of_term a) (of_term b))
| { descr = Expr.App({builtin = Expr.Sub},[],[a;b]); _ } ->
- Some (sub (of_term a) (of_term b))
+ reg (sub (of_term a) (of_term b))
| { descr = Expr.App({builtin = Expr.Minus},[],[a]); _ } ->
- Some (neg (of_term a))
+ reg (neg (of_term a))
| { descr = Expr.App({builtin = Expr.Mul},[],args); _ } -> begin
- let mult_cst c t = Some (mult_cst c (of_term t)) in
+ let mult_cst c t = reg (mult_cst c (of_term t)) in
match args with
| [{descr = Expr.App({builtin = Expr.Integer s; _},[],[])};arg2] ->
mult_cst (Q.of_string s) arg2
@@ -525,23 +532,17 @@ let converter d (f:Expr.Term.t) =
mult_cst (Q.of_string_decimal s) arg2
| [arg2;{descr = Expr.App({builtin = Expr.Rational s; _},[],[])}] ->
mult_cst (Q.of_string_decimal s) arg2
- | _ -> None
+ | _ -> ()
end
| { descr = Expr.App({builtin = Expr.Lt},[],[arg1;arg2]); _ } ->
- Some (lt (of_term arg1) (of_term arg2))
+ reg (lt (of_term arg1) (of_term arg2))
| { descr = Expr.App({builtin = Expr.Leq},[],[arg1;arg2]); _ } ->
- Some (le (of_term arg1) (of_term arg2))
+ reg (le (of_term arg1) (of_term arg2))
| { descr = Expr.App({builtin = Expr.Gt},[],[arg1;arg2]); _ } ->
- Some (gt (of_term arg1) (of_term arg2))
+ reg (gt (of_term arg1) (of_term arg2))
| { descr = Expr.App({builtin = Expr.Geq},[],[arg1;arg2]); _ } ->
- Some (ge (of_term arg1) (of_term arg2))
- | _ -> None
-
-let decvars t n =
- if Expr.Ty.equal (Expr.Term.ty t) Expr.Ty.real
- then Some (ChoLRA.choice n)
- else None
-
+ reg (ge (of_term arg1) (of_term arg2))
+ | _ -> ()
let th_register env =
RDaemonPropa.init env;
@@ -552,7 +553,6 @@ let th_register env =
DaemonPropa.init
env;
SynTerm.register_converter env converter;
- SynTerm.register_decvars env decvars;
Demon.Fast.register_init_daemon_value
~name:"RealValueToDom"
(module RealValue)
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index cfe2b0ead..28db037b4 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -411,27 +411,6 @@ let _false = node_false
let set_true env node = set_bool env node true
let set_false env node = set_bool env node false
-let converter d (f:Expr.Term.t) =
- let of_term t =
- let n = SynTerm.node_of_term t in
- Egraph.register d n;
- n
- in
- match f with
- | { descr = Expr.App({builtin = Expr.Or},[],args); _ } ->
- Some (_or (List.map of_term args))
- | { descr = Expr.App({builtin = Expr.And},[],args); _ } ->
- Some (_and (List.map of_term args))
- | { descr = Expr.App({builtin = Expr.Imply},[],[arg1;arg2]); _ } ->
- Some (gen false [of_term arg1,true;of_term arg2,false])
- | { descr = Expr.App({builtin = Expr.Neg},[],[arg]); _ } ->
- Some (_not (of_term arg))
- | { descr = Expr.App({builtin = Expr.True},[],[]); _ } ->
- Some _true
- | { descr = Expr.App({builtin = Expr.False},[],[]); _ } ->
- Some _false
- | _ -> None
-
(** {2 Choice on bool} *)
module ChoBool = struct
@@ -441,7 +420,9 @@ module ChoBool = struct
let choose_decision node env =
match Egraph.get_value env dom node with
- | Some _ -> Egraph.DecNo
+ | Some _ ->
+ Debug.dprintf2 Egraph.print_decision "[Bool] No decision for %a" Node.pp node;
+ Egraph.DecNo
| None -> DecTodo
(List.map (fun v env -> make_decision env node v)
(Shuffle.shufflel [true;false]))
@@ -453,10 +434,34 @@ let chobool n = {
choice = ChoBool.choose_decision n;
}
-let decvars t n =
- if Ty.equal (Expr.Term.ty t) Dolmen_std.Expr.Ty.bool
- then Some (chobool n)
- else None
+
+let converter d (f:Expr.Term.t) res =
+ let of_term t =
+ let n = SynTerm.node_of_term t in
+ Egraph.register d n;
+ n
+ in
+ let reg n =
+ Egraph.register d n;
+ Egraph.merge d res n
+ in
+ match f with
+ | { descr = App({builtin = Dolmen_std.Expr.Base; _ },_,_); ty }
+ when Expr.Ty.equal ty Expr.Ty.bool ->
+ Egraph.register_decision d (chobool res)
+ | { descr = Expr.App({builtin = Expr.Or},[],args); _ } ->
+ reg (_or (List.map of_term args))
+ | { descr = Expr.App({builtin = Expr.And},[],args); _ } ->
+ reg (_and (List.map of_term args))
+ | { descr = Expr.App({builtin = Expr.Imply},[],[arg1;arg2]); _ } ->
+ reg (gen false [of_term arg1,true;of_term arg2,false])
+ | { descr = Expr.App({builtin = Expr.Neg},[],[arg]); _ } ->
+ reg (_not (of_term arg))
+ | { descr = Expr.App({builtin = Expr.True},[],[]); _ } ->
+ reg _true
+ | { descr = Expr.App({builtin = Expr.False},[],[]); _ } ->
+ reg _false
+ | _ -> ()
let th_register env =
RDaemonPropaNot.init env;
@@ -467,7 +472,6 @@ let th_register env =
Egraph.register env node_true;
Egraph.register env node_false;
SynTerm.register_converter env converter;
- SynTerm.register_decvars env decvars;
()
(** {2 Interpretations} *)
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index e0158476b..948616fb0 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -607,22 +607,28 @@ let () =
)
-let converter d (t:Expr.Term.t) =
+let converter d (t:Expr.Term.t) res =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
+ let reg n =
+ Egraph.register d n;
+ Egraph.merge d res n
+ in
match t with
| { descr = Expr.App({builtin = Expr.Equal},[_],l); _ } ->
- Some (equality (List.map of_term l))
+ reg (equality (List.map of_term l))
| { descr = Expr.App({builtin = Expr.Equiv},[_],[a;b]); _ } ->
- Some (equality [of_term a;of_term b])
+ reg (equality [of_term a;of_term b])
| { descr = Expr.App({builtin = Expr.Distinct},[_],args); _ } ->
- Some (disequality (List.map of_term args))
+ reg (disequality (List.map of_term args))
| { descr = Expr.App({builtin = Expr.Ite},[_],[c;a;b]); _ } ->
- Some (ite (of_term c) (of_term a) (of_term b))
- | _ -> None
+ reg (ite (of_term c) (of_term a) (of_term b))
+ | { descr = Expr.App({builtin = Expr.Xor},[],[a;b]); _ } ->
+ reg (disequality ([of_term a;of_term b]))
+ | _ -> ()
let th_register env =
RDaemonPropa.init env;
diff --git a/src_colibri2/theories/bool/uninterp.ml b/src_colibri2/theories/bool/uninterp.ml
index ddf336ff5..e9f4cba9d 100644
--- a/src_colibri2/theories/bool/uninterp.ml
+++ b/src_colibri2/theories/bool/uninterp.ml
@@ -160,7 +160,7 @@ module DaemonInit = struct
Debug.dprintf2 debug "[Uninterp] @[init %a@]" Th.pp v;
if DaemonPropa.is_unborn d nodesem then
match v with
- | Fun _ -> assert false (** TODO *)
+ | Fun _ -> ()
| App(f,g) ->
Egraph.register d f; Egraph.register d g;
let f' = Egraph.find d f in
@@ -181,20 +181,19 @@ end
module RDaemonInit = Demon.Key.Register(DaemonInit)
-let converter d (t:Term.t) =
+let converter d (t:Term.t) res =
let of_term t =
let n = SynTerm.node_of_term t in
Egraph.register d n;
n
in
- let node = match t with
+ match t with
| { descr = App({builtin = Dolmen_std.Expr.Base; _ } as f,tyl,((_::_) as l)); _ } ->
let f = ThE.node (ThE.index (Fun (f,tyl))) in
let l = List.map of_term l in
- Some (appl f l)
- | _ -> None
- in
- node
+ let l,a = Lists.chop_last l in
+ Egraph.set_thterm d res (ThE.thterm (ThE.index (App(appl f l,a))))
+ | _ -> ()
let th_register env =
RDaemonPropa.init env;
diff --git a/src_colibri2/theories/bool/uninterp.mli b/src_colibri2/theories/bool/uninterp.mli
index 0b1398ace..f4befa96f 100644
--- a/src_colibri2/theories/bool/uninterp.mli
+++ b/src_colibri2/theories/bool/uninterp.mli
@@ -31,8 +31,8 @@ val sem: Th.t ThTermKind.t
(* val fun1 :
* Ty.t -> string ->
- * (Node.t -> Node.t)
- * val fun2 :
+ * (Node.t -> Node.t) *)
+(* val fun2 :
* Ty.t -> string ->
* (Node.t -> Node.t -> Node.t)
* val fun3 :
@@ -43,9 +43,9 @@ val sem: Th.t ThTermKind.t
* (Node.t -> Node.t -> Node.t -> Node.t -> Node.t)
* val fun5 :
* Ty.t -> string ->
- * (Node.t -> Node.t -> Node.t -> Node.t -> Node.t -> Node.t)
- *
- * val fresh_fun: result:Ty.t -> arity:int -> string -> Node.t *)
+ * (Node.t -> Node.t -> Node.t -> Node.t -> Node.t -> Node.t) *)
+
+(* val fresh_fun: result:Ty.t -> arity:int -> string -> Node.t *)
(* val app_fun: Node.t -> Node.t list -> Node.t *)
--
GitLab