search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Unknown result on EPR formula #649

Closed kenmcmil closed 7 years ago

kenmcmil commented 8 years ago

This is an EPR satisfiability problem for which Z3 produces an "unknown" result.

Z3 commit: c7ff05cc78f90f3b10901e4efb5ba8be85246915 Platform: Ubuntu 14.04

; benchmark generated from python API
(set-info :status unknown)
(declare-sort server)
(declare-sort client)
(declare-fun |__fml:y| () server)
(declare-fun |__fml:x| () client)
(declare-fun @SE0 () server)
(declare-fun @CL1 () client)
(declare-fun @CL0 () client)
(declare-fun __link (client server) Bool)
(declare-fun __ts0_b () Bool)
(declare-fun __ts0_d () Bool)
(declare-fun link (client server) Bool)
(declare-fun __semaphore (server) Bool)
(declare-fun semaphore (server) Bool)
(declare-fun __ts0_c () Bool)
(declare-fun __ts0_a () Bool)
(assert
 (let (($x154 (forall ((|V0:client| client) (|V1:server| server) )(let (($x421 (__link |V0:client| |V1:server|)))
(let (($x589 (ite __ts0_b (ite (and (= |V0:client| |__fml:x|) (= |V1:server| |__fml:y|)) or $x421) (ite (and (= |V0:client| |__fml:x|) (= |V1:server| |__fml:y|)) and $x421))))
(= (link |V0:client| |V1:server|) (ite __ts0_d $x421 $x589)))))
))
(let (($x552 (forall ((|V0:server| server) )(let (($x394 (ite __ts0_b (ite (and (= |V0:server| |__fml:y|)) and (__semaphore |V0:server|)) (ite (and (= |V0:server| |__fml:y|)) or (__semaphore |V0:server|)))))
(let (($x555 (__semaphore |V0:server|)))
(= (semaphore |V0:server|) (ite __ts0_d $x555 $x394)))))
))
(let (($x496 (forall ((|CL0:client| client) (|CL1:client| client) (|SE0:server| server) )(not (and (not (= |CL0:client| |CL1:client|)) (__link |CL1:client| |SE0:server|) (__semaphore |SE0:server|))))
))
(let (($x361 (forall ((|CL0:client| client) (|CL1:client| client) (|SE0:server| server) )(not (and (not (= |CL0:client| |CL1:client|)) (__link |CL0:client| |SE0:server|) (__link |CL1:client| |SE0:server|))))
))
(and $x361 $x496 (or __ts0_c __ts0_d) (or (not __ts0_c) (or __ts0_a __ts0_b)) (or (not __ts0_c) (or (not __ts0_a) (__semaphore |__fml:y|))) (or (not __ts0_c) (or (not __ts0_b) (__link |__fml:x| |__fml:y|))) (not (= @CL0 @CL1)) (link @CL1 @SE0) (semaphore @SE0) $x552 $x154))))))
(check-sat)
kenmcmil commented 8 years ago

Here is another formula that produces an "unknown" result. This one is not strictly EPR. Rather, it is an A formula with stratified function symbols. Interesting, when the first check-sat is removed, the result is "unsat", which is correct.

; benchmark generated from python API
(set-info :status unknown)
(declare-sort ltime)
(declare-sort key)
(declare-sort shard)
(declare-sort data)
(declare-sort req)
(declare-sort id)
(declare-fun |__new_loc:lt| () ltime)
(declare-fun |__new_fml:lt_a| () ltime)
(declare-fun shard_hi (shard) key)
(declare-fun |__fml:s| () shard)
(declare-fun |__new_fml:hi| () key)
(declare-fun __reference.evs.data_ (ltime) data)
(declare-fun |__new_fml:lt| () ltime)
(declare-fun |__new_loc:d| () data)
(declare-fun |__fml:rq| () req)
(declare-fun |__prm:X| () id)
(declare-fun |__new_fml:rq_a| () req)
(declare-fun |__new_fml:rq| () req)
(declare-fun |__fml:val| () id)
(declare-fun |__new_loc:0| () id)
(declare-fun |__new_prm:X_a| () id)
(declare-fun |__new_fml:lo| () key)
(declare-fun |__new_fml:dst| () id)
(declare-fun |__new_prm:X_a_a| () id)
(declare-fun |__new_fml:lo_a| () key)
(declare-fun |__new_fml:hi_a| () key)
(declare-fun |__new_fml:dst_a| () id)
(declare-fun __servers.hash.hash (id key) data)
(declare-fun |__new_fml:v| () data)
(declare-fun |__new_fml:k_a| () key)
(declare-fun shard_value (shard key) data)
(declare-fun |__new_fml:s_a| () shard)
(declare-fun shard_lo (shard) key)
(declare-fun servers.hash.hash (id key) data)
(declare-fun |__fml:dst| () id)
(declare-fun |__new_loc:0_a_a| () data)
(declare-fun |__m_loc:d| () data)
(declare-fun |__new_loc:d_a| () data)
(declare-fun |__new_loc:ow| () id)
(declare-fun req_ltime (req) ltime)
(declare-fun |__new_loc:k| () key)
(declare-fun |__fml:res| () shard)
(declare-fun |__new_loc:0_a| () shard)
(declare-fun |__new_fml:d| () data)
(declare-fun req_src (req) id)
(declare-fun |__new_loc:src| () id)
(declare-fun |__fml:lo| () key)
(declare-fun |__new_fml:lo_a_a| () key)
(declare-fun |__new_prm:X| () id)
(declare-fun |__new_prm:X_a_b| () id)
(declare-fun |__fml:v| () data)
(declare-fun |__new_fml:id_| () id)
(declare-fun |__fml:hi| () key)
(declare-fun req_data (req) data)
(declare-fun |__new_fml:s| () shard)
(declare-fun |__new_fml:dst_a_a| () id)
(declare-fun __reference.hash (key) data)
(declare-fun |__new_loc:a| () key)
(declare-fun reference.evs.data_ (ltime) data)
(declare-fun |__new_fml:hi_a_a| () key)
(declare-fun req_key (req) key)
(declare-fun |__new_fml:k| () key)
(declare-fun reference.evs.key_ (ltime) key)
(declare-fun reference.hash (key) data)
(declare-fun @X1 () id)
(declare-fun @X () id)
(declare-fun @S1 () shard)
(declare-fun @S () shard)
(declare-fun @K () key)
(declare-fun __ts0_h () Bool)
(declare-fun __net.requested (id req) Bool)
(declare-fun __m_net.requested (id req) Bool)
(declare-fun __ts0_j () Bool)
(declare-fun __servers.dm.map (id key id) Bool)
(declare-fun |<=:key| (key key) Bool)
(declare-fun __ts0_f () Bool)
(declare-fun servers.dm.map (id key id) Bool)
(declare-fun __ts0_b_a () Bool)
(declare-fun __ts0_d () Bool)
(declare-fun __reference.evs.serialized (ltime) Bool)
(declare-fun reference.evs.serialized (ltime) Bool)
(declare-fun __net.generated (ltime) Bool)
(declare-fun net.generated (ltime) Bool)
(declare-fun __net.delegated (id shard) Bool)
(declare-fun net.delegated (id shard) Bool)
(declare-fun __ts0_b () Bool)
(declare-fun |req_otype:0| (req) Bool)
(declare-fun |__new_loc:op:0| () Bool)
(declare-fun net.requested (id req) Bool)
(declare-fun |<:ltime| (ltime ltime) Bool)
(declare-fun __ts0_i () Bool)
(declare-fun __ts0_c () Bool)
(declare-fun __ts0_a_a () Bool)
(declare-fun |reference.evs.type_:0| (ltime) Bool)
(declare-fun __ts0_a () Bool)
(declare-fun __ts0_g () Bool)
(declare-fun __ts0_e () Bool)
(assert
 (let ((?x558 (shard_hi |__fml:s|)))
 (let (($x511 (= |__new_fml:hi| ?x558)))
 (let ((?x549 (__reference.evs.data_ |__new_fml:lt|)))
 (let (($x540 (forall ((|V0:id| id) (|V1:req| req) )(let (($x2041 (__net.requested |V0:id| |V1:req|)))
 (let (($x345 (__m_net.requested |V0:id| |V1:req|)))
 (= $x345 (ite (and (= |V0:id| |__prm:X|) (= |V1:req| |__fml:rq|)) or $x2041)))))
 ))
 (let (($x521 (= |__new_loc:0| (ite __ts0_j |__fml:val| (ite __ts0_h |__fml:val| |__fml:val|)))))
 (let (($x643 (forall ((|V0:id| id) (|V1:key| key) (|V2:id| id) )(let (($x468 (__servers.dm.map |V0:id| |V1:key| |V2:id|)))
 (let (($x563 (and (not (and (|<=:key| |V1:key| |__new_fml:hi|) (|<=:key| |__new_fml:lo| |V1:key|))) (__servers.dm.map |__new_prm:X_a| |V1:key| |V2:id|))))
 (let (($x559 (and (= |V2:id| |__new_fml:dst|) (and (|<=:key| |V1:key| |__new_fml:hi|) (|<=:key| |__new_fml:lo| |V1:key|)))))
 (let (($x527 (ite __ts0_f (ite (and (= |V0:id| |__new_prm:X_a|)) (or $x559 $x563) $x468) $x468)))
 (let (($x653 (not (and (|<=:key| |V1:key| |__new_fml:hi_a|) (|<=:key| |__new_fml:lo_a| |V1:key|)))))
 (let (($x554 (and (= |V2:id| |__new_fml:dst_a|) (and (|<=:key| |V1:key| |__new_fml:hi_a|) (|<=:key| |__new_fml:lo_a| |V1:key|)))))
 (let (($x578 (ite (and (= |V0:id| |__new_prm:X_a_a|)) (or $x554 (and $x653 (__servers.dm.map |__new_prm:X_a_a| |V1:key| |V2:id|))) $x468)))
 (let (($x556 (servers.dm.map |V0:id| |V1:key| |V2:id|)))
 (= $x556 (ite __ts0_j $x578 (ite __ts0_h $x468 $x527))))))))))))
 ))
 (let (($x471 (forall ((|V0:id| id) (|V1:key| key) )(let ((?x634 (__servers.hash.hash |V0:id| |V1:key|)))
 (let ((?x484 (ite (and (= |V0:id| |__new_prm:X_a|) (= |V1:key| |__new_fml:k_a|)) |__new_fml:v| ?x634)))
 (let (($x467 (and (|<=:key| |V1:key| (shard_hi |__new_fml:s_a|)) (|<=:key| (shard_lo |__new_fml:s_a|) |V1:key|))))
 (let ((?x462 (ite $x467 (shard_value |__new_fml:s_a| |V1:key|) (__servers.hash.hash |__new_prm:X_a_a| |V1:key|))))
 (let ((?x466 (ite __ts0_f (ite (and (= |V0:id| |__new_prm:X_a_a|)) ?x462 ?x634) (ite __ts0_d ?x634 (ite __ts0_b_a ?x484 ?x634)))))
 (let ((?x608 (ite __ts0_j ?x634 (ite __ts0_h (ite __ts0_d ?x634 (ite __ts0_b_a ?x484 ?x634)) ?x466))))
 (let ((?x632 (servers.hash.hash |V0:id| |V1:key|)))
 (= ?x632 ?x608)))))))))
 ))
 (let (($x505 (= |__new_fml:dst_a| |__fml:dst|)))
 (let ((?x386 (ite __ts0_b_a |__m_loc:d| |__new_loc:0_a_a|)))
 (let ((?x388 (ite __ts0_d |__m_loc:d| ?x386)))
 (let (($x437 (= |__new_loc:lt| (ite __ts0_h (req_ltime |__new_fml:rq_a|) (req_ltime |__new_fml:rq_a|)))))
 (let ((?x506 (ite __ts0_h (ite __ts0_b_a |__new_loc:k| |__new_loc:k|) (ite __ts0_b_a |__new_loc:k| |__new_loc:k|))))
 (let (($x515 (= |__new_loc:0_a| |__fml:res|)))
 (let (($x380 (= |__new_loc:src| (ite __ts0_h (req_src |__new_fml:rq_a|) (req_src |__new_fml:rq_a|)))))
 (let (($x429 (= |__new_fml:lo_a_a| |__fml:lo|)))
 (let (($x433 (= |__new_prm:X_a_b| |__prm:X|)))
 (let (($x431 (= |__new_fml:hi_a| |__fml:hi|)))
 (let (($x447 (= |__new_fml:s_a| |__fml:s|)))
 (let (($x412 (= |__m_loc:d| (ite __ts0_h (req_data |__new_fml:rq_a|) (req_data |__new_fml:rq_a|)))))
 (let (($x330 (= |__new_fml:s| |__new_loc:0_a|)))
 (let (($x426 (forall ((|V0:ltime| ltime) )(let (($x508 (__reference.evs.serialized |V0:ltime|)))
 (let (($x449 (ite __ts0_f $x508 (ite __ts0_d $x508 (ite (and (= |V0:ltime| |__new_fml:lt|)) and $x508)))))
 (let (($x424 (ite __ts0_h (ite __ts0_d $x508 (ite (and (= |V0:ltime| |__new_fml:lt|)) and $x508)) $x449)))
 (let (($x441 (reference.evs.serialized |V0:ltime|)))
 (= $x441 (ite __ts0_j $x508 $x424)))))))
 ))
 (let ((?x403 (shard_lo |__fml:s|)))
 (let (($x416 (= |__new_fml:lo| ?x403)))
 (let (($x444 (forall ((|V0:ltime| ltime) )(let (($x435 (__net.generated |V0:ltime|)))
 (let (($x487 (ite __ts0_f $x435 (ite (and (= |V0:ltime| (req_ltime |__fml:rq|))) and $x435))))
 (let (($x422 (net.generated |V0:ltime|)))
 (= $x422 (ite __ts0_j $x435 (ite __ts0_h $x435 $x487)))))))
 ))
 (let (($x446 (forall ((|V0:id| id) (|V1:shard| shard) )(let (($x448 (__net.delegated |V0:id| |V1:shard|)))
 (let (($x492 (ite __ts0_f (ite (and (= |V0:id| |__prm:X|) (= |V1:shard| |__fml:s|)) or $x448) $x448)))
 (let (($x495 (ite (and (= |V0:id| |__new_fml:dst_a_a|) (= |V1:shard| |__new_fml:s|)) and $x448)))
 (let (($x496 (net.delegated |V0:id| |V1:shard|)))
 (= $x496 (ite __ts0_j $x495 (ite __ts0_h $x448 $x492))))))))
 ))
 (let (($x454 (forall ((|V0:ltime| ltime) )(let ((?x192 (__reference.evs.data_ |V0:ltime|)))
 (let ((?x413 (__reference.hash |__new_loc:a|)))
 (let ((?x489 (ite __ts0_d ?x192 (ite __ts0_b ?x192 (ite (and (= |V0:ltime| |__new_fml:lt|)) ?x413 ?x192)))))
 (let ((?x457 (reference.evs.data_ |V0:ltime|)))
 (= ?x457 (ite __ts0_j ?x192 (ite __ts0_h ?x489 (ite __ts0_f ?x192 ?x489)))))))))
 ))
 (let (($x357 (= |__new_fml:hi_a_a| |__fml:hi|)))
 (let (($x355 (= |__new_loc:k| (ite __ts0_h (req_key |__new_fml:rq_a|) (req_key |__new_fml:rq_a|)))))
 (let ((?x293 (ite __ts0_f |__prm:X| (ite __ts0_b_a |__new_prm:X_a_a| |__new_prm:X_a_a|))))
 (let ((?x407 (ite __ts0_j |__prm:X| (ite __ts0_h (ite __ts0_b_a |__new_prm:X_a_a| |__new_prm:X_a_a|) ?x293))))
 (let ((?x409 (ite __ts0_d |__new_loc:ow| |__new_loc:src|)))
 (let ((?x410 (ite __ts0_f |__prm:X| ?x409)))
 (let ((?x405 (ite __ts0_h ?x409 ?x410)))
 (let (($x343 (= |__new_fml:dst| ?x405)))
 (let ((?x322 (ite __ts0_j |__prm:X| (ite __ts0_h |__prm:X| (ite __ts0_f |__prm:X| |__prm:X|)))))
 (let (($x411 (= |__new_fml:lo_a| |__fml:lo|)))
 (let (($x323 (forall ((|K:key| key) )(= |__new_fml:k| (ite __ts0_j |K:key| (ite __ts0_h |__new_loc:k| |__new_loc:k|))))
 ))
 (let (($x307 (|req_otype:0| |__new_fml:rq_a|)))
 (let (($x327 (and (and |__new_loc:op:0| true) (and (ite __ts0_h $x307 $x307) true))))
 (let (($x325 (forall ((|V0:id| id) (|V1:req| req) )(let (($x2041 (__net.requested |V0:id| |V1:req|)))
 (let (($x373 (ite __ts0_d (ite (and (= |V0:id| |__new_fml:dst|) (= |V1:req| |__new_fml:rq|)) and $x2041) $x2041)))
 (let (($x345 (__m_net.requested |V0:id| |V1:req|)))
 (let (($x364 (ite __ts0_d (ite (and (= |V0:id| |__new_fml:dst|) (= |V1:req| |__new_fml:rq|)) and $x345) $x345)))
 (let (($x442 (net.requested |V0:id| |V1:req|)))
 (= $x442 (ite __ts0_j $x2041 (ite __ts0_h $x364 (ite __ts0_f $x2041 $x373))))))))))
 ))
 (let (($x259 (= |__new_fml:dst_a_a| |__fml:dst|)))
 (let ((?x255 (reference.evs.key_ |__new_fml:lt|)))
 (let (($x321 (forall ((|V0:key| key) )(let ((?x371 (__reference.hash |V0:key|)))
 (let ((?x400 (ite __ts0_b (ite (and (= |V0:key| |__new_loc:a|)) |__new_loc:d| ?x371) ?x371)))
 (let ((?x396 (ite __ts0_h (ite __ts0_d ?x371 ?x400) (ite __ts0_f ?x371 (ite __ts0_d ?x371 ?x400)))))
 (let ((?x291 (reference.hash |V0:key|)))
 (= ?x291 (ite __ts0_j ?x371 ?x396)))))))
 ))
 (let (($x344 (forall ((|R:req| req) (|S:req| req) )(let (($x94 (= |R:req| |S:req|)))
 (let (($x398 (or (and (= (|req_otype:0| |R:req|) (|req_otype:0| |S:req|))) (and (and (|req_otype:0| |R:req|) true) (and (|req_otype:0| |S:req|) true)))))
 (let ((?x130 (req_ltime |S:req|)))
 (let (($x109 (= (req_ltime |R:req|) ?x130)))
 (let (($x334 (and (= (req_data |R:req|) (req_data |S:req|)) (= (req_key |R:req|) (req_key |S:req|)) $x109 $x398 (= (req_src |R:req|) (req_src |S:req|)))))
 (=> $x334 $x94)))))))
 ))
 (let (($x262 (forall ((|T:key| key) (|U:key| key) )(let (($x279 (|<=:key| |U:key| |T:key|)))
 (let (($x304 (|<=:key| |T:key| |U:key|)))
 (or $x304 $x279))))
 ))
 (let (($x348 (forall ((|T:key| key) (|U:key| key) )(=> (and (|<=:key| |T:key| |U:key|) (|<=:key| |U:key| |T:key|)) (= |T:key| |U:key|)))
 ))
 (let (($x257 (forall ((|T:key| key) )(|<=:key| |T:key| |T:key|))
 ))
 (let (($x305 (forall ((|T:key| key) (|U:key| key) (|V:key| key) )(=> (and (|<=:key| |T:key| |U:key|) (|<=:key| |U:key| |V:key|)) (|<=:key| |T:key| |V:key|)))
 ))
 (let (($x295 (forall ((|T:ltime| ltime) (|U:ltime| ltime) )(let (($x260 (|<:ltime| |U:ltime| |T:ltime|)))
 (let (($x278 (|<:ltime| |T:ltime| |U:ltime|)))
 (or (= |T:ltime| |U:ltime|) $x278 $x260))))
 ))
 (let (($x311 (forall ((|T:ltime| ltime) (|U:ltime| ltime) )(not (and (|<:ltime| |T:ltime| |U:ltime|) (|<:ltime| |U:ltime| |T:ltime|))))
 ))
 (let (($x312 (forall ((|T:ltime| ltime) (|U:ltime| ltime) (|V:ltime| ltime) )(=> (and (|<:ltime| |T:ltime| |U:ltime|) (|<:ltime| |U:ltime| |V:ltime|)) (|<:ltime| |T:ltime| |V:ltime|)))
 ))
 (let (($x300 (forall ((|X:key| key) )(let (($x289 (= (shard_value |__fml:res| |X:key|) (__servers.hash.hash |__new_prm:X_a_b| |X:key|))))
 (let (($x288 (=> (and (|<=:key| |X:key| |__new_fml:hi_a_a|) (|<=:key| |__new_fml:lo_a_a| |X:key|)) $x289)))
 (let (($x242 (not __ts0_j)))
 (or $x242 $x288)))))
 ))
 (let (($x242 (not __ts0_j)))
 (let ((?x250 (shard_hi |__fml:res|)))
 (let (($x251 (= ?x250 |__new_fml:hi_a_a|)))
 (let (($x272 (or $x251 $x242)))
 (let ((?x246 (shard_lo |__fml:res|)))
 (let (($x247 (= ?x246 |__new_fml:lo_a_a|)))
 (let (($x248 (or $x247 $x242)))
 (let (($x265 (forall ((|K:key| key) )(let (($x249 (= |__new_loc:0| |__prm:X|)))
 (let (($x242 (not __ts0_j)))
 (or $x242 (=> (and (|<=:key| |K:key| |__fml:hi|) (|<=:key| |__fml:lo| |K:key|)) $x249)))))
 ))
 (let (($x244 (__servers.dm.map |__new_prm:X_a| |__new_fml:k| |__fml:val|)))
 (let (($x245 (or $x242 $x244)))
 (let (($x240 (= |__fml:dst| |__prm:X|)))
 (let (($x241 (not $x240)))
 (let (($x243 (or $x241 $x242)))
 (let (($x214 (not __ts0_h)))
 (let (($x238 (or $x214 (or (not (= |__new_loc:ow| |__new_prm:X_a_a|)) (not __ts0_d)))))
 (let (($x762 (not __ts0_i)))
 (let (($x175 (not __ts0_b_a)))
 (let (($x151 (or (and (= |__new_loc:op:0| false)) (and (and |__new_loc:op:0| true) (and false true)))))
 (let (($x117 (not __ts0_c)))
 (let (($x152 (not __ts0_a_a)))
 (let ((?x189 (__servers.hash.hash |__new_prm:X_a| |__new_fml:k_a|)))
 (let (($x190 (= |__fml:v| ?x189)))
 (let (($x69 (not __ts0_b)))
 (let (($x199 (and (and (|reference.evs.type_:0| |__new_fml:lt|) true) (and false true))))
 (let (($x86 (or (not (or (and (= (|reference.evs.type_:0| |__new_fml:lt|) false)) $x199)) $x69)))
 (let (($x1953 (not __ts0_a)))
 (let (($x1960 (or (or (and (= (|reference.evs.type_:0| |__new_fml:lt|) false)) $x199) $x1953)))
 (let (($x219 (or $x762 (or $x214 (__servers.dm.map |__new_prm:X| |__new_fml:k| |__fml:val|)))))
 (let (($x65 (not __ts0_g)))
 (let (($x213 (or $x762 (or $x65 (or (not __ts0_f) (__net.delegated |__prm:X| |__fml:s|))))))
 (let (($x2109 (not __ts0_e)))
 (let (($x205 (or $x2109 (or (not (= |__new_loc:ow| |__new_prm:X_a_a|)) (not __ts0_d)))))
 (let (($x135 (or $x762 (or $x65 (or $x2109 (or (= |__new_loc:ow| |__new_prm:X_a_a|) $x117))))))
 (let (($x116 (or $x65 (or $x2109 (__servers.dm.map |__new_prm:X| |__new_fml:k| |__fml:val|)))))
 (let (($x170 (forall ((|L:ltime| ltime) )(let (($x193 (or (and (= (|req_otype:0| |__fml:rq|) true)) (and (and (|req_otype:0| |__fml:rq|) true) (and true true)))))
 (let (($x138 (and (and (|req_otype:0| |__fml:rq|) true) (and (|reference.evs.type_:0| |L:ltime|) true))))
 (let (($x1306 (or (and (= (|req_otype:0| |__fml:rq|) (|reference.evs.type_:0| |L:ltime|))) $x138)))
 (let (($x61 (and (= (req_key |__fml:rq|) (reference.evs.key_ |L:ltime|)) $x1306 (=> $x193 (= (req_data |__fml:rq|) (__reference.evs.data_ |L:ltime|))))))
 (let ((?x62 (req_ltime |__fml:rq|)))
 (let (($x56 (= |L:ltime| ?x62)))
 (let (($x2109 (not __ts0_e)))
 (let (($x65 (not __ts0_g)))
 (let (($x762 (not __ts0_i)))
 (or $x762 (or $x65 (or $x2109 (=> $x56 $x61))))))))))))))
 ))
 (let (($x26 (or $x762 (or $x65 (or (not (__net.generated (req_ltime |__fml:rq|))) $x2109)))))
 (let (($x1003 (or __ts0_i __ts0_j)))
 (let (($x561 (forall ((|K:key| key) (|S:shard| shard) (|X:id| id) )(let (($x100 (__net.delegated |X:id| |S:shard|)))
 (=> (and (|<=:key| |K:key| (shard_hi |S:shard|)) (|<=:key| (shard_lo |S:shard|) |K:key|) $x100) (= (shard_value |S:shard| |K:key|) (__reference.hash |K:key|)))))
 ))
 (let (($x74 (forall ((|D1:id| id) (|D2:id| id) (|R1:req| req) (|R2:req| req) )(let (($x990 (__net.requested |D2:id| |R2:req|)))
 (let (($x108 (__net.requested |D1:id| |R1:req|)))
 (let ((?x130 (req_ltime |R2:req|)))
 (let (($x109 (= (req_ltime |R1:req|) ?x130)))
 (=> (and $x109 $x108 $x990) (and (= |D1:id| |D2:id|) (= |R1:req| |R2:req|))))))))
 ))
 (let (($x1850 (forall ((|D:id| id) (|R:req| req) )(let (($x2041 (__net.requested |D:id| |R:req|)))
 (=> $x2041 (__net.generated (req_ltime |R:req|)))))
 ))
 (let (($x77 (forall ((|D:id| id) (|L:ltime| ltime) (|R:req| req) )(let (($x1122 (or (and (= (|req_otype:0| |R:req|) true)) (and (and (|req_otype:0| |R:req|) true) (and true true)))))
 (let (($x2019 (|req_otype:0| |R:req|)))
 (let (($x124 (and $x2019 true)))
 (let (($x1697 (or (and (= $x2019 (|reference.evs.type_:0| |L:ltime|))) (and $x124 (and (|reference.evs.type_:0| |L:ltime|) true)))))
 (let (($x2004 (and (= (req_key |R:req|) (reference.evs.key_ |L:ltime|)) $x1697 (=> $x1122 (= (req_data |R:req|) (__reference.evs.data_ |L:ltime|))))))
 (=> (and (= |L:ltime| (req_ltime |R:req|)) (__net.requested |D:id| |R:req|)) $x2004)))))))
 ))
 (let (($x66 (forall ((|K:key| key) (|S:shard| shard) (|S1:shard| shard) (|X:id| id) (|X1:id| id) )(let (($x73 (__net.delegated |X1:id| |S1:shard|)))
 (let (($x85 (__net.delegated |X:id| |S:shard|)))
 (let (($x103 (|<=:key| |K:key| (shard_hi |S:shard|))))
 (let (($x79 (and $x103 (|<=:key| |K:key| (shard_hi |S1:shard|)) (|<=:key| (shard_lo |S:shard|) |K:key|) (|<=:key| (shard_lo |S1:shard|) |K:key|) $x85 $x73)))
 (=> $x79 (and (= |S:shard| |S1:shard|) (= |X:id| |X1:id|))))))))
 ))
 (let (($x102 (forall ((|K:key| key) (|S:shard| shard) (|X:id| id) (|X_a:id| id) )(let (($x1359 (__net.delegated |X:id| |S:shard|)))
 (let (($x22 (not (and (|<=:key| |K:key| (shard_hi |S:shard|)) (|<=:key| (shard_lo |S:shard|) |K:key|) $x1359))))
 (let (($x58 (__servers.dm.map |X_a:id| |K:key| |X_a:id|)))
 (=> $x58 $x22)))))
 ))
 (let (($x2148 (forall ((|K:key| key) (|X:id| id) (|X_a:id| id) )(=> (and (not (= |X:id| |X_a:id|)) (__servers.dm.map |X_a:id| |K:key| |X_a:id|)) (not (__servers.dm.map |X:id| |K:key| |X:id|))))
 ))
 (let (($x815 (forall ((|K:key| key) (|X:id| id) )(let (($x1345 (__servers.dm.map |X:id| |K:key| |X:id|)))
 (=> $x1345 (= (__servers.hash.hash |X:id| |K:key|) (__reference.hash |K:key|)))))
 ))
 (and $x815 $x2148 $x102 $x66 $x77 $x1850 $x74 $x561 $x1003 (or $x762 (or __ts0_g __ts0_h)) (or $x762 (or $x65 (or __ts0_e __ts0_f))) $x26 $x170 (or $x762 $x116) (or $x762 (or $x65 (or $x2109 (or __ts0_c __ts0_d)))) $x135 (or $x762 (or $x65 (or $x2109 (or $x117 (or __ts0_a __ts0_b))))) (or $x762 (or $x65 (or $x2109 (or $x117 $x1960)))) (or $x762 (or $x65 (or $x2109 (or $x117 $x86)))) (or $x762 (or $x65 (or $x2109 (or $x117 (or __ts0_a_a __ts0_b_a))))) (or $x762 (or $x65 (or $x2109 (or $x117 (or $x151 $x152))))) (or $x762 (or $x65 (or $x2109 (or $x117 (or $x190 $x152))))) (or $x762 (or $x65 (or $x2109 (or $x117 (or (not $x151) $x175))))) (or $x762 (or $x65 $x205)) $x213 (or $x762 (or $x214 (__net.requested |__prm:X| |__fml:rq|))) $x219 (or $x762 (or $x214 (or __ts0_c __ts0_d))) (or $x762 (or $x214 (or (= |__new_loc:ow| |__new_prm:X_a_a|) $x117))) (or $x762 (or $x214 (or $x117 (or __ts0_a __ts0_b)))) (or $x762 (or $x214 (or $x117 $x1960))) (or $x762 (or $x214 (or $x117 $x86))) (or $x762 (or $x214 (or $x117 (or __ts0_a_a __ts0_b_a)))) (or $x762 (or $x214 (or $x117 (or $x151 $x152)))) (or $x762 (or $x214 (or $x117 (or $x190 $x152)))) (or $x762 (or $x214 (or $x117 (or (not $x151) $x175)))) (or $x762 $x238) $x243 $x245 $x265 $x248 $x272 $x300 $x312 $x311 $x295 $x305 $x257 $x348 $x262 $x344 $x321 (= |__new_loc:a| (ite __ts0_h ?x255 ?x255)) $x259 $x325 (or (and (= |__new_loc:op:0| (ite __ts0_h $x307 $x307))) $x327) $x323 $x411 (= |__new_prm:X_a_a| ?x322) $x343 (= |__new_prm:X_a| ?x407) $x355 $x357 (= |__new_fml:v| (ite __ts0_h |__m_loc:d| |__m_loc:d|)) $x454 $x446 $x444 $x416 $x426 $x330 $x412 $x447 $x431 (= |__new_fml:id_| (ite __ts0_h |__new_prm:X_a_a| |__new_prm:X_a_a|)) (= |__new_loc:0_a_a| (ite __ts0_h |__fml:v| |__fml:v|)) $x433 (= |__new_prm:X| (ite __ts0_h |__new_prm:X_a_a| |__new_prm:X_a_a|)) $x429 $x380 (= |__new_fml:d| (ite __ts0_h |__new_loc:d_a| |__new_loc:d_a|)) (= |__new_fml:rq_a| (ite __ts0_h |__fml:rq| |__fml:rq|)) $x515 (= |__new_fml:k_a| ?x506) $x437 (= |__new_loc:ow| (ite __ts0_h |__new_loc:0| |__new_loc:0|)) (= |__new_loc:d_a| (ite __ts0_h ?x388 ?x388)) $x505 (= |__new_fml:lt| (ite __ts0_h |__new_loc:lt| |__new_loc:lt|)) $x471 $x643 $x521 (= |__new_fml:rq| (ite __ts0_h |__new_fml:rq_a| |__new_fml:rq_a|)) $x540 (= |__new_loc:d| (ite __ts0_h ?x549 ?x549)) $x511 (= |__new_fml:lt_a| (ite __ts0_h |__new_loc:lt| |__new_loc:lt|)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(assert
 (let (($x1897 (net.delegated @X1 @S1)))
(let (($x1534 (net.delegated @X @S)))
(let ((?x1546 (shard_lo @S1)))
(let (($x1115 (|<=:key| ?x1546 @K)))
(let ((?x863 (shard_lo @S)))
(let (($x1540 (|<=:key| ?x863 @K)))
(let ((?x748 (shard_hi @S1)))
(let (($x966 (|<=:key| @K ?x748)))
(let ((?x672 (shard_hi @S)))
(let (($x1815 (|<=:key| @K ?x672)))
(let (($x1886 (=> (and $x1815 $x966 $x1540 $x1115 $x1534 $x1897) (and (= @S @S1) (= @X @X1)))))
(and (not $x1886))))))))))))))
(check-sat)
NikolajBjorner commented 8 years ago

It reaches a threshold of maximal mbqi instantiations. You can modify the number of instantiations by:

  z3 <filename>.smt2 smt.mbqi.max_iterations=1000000

I will try to make this diagnostic message surface better. It took some digging. I am not sure what can be done about reducing the set of instantiations: it seems to expand the domain size gratuitiously and not realize that it can settle for a small domain.

One possible experiment is to limit the domain size as part of the formula, e.g., by using enumeration types (ADTs or bit-vectors).

kenmcmil commented 8 years ago

I'm a bit puzzled by this. In the first formula, there are 3 constants of sort client and 2 of sort server and no function symbols. If I count correctly, that gives 42 instantiations of the universals in a full grounding. How can it take 1000000 iterations to get 42 instantiations? How can MBQI possibly get a model with more than 3 of sort client and 2 of sort server?

kenmcmil commented 8 years ago

I think I found the source of the problem. It's not that the model it gets is too large. It's that the model contains a spurious constant with the enigmatic name elem!13. MBQI uses this bogus constant in an instantiation. This leads to divergence. A partial trace of the model checker is attached, showing the problem: z3-trace.txt

kenmcmil commented 8 years ago

A few more observations. The spurious constant is created in model_finder::add_elem_to_empty_inst_sets. It then gets into the model as a side effect of eval with model completion. One way to fix this could be to remember the extra constants in auf_solver::fix_model and remove them from the model after processing it.

kenmcmil commented 8 years ago

Another clue: the first example contains a constant that appears only in a disequality. This constant appears in the model but seems to have gotten lost in the auf_solver nodes, which is why the spurious elem constant is being created.

NikolajBjorner commented 8 years ago

It keeps creating new elements. In the new model, previous elements have the same value, client!val!2, and the newly generated elem has a distinct value, client!val!1. The values client!val!1 and 2 are opaque outside of the finite model, so the solver has to figure out how to instantiate using named elements that correspond to distinct values. In the end, it ends up diverging.

(define elem!27 client!val!2) (define elem!41 client!val!2) (define elem!55 client!val!2) (define elem!69 client!val!2) (define elem!83 client!val!2) (define elem!97 client!val!2) (define elem!111 client!val!2) (define elem!125 client!val!2) (define elem!139 client!val!2) (define elem!153 client!val!2) (define elem!167 client!val!1)

kenmcmil commented 8 years ago

If you look at the model, you see that both client!val!1 and client!val!2 have associated constants. So there is no need to invent a new constant. Somehow the heuristics that produce the instantiation candidates have failed. At the point where the new constant elem!1 is generated, one could instead use an existing constant in the same equivalence class.

kenmcmil commented 8 years ago

By the way, is there anything wrong with just putting all of the constants of the given sort in the instantiation set in case it is empty? I tried this and it at least works for this example. By constants, I mean the constants in the model signature, not the ones like client!val!1 that give the sorts in extension.

NikolajBjorner commented 8 years ago

Something like that,

The first example we have models with elements of the form:

(define @CL0 client!val!1) (define @CL1 client!val!2) (define @SE0 server!val!1) (define elem!13 client!val!1)

Instead of using elem!13, it seems to me the instantiation should have used @CL0.

kenmcmil commented 8 years ago

Is there a way of filtering the list of constants? Maybe using the e-graph? Or would it be better to use the whole list? I'm thinking this case might be rare. If I understand correctly, it happens here because there is a bound variable that occurs under no predicates or function symbols. Are there other cases when you would get an empty instantiation set? Anyway, I can submit a pull request if you'd like to try out the change.