From 1c7ff72ae21c3da0f39c4d3c96e90764d6aeadce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Jan 2023 18:58:20 -0800 Subject: [PATCH] add tactic doc Signed-off-by: Nikolaj Bjorner --- src/tactic/core/split_clause_tactic.h | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/src/tactic/core/split_clause_tactic.h b/src/tactic/core/split_clause_tactic.h index 7573f075e..ef9c36a38 100644 --- a/src/tactic/core/split_clause_tactic.h +++ b/src/tactic/core/split_clause_tactic.h @@ -5,16 +5,28 @@ Module Name: 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: 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