z3 - Why the unstable branch is not able to prove a theorem but the master branch is able? -

-

i trying prove theorem in group theory using following z3 smt-lib code

 (declare-sort s) (declare-fun identity () s) (declare-fun product (s s s) bool) (declare-fun inverse (s) s) (declare-fun multiply (s s) s)  (assert (forall ((x s)) (product identity x x) )) (assert (forall ((x s)) (product x identity x) )) (assert (forall ((x s)) (product (inverse x) x identity) )) (assert (forall ((x s)) (product x (inverse x) identity) )) (assert (forall ((x s) (y s)) (product x y (multiply x y)) )) ;;(assert (forall ((x s) (y s) (z s) (w s)) (or (not (product x y z))  ;;                                              (not (product x y w)) ;;                                              (= z w))))   (assert (forall ((x s) (y s) (z s) (u s) (v s) (w s)) (or (not (product x y u))                                                (not (product y z v))                                               (not (product u z w) )                                               (product x v w))))  (assert (forall ((x s) (y s) (z s) (u s) (v s) (w s)) (or (not (product x y u))                                                (not (product y z v))                                               (not (product x v w) )                                               (product u z w))))    (check-sat)   (push) ;; file     : grp001-1 : tptp v6.0.0. released v1.0.0. ;; domain   : group theory ;; problem  : x^2 = identity => commutativity ;; version  : [mow76] axioms. ;; english  : if square of every element identity, system ;;            commutative. (declare-fun () s) (declare-fun b () s) (declare-fun c () s) (assert (forall ((x s)) (product x x identity) )) (assert (product b c)) (assert (not (product b c))) (check-sat) (pop)

please run code online here.

the master branch z3 able prove such theorem unstable branch not able. please let me know why. many thanks.


Comments

Post a Comment

Popular posts from this blog

My HTML document is not linking to my CSS stylesheet properly -

-
i have been copy , pasting html , css tutorials try make work, right have; page (html) <!doctype html> <html> <head> <meta charset="utf-8"> <title>title of document</title> <link rel="stylesheet" type="text/css" href="style/style.css" /> </head> <body> <h1>1this site</h1> <p>welcome site</p> </body> </html> style.css body {background-image:url(“background.png”);} h1 {font-family:arial, sans-serif;} the when load html in safari still unformatted. thanks in advance! check see if setting paths right if still have problem try use fill path : <link rel="stylesheet" type="text/css" href="http://127.0.0.1/test/style/style.css" />
Read more

php array slice every 2th rule -

-
i have array on php outputs in txt file: printing grid -- 1 values -- undef = -9.99e+08 20.2 \nprinting grid -- 1 values -- undef = -9.99e+08 102.0 \nprinting grid -- 1 values -- undef = -9.99e+08 55.1 \nprinting grid -- 1 values -- undef = -9.99e+08 -18.3 \n what point, need nummeric values @ beginning of each rule. 20.2, 102.0, 55.1, -18,3 etc... example, there can more or less in txt file. now do? have tested array slice function can't exclude rule: printing grid -- 1 values -- undef = -9.99e+08 this array slice code... $arraygood = array_slice($arraybad, 1, 4); and foreach loop create text file: $file = fopen("array.txt","w"); foreach ($arraygood $meting => $waarde) { echo fwrite($file,$waarde . '\n'); } fclose($file); thanks! as posted in comments, understanding have array of strings similar following: $lines = array( "printing grid -- 1 values -- undef = -9.99e+08", "20.2 \nprinting grid --...
Read more

node.js - Sending sockets to client side, Error: Converting circular structure to JSON -

-
i'm working in node js , i'm trying send array, clients, server every client normal emit, keeps giving me error: data = json.stringify(ev); typeerror: converting circular structure json shortly, do. var clients = new array(); io.sockets.on('connection', function(socket) { clients.push(socket); socket.on('loginuser', function(data){ io.sockets.emit("getusers", clients); }); i've seen couple of other people having problem, answers didn't work out me. looking @ bigger problem, can't send array of sockets client side. sockets objects make sense in current context/process. if want control sockets client side, instead add sort of rpc functionality.
Read more