mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fix typos.
This commit is contained in:
parent
3f7453f5c5
commit
50f3e9c3c0
|
@ -260,7 +260,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
|
|||
vidx = to_var(t)->get_idx();
|
||||
if (fr.second == 0) {
|
||||
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
|
||||
// Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
|
||||
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
|
||||
if (definitions.get(vidx, 0) != 0) {
|
||||
if (visiting.is_marked(t)) {
|
||||
// cycle detected: remove t
|
||||
|
|
|
@ -722,7 +722,7 @@ namespace Duality {
|
|||
|
||||
check_result CheckUpdateModel(Node *root, std::vector<expr> assumps);
|
||||
|
||||
/** Determines the value in the counterexample of a symbol occuring in the transformer formula of
|
||||
/** Determines the value in the counterexample of a symbol occurring in the transformer formula of
|
||||
* a given edge. */
|
||||
|
||||
Term Eval(Edge *e, Term t);
|
||||
|
@ -731,7 +731,7 @@ namespace Duality {
|
|||
|
||||
Term EvalNode(Node *p);
|
||||
|
||||
/** Returns true if the given node is empty in the primal solution. For proecudure summaries,
|
||||
/** Returns true if the given node is empty in the primal solution. For procedure summaries,
|
||||
this means that the procedure is not called in the current counter-model. */
|
||||
|
||||
bool Empty(Node *p);
|
||||
|
@ -854,7 +854,7 @@ namespace Duality {
|
|||
/** Write the RPFP to a file (currently in SMTLIB 1.2 format) */
|
||||
void WriteProblemToFile(std::string filename, FileFormat format = DualityFormat);
|
||||
|
||||
/** Read the RPFP from a file (in specificed format) */
|
||||
/** Read the RPFP from a file (in specified format) */
|
||||
void ReadProblemFromFile(std::string filename, FileFormat format = DualityFormat);
|
||||
|
||||
/** Translate problem to Horn clause form */
|
||||
|
@ -870,9 +870,9 @@ namespace Duality {
|
|||
std::vector<Edge *> edges;
|
||||
|
||||
/** Fuse a vector of transformers. If the total number of inputs of the transformers
|
||||
is N, then the result is an N-ary transfomer whose output is the union of
|
||||
the outputs of the given transformers. The is, suppose we have a vetor of transfoermers
|
||||
{T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer
|
||||
is N, then the result is an N-ary transformer whose output is the union of
|
||||
the outputs of the given transformers. The is, suppose we have a vector of transformers
|
||||
{T_i(r_i1,...,r_iN(i) : i=1..M}. The result is a transformer
|
||||
|
||||
F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) =
|
||||
T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M))
|
||||
|
|
|
@ -1491,7 +1491,7 @@ namespace Duality {
|
|||
return res;
|
||||
}
|
||||
|
||||
/** Determines the value in the counterexample of a symbol occuring in the transformer formula of
|
||||
/** Determines the value in the counterexample of a symbol occurring in the transformer formula of
|
||||
* a given edge. */
|
||||
|
||||
RPFP::Term RPFP::Eval(Edge *e, Term t)
|
||||
|
@ -1500,7 +1500,7 @@ namespace Duality {
|
|||
return dualModel.eval(tl);
|
||||
}
|
||||
|
||||
/** Returns true if the given node is empty in the primal solution. For proecudure summaries,
|
||||
/** Returns true if the given node is empty in the primal solution. For proceudure summaries,
|
||||
this means that the procedure is not called in the current counter-model. */
|
||||
|
||||
bool RPFP::Empty(Node *p)
|
||||
|
|
|
@ -1421,7 +1421,7 @@ namespace polynomial {
|
|||
}
|
||||
}
|
||||
|
||||
// Return the maximal variable y occuring in [m_ms + start, m_ms + end) that is smaller than x
|
||||
// Return the maximal variable y occurring in [m_ms + start, m_ms + end) that is smaller than x
|
||||
var max_smaller_than(unsigned start, unsigned end, var x) {
|
||||
var max = null_var;
|
||||
for (unsigned i = start; i < end; i++) {
|
||||
|
@ -1456,7 +1456,7 @@ namespace polynomial {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Make sure that the first monomial contains the maximal variable x occuring in the polynomial,
|
||||
\brief Make sure that the first monomial contains the maximal variable x occurring in the polynomial,
|
||||
and x occurs with maximal degree.
|
||||
*/
|
||||
void make_first_maximal() {
|
||||
|
@ -3209,7 +3209,7 @@ namespace polynomial {
|
|||
typedef sbuffer<var, 32> var_buffer;
|
||||
|
||||
/**
|
||||
Store in pws the variables occuring in p and their (minimal or maximal) degrees.
|
||||
Store in pws the variables occurring in p and their (minimal or maximal) degrees.
|
||||
*/
|
||||
unsigned_vector m_var_degrees_tmp;
|
||||
template<bool Max>
|
||||
|
@ -3470,7 +3470,7 @@ namespace polynomial {
|
|||
pp = mk_one();
|
||||
return;
|
||||
}
|
||||
// Apply filter and collect powers of x occuring in p
|
||||
// Apply filter and collect powers of x occurring in p
|
||||
// The quick filter is the following:
|
||||
// If p contains a monomial x^k and no monomial of the form m*x^k m != 1, then
|
||||
// c = m_unit_poly
|
||||
|
@ -3479,7 +3479,7 @@ namespace polynomial {
|
|||
// - found monomial x^k then iccp_powers[k]++;
|
||||
// - found monomial m*x^k then iccp_powers[k]+=2;
|
||||
// If after traversing p, there is a k s.t. iccp_powers[k] == 1, we know c == 1
|
||||
// We store iccp_powers the powers of x occuring in p.
|
||||
// We store iccp_powers the powers of x occurring in p.
|
||||
sbuffer<unsigned, 128> iccp_filter;
|
||||
sbuffer<unsigned, 128> iccp_powers;
|
||||
iccp_filter.resize(d+1, 0);
|
||||
|
|
|
@ -46,7 +46,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
|
|||
verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
|
||||
);
|
||||
|
||||
// compute symbols occuring in B
|
||||
// compute symbols occurring in B
|
||||
collect_symbols_b(asserted_b);
|
||||
|
||||
// traverse proof
|
||||
|
|
|
@ -125,7 +125,7 @@ namespace eq {
|
|||
vidx = to_var(t)->get_idx();
|
||||
if (fr.second == 0) {
|
||||
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
|
||||
// Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
|
||||
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
|
||||
if (definitions.get(vidx, 0) != 0) {
|
||||
if (visiting.is_marked(t)) {
|
||||
// cycle detected: remove t
|
||||
|
|
|
@ -40,7 +40,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void theory_arith<Ext>::found_underspecified_op(app * n) {
|
||||
if (!m_found_underspecified_op) {
|
||||
TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
|
||||
TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, get_manager()) << "\n";);
|
||||
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
|
||||
m_found_underspecified_op = true;
|
||||
}
|
||||
|
|
|
@ -141,8 +141,8 @@ namespace smt {
|
|||
\brief Return the number of variables that
|
||||
do not have bounds associated with it.
|
||||
The result is 0, 1, or 2. The value 2 means "2 or more".
|
||||
The second value is the idx of the a variable that does not
|
||||
have bounds associated with it. It is only usefull when the first value is 1.
|
||||
The second value is the idx of the variable that does not
|
||||
have bounds associated with it. It is only useful when the first value is 1.
|
||||
The second value is -1 if such variable does not exist, that is, the first
|
||||
value is 0.
|
||||
|
||||
|
|
|
@ -196,7 +196,7 @@ class fix_dl_var_tactic : public tactic {
|
|||
|
||||
app * most_occs() {
|
||||
// We try to choose a variable that when set to 0 will generate many bounded variables.
|
||||
// That is why we give preference to variables occuring in non-nested inequalities.
|
||||
// That is why we give preference to variables occurring in non-nested inequalities.
|
||||
unsigned best1, best2;
|
||||
app * r1, * r2;
|
||||
r1 = most_occs(m_non_nested_occs, best1);
|
||||
|
|
|
@ -9,7 +9,7 @@ Abstract:
|
|||
|
||||
Put clauses in the assertion set in
|
||||
OOC (one constraint per clause) form.
|
||||
Constraints occuring in formulas that
|
||||
Constraints occurring in formulas that
|
||||
are not clauses are ignored.
|
||||
The formula can be put into CNF by
|
||||
using mk_sat_preprocessor strategy.
|
||||
|
|
|
@ -9,7 +9,7 @@ Abstract:
|
|||
|
||||
Put clauses in the assertion set in
|
||||
OOC (one constraint per clause) form.
|
||||
Constraints occuring in formulas that
|
||||
Constraints occurring in formulas that
|
||||
are not clauses are ignored.
|
||||
The formula can be put into CNF by
|
||||
using mk_sat_preprocessor strategy.
|
||||
|
|
Loading…
Reference in a new issue