Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Preserve mapping between old and new representatives with AC symbols #823

Draft
wants to merge 1 commit into
base: next
Choose a base branch
from
Draft

Preserve mapping between old and new representatives with AC symbols #823

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 23 additions & 4 deletions src/lib/reasoners/uf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -683,8 +683,8 @@ module Env = struct
let up_uf_rs dep env tch =
if RS.is_empty env.ac_rs then env, tch
else
let env, tch, neqs_to_up = MapX.fold
(fun r (rr,ex) ((env, tch, neqs_to_up) as acc) ->
let env, tch, neqs_to_up, to_up = MapX.fold
(fun r (rr,ex) ((env, tch, neqs_to_up, to_up) as acc) ->
Options.exec_thread_yield ();
let nrr, ex_nrr = normal_form env rr in
if X.equal nrr rr then acc
Expand All @@ -699,8 +699,27 @@ module Env = struct
if X.is_a_leaf r then (r,[r, nrr, ex],nrr) :: tch
else tch
in
env, tch, SetXX.add (rr, nrr) neqs_to_up
) env.repr (env, tch, SetXX.empty)
(* With AC symbols, we can have r --> rr with rr not appearing in
repr (e.g. [rr = f(0, 0)] when the initial term was
[f(zero, zero)] with [zero --> 0]).

This means that the mapping [rr --> nrr] will not appear in
[tch], which will confuse the relations.

Hence, when a new mapping r --> nrr is introduced, we manually
add rr --> nrr as a PIVOT in this case. *)
let to_up =
match X.ac_extract rr with
| Some _ when not (MapX.mem rr env.repr) ->
MapX.add rr (nrr, ex_nrr) to_up
| _ -> to_up
in
env, tch, SetXX.add (rr, nrr) neqs_to_up, to_up
) env.repr (env, tch, SetXX.empty, MapX.empty)
in
let tch =
MapX.fold (fun rr (nrr, ex) tch ->
(rr, [rr, nrr, ex], nrr) :: tch) to_up tch
in
(* Correction : Do not update neqs twice for the same r *)
update_aux dep neqs_to_up env, tch
Expand Down
264 changes: 264 additions & 0 deletions tests/dune.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179829,6 +179829,270 @@
(package alt-ergo)
(action
(diff 479.expected 479_fpa.output)))
(rule
(target 474_ci_cdcl_no_minimal_bj.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL
--no-minimal-bj
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff 474.expected 474_ci_cdcl_no_minimal_bj.output)))
(rule
(target 474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL-Tableaux
--no-minimal-bj
--no-tableaux-cdcl-in-theories
--no-tableaux-cdcl-in-instantiation
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff
474.expected
474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
(rule
(target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL-Tableaux
--no-tableaux-cdcl-in-theories
--no-tableaux-cdcl-in-instantiation
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff
474.expected
474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
(rule
(target 474_ci_no_tableaux_cdcl_in_instantiation.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL-Tableaux
--no-tableaux-cdcl-in-instantiation
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff 474.expected 474_ci_no_tableaux_cdcl_in_instantiation.output)))
(rule
(target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL-Tableaux
--no-tableaux-cdcl-in-theories
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff
474.expected
474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
(rule
(target 474_ci_tableaux_cdcl_no_minimal_bj.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL-Tableaux
--no-minimal-bj
%{input})))))))
(rule
(alias runtest-ci)
(package alt-ergo)
(action
(diff 474.expected 474_ci_tableaux_cdcl_no_minimal_bj.output)))
(rule
(target 474_cdcl.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver CDCL
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_cdcl.output)))
(rule
(target 474_tableaux_cdcl.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver Tableaux-CDCL
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_tableaux_cdcl.output)))
(rule
(target 474_tableaux.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
--sat-solver Tableaux
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_tableaux.output)))
(rule
(target 474_legacy.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend legacy
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_legacy.output)))
(rule
(target 474_dolmen.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--frontend dolmen
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_dolmen.output)))
(rule
(target 474_fpa.output)
(deps (:input 474.ae))
(package alt-ergo)
(action
(chdir %{workspace_root}
(with-stdout-to %{target}
(ignore-stderr
(with-accepted-exit-codes 0
(run %{bin:alt-ergo}
--timelimit=2
--enable-assertions
--output=smtlib2
--enable-theories fpa
%{input})))))))
(rule
(alias runtest-quick)
(package alt-ergo)
(action
(diff 474.expected 474_fpa.output)))
(rule
(target 460_ci_cdcl_no_minimal_bj.output)
(deps (:input 460.ae))
Expand Down
12 changes: 12 additions & 0 deletions tests/issues/474.ae
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
logic ac f : real, real -> real

function id_2() : real = 2.

axiom ax_1:
f(f(id_2, 1.), 0.) <= 0.0

function f_2_1() : real = f(2., 1.)

axiom ax_2: f_2_1 <= 0.0

goal goal_1: false
2 changes: 2 additions & 0 deletions tests/issues/474.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

unknown
Loading