mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

typo

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-06 15:51:38 -08:00
parent 1e06c7414a
commit d125d87aed
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/core/solve_eqs_tactic.h
View file

@ -35,7 +35,7 @@ everywhere by `f(x + y)`. It depends on a set of theory specific equality solver
* Arithmetic equations * Arithmetic equations
* It solves `x mod k = s` to `x = k * m' + s`, where m'` is a fresh constant. * It solves `x mod k = s` to `x = k * m' + s`, where m'` is a fresh constant.
* It finds variables with unit coefficients in integer linear equations. * It finds variables with unit coefficients in integer linear equations.
* It solves for `x * Y = Z$ under the side-condition `Y != 0` as `x = Z/Y`. * It solves for `x * Y = Z` under the side-condition `Y != 0` as `x = Z/Y`.
It also allows solving for uninterpreted constants that only appear in a single disjuction. For example, It also allows solving for uninterpreted constants that only appear in a single disjuction. For example,
`(or (= x (+ 5 y)) (= y (+ u z)))` allows solving for `x`. `(or (= x (+ 5 y)) (= y (+ u z)))` allows solving for `x`.