mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 05:41:23 +00:00
Code Activity

Merge pull request #1931 from waywardmonkeys/fix-more-typos

Browse source 
Fix typos.
This commit is contained in:
Nikolaj Bjorner 2018-11-11 09:29:45 -08:00 • committed by GitHub
commit 9bd7e8ea7e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/csp_decl_plugin.cpp
View file

@ -104,7 +104,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer");
if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer");
if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer"); if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer");
if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties"); if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be a list of properties");
name = symbol("add-job-resource"); name = symbol("add-job-resource");
rng = m_alist_sort; rng = m_alist_sort;
break; break;
@ -115,7 +115,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer");
if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer");
if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer"); if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer");
if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be an a list of properties"); if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be a list of properties");
name = symbol("add-resource-available"); name = symbol("add-resource-available");
rng = m_alist_sort; rng = m_alist_sort;
break; break;

4
src/muz/rel/dl_relation_manager.h
View file

@ -263,7 +263,7 @@ namespace datalog {
} }
/** /**
\brief Return an operation that is a composition of a join an a project operation. \brief Return an operation that is a composition of a join and a project operation.
*/ */
relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2, relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2,
unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2,
@ -433,7 +433,7 @@ namespace datalog {
} }
/** /**
\brief Return an operation that is a composition of a join an a project operation. \brief Return an operation that is a composition of a join and a project operation.
This operation is equivalent to the two operations performed separately, unless functional This operation is equivalent to the two operations performed separately, unless functional
columns are involved. columns are involved.

4
src/smt/theory_jobscheduler.cpp
View file

@ -315,7 +315,7 @@ namespace smt {
/** /**
* For time interval [t0, t1] the end-time can be computed as a function * For time interval [t0, t1] the end-time can be computed as a function
* of start time based on reource load availability. * of start time based on resource load availability.
* *
* r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0 * r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0
*/ */
@ -672,7 +672,7 @@ namespace smt {
} }
/* /*
* Initialze the state based on the set of jobs and resources added. * Initialize the state based on the set of jobs and resources added.
* Ensure that the availability slots for each resource is sorted by time. * Ensure that the availability slots for each resource is sorted by time.
* *
* For each resource j: * For each resource j: