Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

Missing back translation of integers to global set elements

Description

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

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

Assignee

Reporter

Priority

Created October 29, 2020 at 5:41 PM
Updated October 30, 2020 at 9:53 AM
Resolved October 30, 2020 at 9:53 AM
Configure