diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 8ddf7328a5b19d549a6f699c521f77eab0b2a7bf..48ac3a80c08049bacdc08061fff7a1b8794b38a4 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -542,7 +542,7 @@ smt_solve_bis(Test,FILE,TO,Code) :-
setval(simplex_steps,0)@eclipse,
setval(solve,1),
setval(time_limit,0),
- setval(smt_status,0),
+ %setval(smt_status,0),
(nonvar(Test) ->
setval(scrambler,1)
; setval(scrambler,0)),
@@ -735,8 +735,8 @@ smt_test :-
smt_test(TO,Size) :-
%StrDir = "./colibri-master-tests/tests/",
%StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!)
- %StrDir = "./colibri-master-tests/tests/unsat/", %0
- StrDir = "./colibri-master-tests/tests/unknown/",
+ StrDir = "./colibri-master-tests/tests/unsat/", %0
+ %StrDir = "./colibri-master-tests/tests/unknown/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
@@ -893,7 +893,7 @@ smt_test(TO,Size) :-
%-----------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/", % 4
- %StrDir = "QF_AX/swap/", % 8
+ %StrDir = "QF_AX/swap/", % 8 -> 15
%StrDir = "QF_AX/storecomm/", % 0
%StrDir = "QF_AX/cvc/", % 0
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index e1c8c78bbf82ba1dcb4eb71a072f565dc5710d4d..cad874d219226f8158b624d563fde9840e5bf47e 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -475,7 +475,7 @@ lin_solve1(Status) :-
% quand meme si il n'y a plus de contraintes
((current_suspension(Susp),
get_suspension_data(Susp,goal,Goal),
- not (Goal = uninterp(_,_,_);
+ not (Goal = uninterp(_,_,_,_,_,_);
Goal = fp_eq1(_,_,_);
Goal = op_real1(_,_,_);
Goal = real_to_float_bis(Type,A,_),
@@ -699,7 +699,7 @@ try_lin_solution0(LVars,LSol,Status) :-
set_priority(Prio),
((current_suspension(Susp),
get_suspension_data(Susp,goal,Goal),
- not (Goal = uninterp(_,_,_);
+ not (Goal = uninterp(_,_,_,_,_,_);
(Goal = fp_eq1(Type,Z,_);
Goal = op_real1(Type,Z,_)),
Type \== real,
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 8f743bfdd8f628777149122bd97442ade2331116..e5f78c01818e56c1ec86a416ba9faaed10e2a589 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -7331,7 +7331,7 @@ cast_fp_int(Type,A,B) :-
cast_fp_int(0,Type,A,B) ?- !,
cast_real_int(Type,A,B).
cast_fp_int(1,Type,A,B) ?- !,
- uninterp(cast_fp_int,cast_fp_int,[Type,A],B).
+ uninterp(cast_fp_int,cast_fp_int,[Type],int,[A],B).
cast_fp_int(Cond,Type,A,B) :-
get_priority(Prio),
set_priority(1),
@@ -17680,7 +17680,7 @@ min_real_bis(Type,A,B,C) :-
B == -0.0)
->
concat_atom([fp_min,Type],F),
- uninterp(F,F,[A,B],C)
+ uninterp(F,F,[Type,Type],Type,[A,B],C)
; set_prio_inst([A,B,C],3,4,Prio),
my_suspend(min_real(Type,A,B,C),Prio,(A,B,C)->suspend:constrained))
; true).
@@ -17947,7 +17947,7 @@ max_real_bis(Type,A,B,C) :-
B == -0.0)
->
concat_atom([fp_max,Type],F),
- uninterp(F,F,[A,B],C)
+ uninterp(F,F,[Type,Type],Type,[A,B],C)
; my_suspend(max_real(Type,A,B,C),Prio,(A,B,C) -> suspend:constrained))
; true).
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index cdc395df8282f41855d9969464a9fbac4455b762..3f70dce4d4680677a8388e150532253096000f5d 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -566,7 +566,7 @@ check_sat0 :-
suspensions(LSusp),
(foreach(Susp,LSusp) do
get_suspension_data(Susp,goal,Goal),
- (Goal = uninterp(_,_,_,_) ->
+ (Goal = uninterp(_,_,_,_,_,_) ->
% on garde les uninterp pour check_sat_vars
true
; kill_suspension(Susp)),
@@ -1143,7 +1143,7 @@ factorize_and_dump_uninterps([(VN,InSorts,OutSort)|Uninterps]) :-
(LSusp \== [] ->
findall((Ins,Out),
(member(Susp,LSusp),
- get_suspension_data(Susp,goal,uninterp(VN,Trigger,Ins,Out)),
+ get_suspension_data(Susp,goal,uninterp(VN,Trigger,_,_,Ins,Out)),
kill_suspension(Susp)),
Profiles),
(foreach(Is,InSorts),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index e57447fa5f653d8f4a82a8ba9b47f6f88e6cd791..3d18795f661c42c7a875ae34d0b1ea39ae1505eb 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -3321,7 +3321,7 @@ unfold_int_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
!,
%int_vars(Type,R),
insert_dep_inst(dep(R,D,IArgs)),
- make_conj(ACstrs,(int_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,IArgs,R)),Cstr).
+ make_conj(ACstrs,(int_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
unfold_int_expr(Val,D,Cstr,Type,R) :-
atomic(Val),
@@ -4803,12 +4803,12 @@ diff_array(Type,A,const_array(TI,TE,Const)) ?- !,
diff_array(Type,A,B) :-
get_priority(P),
set_priority(1),
+ Type = array(TI,TE),
(getval(check_sat_vars,1)@eclipse ->
% Il existe un indice commun ou les elements sont non
% unifiables
- check_diff_array(A,B)
- ; Type = array(TI,TE),
- (real_type(TI,_) ->
+ check_diff_array(TE,A,B)
+ ; (real_type(TI,_) ->
real_vars(TI,I)
; % ok pour les "sort" aussi
int_vars(TI,I)),
@@ -5129,9 +5129,9 @@ remove_common_stores0(storec(A,IA,v(_,EA,CEA)),SureA,SureB,NA) :-
-check_diff_array(const_array(_,_,CA),const_array(_,_,CB)) ?- !,
+check_diff_array(_,const_array(_,_,CA),const_array(_,_,CB)) ?- !,
not_unify(CA,CB).
-check_diff_array(const_array(_,_,Const),A) ?- !,
+check_diff_array(TE,const_array(_,_,Const),A) ?- !,
hash_create(HA),
clean_array(A,NA,(HA,[]),SureA),
SureA = (_,LA),
@@ -5139,10 +5139,12 @@ check_diff_array(const_array(_,_,Const),A) ?- !,
once ((member(I,GIAs);
member((I,_),LA)),
get_sure_index(SureA,I,EA),
- not_unify(EA,Const)).
-check_diff_array(A,const_array(_,_,Const)) ?- !,
- check_diff_array(const_array(_,_,Const),A).
-check_diff_array(A,B) :-
+ (TE = array(_,TEE) ->
+ check_diff_array(TEE,EA,Const)
+ ; not_unify(EA,Const))).
+check_diff_array(TE,A,const_array(_,_,Const)) ?- !,
+ check_diff_array(TE,const_array(_,_,Const),A).
+check_diff_array(TE,A,B) :-
hash_create(HA),
hash_create(HB),
clean_array(A,NA,(HA,[]),SureA),
@@ -5153,7 +5155,9 @@ check_diff_array(A,B) :-
member((I,_),LA)),
get_sure_index(SureA,I,EA),
get_sure_index(SureB,I,EB),
- not_unify(EA,EB)).
+ (TE = array(_,TEE) ->
+ check_diff_array(TEE,EA,EB)
+ ; not_unify(EA,EB))).
@@ -7526,7 +7530,7 @@ unfold_real_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
make_conj(IC,(SetType,AC),OC)),
!,
insert_dep_inst(dep(R,D,IArgs)),
- make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,IArgs,R)),Cstr).
+ make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
unfold_real_expr(Expr,_,_,_,_) :-
spy_here,
@@ -9689,7 +9693,7 @@ uninterp_trigger(F,Types0,Type0,Trigger) :-
concat_string([SFTerm,":",SType],STrigger)),
atom_string(Trigger,STrigger).
-uninterp(F,Trigger,Args,R) :-
+uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
get_priority(P),
set_priority(1),
save_cstr_suspensions((Args,R)),
@@ -9698,39 +9702,41 @@ uninterp(F,Trigger,Args,R) :-
attached_suspensions(Trigger,LSusp1),
append(LSusp0,LSusp1,LSusp),
(foreach(PairOrSusp,LSusp),
- param(F,Args,R,TypeR) do
+ param(F,Args,R,TypeArgs,TypeR) do
(PairOrSusp = (Susp,Goal) ->
true
; Susp = PairOrSusp,
(get_suspension_data(Susp,goal,Goal) ->
true
; Goal = dead)),
- (Goal = uninterp(F,Trigger,CArgs,CR) ->
+ (Goal = uninterp(F,Trigger,TypeArgs,TypeR,CArgs,CR) ->
(Args == CArgs ->
% factorisation
kill_suspension(Susp),
- protected_unify(R,CR)
- ; ((not_unify(R,CR),
- only_one_neq_args_pair(Args,CArgs,A,CA))
+ (TypeR = array(_,_) ->
+ call(spy_here)@eclipse,
+ eq_array(TypeR,R,CR)
+ ; protected_unify(R,CR))
+ ; (((TypeR = array(_,TE) ->
+ check_diff_array(TE,R,CR)
+ ; not_unify(R,CR)),
+ only_one_neq_args_pair(TypeArgs,Args,CArgs,TA,A,CA))
->
- (term_variables((A,CA),[V|_]) ->
- (get_type(V,T) ->
- diff_reif(T,Kill,A,CA,1)
- ; launch_delta(A,CA,#,-1..1))
- ; % A <> CA
- true)
+ diff_reif(TA,Kill,A,CA,1)
; true))
; true)),
(ground(Args) ->
- my_suspend(uninterp(F,Trigger,Args,R),0,trigger(Trigger))
- ; my_suspend(uninterp(F,Trigger,Args,R),0,(Args,R)->suspend:constrained)),
+ my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,trigger(Trigger))
+ ; my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,(Args,R)->suspend:constrained)),
set_priority(P),
wake_if_other_scheduled(P).
-only_one_neq_args_pair([A1|Args],[CA1|CArgs],A,CA) :-
+only_one_neq_args_pair([T|TArgs],[A1|Args],[CA1|CArgs],TA,A,CA) :-
(A1 == CA1 ->
- only_one_neq_args_pair(Args,CArgs,A,CA)
- ; Args == CArgs,
+ only_one_neq_args_pair(TArgs,Args,CArgs,TA,A,CA)
+ ; % T \= array(_,_), % meme dans ce cas
+ Args == CArgs,
+ TA = T,
A = A1,
CA = CA1).
@@ -9761,7 +9767,7 @@ chk_undef_div_real(Bool,A,B,R) :-
wake_if_other_scheduled(P).
undef_div_real(A,R) :-
- uninterp(div_real,div_real,[A],R).
+ uninterp(div_real,div_real,[real],real,[A],R).
chk_undef_idiv_real(Bool,Type,A,B,R) :-
get_priority(P),
@@ -9797,7 +9803,7 @@ undef_idiv_real(Type,A,R) :-
launch_float_int_number(A),
launch_float_int_number(R),
uninterp_trigger(idiv_real,[Type],Type,Trigger),
- uninterp(idiv_real,Trigger,[A],R).
+ uninterp(idiv_real,Trigger,[Type],Type,[A],R).
chk_undef_imod_real(Bool,Type,A,B,R) :-
get_priority(P),
@@ -9833,8 +9839,8 @@ undef_imod_real(Type,A,R) :-
real_vars(real,(A,R)),
launch_float_int_number(A),
launch_float_int_number(R),
- uninterp_trigger(imod_real,[Type],type,Trigger),
- uninterp(imod_real,Type,[A],R).
+ uninterp_trigger(imod_real,[Type],Type,Trigger),
+ uninterp(imod_real,Type,[Type],Type,[A],R).
chk_undef_float_to_real(Bool,TypeF,A,R) :-
set_lazy_domain(real,R),
@@ -9862,7 +9868,7 @@ chk_undef_float_to_real(Bool,TypeF,A,R) :-
undef_float_to_real(Type,A,R) :-
uninterp_trigger(float_to_real,[Type],real,Trigger),
- uninterp(float_to_real,Trigger,[Type,A],R).
+ uninterp(float_to_real,Trigger,[Type],real,[A],R).
/*
undef_float_to_real(Type,A,R) :-
get_priority(Prio),
@@ -9905,7 +9911,7 @@ chk_undef_float_to_ubv(Bool,TypeF,Size,A,R) :-
(Bool,A)->suspend:constrained))).
undef_float_to_ubv(Type,Size,A,R) :-
uninterp_trigger(float_to_ubv,[Type],uint(Size),Trigger),
- uninterp(float_to_ubv,Trigger,[A],R).
+ uninterp(float_to_ubv,Trigger,[Type],uint(Size),[A],R).
/*
undef_float_to_ubv(Type,Size,A,R) :-
get_priority(Prio),
@@ -9952,7 +9958,7 @@ chk_undef_float_to_sbv(Bool,TypeF,Size,A,R) :-
undef_float_to_sbv(Type,Size,A,R) :-
uninterp_trigger(float_to_sbv,[Type],uint(Size),Trigger),
- uninterp(float_to_sbv,Trigger,[A],R).
+ uninterp(float_to_sbv,Trigger,[Type],uint(Size),[A],R).
/*
undef_float_to_sbv(Type,Size,A,R) :-
get_priority(Prio),
@@ -10012,7 +10018,7 @@ chk_undef_ediv_mod(Bool,Type,A,B,Q,R) :-
undef_ediv_mod(int,A,Q,R) :- !,
uninterp_trigger(smt_ediv_mod_int,[int],int,Trigger),
- uninterp(smt_ediv_mod_int,Trigger,[A],(Q,R)).
+ uninterp(smt_ediv_mod_int,Trigger,[int],int,[A],(Q,R)).
undef_ediv_mod(Type,A,Q,R) :-
arg(1,Type,N),
All1 is 2^N-1,
@@ -10178,7 +10184,7 @@ chk_undef_div_rem(Bool,Type,A,B,Q,R,UO) :-
(Bool,A,B)->suspend:constrained))).
undef_div_rem(int,A,Q,R,UO) :- !,
uninterp_trigger(div_rem_int,[int],int,Trigger),
- uninterp(div_rem_int,Trigger,[A],(Q,R)).
+ uninterp(div_rem_int,Trigger,[int],int,[A],(Q,R)).
undef_div_rem(Type,A,Q,R,UO) :-
% uint(N)
% Q = 0
@@ -10225,7 +10231,7 @@ chk_undef_cdiv_crem(Bool,A,B,Q,R) :-
undef_cdiv_crem(A,Q,R) :-
uninterp_trigger(cdiv_crem,[real],real,Trigger),
- uninterp(cdiv_crem,Trigger,[A],(Q,R)).
+ uninterp(cdiv_crem,Trigger,[real],real,[A],(Q,R)).
cdiv_crem(A,B,Q,R) :-
diff --git a/test.sh b/test.sh
index 0a21834026cbd9f3ad91d5e7ccb67c7cf816f39d..0f213488de58579a0202b1d49b35d5968851fae6 100755
--- a/test.sh
+++ b/test.sh
@@ -5,13 +5,30 @@ FAIL=false
echo check SAT tests
-find tests/sat -name "*.smt2" | parallel "$@" --timeout 200 --joblog sat.log "./neno 1 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' sat.log && FAIL=true)
+if find tests/sat -name "*.smt2" | parallel "$@" --timeout 200 --joblog sat.log "./neno 1 bundle/colibri --max-steps $STEPS {}"; then
+ echo OK
+else
+ echo KO
+ awk '$7 == -1' sat.log
+ FAIL=true
+fi
echo check UNSAT tests
-find tests/unsat -name "*.smt2" | parallel "$@" --timeout 200 --joblog unsat.log "./neno 0 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unsat.log && FAIL=true)
+if find tests/unsat -name "*.smt2" | parallel "$@" --timeout 200 --joblog unsat.log "./neno 0 bundle/colibri --max-steps $STEPS {}"; then
+ echo OK
+else
+ echo KO
+ awk '$7 == -1' unsat.log
+ FAIL=true
+fi
echo check UNKNOWN tests
-find tests/unknown -name "*.smt2" | parallel "$@" --timeout 200 --joblog unknown.log "./neno 2 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unknown.log && FAIL=true)
+if find tests/unknown -name "*.smt2" | parallel "$@" --timeout 200 --joblog unknown.log "./neno 2 bundle/colibri --max-steps $STEPS {}"; then
+ echo OK
+else
+ awk '$7 == -1' unknown.log
+ FAIL=true
+fi
if $FAIL; then exit 1; fi
diff --git a/tests/sat/arr.smt2 b/tests/sat/arr.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..ad58211f5b92c814aaff9afdd49dea7206205e48
--- /dev/null
+++ b/tests/sat/arr.smt2
@@ -0,0 +1,27 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+
+(declare-sort u 0)
+
+(declare-fun to_rep (u) Int)
+
+(declare-sort t 0)
+
+(declare-fun mk ((Array Int u) Bool) t)
+
+(declare-fun get_a (t) (Array Int u))
+
+(declare-fun get_b (t) Bool)
+(declare-const rliteral u)
+
+(declare-const r t)
+
+
+(assert
+ (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 3)) 5))
+
+(assert
+ (not
+ (= (to_rep (select (get_a (mk (store (get_a r) 3 rliteral) (get_b r))) 1)) 5)))
+(check-sat)