Z3 Model Incorrect -

-


Z3 Model Incorrect -

i hacking away @ problem of finding hamiltonian cycle in undirected graph. recent experiment produced should have been impossible model. here input:

;number of vertices = 4 ;5 edges: ;e1 = 0 1 ;e2 = 1 2 ;e3 = 2 3 ;e4 = 3 0 ;e5 = 1 3 (declare-const v0 bool) (declare-const v1 bool) (declare-const v2 bool) (declare-const v3 bool) (declare-const e1 bool) (declare-const e2 bool) (declare-const e3 bool) (declare-const e4 bool) (declare-const e5 bool) (assert (xor (and e2 e3 e4 e5) (and e1 e3 e4 e5) (and e1 e2 e4 e5) (and e1 e2 e3 e5) (and e1 e2 e3 e4))) (assert (and v0 v1 v2 v3)) ;(assert (=> (and e2 e3 e4 e5) (and v0 v1 v2 v3))) ;(assert (=> (and e1 e3 e4 e5) (and v0 v1 v2 v3))) ;(assert (=> (and e1 e2 e4 e5) (and v0 v1 v2 v3))) ;(assert (=> (and e1 e2 e3 e5) (and v0 v1 v2 v3))) ;(assert (=> (and e1 e2 e3 e4) (and v0 v1 v2 v3))) (assert (=> e1 (or e2 e4 e5))) (assert (=> e2 (or e1 e3 e5))) (assert (=> e3 (or e2 e4 e5))) (assert (=> e4 (or e1 e3 e5))) (assert (=> e5 (or e1 e2 e4))) (assert (and (=> e1 e2) (=> e2 e3) (=> e3 e4) (=> e4 e1))) (check-sat) (get-model)

here output showing of e1, e2, e3, e4, , e5 true despite xor statement in input prohibits this:

sat (model (define-fun e2 () bool true) (define-fun e5 () bool true) (define-fun e3 () bool true) (define-fun e4 () bool true) (define-fun e1 () bool true) (define-fun v3 () bool true) (define-fun v2 () bool true) (define-fun v1 () bool true) (define-fun v0 () bool true) )

does have opinions on what's going wrong here?

regards.

i don't know you're trying do, seems misused xor.

since (simplify (xor true true true true true)) returns true, encoding doesn't prohibit current model.

in general, guarantee a1, a2 , a3 has 1 true, follows:

(assert (or a1 a2 a3)) ; @ to the lowest degree 1 true (assert (and (=> a1 (and (not a2) (not a3))) (=> a2 (and (not a1) (not a3))) (=> a3 (and (not a1) (not a2))))); @ 1 true

z3

Comments

Post a Comment

Popular posts from this blog

How do I check if an insert was successful with MySQLdb in Python? -

-
How do I check if an insert was successful with MySQLdb in Python? - i have code: cursor = conn.cursor() cursor.execute(("insert new_files (videos_id, filename, " "is_processing) values (%s,%s,1)"), (id, filename)) logging.warn("%d", cursor.rowcount) if (cursor.rowcount == 1): logging.info("inserted values %d, %s", id, filename) else: logging.warn("failed insert values %d, %s", id, filename) cursor.close() fun is, cursor.rowcount always one, though updated database create videos_id unique key. is, insert fails because in tests same videos_id going appear (and when check database, nil inserted). whatever reason, rowcount 1 - logging.warn have spits out rowcount of 1. so, question: can utilize rowcount work out if insert went fine? if so, (presumably) doing wrong? otherwise, how check if insert went fine? your code not commit after modifications (your modifications rolled back). should...
Read more

delphi - blogger via idHTTP : error 400 bad request -

-
delphi - blogger via idHTTP : error 400 bad request - i'm trying post blogger using idhttp component, however, i'm getting "http/1.0 400 bad request" error. procedure tform1.button1click(sender: tobject); var request,response,req : tstringlist; auth,blogid : string; begin blogid := '00000000000000000000000'; request := tstringlist.create; response := tstringlist.create; req := tstringlist.create; idhttp1.request.connection := 'keep-alive'; idhttp1.request.contenttype := 'application/x-www-form-urlencoded'; idssliohandlersocket1.ssloptions.method := sslvsslv23; request.clear(); request.values['accounttype'] := 'google'; request.values['email'] := 'xxx@gmail.com'; request.values['passwd'] := 'yyy'; request.values['service'] := 'blogger'; response.text :=idhttp1.post('https://www.google.com/accounts/clientlogin',request); auth := resp...
Read more

postgresql - ERROR: operator is not unique: unknown + unknown -

-
postgresql - ERROR: operator is not unique: unknown + unknown - i have postgis database , have compute new values rows in new column. these values should average of values of several columns. query: insert bdps (da_m) values (avg('da_1'+'da_2'+'da_3'+'da_4'+'da_5'+'da_6'+'da_7')); in query bdps database, da_m new column , da_1 da_7 existing columns have double precision type. da_m created using alter table bdps add together column da_m double precision; i next error: error: operator not unique: unknown + unknown line 2: values (avg('da_1'+'da_2'+'da_3'+'da_4'+'da_5'+'da_6'+'da_7... ^ hint: not take best candidate operator. might need add together explicit type casts. ********** error ********** error: operator not unique: unknown + unknown sql state: 42725 hint: not take best candidate operator. might need add togethe...
Read more