From c45c40e782d6c8c95771cc9ec8944600c78de760 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Dec 2022 08:51:18 -0800
Subject: [PATCH] doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/tactic/core/blast_term_ite_tactic.cpp | 2 -
src/tactic/core/blast_term_ite_tactic.h | 38 +++++++++++++++----
src/tactic/core/ctx_simplify_tactic.h | 25 +++++++++++-
src/tactic/core/elim_term_ite_tactic.h | 35 ++++++++++++++---
src/tactic/core/pb_preprocess_tactic.cpp | 32 ++++------------
src/tactic/core/pb_preprocess_tactic.h | 46 ++++++++++++++++++++++-
src/tactic/core/tseitin_cnf_tactic.cpp | 39 +------------------
src/tactic/core/tseitin_cnf_tactic.h | 32 +++++++++++++++-
8 files changed, 167 insertions(+), 82 deletions(-)
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index 49e43e633..987ab9f90 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -13,8 +13,6 @@ Author:
Nikolaj Bjorner (nbjorner) 2013-11-4
-Notes:
-
--*/
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h"
diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h
index b5f643a1e..a322b8e11 100644
--- a/src/tactic/core/blast_term_ite_tactic.h
+++ b/src/tactic/core/blast_term_ite_tactic.h
@@ -4,20 +4,42 @@ Copyright (c) 2013 Microsoft Corporation
Module Name:
blast_term_ite_tactic.h
-
-Abstract:
-
- Blast term if-then-else by hoisting them up.
- This is expensive but useful in some cases, such as
- for enforcing constraints being in difference logic.
- Use elim-term-ite elsewhere when possible.
Author:
Nikolaj Bjorner (nbjorner) 2013-11-4
-Notes:
+Tactic Documentation:
+
+## Tactic blast-term-ite
+
+### Short Description:
+
+Blast term if-then-else by hoisting them up.
+This is expensive but useful in some cases, such as
+for enforcing constraints being in difference logic.
+Use `elim-term-ite` elsewhere when possible.
+
+### Example
+
+```z3
+(declare-fun f (Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(declare-const c3 Bool)
+(declare-const e1 Int)
+(declare-const e2 Int)
+(declare-const e3 Int)
+(declare-const e4 Int)
+(assert (p (f (if c1 (if c2 e1 (if c3 e2 e3)) e4))))
+(apply blast-term-ite)
+```
+
+### Notes
+
+
--*/
#pragma once
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index c8e34f33d..213f01f62 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -13,7 +13,30 @@ Author:
Leonardo (leonardo) 2011-10-26
-Notes:
+Tactic Documentation:
+
+## Tactic ctx-simplify
+
+### Short Description:
+
+The tactic performs simplifies sub-formulas using context built up by walking assertions and sub-formulas.
+
+### Example
+
+```z3
+ (declare-const p Bool)
+ (declare-const q Bool)
+ (declare-const r Bool)
+ (declare-fun f (Bool) Bool)
+ (assert p)
+ (assert (or (f p) (and r (or (not r) q))))
+ (apply ctx-simplify)
+```
+
+### Notes
+
+* supports proof terms with limited features
+
--*/
#pragma once
diff --git a/src/tactic/core/elim_term_ite_tactic.h b/src/tactic/core/elim_term_ite_tactic.h
index 8fa9f9031..ca8d3d43e 100644
--- a/src/tactic/core/elim_term_ite_tactic.h
+++ b/src/tactic/core/elim_term_ite_tactic.h
@@ -5,16 +5,39 @@ Module Name:
elim_term_ite_tactic.h
-Abstract:
-
- Eliminate term if-then-else by adding
- new fresh auxiliary variables.
-
Author:
Leonardo (leonardo) 2011-12-29
-Notes:
+Tactic Documentation:
+
+## Tactic elim-term-ite
+
+### Short Description:
+
+Eliminate term if-then-else by adding
+new fresh auxiliary variables.
+
+
+### Example
+
+```z3
+(declare-fun f (Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(declare-const c3 Bool)
+(declare-const e1 Int)
+(declare-const e2 Int)
+(declare-const e3 Int)
+(declare-const e4 Int)
+(assert (p (f (if c1 (if c2 e1 (if c3 e2 e3)) e4))))
+(apply elim-term-ite)
+```
+
+### Notes
+
+* supports proof terms and unsat cores
--*/
#pragma once
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 9f0717135..05ed6eee9 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -14,22 +14,6 @@ Author:
Nikolaj Bjorner (nbjorner) 2013-12-23
-Notes:
-
- Resolution for PB constraints require the implicit
- inequalities that each variable ranges over [0,1]
- so not all resolvents produce smaller sets of clauses.
-
- We here implement subsumption resolution.
-
- x + y >= 1
- A~x + B~y + Cz >= k
- ---------------------
- Cz >= k - B
-
- where A <= B, x, y do not occur elsewhere.
-
-
--*/
#include "tactic/core/pb_preprocess_tactic.h"
#include "tactic/tactical.h"
@@ -106,22 +90,20 @@ public:
return alloc(pb_preprocess_tactic, m);
}
- char const* name() const override { return "pb_preprocess"; }
+ char const* name() const override { return "pb-preprocess"; }
void operator()(
goal_ref const & g,
goal_ref_buffer & result) override {
tactic_report report("pb-preprocess", *g);
- if (g->proofs_enabled()) {
- throw tactic_exception("pb-preprocess does not support proofs");
- }
-
- generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");
-
g->inc_depth();
result.push_back(g.get());
- while (simplify(g, *pp));
- g->add(pp);
+
+ if (!g->proofs_enabled()) {
+ generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");
+ while (simplify(g, *pp));
+ g->add(pp);
+ }
// decompose(g);
}
diff --git a/src/tactic/core/pb_preprocess_tactic.h b/src/tactic/core/pb_preprocess_tactic.h
index ec387e6e0..83e8723f6 100644
--- a/src/tactic/core/pb_preprocess_tactic.h
+++ b/src/tactic/core/pb_preprocess_tactic.h
@@ -14,7 +14,51 @@ Author:
Nikolaj Bjorner (nbjorner) 2013-12-23
-Notes:
+Documentation:
+
+## Tactic pb-preprocess
+
+### Short Description:
+
+The tactic eliminates variables from pseudo-Boolean inequalities and performs algebraic simplifcations on formulas
+
+### Long Description
+
+Resolution for PB constraints require the implicit
+inequalities that each variable ranges over [0,1]
+so not all resolvents produce smaller sets of clauses.
+
+We here implement subsumption resolution.
+
+```
+ x + y >= 1
+ A~x + B~y + Cz >= k
+ ---------------------
+ Cz >= k - B
+```
+
+where `A <= B` and `x, y` do not occur elsewhere.
+
+
+### Example
+
+```z3
+ (declare-const x Bool)
+ (declare-const y Bool)
+ (declare-const z Bool)
+ (declare-const u Bool)
+ (declare-const v Bool)
+ (assert ((_ pbge 1 1 1 2) (not x) (not y) (not z)))
+ (assert ((_ pbge 1 1 1 2) x u v))
+ (assert (not (and y v)))
+ (assert (not (and z u)))
+ (apply pb-preprocess)
+```
+
+### Notes
+
+* supports unsat cores
+* does not support proof terms
--*/
#pragma once
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index e4476548a..667d53626 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -5,49 +5,14 @@ Module Name:
tseitin_cnf_tactic.cpp
-Abstract:
-
- Puts an assertion set in CNF.
- Auxiliary variables are used to avoid blowup.
-
- Features:
-
- - Efficient encoding is used for commonly used patterns such as:
- (iff a (iff b c))
- (or (not (or a b)) (not (or a c)) (not (or b c)))
-
- - Efficient encoding is used for chains of if-then-elses
-
- - Distributivity is applied to non-shared nodes if the blowup is acceptable.
-
- - The features above can be disabled/enabled using parameters.
-
- - The assertion-set is only modified if the resultant set of clauses
- is "acceptable".
-
- Notes:
-
- - Term-if-then-else expressions are not handled by this strategy.
- This kind of expression should be processed by other strategies.
-
- - Quantifiers are treated as "theory" atoms. They are viewed
- as propositional variables by this strategy.
-
- - The assertion set may contain free variables.
-
- - This strategy assumes the assertion_set_rewriter was
- used before invoking it.
- In particular, it is more effective when "and" operators
- were eliminated.
-
- TODO: add proof production
-
Author:
Leonardo (leonardo) 2011-12-29
Notes:
+ TODO: add proof production
+
--*/
#include "ast/ast_pp.h"
#include "tactic/tactical.h"
diff --git a/src/tactic/core/tseitin_cnf_tactic.h b/src/tactic/core/tseitin_cnf_tactic.h
index 363a1fafc..a5e116825 100644
--- a/src/tactic/core/tseitin_cnf_tactic.h
+++ b/src/tactic/core/tseitin_cnf_tactic.h
@@ -10,12 +10,40 @@ Abstract:
Puts an assertion set in CNF.
Auxiliary variables are used to avoid blowup.
+ Features:
+
+ - Efficient encoding is used for commonly used patterns such as:
+ (iff a (iff b c))
+ (or (not (or a b)) (not (or a c)) (not (or b c)))
+
+ - Efficient encoding is used for chains of if-then-elses
+
+ - Distributivity is applied to non-shared nodes if the blowup is acceptable.
+
+ - The features above can be disabled/enabled using parameters.
+
+ - The assertion-set is only modified if the resultant set of clauses
+ is "acceptable".
+
+ Notes:
+
+ - Term-if-then-else expressions are not handled by this strategy.
+ This kind of expression should be processed by other strategies.
+
+ - Quantifiers are treated as "theory" atoms. They are viewed
+ as propositional variables by this strategy.
+
+ - The assertion set may contain free variables.
+
+ - This strategy assumes the assertion_set_rewriter was
+ used before invoking it.
+ In particular, it is more effective when "and" operators
+ were eliminated.
+
Author:
Leonardo (leonardo) 2011-12-29
-Notes:
-
--*/
#pragma once