mirror of
https://github.com/Z3Prover/z3
synced 2025-06-13 17:36:15 +00:00
add tactic doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d415f07386
commit
1c7ff72ae2
1 changed files with 18 additions and 6 deletions
|
@ -5,16 +5,28 @@ Module Name:
|
||||||
|
|
||||||
split_clause_tactic.h
|
split_clause_tactic.h
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Tactic that creates a subgoal for each literal in a clause (l_1 or ... or l_n).
|
|
||||||
The tactic fails if the main goal does not contain any clause.
|
|
||||||
|
|
||||||
Author:
|
Author:
|
||||||
|
|
||||||
Leonardo (leonardo) 2011-11-21
|
Leonardo (leonardo) 2011-11-21
|
||||||
|
|
||||||
Notes:
|
Tactic Documentation:
|
||||||
|
|
||||||
|
## Tactic split-clause
|
||||||
|
|
||||||
|
### Short Description
|
||||||
|
|
||||||
|
Tactic that creates a subgoal for each literal in a clause `(l_1 or ... or l_n)`.
|
||||||
|
The tactic fails if the main goal does not contain any clause.
|
||||||
|
|
||||||
|
### Example
|
||||||
|
|
||||||
|
```z3
|
||||||
|
(declare-const p Bool)
|
||||||
|
(declare-const q Bool)
|
||||||
|
(assert (or p q))
|
||||||
|
(apply split-clause)
|
||||||
|
```
|
||||||
|
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
#pragma once
|
#pragma once
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue