mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00
Code Activity

Fix typos.

Browse source
This commit is contained in:
Bruce Mitchener 2018-12-23 21:58:57 -05:00
parent 9379ec3a68
commit 44bc00f13d
9 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/c/test_capi.c
View file

@ -1697,7 +1697,7 @@ void parser_example3()
LOG_MSG("parser_example3");
cfg = Z3_mk_config();
/* See quantifer_example1 */
/* See quantifier_example1 */
Z3_set_param_value(cfg, "model", "true");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);

4
examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs
View file

@ -33,14 +33,14 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
#region Solver construction and destruction
/// <summary>Constructor that initializes the base clases</summary>
/// <summary>Constructor that initializes the base classes</summary>
public Z3MILPSolver() : base(null)
{
_result = LinearResult.Feasible;
_solver = new Z3BaseSolver(this);
}
/// <summary>Constructor that initializes the base clases</summary>
/// <summary>Constructor that initializes the base classes</summary>
public Z3MILPSolver(ISolverEnvironment context) : this() { }
/// <summary>

4
examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs
View file

@ -29,13 +29,13 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
private NonlinearResult _result;
private Z3BaseSolver _solver;
/// <summary>Constructor that initializes the base clases</summary>
/// <summary>Constructor that initializes the base classes</summary>
public Z3TermSolver() : base(null)
{
_solver = new Z3BaseSolver(this);
}
/// <summary>Constructor that initializes the base clases</summary>
/// <summary>Constructor that initializes the base classes</summary>
public Z3TermSolver(ISolverEnvironment context) : this() { }
/// <summary>

2
src/api/z3_api.h
View file

@ -4094,7 +4094,7 @@ extern "C" {
The remaining fields are left unchanged. It is the record
equivalent of an array store (see \sa Z3_mk_store).
If the datatype has more than one constructor, then the update function
behaves as identity if there is a miss-match between the accessor and
behaves as identity if there is a mismatch between the accessor and
constructor. For example ((_ update-field car) nil 1) is nil,
while ((_ update-field car) (cons 2 nil) 1) is (cons 1 nil).

12
src/ast/dl_decl_plugin.cpp
View file

@ -147,7 +147,7 @@ namespace datalog {
for (unsigned i = 0; i < n; ++i) {
parameter const& p = r->get_parameter(i);
if (!p.is_ast() || !is_sort(p.get_ast())) {
m_manager->raise_exception("exptected sort parameter");
m_manager->raise_exception("expected sort parameter");
return false;
}
sorts.push_back(to_sort(p.get_ast()));
@ -185,7 +185,7 @@ namespace datalog {
verbose_stream() << "Domain: " << mk_pp(domain[0], m) << "\n" <<
mk_pp(sorts[i], m) << "\n" <<
mk_pp(domain[i+1], m) << "\n";);
m_manager->raise_exception("sort miss-match for relational access");
m_manager->raise_exception("sort mismatch for relational access");
return nullptr;
}
}
@ -252,7 +252,7 @@ namespace datalog {
func_decl * dl_decl_plugin::mk_unionw(decl_kind k, sort* s1, sort* s2) {
ast_manager& m = *m_manager;
if (s1 != s2) {
m_manager->raise_exception("sort miss-match for arguments to union");
m_manager->raise_exception("sort mismatch for arguments to union");
return nullptr;
}
if (!is_rel_sort(s1)) {
@ -298,7 +298,7 @@ namespace datalog {
return nullptr;
}
if (sorts[idx] != m.get_sort(e)) {
m_manager->raise_exception("sort miss-match in filter");
m_manager->raise_exception("sort mismatch in filter");
return nullptr;
}
break;
@ -391,7 +391,7 @@ namespace datalog {
return nullptr;
}
if (sorts1[i1] != sorts2[i2]) {
m_manager->raise_exception("sort miss-match in join");
m_manager->raise_exception("sort mismatch in join");
return nullptr;
}
}
@ -435,7 +435,7 @@ namespace datalog {
return nullptr;
}
if (sorts1[i1] != sorts2[i2]) {
m_manager->raise_exception("sort miss-match in join");
m_manager->raise_exception("sort mismatch in join");
return nullptr;
}
}

4
src/muz/base/dl_context.cpp
View file

@ -658,7 +658,7 @@ namespace datalog {
void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) {
if (pred->get_arity() != num_args) {
std::ostringstream out;
out << "miss-matched number of arguments passed to " << mk_ismt2_pp(pred, m) << " " << num_args << " passed";
out << "mismatched number of arguments passed to " << mk_ismt2_pp(pred, m) << " " << num_args << " passed";
throw default_exception(out.str());
}
table_fact fact;
@ -1243,7 +1243,7 @@ namespace datalog {
void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) {
//
// replace bound variables in rules by 'var declarations'
// First remove quantifers, then replace bound variables
// First remove quantifiers, then replace bound variables
// by fresh constants.
//
smt2_pp_environment_dbg env(m);

2
src/sat/sat_solver.cpp
View file

@ -2665,7 +2665,7 @@ namespace sat {
for (unsigned i = head; i < sz; i++) {
literal l = m_trail[i];
bool_var v = l.var();
TRACE("forget_phase", tout << "forgeting phase of l: " << l << "\n";);
TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";);
m_phase[v] = PHASE_NOT_AVAILABLE;
}
}

8
src/smt/smt_context.cpp
View file

@ -1813,7 +1813,7 @@ namespace smt {
}
/**
\brief Execute next clase split, return false if there are no
\brief Execute next case split, return false if there are no
more case splits to be performed.
*/
bool context::decide() {
@ -1858,7 +1858,7 @@ namespace smt {
if (is_quantifier(m_bool_var2expr[var])) {
// Overriding any decision on how to assign the quantifier.
// assigining a quantifier to false is equivalent to make it irrelevant.
// assigning a quantifier to false is equivalent to make it irrelevant.
phase = l_false;
}
@ -2134,7 +2134,7 @@ namespace smt {
\brief When a clause is reinitialized (see reinit_clauses) enodes and literals may
need to be recreated. When an enode is recreated, I want to use the same generation
number it had before being deleted. Otherwise the generation will be 0, and will affect
the loop prevetion heuristics used to control quantifier instantiation.
the loop prevention heuristics used to control quantifier instantiation.
Thus, I cache the generation number of enodes that will be deleted during backtracking
and recreated by reinit_clauses.
*/
@ -3872,7 +3872,7 @@ namespace smt {
for (unsigned i = head; i < sz; i++) {
literal l = m_assigned_literals[i];
bool_var v = l.var();
TRACE("forget_phase", tout << "forgeting phase of l: " << l << "\n";);
TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";);
m_bdata[v].m_phase_available = false;
}
}

2
src/smt/smt_model_finder.cpp
View file

@ -1703,7 +1703,7 @@ namespace smt {
friend class quantifier_analyzer;
void checkpoint() {
m_mf.checkpoint("quantifer_info");
m_mf.checkpoint("quantifier_info");
}
void insert_qinfo(qinfo * qi) {