(set-option :macro-finder true): does not work in a theorem of group theory

Question

I am trying to prove the right-cancellation property in group theory using the following code

(set-option :macro-finder true)

(declare-sort S)
(declare-fun e () S)
(declare-fun mult (S S) S)
(declare-fun inv (S) S)
(assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
(assert (forall ((x S)) (= (mult e x)  x)))
(assert (forall ((x S)) (= (mult (inv x) x) e)))
(assert (forall ((x S)) (= (mult x e)  x)))
(assert (forall ((x S)) (= (mult x (inv x)) e)))

(check-sat)
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult y x) (mult z x)) (= y z)))))
(check-sat)

but I am obtaining

sat
(error: "out of memory")

Please let me know what happens. Many thanks.

Answer 1

Z3 is not particularly tuned for proving theorems in universal algebra. Theorem provers with super-position, such as E, Spass, Vampire, are traditionally well suited for such theorems.

That said, the version of Z3 in the unstable branch has no problems. Here is what I get:

z3.exe ua.smt2 /v:10
(simplifier :num-exprs 23 :num-asts 196 :time 0.00 :before-memory 2.61 :after-memory 2.61)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
sat
(smt.simplifier-done)
(smt.searching)
(smt.mbqi)
(smt.simplifier-done)
(smt.searching) 
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifier-done)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.mbqi :failed k!6)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!7)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!8)
(smt.simplifier-done)
(smt.searching)
(smt.simplifier-done)
(smt.searching)
(smt.mbqi :failed k!9)
(smt.restarting :propagations 0 :decisions 0 :conflicts 0 :restart 100 :restart-outer 100 :agility 0.00)
unsat

you can download the latest versions of the so-called "unstable" branch of Z3 from z3.codeplex.com > Downloads > "Planned"

Answer 2

For the master branch version of Z3 this is simply a hard problem and it runs out of memory while running the second check-sat. The current version (unstable branch) solves it very quickly. (Note that the macro-finder option has been renamed to smt.macro_finder, but that doesn't make a big difference on this file.)