Simplifications

[Yag000]

I've added a set of simplification rules for the output of the uniform interpolant for iSL (simplifications ignore boxes). These rules have been proven correct in Coq, meaning the simplified formula is still a uniform interpolant. However, since we need cut-admissibility, the corresponding theorem has been added but admitted.

The impact of these simplifications can be evaluated on a set of examples by running

dune exec benchmark

after compiling the demo.

The UI has been update to directly show the simplified output.

Rules

Given two formulas φ and ψ, we recursively apply the following simplification rules:

Conjunction

• ⊥ ∧ ψ ≡ ⊥
• φ ∧ ⊥≡ ⊥
• ⊤∧ ψ ≡ ψ
• φ ∧⊤ ≡ φ
• φ ∧ φ ≡ φ

Disjunction

• ⊥ ∨ ψ ≡ ψ
• φ ∨ ⊥≡ φ
• ⊤∨ ψ ≡ ⊤
• φ ∨⊤ ≡ ⊤
• φ ∨ φ ≡ φ

Implication

• ⊥ → ψ ≡ ψ
• ⊥→ ψ ≡ ⊤
• φ → φ ≡ ⊤

Performance

The latest performance measurements are:

Formula	Interpolant weight	Simplified interpolant weight	Percentage reduction
A (p ∧ q) -> ~p	19	5	73.68
E (p ∧ q) -> ~p	3	3	0.00
A t ∨ q ∨ t	9	9	0.00
E t ∨ q ∨ t	9	9	0.00
A ~((F & p) -> ~p	F)	5	1	80.00
E ~((F & p) -> ~p	F)	5	1	80.00
A (q -> p) & (p -> ~r)	12	8	33.33
E (q -> p) & (p -> ~r)	5	5	0.00
A (q -> (p -> r)) -> r	12	8	33.33
E (q -> (p -> r)) -> r	870	230	73.56
A ((q -> p) -> r) -> r	24	16	33.33
E ((q -> p) -> r) -> r	102	94	7.84
A (a → (q ∧ r)) → s	21	21	0.00
E (a → (q ∧ r)) → s	768	768	0.00
A (a → (q ∧ r)) → ~p	88	72	18.18
E (a → (q ∧ r)) → ~p	3	3	0.00
A (a → (q ∧ r)) → ~p → k	95	87	8.42
E (a → (q ∧ r)) → ~p → k	3159	1261	60.08
A (q -> (p -> r)) -> ~t	21	17	19.05
E (q -> (p -> r)) -> ~t	1456	1456	0.00
A (q -> (p -> r)) -> ~t	21	17	19.05
E (q -> (p -> r)) -> ~t	1456	1456	0.00
A (q → (q ∧ (k -> p)) -> k)	40	40	0.00
E (q → (q ∧ (k -> p)) -> k)	13	9	30.77
A (q -> (p ∨ r)) -> ~(t ∨ p)	467	1	99.79
E (q -> (p ∨ r)) -> ~(t ∨ p)	976	976	0.00
A ((q -> (p ∨ r)) ∧ (t -> p)) -> t	81	65	19.75
E ((q -> (p ∨ r)) ∧ (t -> p)) -> t	1022	882	13.70
A ((~t -> (q ∧ p)) ∧ (t -> p)) -> t	99	73	26.26
E ((~t -> (q ∧ p)) ∧ (t -> p)) -> t	57	49	14.04
A (~p ∧ q) -> (p ∨ r -> t) -> o	237	237	0.00
E (~p ∧ q) -> (p ∨ r -> t) -> o	226	3	98.67

Average percentage reduction: 26.34

Formula	Interpolant computation time (s)	Simplified interpolant computation time (s)	Percentage increase
A (p ∧ q) -> ~p	0.0021	0.0063	194.33
E (p ∧ q) -> ~p	0.0007	0.0010	37.45
A t ∨ q ∨ t	0.0000	0.0000	75.00
E t ∨ q ∨ t	0.0005	0.0005	0.89
A ~((F & p) -> ~p	F)	0.0002	0.0002	6.50
E ~((F & p) -> ~p	F)	0.6709	0.6240	-6.99
A (q -> p) & (p -> ~r)	0.0001	0.0001	31.82
E (q -> p) & (p -> ~r)	0.0007	0.0008	20.09
A (q -> (p -> r)) -> r	0.0001	0.0001	11.39
E (q -> (p -> r)) -> r	0.1415	0.2794	97.44
A ((q -> p) -> r) -> r	0.0004	0.0004	3.57
E ((q -> p) -> r) -> r	0.0024	0.0024	1.06
A (a → (q ∧ r)) → s	0.0004	0.0006	29.30
E (a → (q ∧ r)) → s	0.0724	0.0750	3.62
A (a → (q ∧ r)) → ~p	0.0062	0.0061	-2.18
E (a → (q ∧ r)) → ~p	0.1199	0.2115	76.37
A (a → (q ∧ r)) → ~p → k	0.0180	0.0168	-6.28
E (a → (q ∧ r)) → ~p → k	1.6248	1.4323	-11.85
A (q -> (p -> r)) -> ~t	0.0011	0.0011	1.15
E (q -> (p -> r)) -> ~t	0.3903	0.5142	31.74
A (q -> (p -> r)) -> ~t	0.0011	0.0011	-5.52
E (q -> (p -> r)) -> ~t	0.2595	0.3733	43.86
A (q → (q ∧ (k -> p)) -> k)	0.0077	0.0162	111.67
E (q → (q ∧ (k -> p)) -> k)	0.0075	0.0054	-27.95
A (q -> (p ∨ r)) -> ~(t ∨ p)	0.0551	0.0521	-5.41
E (q -> (p ∨ r)) -> ~(t ∨ p)	2.2690	2.3011	1.42
A ((q -> (p ∨ r)) ∧ (t -> p)) -> t	0.0119	0.0125	4.75
E ((q -> (p ∨ r)) ∧ (t -> p)) -> t	7.0140	7.3034	4.13
A ((~t -> (q ∧ p)) ∧ (t -> p)) -> t	0.0204	0.0209	2.50
E ((~t -> (q ∧ p)) ∧ (t -> p)) -> t	0.4378	0.2843	-35.07
A (~p ∧ q) -> (p ∨ r -> t) -> o	0.0963	0.1215	26.10
E (~p ∧ q) -> (p ∨ r -> t) -> o	0.1215	0.1365	12.38

Average percentage increase: 22.73 Average absolute time increase (s): 0.01396