mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix misspelled \brief for doxygen (#5632)

Browse source
This commit is contained in:
Alexander Traud 2021-10-29 15:34:28 +02:00 committed by GitHub
parent 780761a29e
commit d1592c6abf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/model/array_factory.cpp
View file

@ -38,7 +38,7 @@ array_factory::array_factory(ast_manager & m, model_core & md):
} }
/** /**
\brieft Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s. \brief Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s.
Store in fi the function interpretation for f. Store in fi the function interpretation for f.
*/ */
expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) { expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {

2
src/muz/spacer/spacer_mbc.h
View file

@ -34,7 +34,7 @@ public:
typedef obj_map<func_decl, unsigned> partition_map; typedef obj_map<func_decl, unsigned> partition_map;
/** /**
\Brief Model Based Cartesian projection of lits \brief Model Based Cartesian projection of lits
*/ */
void operator()(const partition_map &pmap, expr_ref_vector &lits, model &mdl, void operator()(const partition_map &pmap, expr_ref_vector &lits, model &mdl,
vector<expr_ref_vector> &res); vector<expr_ref_vector> &res);

2
src/smt/seq_offset_eq.h
View file

@ -42,7 +42,7 @@ namespace smt {
seq_offset_eq(theory& th, ast_manager& m); seq_offset_eq(theory& th, ast_manager& m);
bool empty() const { return m_offset_equalities.empty(); } bool empty() const { return m_offset_equalities.empty(); }
/** /**
\breif determine if r1 = r2 + offset \brief determine if r1 = r2 + offset
*/ */
bool find(enode* r1, enode* r2, int& offset) const; bool find(enode* r1, enode* r2, int& offset) const;
bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); } bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }

4
src/smt/smt_relevancy.h
View file

@ -169,12 +169,12 @@ namespace smt {
bool enabled() const; bool enabled() const;
/** /**
\Brief Return the region allocator for the smt::context that owns this propagator. \brief Return the region allocator for the smt::context that owns this propagator.
*/ */
region & get_region() const; region & get_region() const;
/** /**
\Brief Return the ast_manager for the smt::context that owns this propagator. \brief Return the ast_manager for the smt::context that owns this propagator.
*/ */
ast_manager & get_manager() const; ast_manager & get_manager() const;