From 7afcaa5364370dc20ba73b05304c138eb9dd7aed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Dec 2022 18:56:21 -0800 Subject: [PATCH] update doc Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/eq2bv_tactic.h | 28 ++++++++++++++---- src/tactic/arith/factor_tactic.cpp | 2 +- src/tactic/arith/factor_tactic.h | 16 ++++++++++- src/tactic/arith/fix_dl_var_tactic.h | 29 +++++++++++++++---- src/tactic/arith/fm_tactic.cpp | 18 ++++++------ src/tactic/arith/fm_tactic.h | 43 +++++++++++++++++++++------- 6 files changed, 102 insertions(+), 34 deletions(-) diff --git a/src/tactic/arith/eq2bv_tactic.h b/src/tactic/arith/eq2bv_tactic.h index e8c29715cc0..81d2718a6be 100644 --- a/src/tactic/arith/eq2bv_tactic.h +++ b/src/tactic/arith/eq2bv_tactic.h @@ -5,16 +5,32 @@ Module Name: eq2bv_tactic.h -Abstract: - - Extract integer variables that are used as finite domain indicators. - The integer variables can only occur in equalities. - Author: Nikolaj Bjorner (nbjorner) 2015-8-19 -Notes: +Tactic Documentation: + +## Tactic eq2bv + +### Short Description + +Extract integer variables that are used as finite domain indicators. +The integer variables can only occur in equalities. + +### Example + +```z3 +(declare-const x Int) +(declare-const y Int) +(assert (or (= x 5) (> y 3))) +(assert (or (= x 4) (= y 2))) +(apply eq2bv) +``` + +### Notes + +* does not support proofs --*/ #pragma once diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 6b9b226b3c7..565f43af9c6 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -303,7 +303,7 @@ class factor_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { r.insert("split_factors", CPK_BOOL, - "(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0))."); + "apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).", "true"); polynomial::factor_params::get_param_descrs(r); } diff --git a/src/tactic/arith/factor_tactic.h b/src/tactic/arith/factor_tactic.h index b02f674484f..7be5c5df66b 100644 --- a/src/tactic/arith/factor_tactic.h +++ b/src/tactic/arith/factor_tactic.h @@ -13,7 +13,21 @@ Module Name: Leonardo de Moura (leonardo) 2012-02-03 -Revision History: +Tactic Documentation: + +## Tactic factor + +### Short Description + +Factor polynomials in equalities and inequalities. + +### Example +```z3 +(declare-const x Real) +(declare-const y Real) +(assert (> (* x x) (* x y))) +(apply factor) +``` --*/ #pragma once diff --git a/src/tactic/arith/fix_dl_var_tactic.h b/src/tactic/arith/fix_dl_var_tactic.h index d7a79bf4b0d..f8b03557f9a 100644 --- a/src/tactic/arith/fix_dl_var_tactic.h +++ b/src/tactic/arith/fix_dl_var_tactic.h @@ -7,18 +7,35 @@ Module Name: Abstract: - Fix a difference logic variable to 0. - If the problem is in the difference logic fragment, that is, all arithmetic terms - are of the form (x + k), and the arithmetic atoms are of the - form x - y <= k or x - y = k. Then, we can set one variable to 0. - This is useful because, many bounds can be exposed after this operation is performed. Author: Leonardo (leonardo) 2011-12-29 -Notes: +Tactic Documentation: + +## Tactic fix-dl-var + +### Short Description + +Fix a difference logic variable to `0`. +If the problem is in the difference logic fragment, that is, all arithmetic terms +are of the form `(x + k)`, and the arithmetic atoms are of the +form `x - y <= k` or `x - y = k`. Then, we can set one variable to `0`. + +This is useful because, many bounds can be exposed after this operation is performed. + +### Example + +```z3 +(declare-const x Real) +(declare-const y Real) +(declare-const z Real) +(assert (<= (+ x (* -1.0 y)) 3.0)) +(assert (<= (+ x (* -1.0 z)) 5.0)) +(apply fix-dl-var) +``` --*/ #pragma once diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index d0564139ad0..1d3bc277058 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -467,10 +467,8 @@ class fm_tactic : public tactic { x = t; return true; } - else if (m_util.is_to_real(t) && is_uninterp_const(to_app(t)->get_arg(0))) { - x = to_app(t)->get_arg(0); - return true; - } + else if (m_util.is_to_real(t, x) && is_uninterp_const(x)) + return true; return false; } @@ -1675,12 +1673,12 @@ class fm_tactic : public tactic { void collect_param_descrs(param_descrs & r) override { insert_produce_models(r); insert_max_memory(r); - r.insert("fm_real_only", CPK_BOOL, "(default: true) consider only real variables for fourier-motzkin elimination."); - r.insert("fm_occ", CPK_BOOL, "(default: false) consider inequalities occurring in clauses for FM."); - r.insert("fm_limit", CPK_UINT, "(default: 5000000) maximum number of constraints, monomials, clauses visited during FM."); - r.insert("fm_cutoff1", CPK_UINT, "(default: 8) first cutoff for FM based on maximum number of lower/upper occurrences."); - r.insert("fm_cutoff2", CPK_UINT, "(default: 256) second cutoff for FM based on num_lower * num_upper occurrences."); - r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step."); + r.insert("fm_real_only", CPK_BOOL, "consider only real variables for fourier-motzkin elimination.", "true"); + r.insert("fm_occ", CPK_BOOL, "consider inequalities occurring in clauses for FM.", "false"); + r.insert("fm_limit", CPK_UINT, "maximum number of constraints, monomials, clauses visited during FM.", "5000000"); + r.insert("fm_cutoff1", CPK_UINT, "first cutoff for FM based on maximum number of lower/upper occurrences.", "8"); + r.insert("fm_cutoff2", CPK_UINT, "second cutoff for FM based on num_lower * num_upper occurrences.", "256"); + r.insert("fm_extra", CPK_UINT, "max. increase on the number of inequalities for each FM variable elimination step.", "0"); } diff --git a/src/tactic/arith/fm_tactic.h b/src/tactic/arith/fm_tactic.h index 622007703a1..7021dc27304 100644 --- a/src/tactic/arith/fm_tactic.h +++ b/src/tactic/arith/fm_tactic.h @@ -5,20 +5,43 @@ Module Name: fm_tactic.h -Abstract: - - Use Fourier-Motzkin to eliminate variables. - This strategy can handle conditional bounds - (i.e., clauses with at most one constraint). - - The strategy mk_occf can be used to put the - formula in OCC form. - Author: Leonardo de Moura (leonardo) 2012-02-04. -Revision History: +Tactic Documentation: + +## Tactic fm + +### Short Description + +Use Fourier-Motzkin to eliminate variables. +This strategy can handle conditional bounds +(i.e., clauses with at most one constraint). + +The strategy mk_occf can be used to put the +formula in OCC form. + +### Example + +```z3 +(declare-const x Real) +(declare-const y Real) +(declare-const z Real) +(declare-const u Real) +(declare-const v Real) +(declare-const w Real) +(declare-fun P (Real) Bool) +(assert (<= x (+ y (* 2.0 z)))) +(assert (>= x (- y z))) +(assert (>= x (- y 3 (* 3 z)))) +(assert (>= x 5)) +(assert (<= x u)) +(assert (>= x v)) +(assert (P u)) +(assert (P v)) +(apply fm) +``` --*/ #pragma once