mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
add tactic descriptions
This commit is contained in:
parent
f01d9d29d2
commit
d5316e017e
|
@ -144,10 +144,12 @@ public:
|
|||
|
||||
bool get_subst(expr * s, expr * & t, proof * & t_pr)
|
||||
{
|
||||
if (!is_app(s)) { return false; }
|
||||
if (!is_app(s))
|
||||
return false;
|
||||
app * a = to_app(s);
|
||||
func_decl * sym = a->get_decl();
|
||||
if (!m_parent.has_index(sym, m_from_idx)) {
|
||||
CTRACE("spacer", m_homogenous && m_parent.is_muxed(sym), tout << "not found " << mk_pp(a, m) << "\n");
|
||||
SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
|
||||
return false;
|
||||
}
|
||||
|
|
|
@ -13,7 +13,32 @@ Author:
|
|||
|
||||
Christoph (cwinter) 2012-02-15
|
||||
|
||||
Notes:
|
||||
Tactic Documentation:
|
||||
|
||||
## Tactic pb2bv
|
||||
|
||||
### Short Description
|
||||
|
||||
Convert pseudo-boolean constraints to bit-vectors
|
||||
|
||||
### Example
|
||||
|
||||
```z3
|
||||
(declare-const x Int)
|
||||
(declare-const y Int)
|
||||
(declare-const z Int)
|
||||
(declare-const u Int)
|
||||
(assert (<= 0 x))
|
||||
(assert (<= 0 y))
|
||||
(assert (<= 0 z))
|
||||
(assert (<= 0 u))
|
||||
(assert (<= x 1))
|
||||
(assert (<= y 1))
|
||||
(assert (<= z 1))
|
||||
(assert (<= u 1))
|
||||
(assert (>= (+ (* 3 x) (* 2 y) (* 2 z) (* 2 u)) 4))
|
||||
(apply pb2bv)
|
||||
```
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
|
|
@ -4,30 +4,49 @@ Copyright (c) 2012 Microsoft Corporation
|
|||
Module Name:
|
||||
|
||||
propagate_ineqs_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
This tactic performs the following tasks:
|
||||
|
||||
- Propagate bounds using the bound_propagator.
|
||||
- Eliminate subsumed inequalities.
|
||||
For example:
|
||||
x - y >= 3
|
||||
can be replaced with true if we know that
|
||||
x >= 3 and y <= 0
|
||||
|
||||
- Convert inequalities of the form p <= k and p >= k into p = k,
|
||||
where p is a polynomial and k is a constant.
|
||||
|
||||
This strategy assumes the input is in arith LHS mode.
|
||||
This can be achieved by using option :arith-lhs true in the
|
||||
simplifier.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-02-19
|
||||
|
||||
Notes:
|
||||
Tactic Documentation:
|
||||
|
||||
## Tactic propagate-ineqs
|
||||
|
||||
### Short Description
|
||||
|
||||
Propagate ineqs/bounds, remove subsumed inequalities
|
||||
|
||||
### Long Description
|
||||
|
||||
This tactic performs the following tasks:
|
||||
|
||||
- Propagate bounds using the bound_propagator.
|
||||
- Eliminate subsumed inequalities.
|
||||
- For example:
|
||||
`x - y >= 3` can be replaced with true if we know that `x >= 3` and `y <= 0`
|
||||
|
||||
- Convert inequalities of the form `p <= k` and `p >= k` into `p = k`,
|
||||
where `p` is a polynomial and `k` is a constant.
|
||||
|
||||
This strategy assumes the input is in arith LHS mode.
|
||||
This can be achieved by using option :arith-lhs true in the simplifier.
|
||||
|
||||
### Example
|
||||
```z3
|
||||
(declare-const x Int)
|
||||
(declare-const y Int)
|
||||
(declare-const z Int)
|
||||
(declare-const u Int)
|
||||
(declare-const v Int)
|
||||
(declare-const w Int)
|
||||
(assert (>= x 3))
|
||||
(assert (<= y 0))
|
||||
(assert (>= (- x y) 3))
|
||||
(assert (>= (* u v w) 2))
|
||||
(assert (<= (* v u w) 2))
|
||||
(apply (and-then simplify propagate-ineqs))
|
||||
```
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
|
|
@ -42,7 +42,28 @@ Author:
|
|||
|
||||
Leonardo de Moura (leonardo) 2011-12-30.
|
||||
|
||||
Revision History:
|
||||
Tactic Documentation:
|
||||
|
||||
## Tactic purify-arith
|
||||
|
||||
### Short Description
|
||||
|
||||
Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.
|
||||
These operators can be replaced by introcing fresh variables and using multiplication and addition.
|
||||
|
||||
### Example
|
||||
```z3
|
||||
(declare-const x Int)
|
||||
(declare-const y Int)
|
||||
(declare-const z Int)
|
||||
(declare-const u Int)
|
||||
(declare-const v Int)
|
||||
(declare-const w Int)
|
||||
(assert (= (div x 3) y))
|
||||
(assert (= (mod z 4) u))
|
||||
(assert (> (mod v w) u))
|
||||
(apply purify-arith)
|
||||
```
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
|
Loading…
Reference in a new issue