mirror of
https://github.com/Z3Prover/z3
synced 2025-08-07 11:41:22 +00:00
107981f099
- update proof format for quantifier instantiation to track original literals
- update proof replay tools with ability to extract proof object
The formats and features are subject to heavy revisions.
Example
```
(set-option :sat.euf true)
(set-option :sat.smt.proof eufproof.smt2)
(declare-fun f (Int) Int)
(declare-const x Int)
(assert (or (= (f (f (f x))) x) (= (f (f x)) x)))
(assert (not (= (f (f (f (f (f (f x)))))) x)))
(check-sat)
```
eufproof.smt2 is:
```
(declare-fun x () Int)
(declare-fun f (Int) Int)
(define-const $24 Int (f x))
(define-const $25 Int (f $24))
(define-const $26 Int (f $25))
(define-const $27 Bool (= $26 x))
(define-const $28 Bool (= $25 x))
(assume $27 $28)
(define-const $30 Int (f $26))
(define-const $31 Int (f $30))
(define-const $32 Int (f $31))
(define-const $33 Bool (= $32 x))
(assume (not $33))
(declare-fun rup () Proof)
(infer (not $33) rup)
(declare-fun euf (Bool Bool Proof Proof Proof Proof) Proof)
(declare-fun cc (Bool) Proof)
(define-const $42 Bool (= $32 $30))
(define-const $43 Proof (cc $42))
(define-const $40 Bool (= $31 $24))
(define-const $41 Proof (cc $40))
(define-const $38 Bool (= $30 $25))
(define-const $39 Proof (cc $38))
(define-const $36 Bool (= $24 $26))
(define-const $37 Proof (cc $36))
(define-const $34 Bool (not $33))
(define-const $44 Proof (euf $34 $28 $37 $39 $41 $43))
(infer (not $28) $33 $44)
(infer (not $28) rup)
(infer $27 rup)
(declare-fun euf (Bool Bool Proof Proof Proof) Proof)
(define-const $49 Bool (= $32 $26))
(define-const $50 Proof (cc $49))
(define-const $47 Bool (= $31 $25))
(define-const $48 Proof (cc $47))
(define-const $45 Bool (= $24 $30))
(define-const $46 Proof (cc $45))
(define-const $51 Proof (euf $34 $27 $46 $48 $50))
(infer $33 $51)
(infer rup)
```
Example of inspecting proof from Python:
```
from z3 import *
def parse(file):
s = Solver()
set_option("solver.proof.save", True)
set_option("solver.proof.check", False)
s.from_file(file)
for step in s.proof().children():
print(step)
parse("../eufproof.smt2")
```
Proof checking (self-validation) is on by default.
Proof saving is off by default.
You can use the proof logs and the proof terms to retrieve quantifier instantiations from the new core.
The self-checker contains a few built-in tuned checkers but falls back to self-checking inferred clauses using SMT.
55 lines
1.8 KiB
C++
55 lines
1.8 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
solver_na2as.h
|
|
|
|
Abstract:
|
|
|
|
Solver that implements "named" assertions using assumptions (aka answer literals).
|
|
That is, a named assertion assert_expr(t, a) is mapped into
|
|
a implies t
|
|
and 'a' is used as an extra assumption for check_sat.
|
|
|
|
Author:
|
|
|
|
Leonardo (leonardo) 2012-11-02
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "solver/solver.h"
|
|
|
|
class solver_na2as : public solver {
|
|
protected:
|
|
expr_ref_vector m_assumptions;
|
|
unsigned_vector m_scopes;
|
|
void restore_assumptions(unsigned old_sz);
|
|
public:
|
|
solver_na2as(ast_manager & m);
|
|
~solver_na2as() override;
|
|
|
|
void assert_expr_core2(expr * t, expr * a) override;
|
|
|
|
// Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
|
|
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
|
|
lbool check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) override;
|
|
void push() override;
|
|
void pop(unsigned n) override;
|
|
unsigned get_scope_level() const override;
|
|
|
|
unsigned get_num_assumptions() const override { return m_assumptions.size(); }
|
|
expr * get_assumption(unsigned idx) const override { return m_assumptions[idx]; }
|
|
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override;
|
|
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
|
|
protected:
|
|
virtual lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) = 0;
|
|
virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) { NOT_IMPLEMENTED_YET(); return l_undef; }
|
|
virtual void push_core() = 0;
|
|
virtual void pop_core(unsigned n) = 0;
|
|
};
|
|
|
|
|