mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fix typos. (#6291)
This commit is contained in:
parent
706f7fbdc7
commit
6ba9ada1e2
|
@ -8,7 +8,7 @@ import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types';
|
|||
*
|
||||
* **NOTE**: The set of solutions might be infinite.
|
||||
* Always ensure to limit amount generated, either by knowing that the
|
||||
* solution space is constrainted, or by taking only a specified
|
||||
* solution space is constrained, or by taking only a specified
|
||||
* amount of solutions
|
||||
* ```typescript
|
||||
* import { sliceAsync } from 'iter-tools';
|
||||
|
@ -46,7 +46,7 @@ async function* allSolutions<Name extends string>(...assertions: Bool<Name>[]):
|
|||
.filter(decl => decl.arity() === 0)
|
||||
.map(decl => {
|
||||
const term = decl.call();
|
||||
// TODO(ritave): Assert not an array / uinterpeted sort
|
||||
// TODO(ritave): Assert not an array / uninterpreted sort
|
||||
const value = model.eval(term, true);
|
||||
return term.neq(value);
|
||||
}),
|
||||
|
|
|
@ -617,7 +617,7 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
|
|||
*/
|
||||
mul(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
/**
|
||||
* Substract second number from the first one
|
||||
* Subtract second number from the first one
|
||||
*/
|
||||
sub(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
/**
|
||||
|
@ -709,7 +709,7 @@ export interface RatNum<Name extends string = 'main'> extends Arith<Name> {
|
|||
}
|
||||
|
||||
/**
|
||||
* A Sort represting Bit Vector numbers of specified {@link BitVecSort.size size}
|
||||
* A Sort representing Bit Vector numbers of specified {@link BitVecSort.size size}
|
||||
*
|
||||
* @typeParam Bits - A number representing amount of bits for this sort
|
||||
* @category Bit Vectors
|
||||
|
@ -878,42 +878,42 @@ export interface BitVec<Bits extends number = number, Name extends string = 'mai
|
|||
|
||||
/**
|
||||
* Creates a signed less-or-equal operation (`<=`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
sle(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates an unsigned less-or-equal operation (`<=`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
ule(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates a signed less-than operation (`<`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
slt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates an unsigned less-than operation (`<`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
ult(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates a signed greater-or-equal operation (`>=`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
sge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates an unsigned greater-or-equal operation (`>=`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
uge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates a signed greater-than operation (`>`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
sgt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
/**
|
||||
* Creates an unsigned greater-than operation (`>`)
|
||||
* @category Comparision
|
||||
* @category Comparison
|
||||
*/
|
||||
ugt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
|
|
|
@ -39,7 +39,7 @@ $ ldd ./run
|
|||
/lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)
|
||||
```
|
||||
|
||||
The bytecode version will have a depedency on z3 and other external
|
||||
The bytecode version will have a dependency on z3 and other external
|
||||
libraries (packed as dlls and usually installed in opam switch):
|
||||
```
|
||||
$ ocamlobjinfo run | grep 'Used DLL' -A5
|
||||
|
@ -126,7 +126,7 @@ Using Dynlink
|
|||
-------------
|
||||
|
||||
The built z3ml.cmxs file is a self-contained shared library that
|
||||
doesn't have any depndencies on z3 (the z3 code is included in it) and
|
||||
doesn't have any dependencies on z3 (the z3 code is included in it) and
|
||||
could be loaded with `Dynlink.loadfile` in runtime.
|
||||
|
||||
Installation
|
||||
|
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
Abstract:
|
||||
|
||||
intervals with depedency tracking.
|
||||
intervals with dependency tracking.
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
|
|
|
@ -7,7 +7,7 @@
|
|||
|
||||
Abstract:
|
||||
|
||||
intervals with depedency tracking.
|
||||
intervals with dependency tracking.
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
|
|
|
@ -93,7 +93,7 @@ class lar_solver : public column_namer {
|
|||
unsigned_vector m_row_bounds_to_replay;
|
||||
|
||||
u_set m_basic_columns_with_changed_cost;
|
||||
// these are basic columns with the value changed, so the the corresponding row in the tableau
|
||||
// these are basic columns with the value changed, so the corresponding row in the tableau
|
||||
// does not sum to zero anymore
|
||||
u_set m_incorrect_columns;
|
||||
// copy of m_r_solver.inf_set()
|
||||
|
|
|
@ -226,7 +226,7 @@ public:
|
|||
void set_next_arg(cmd_context & ctx, func_decl* t) override {
|
||||
m_target = t;
|
||||
if (t->get_family_id() != null_family_id) {
|
||||
throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted");
|
||||
throw cmd_exception("Invalid query argument, expected uninterpreted function name, but argument is interpreted");
|
||||
}
|
||||
datalog::context& dlctx = m_dl_ctx->dlctx();
|
||||
if (!dlctx.get_predicates().contains(t)) {
|
||||
|
|
|
@ -25,7 +25,7 @@ Revision History:
|
|||
Let x_i, y_i, z_i be indices into the vectors x, y, z.
|
||||
|
||||
Suppose that positions in P and R are annotated with what is
|
||||
slicable.
|
||||
sliceable.
|
||||
|
||||
Sufficient conditions for sliceability:
|
||||
|
||||
|
@ -43,9 +43,9 @@ Revision History:
|
|||
and the positions where z_i is used in P and R are sliceable
|
||||
|
||||
|
||||
A more refined approach may be using Gaussean elimination based
|
||||
A more refined approach may be using Gaussian elimination based
|
||||
on x,z and eliminating variables from x,y (expressing them in terms
|
||||
of a disjoint subeset of x,z).
|
||||
of a disjoint subset of x,z).
|
||||
|
||||
|
||||
--*/
|
||||
|
@ -441,7 +441,7 @@ namespace datalog {
|
|||
|
||||
void mk_slice::filter_unique_vars(rule& r) {
|
||||
//
|
||||
// Variables that occur in multiple uinterpreted predicates are not sliceable.
|
||||
// Variables that occur in multiple uninterpreted predicates are not sliceable.
|
||||
//
|
||||
uint_set used_vars;
|
||||
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
|
||||
|
|
|
@ -37,7 +37,7 @@ namespace smt {
|
|||
return;
|
||||
|
||||
SASSERT(is_fixed(v));
|
||||
// WARNINING: it is not safe to use get_value(v) here, since
|
||||
// WARNING: it is not safe to use get_value(v) here, since
|
||||
// get_value(v) may not satisfy v bounds at this point.
|
||||
if (!lower_bound(v).is_rational())
|
||||
return;
|
||||
|
|
|
@ -711,7 +711,7 @@ namespace smt {
|
|||
for (; it != end; ++it) {
|
||||
if (!it->is_dead()) {
|
||||
if (is_fixed(it->m_var)) {
|
||||
// WARNINING: it is not safe to use get_value(it->m_var) here, since
|
||||
// WARNING: it is not safe to use get_value(it->m_var) here, since
|
||||
// get_value(it->m_var) may not satisfy it->m_var bounds at this point.
|
||||
numeral aux = lcm_den * it->m_coeff;
|
||||
consts += aux * lower_bound(it->m_var).get_rational();
|
||||
|
|
Loading…
Reference in a new issue