CODEWITHSUNDEEP
z3z3py
user1953221
user1953221

Reputation: 429

Getting a witness from a proof of an existential statement

I'm trying to get hold of the values that Z3 instantiates existentials with, for the purpose of reconstructing proofs in Coq.

I started with this (adapted from here with some errors fixed):

from z3 import *

x = Int("x")
s = Solver()
s.add(Not(Exists([x], And(x > 1))))

def log_instance(pr, clause, q):
    if pr.decl().name() == "inst":
        print("instantiated", q, "with", pr.children()[2].children()[0].as_long())

onc = OnClause(s, log_instance)
print(s.check())

This prints

instantiated [Not(ForAll(x, x <= 1))] with 2
unsat

which seems to work, but is it the right way to do it? Will there be multiple answers as Z3 backtracks? I want only the final instantiation for a successful proof.

Also, proof logs don't seem to be available in the OCaml API, which is what I intend to use.

Any pointers to other proof reconstruction efforts for Coq/Z3 would be helpful too. Thank you.

Upvotes: 0

Views: 36

Answers (0)

Related Questions