Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
C
COLIBRI
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
COLIBRI
Commits
9794c2ab
Commit
9794c2ab
authored
3 years ago
by
François Bobot
Browse files
Options
Downloads
Patches
Plain Diff
Import from Bin:a1af7a0 Src:f66bd1f8c farith:a93db57
parent
68cc1e86
No related branches found
Branches containing commit
No related tags found
Tags containing commit
1 merge request
!26
Fix 46
Pipeline
#38721
passed
3 years ago
Stage: test
Changes
3
Pipelines
1
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
Src/COLIBRI/arith.pl
+799
-805
799 additions, 805 deletions
Src/COLIBRI/arith.pl
Src/COLIBRI/check_ineq.pl
+142
-141
142 additions, 141 deletions
Src/COLIBRI/check_ineq.pl
Src/COLIBRI/col_solve.pl
+4
-3
4 additions, 3 deletions
Src/COLIBRI/col_solve.pl
with
945 additions
and
949 deletions
Src/COLIBRI/arith.pl
+
799
−
805
View file @
9794c2ab
This diff is collapsed.
Click to expand it.
Src/COLIBRI/check_ineq.pl
+
142
−
141
View file @
9794c2ab
...
...
@@ -13,25 +13,25 @@ saturate_add_inequalities(A,B,C):-
getval
(
use_delta
,
1
)
@
eclipse
,
!,
ndelta
:
disable_delta_check
,
(
nonvar
(
A
)
->
((
var
(
B
),
var
(
C
))
->
launch_delta_add_res_inst
(
A
,
B
,
C
)
;
true
)
;
(
var
(
B
)
->
(
var
(
C
)
->
launch_delta_add
(
A
,
B
,
C
),
%
% Les update_var sont indispensables ici pour NETON !
update_var_from_delta
(
B
,
C
,
A
),
update_var_from_delta
(
C
,
B
,
A
)
;
%
% A = B + cste
launch_delta_equal
(
A
,
B
,
C
))
;
(
var
(
C
)
->
%
% A = C + cste
launch_delta_equal
(
A
,
C
,
B
)
;
%
% Normalement inutile !
true
))),
(
nonvar
(
A
)
->
((
var
(
B
),
var
(
C
))
->
launch_delta_add_res_inst
(
A
,
B
,
C
)
;
true
)
;
(
var
(
B
)
->
(
var
(
C
)
->
launch_delta_add
(
A
,
B
,
C
),
% Les update_var sont indispensables ici pour NETON !
update_var_from_delta
(
B
,
C
,
A
),
update_var_from_delta
(
C
,
B
,
A
)
;
% A = B + cste
launch_delta_equal
(
A
,
B
,
C
))
;
(
var
(
C
)
->
% A = C + cste
launch_delta_equal
(
A
,
C
,
B
)
;
% Normalement inutile !
true
))),
ndelta
:
allow_delta_check
.
saturate_add_inequalities
(
A
,
B
,
C
).
...
...
@@ -172,23 +172,23 @@ launch_delta_equal(A,B,Cste) :-
%update_var_from_delta(B,A,C) :- !.
update_var_from_delta
(
B
,
A
,
C
)
:-
%
% C = A + B
(
ndelta
:
get_deltas
(
A
,
C
,
RelAC
,
DistAC
)
->
update_var_from_delta_rel
(
RelAC
,
DistAC
,
B
,
A
,
C
)
;
true
),!.
% C = A + B
(
ndelta
:
get_deltas
(
A
,
C
,
RelAC
,
DistAC
)
->
update_var_from_delta_rel
(
RelAC
,
DistAC
,
B
,
A
,
C
)
;
true
),!.
update_var_from_delta
(
B
,
A
,
C
)
:-
ndelta
:
fail_delta
.
ndelta
:
fail_delta
.
update_var_from_delta_rel
(
'#'
,
L
..
H
,
B
,
A
,
C
)
:-
interval_from_bounds
(
L
,
-
1
,
Neg
),
interval_from_bounds
(
1
,
H
,
Pos
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
Neg
,
Pos
]).
interval_from_bounds
(
L
,
-
1
,
Neg
),
interval_from_bounds
(
1
,
H
,
Pos
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
Neg
,
Pos
]).
update_var_from_delta_rel
(
'='
,
DistAC
,
B
,
_
,
_
)
:-
protected_unify
(
B
=
DistAC
).
protected_unify
(
B
=
DistAC
).
update_var_from_delta_rel
(
'+'
,
DistAC
,
B
,
A
,
C
)
:-
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
DistAC
]).
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
DistAC
]).
%% Mise a jour du range de A et B de maniere
%% compatible avec leur delta
...
...
@@ -197,10 +197,11 @@ update_var_from_delta_rel('+',DistAC,B,A,C) :-
%% des intervalles compatibles de A et B pour ajuster les bornes
%% (on pourrait alors provoquer des convergences lentes)
%update_args_from_delta(?,?,A,B) :- !.
% FAUX !!!
% PROVOQUE DES BUGS DANS div_mod_rec
update_args_from_delta
(
?,?,
A
,
B
)
:-
!.
update_args_from_delta
(
Rel
,
Delta
,
A
,
B
)
:-
update_args_from_delta0
(
Rel0
,
Delta0
,
A
,
B
),
update_args_from_delta0
(
Rel0
,
Delta0
,
A
,
B
),
((
nonvar
(
Rel
),
nonvar
(
Delta
))
->
...
...
@@ -212,141 +213,141 @@ update_args_from_delta(Rel,Delta,A,B) :-
% on exploite pas ce delta dans les compositions d intervalles
Rel
=
?,
Delta
=
?
;
Rel
=
Rel0
,
;
Rel
=
Rel0
,
Delta
=
Delta0
)).
update_args_from_delta0
(
Rel
,
Delta
,
A
,
A
)
?-
!,
Rel
=
'='
,
Delta
=
0
.
Rel
=
'='
,
Delta
=
0
.
update_args_from_delta0
(
Rel
,
Delta
,
A
,
B
)
:-
(
exists_delta_Rel
(
A
,
B
,
Rel0
,
S
,
C
)
->
update_args_from_delta
(
Rel0
,
S
,
C
,
A
,
B
,
Rel
,
Delta
)
;
Rel
=
?,
Delta
=
?
),
!.
(
exists_delta_Rel
(
A
,
B
,
Rel0
,
S
,
C
)
->
update_args_from_delta
(
Rel0
,
S
,
C
,
A
,
B
,
Rel
,
Delta
)
;
Rel
=
?,
Delta
=
?
),
!.
update_args_from_delta0
(
Rel
,
Delta
,
A
,
B
)
:-
ndelta
:
fail_delta
.
ndelta
:
fail_delta
.
update_args_from_delta
(
Rel0
,
S
,
C
,
A
,
B
,
Rel
,
Delta
)
:-
update_delta_cost_with_congr
(
A
,
B
,
S
,
C
,
NS
,
NC
),
((
S
,
C
)
==
(
NS
,
NC
)
->
Rel
=
Rel0
,
Delta
=
C
,
update_A_B_from_delta
(
Rel0
,
C
,
A
,
B
)
;
%
% On peut devoir unifier A et B
(
NC
==
0
->
protected_unify
(
A
=
B
),
Rel
=
'='
,
Delta
=
0
;
%
% on met a jour le delta sans provoquer
%
% une analyse
ndelta
:
update_deltas_between
(
A
,
B
,
NS
,
NC
),
exists_delta_Rel
(
A
,
B
,
Rel
,
_
,
Delta
),
update_A_B_from_delta
(
Rel
,
Delta
,
A
,
B
))).
update_delta_cost_with_congr
(
A
,
B
,
S
,
C
,
NS
,
NC
),
((
S
,
C
)
==
(
NS
,
NC
)
->
Rel
=
Rel0
,
Delta
=
C
,
update_A_B_from_delta
(
Rel0
,
C
,
A
,
B
)
;
% On peut devoir unifier A et B
(
NC
==
0
->
protected_unify
(
A
=
B
),
Rel
=
'='
,
Delta
=
0
;
% on met a jour le delta sans provoquer
% une analyse
ndelta
:
update_deltas_between
(
A
,
B
,
NS
,
NC
),
exists_delta_Rel
(
A
,
B
,
Rel
,
_
,
Delta
),
update_A_B_from_delta
(
Rel
,
Delta
,
A
,
B
))).
update_A_B_from_delta
(
Rel
,
Delta
,
A
,
B
)
:-
update_A_B_from_delta0
(
Rel
,
Delta
,
A
,
B
).
update_A_B_from_delta0
(
Rel
,
Delta
,
A
,
B
).
update_A_B_from_delta0
(
?,?,
A
,
B
)
:-
!.
update_A_B_from_delta0
(
_
,
0
,
A
,
B
)
:-
!,
protected_unify
(
A
=
B
).
protected_unify
(
A
=
B
).
update_A_B_from_delta0
(
Rel
,
Delta
,
A
,
B
)
:-
A
\
==
B
,
mfd
:
dvar_range
(
A
,
MinA
,
MaxA
),
mfd
:
dvar_range
(
B
,
MinB
,
MaxB
),
update_A_B_from_delta
(
Rel
,
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
),
((
NMinA
,
NMaxA
)
==
(
MinA
,
MaxA
)
->
true
;
interval_from_bounds
(
NMinA
,
NMaxA
,
IA
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
A
,[
IA
])),
((
NMinB
,
NMaxB
)
==
(
MinB
,
MaxB
)
->
true
;
interval_from_bounds
(
NMinB
,
NMaxB
,
IB
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
IB
])).
A
\
==
B
,
mfd
:
dvar_range
(
A
,
MinA
,
MaxA
),
mfd
:
dvar_range
(
B
,
MinB
,
MaxB
),
update_A_B_from_delta
(
Rel
,
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
),
((
NMinA
,
NMaxA
)
==
(
MinA
,
MaxA
)
->
true
;
interval_from_bounds
(
NMinA
,
NMaxA
,
IA
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
A
,[
IA
])),
((
NMinB
,
NMaxB
)
==
(
MinB
,
MaxB
)
->
true
;
interval_from_bounds
(
NMinB
,
NMaxB
,
IB
),
% pas de notify_constrained
mfd
:
quiet_set_intervals
(
B
,[
IB
])).
update_A_B_from_delta
(
'#'
,
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
:-
!,
update_A_B_from_delta_diff
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
).
update_A_B_from_delta_diff
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
).
update_A_B_from_delta
(
_
,
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
:-
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
),
NMinA
=<
NMaxA
,
NMinB
=<
NMaxB
.
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
),
NMinA
=<
NMaxA
,
NMinB
=<
NMaxB
.
% Reduction possible si A ou B est instancie
update_A_B_from_delta_diff
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
:-
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
MinA0
,
MaxA0
,
MinB0
,
MaxB0
),
(
MinA0
==
MaxA0
->
(
MinB0
==
MaxB0
->
MinA0
\
==
MinB0
,
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
NMinB
=
MinB0
,
NMaxB
=
MaxB0
;
%
% MinA0 interdit pour MinB0 et MaxB0
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
(
MinA0
==
MinB0
->
NMaxB
=
MaxB0
,
NMinB
is
MinB0
+
1
;
(
MinA0
==
MaxB0
->
NMinB
=
MinB0
,
NMaxB
is
MaxB0
-
1
;
NMinB
=
MinB0
,
NMaxB
=
MaxB0
)))
;
(
MinB0
==
MaxB0
->
%
% MinB0 interdit pour MinA0 et MaxA0
NMinB
=
MinB0
,
NMaxB
=
MaxB0
,
(
MinB0
==
MinA0
->
NMaxA
=
MaxA0
,
NMinA
is
MinA0
+
1
;
(
MinB0
==
MaxA0
->
NMinA
=
MinA0
,
NMaxA
is
MaxA0
-
1
;
NMinA
=
MinA0
,
NMaxA
=
MaxA0
))
;
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
NMinB
=
MinB0
,
NMaxB
=
MaxB0
)),
NMinA
=<
NMaxA
,
NMinB
=<
NMaxB
.
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
MinA0
,
MaxA0
,
MinB0
,
MaxB0
),
(
MinA0
==
MaxA0
->
(
MinB0
==
MaxB0
->
MinA0
\
==
MinB0
,
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
NMinB
=
MinB0
,
NMaxB
=
MaxB0
;
% MinA0 interdit pour MinB0 et MaxB0
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
(
MinA0
==
MinB0
->
NMaxB
=
MaxB0
,
NMinB
is
MinB0
+
1
;
(
MinA0
==
MaxB0
->
NMinB
=
MinB0
,
NMaxB
is
MaxB0
-
1
;
NMinB
=
MinB0
,
NMaxB
=
MaxB0
)))
;
(
MinB0
==
MaxB0
->
% MinB0 interdit pour MinA0 et MaxA0
NMinB
=
MinB0
,
NMaxB
=
MaxB0
,
(
MinB0
==
MinA0
->
NMaxA
=
MaxA0
,
NMinA
is
MinA0
+
1
;
(
MinB0
==
MaxA0
->
NMinA
=
MinA0
,
NMaxA
is
MaxA0
-
1
;
NMinA
=
MinA0
,
NMaxA
=
MaxA0
))
;
NMinA
=
MinA0
,
NMaxA
=
MaxA0
,
NMinB
=
MinB0
,
NMaxB
=
MaxB0
)),
NMinA
=<
NMaxA
,
NMinB
=<
NMaxB
.
update_A_B_from_delta
(
0
,
MinA
,
MaxA
,
MinB
,
MaxB
,
MinA
,
MaxA
,
MinB
,
MaxB
)
:-
!.
update_A_B_from_delta
(
Delta
,
A
,
A
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
?-
!,
NMinA
=
A
,
NMaxA
=
A
,
min_max_inter
(
Delta
,
L
,
H
),
(
MinB
==
MaxB
->
A
+
L
=<
MinB
,
MinB
=<
A
+
H
,
NMinB
=
MinB
,
NMaxB
=
MinB
;
NMinB
is
max
(
MinB
,
A
+
L
),
NMaxB
is
min
(
MaxB
,
A
+
H
)).
NMinA
=
A
,
NMaxA
=
A
,
min_max_inter
(
Delta
,
L
,
H
),
(
MinB
==
MaxB
->
A
+
L
=<
MinB
,
MinB
=<
A
+
H
,
NMinB
=
MinB
,
NMaxB
=
MinB
;
NMinB
is
max
(
MinB
,
A
+
L
),
NMaxB
is
min
(
MaxB
,
A
+
H
)).
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
B
,
B
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
?-
!,
NMinB
=
B
,
NMaxB
=
B
,
min_max_inter
(
Delta
,
L
,
H
),
%
% MinA < MaxA
NMinA
is
max
(
MinA
,
B
-
H
),
NMaxA
is
min
(
MaxA
,
B
-
L
).
NMinB
=
B
,
NMaxB
=
B
,
min_max_inter
(
Delta
,
L
,
H
),
% MinA < MaxA
NMinA
is
max
(
MinA
,
B
-
H
),
NMaxA
is
min
(
MaxA
,
B
-
L
).
update_A_B_from_delta
(
Delta
,
MinA
,
MaxA
,
MinB
,
MaxB
,
NMinA
,
NMaxA
,
NMinB
,
NMaxB
)
:-
%
% MinA..MaxA + L..H = MinB..MaxB sans toucher L..H
add_intervals
(
MinA
..
MaxA
,
Delta
,
MinB0
,
MaxB0
),
NMinB
is
max
(
MinB
,
MinB0
),
NMaxB
is
min
(
MaxB
,
MaxB0
),
((
NMinB
,
NMaxB
)
==
(
MinB0
,
MaxB0
)
->
NMinA
=
MinA
,
NMaxA
=
MaxA
;
minus_intervals
(
NMinB
..
NMaxB
,
Delta
,
MinA0
,
MaxA0
),
NMinA
is
max
(
MinA
,
MinA0
),
NMaxA
is
min
(
MaxA
,
MaxA0
)).
% MinA..MaxA + L..H = MinB..MaxB sans toucher L..H
add_intervals
(
MinA
..
MaxA
,
Delta
,
MinB0
,
MaxB0
),
NMinB
is
max
(
MinB
,
MinB0
),
NMaxB
is
min
(
MaxB
,
MaxB0
),
((
NMinB
,
NMaxB
)
==
(
MinB0
,
MaxB0
)
->
NMinA
=
MinA
,
NMaxA
=
MaxA
;
minus_intervals
(
NMinB
..
NMaxB
,
Delta
,
MinA0
,
MaxA0
),
NMinA
is
max
(
MinA
,
MinA0
),
NMaxA
is
min
(
MaxA
,
MaxA0
)).
...
...
This diff is collapsed.
Click to expand it.
Src/COLIBRI/col_solve.pl
+
4
−
3
View file @
9794c2ab
...
...
@@ -872,7 +872,8 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_BV/crafted/",
%-----------------------------------------------------------------------
%StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1 (durdur)
%StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 0
% devenu sat après correction d'un mauvais appel a smtlib_select !!!!
%-----------------------------------------------------------------------
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/", %0
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_non_terminating_klee_bug.x86_64/", % 0
...
...
@@ -880,7 +881,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 10
6
(177 unsupported) (cvc4 55)
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 10
9
(177 unsupported) (cvc4 55)
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
...
...
@@ -891,7 +892,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/", %
2
1 (cvc4 50)(bitwuzla
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 1
6
(cvc4 50)(bitwuzla
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment