From 47c349f02b4935b05f72883cbdee48526607c10e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 16 Mar 2022 10:02:30 +0100
Subject: [PATCH 1/2] Import from Bin:a1af7a0 Src:a835b4644 farith:a93db57
---
Src/COLIBRI/arith.pl | 1 +
Src/COLIBRI/smt_import.pl | 9 ++++++++-
2 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index ba4242477..be17f34c6 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -6932,6 +6932,7 @@ mult_intervals_diff_both_both(Min1,Max1,Min2,Max2,B1,B2) :-
%% GESTION DES CONGRUENCES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- export launch_congr/3.
+%launch_congr(A,C0,Mod0) :- !.
launch_congr(A,C0,Mod0) :-
(launch_congr1(A,C0,Mod0) ->
true
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 4dc76a9a0..4aa3320d4 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -1381,7 +1381,10 @@ defined_smt_func(F/Ar,IArgs,Type,IExpr) :-
foreach(CFV,CFVars),
fromto(VarsAss,OVA,IVA,[]),
param(LetVars) do
- (occurs(FV,LetVars) ->
+ % pas d'unification plus tard !
+ ((occurs(FV,LetVars);
+ is_quantifier_abstraction(FV))
+ ->
OVA = IVA
; OVA = [[FV|CFV]|IVA])),
(foreach((IArg,IArgType),IArgs),
@@ -2902,6 +2905,10 @@ new_quantifier_abstraction(Res) :-
setval(decl,ODecl-NEnd),
Res = as(NVar,bool).
+is_quantifier_abstraction(Var) :-
+ protected_get_var_name(Var,VS),
+ append_strings("ColQuant",_,VS).
+
% on garde les realString
check_eval(Type,realString(Str),RE) ?- !,
RE = as(realString(Str),Type).
--
GitLab
From 41a7251857fb99ac5f9ab6ab18b34470f3137144 Mon Sep 17 00:00:00 2001
From: Bruno Marre <bruno.marre@cea.fr>
Date: Wed, 16 Mar 2022 10:41:00 +0100
Subject: [PATCH 2/2] nouveaux tests pour issue 53
---
tests/sat/zero_neg_plus.smt2 | 18 ------------------
tests/unknown/bool_eq.smt2 | 28 ++++++++++++++++++++++++++++
tests/unsat/bool_eq_unsat.smt2 | 28 ++++++++++++++++++++++++++++
3 files changed, 56 insertions(+), 18 deletions(-)
delete mode 100644 tests/sat/zero_neg_plus.smt2
create mode 100644 tests/unknown/bool_eq.smt2
create mode 100644 tests/unsat/bool_eq_unsat.smt2
diff --git a/tests/sat/zero_neg_plus.smt2 b/tests/sat/zero_neg_plus.smt2
deleted file mode 100644
index 4e39c693f..000000000
--- a/tests/sat/zero_neg_plus.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-(set-info :status sat)
-;; produced by colibri.drv ;;
-(set-logic ALL)
-(set-info :smt-lib-version 2.6)
-
-(declare-const zero_plus Float32)
-
-(declare-const zero_neg Float32)
-
-(declare-fun magic (Float32) Int)
-
-(assert (fp.eq zero_plus zero_neg))
-
-(assert (distinct (magic zero_neg) 0))
-
-(assert (not (not (= (magic zero_plus) 0))))
-
-(check-sat)
diff --git a/tests/unknown/bool_eq.smt2 b/tests/unknown/bool_eq.smt2
new file mode 100644
index 000000000..56834b15d
--- /dev/null
+++ b/tests/unknown/bool_eq.smt2
@@ -0,0 +1,28 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;; sat normalement mais unknown à cause du forall
+
+;; bool_eq
+(define-fun bool_eq ((arg1 (Array Int Bool)) (a__first Int) (a__last Int) (b (Array Int Bool)) (b__first Int) (b__last Int)) Bool
+ (and
+ (ite (<= a__first a__last)
+ (and
+ (<= b__first b__last)
+ (= (- a__last a__first) (- b__last b__first)))
+ (< b__last b__first))
+ (forall ((idx Int))
+ (=>
+ (and (<= a__first idx) (<= idx a__last))
+ (= (ite (select arg1 idx) 1 0) (ite (select b (+ (- b__first a__first) idx)) 1 0))))))
+
+
+(declare-const a (Array Int Bool))
+(declare-const b (Array Int Bool))
+(declare-const c (Array Int Bool))
+
+(assert (not (bool_eq c 0 1 a 0 1)))
+(assert (bool_eq b 0 1 c 0 1))
+
+
+(check-sat)
diff --git a/tests/unsat/bool_eq_unsat.smt2 b/tests/unsat/bool_eq_unsat.smt2
new file mode 100644
index 000000000..9c1bf81aa
--- /dev/null
+++ b/tests/unsat/bool_eq_unsat.smt2
@@ -0,0 +1,28 @@
+(set-info :status unsat)
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+;; bool_eq
+(define-fun bool_eq ((arg1 (Array Int Bool)) (a__first Int) (a__last Int) (b (Array Int Bool)) (b__first Int) (b__last Int)) Bool
+ (and
+ (ite (<= a__first a__last)
+ (and
+ (<= b__first b__last)
+ (= (- a__last a__first) (- b__last b__first)))
+ (< b__last b__first))
+ (forall ((idx Int))
+ (=>
+ (and (<= a__first idx) (<= idx a__last))
+ (= (ite (select arg1 idx) 1 0) (ite (select b (+ (- b__first a__first) idx)) 1 0))))))
+
+
+(declare-const a (Array Int Bool))
+(declare-const b (Array Int Bool))
+(declare-const c (Array Int Bool))
+
+(assert (not (bool_eq c 0 1 a 0 1)))
+(assert (bool_eq c 0 1 a 0 1))
+
+
+(check-sat)
--
GitLab