theorem proving - Z3 will not case split on hand-crafted data types -

-

i have defined own booleans, called boolean smt2, , and function boolean_and on them. conjecture , commutative:

(declare-sort boolean) (declare-const sk_x boolean) (declare-const sk_y boolean) (declare-const boolean_false boolean) (declare-const boolean_true boolean) (declare-fun boolean_and (boolean boolean) boolean)  ;; axiomatize booleans: false /= true , every bool true or false (assert (forall ((x boolean)) (or (= x boolean_false)                                   (= x boolean_true))))  (assert (not (= boolean_false boolean_true)))  ;; definition of , (assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false))) (assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))  ;; try prove , commutative (assert (not (= (boolean_and sk_x sk_y)                 (boolean_and sk_y sk_x))))  (check-sat)

however, z3 reports unknown on problem after while, though thought should able use case split assertions on skolemised variables sk_x , sk_y.

curiously, if remove boolean axiomatization , replace declare-datatypes, z3 report unsat:

(declare-datatypes () ((boolean (boolean_true) (boolean_false))))  (declare-const sk_x boolean) (declare-const sk_y boolean) (declare-fun boolean_and (boolean boolean) boolean)  (assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false))) (assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))  (assert (not (= (boolean_and sk_x sk_y)                 (boolean_and sk_y sk_x))))  (check-sat)

what doing wrong? how can z3 case split using axiomatization?

you not doing wrong. official release (v4.3.1) may fail on problems containing cardinality constraints such as

(assert (forall ((x boolean)) (or (= x boolean_false)                                   (= x boolean_true))))

this constraint asserting uninterpreted sort boolean has @ 2 elements. fixed problem. fix available in unstable branch. here instructions on how compile unstable branch. tomorrow, nightly builds contain fix.


Comments

Post a Comment

Popular posts from this blog

sql - VB.NET Operand type clash: date is incompatible with int error -

-
i trying display records table named staffpresentee database using clause... i using visual studio 2010... the table design follows- .......fieldname..................datatype........allownull 1......staff_id (fk).............numeric(18,0)......yes 2.......date........................date.............no 3......present.....................char(1)..........yes note type of 2nd field date , not datetime... i want display records table have today's date int 'date' field... current query is- cmd = new sqlclient.sqlcommand("select * staffpresentee date=" & date.now.date, cn) dr = cmd.executereader for dr = cmd.executereader error "operand type clash: date incompatible int" i tried select * staffpresentee query without clause runs correctly. try putting date value in sigle quotes maybe. cmd = new sqlclient.sqlcommand("select * staffpresentee date='" & _
Read more

SVG stroke-linecap doesn't work for circles in Firefox? -

-
i've got problem svg stroke-linecap attribute. i've got circular progress bar in angularjs , set outer circle (blue one) have rounded "ends". @ fiddle . <svg ... height="130" width="130"> <!-- ngif: background --> <circle ... ng-if="background" fill="#fff" class="ng-scope" stroke-width="13" stroke="#cc3399" r="57.5" cy="65" cx="65" stroke-linecap="round" /> <!-- end ngif: background --> <circle ... fill="none" stroke-dashoffset="36.12831551628261" stroke-dasharray="361.28315516282623" stroke-width="13" stroke="#432db3" stroke-linecap="round" r="57.5" cy="65" cx="65" transform="rotate(-89.9, 65, 65)" /> </svg> how can that?
Read more

python - TypeError: Scalar value for argument 'color' is not numeric in openCV -

-
here code im = cv2.imread('luffy.jpg') gray = cv2.cvtcolor(im,cv2.color_bgr2gray) ret,thresh = cv2.threshold(gray,127,255,0) contours,h = cv2.findcontours(thresh,cv2.retr_tree,cv2.chain_approx_simple) cnt in contours: moment = cv2.moments(cnt) c_y = moment['m10']/(moment['m00']+0.01) c_x = moment['m01']/(moment['m00']+0.01) centroid_color = im[c_x,c_y] centroid_color = np.array((centroid_color[0],centroid_color[1],centroid_color[2])) print type(centroid_color) cv2.fillpoly(im,cnt,centroid_color) i getting error on last line try , pass centroid_color color argument. <type 'numpy.ndarray'> , have been able pass data type cv2.fillpoly color in other instances, not sure why having problem here. fillpoly() expects iterable, i.e. put cnt in brackets. believe duplicate of https://stackoverflow.com/a/17582850/5818240 . moreover, centroid color variable contains strings. need convert them i
Read more