blob: 1de6ac9912b7ff8533a685f3828a09b15f761659 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
To understand the new proof infrastructre:
PfRule <=> Kind
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof_rule.h
ProofNode <=> Node
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof_node.h
ProofRuleChecker <=> custom theory type checker
ProofChecker <=> TypeChecker
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof_checker.h
ProofNodeManager <=> NodeManager
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof_node_manager.h
CDProof
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof.h
ProofGenerator
EagerProofGenerator
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/proof_generator.h
// Must know what EqualityEngine is beyond here
ProofEqEngine <=> EqualityEngine
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/uf/proof_equality_engine.h
TrustNode
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/trust_node.h
// Must know what OutputChannel is beyond here
ProofOutputChannel <=> OutputChannel
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/proof_output_channel.h
ProofSkolemCache
https://github.com/ajreynol/CVC4/blob/stringsPf/src/expr/proof_skolem_cache.h
// Specific checkers and proof_kinds
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/builtin/proof_checker.h
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/builtin/proof_kinds
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/booleans/proof_checker.h
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/booleans/proof_kinds
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/uf/proof_checker.h
https://github.com/ajreynol/CVC4/blob/stringsPf/src/theory/uf/proof_kinds
High level changes needed:
- TheoryEngine passes a ProofOutputChannel to each Theory instead of an OutputChannel when in proof producing mode. It uses this object to extract proofs for theory lemmas when needed.
- TheoryEngine owns a ProofChecker that can check any kind of proof in proof_kinds files.
- Based on proof_kinds, we auto-generate:
(1) The PfRule enumeration,
(2) Printing for PfRule,
(3) Initialization of the ProofChecker owned by TheoryEngine,
(4) The code for checking (?)
Notes:
- Theory does not need to be concerned what a ProofNode is. It manages TrustNode objects but doesnt care about their contents.
- Similar to above, the user of a ProofEqEngine does not care about what a ProofNode is. Its input interface is similar to EqualityEngine, i.e. Node, its output interface is in terms of TrustNode.
- Theory can have as many ProofGenerator objects as it wants. It should have one for each kind of reasoning it does.
- ProofNodeManager does not need to be global.
PRs:
- SEXPR simply typed?
(1) ProofChecker improve tracing
- Add ProofNode printing as dag (SEXPR)
- Proof kinds infrastructure
- Rewriter new infrastructure (rewriteEqualityExt)
(2) Builtin rules, builtin checker.
(3) Boolean rules, boolean checker.
(4) UF rules, UF checker.
- EqProof conversion (Haniel)
(5) String rules, string checker
(6) Split EngineOutputChannel from TheoryEngine to its own file
(7) Add LazyCDProof and ProofGenerator
(8) Add TrustNode
- Add EagerProofGenerator
(10) ProofEqEngine
(11) TheoryEngine proof checker initialize
(12) ProofSkolemCache
- strings SkolemCache uses ProofSkolemCache
(13) strings InferProofCons
(14) update strings inference manager to use ProofEqEngine
- static strings preprocess reduce
- static regular expression operation reduce
|
