From 44bc00f13dcee1ed8198f0dd72f687bf57784647 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 23 Dec 2018 21:58:57 -0500 Subject: [PATCH] Fix typos. --- examples/c/test_capi.c | 2 +- .../msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs | 4 ++-- .../msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs | 4 ++-- src/api/z3_api.h | 2 +- src/ast/dl_decl_plugin.cpp | 12 ++++++------ src/muz/base/dl_context.cpp | 4 ++-- src/sat/sat_solver.cpp | 2 +- src/smt/smt_context.cpp | 8 ++++---- src/smt/smt_model_finder.cpp | 2 +- 9 files changed, 20 insertions(+), 20 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 980592f25..f9c108b92 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -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); diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs index f3a8f9f2c..4f8cdc759 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs @@ -33,14 +33,14 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 #region Solver construction and destruction - /// Constructor that initializes the base clases + /// Constructor that initializes the base classes public Z3MILPSolver() : base(null) { _result = LinearResult.Feasible; _solver = new Z3BaseSolver(this); } - /// Constructor that initializes the base clases + /// Constructor that initializes the base classes public Z3MILPSolver(ISolverEnvironment context) : this() { } /// diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs index 530df3394..de91c7b6e 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs @@ -29,13 +29,13 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 private NonlinearResult _result; private Z3BaseSolver _solver; - /// Constructor that initializes the base clases + /// Constructor that initializes the base classes public Z3TermSolver() : base(null) { _solver = new Z3BaseSolver(this); } - /// Constructor that initializes the base clases + /// Constructor that initializes the base classes public Z3TermSolver(ISolverEnvironment context) : this() { } /// diff --git a/src/api/z3_api.h b/src/api/z3_api.h index f3d61c1cf..5ee7fcb99 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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). diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index f4a538abd..01b06518e 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -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; } } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 1c9abf78c..e8578f327 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -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); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d48a6410c..fc5fce252 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -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; } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7ee6d4a92..3c601f400 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; } } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 30ea7b18e..111b9a0c0 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -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) {