Missing back translation of integers to global set elements
Description
Environment
None
Activity
Show:
Michael Leuschel October 30, 2020 at 9:53 AM
This issue is now solved, depending on version of Z3 we get:
>>> :z3 not(c1:res) & c2:res
Result of get_model_string: (store ((as const (Array Code Bool)) false) 1 true)
PREDICATE is TRUE
Solution:
res = {c2}
>>> :z3 not(c1:res) & c2:res
Result of get_model_string: (lambda ((x!1 Code)) (= x!1 1))
PREDICATE is TRUE
Solution:
res = {c2}
Michael Leuschel October 29, 2020 at 5:43 PM
The Z3 translation of the above example is:
; Z3 Solver Store (SMT2 format):
;
(set-info :status unknown)
(declare-fun c4 () (Code Code 4))
(declare-fun c3 () (Code Code 4))
(declare-fun c2 () (Code Code 4))
(declare-fun c1 () (Code Code 4))
(declare-fun res () (Array (Code Code 4) Bool))
(assert
(and (distinct c1 c2 c3 c4) true))
(assert
(= c1 (_ N 0 (Code Code 4))))
(assert
(= c2 (_ N 1 (Code Code 4))))
(assert
(= c3 (_ N 2 (Code Code 4))))
(assert
(= c4 (_ N 3 (Code Code 4))))
(assert
(let (($x45 (select res c2)))
(let (($x43 (select res c1)))
(let (($x44 (not $x43)))
(and $x44 $x45)))))
(check-sat)
Fixed
Details
Details
Assignee
Michael Leuschel
Michael LeuschelReporter
Michael Leuschel
Michael LeuschelPriority
Created October 29, 2020 at 5:41 PM
Updated October 30, 2020 at 9:53 AM
Resolved October 30, 2020 at 9:53 AM
In the context of seval ../prob_examples/public_examples/B/Benchmarks/phonebook7.mch with a SET Code ={c1,c2,c3,c4} we did get an empty set for res:
:z3 not(c1:res) & c2:res
Now at least an internal error is raised
>>> :z3 not(c1:res) & c2:res
Result of get_model_string: (lambda ((x!1 Code)) (= x!1 1))
! Creating equality with incompatible types: equal(global('Code'),integer)
Unknown exception in solver z3: model_translation_failed
PREDICATE is UNKNOWN: model_translation_failed
But we need to fix this