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

Fix typos.

Browse source
This commit is contained in:
Bruce Mitchener 2018-11-30 22:19:30 +07:00
parent 57318bab5b
commit 3149d7f7a4
7 changed files with 24 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.cpp
View file

@ -682,7 +682,7 @@ namespace datatype {
/** /**
\brief Return true if the inductive datatype is well-founded. \brief Return true if the inductive datatype is well-founded.
Pre-condition: The given argument constains the parameters of an inductive datatype. Pre-condition: The given argument constrains the parameters of an inductive datatype.
*/ */
bool util::is_well_founded(unsigned num_types, sort* const* sorts) { bool util::is_well_founded(unsigned num_types, sort* const* sorts) {
buffer<bool> well_founded(num_types, false); buffer<bool> well_founded(num_types, false);

10
src/math/realclosure/realclosure.cpp
View file

@ -154,7 +154,7 @@ namespace realclosure {
struct value { struct value {
unsigned m_ref_count; //!< Reference counter unsigned m_ref_count; //!< Reference counter
bool m_rational; //!< True if the value is represented as an abitrary precision rational value. bool m_rational; //!< True if the value is represented as an arbitrary precision rational value.
mpbqi m_interval; //!< approximation as an interval with binary rational end-points mpbqi m_interval; //!< approximation as an interval with binary rational end-points
// When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small. // When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small.
// The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations, // The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations,
@ -283,7 +283,7 @@ namespace realclosure {
struct algebraic : public extension { struct algebraic : public extension {
polynomial m_p; polynomial m_p;
mpbqi m_iso_interval; mpbqi m_iso_interval;
sign_det * m_sign_det; //!< != 0 if m_iso_interval constains more than one root of m_p. sign_det * m_sign_det; //!< != 0 if m_iso_interval constrains more than one root of m_p.
unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size() unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size()
bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions. bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions.
@ -1741,7 +1741,7 @@ namespace realclosure {
\brief In the sign determination algorithm main loop, we keep processing polynomials q, \brief In the sign determination algorithm main loop, we keep processing polynomials q,
and checking whether they discriminate the roots of the target polynomial. and checking whether they discriminate the roots of the target polynomial.
The vectors sc_cardinalities contains the cardinalites of the new realizable sign conditions. The vectors sc_cardinalities contains the cardinalities of the new realizable sign conditions.
That is, we started we a sequence of sign conditions That is, we started we a sequence of sign conditions
sc_1, ..., sc_n, sc_1, ..., sc_n,
If q2_used is true, then we expanded this sequence as If q2_used is true, then we expanded this sequence as
@ -1750,7 +1750,7 @@ namespace realclosure {
Thus, q is useful (i.e., it is a discriminator for the roots of p) IF Thus, q is useful (i.e., it is a discriminator for the roots of p) IF
If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0
If q2_used, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) If q2_used, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0)
*/ */
bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) { bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) {
SASSERT(q2_used || sz % 2 == 0); SASSERT(q2_used || sz % 2 == 0);
@ -2038,7 +2038,7 @@ namespace realclosure {
// We should keep q only if it discriminated something. // We should keep q only if it discriminated something.
// That is, // That is,
// If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 // If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0
// If use_q2, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) // If use_q2, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0)
if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) { if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) {
// skip q since it did not reduced the cardinality of the existing sign conditions. // skip q since it did not reduced the cardinality of the existing sign conditions.
continue; continue;

2
src/sat/tactic/sat_tactic.cpp
View file

@ -105,7 +105,7 @@ class sat_tactic : public tactic {
else { else {
// get simplified problem. // get simplified problem.
#if 0 #if 0
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";);
#endif #endif
m_solver.pop_to_base_level(); m_solver.pop_to_base_level();
ref<sat2goal::mc> mc; ref<sat2goal::mc> mc;

2
src/smt/smt_setup.cpp
View file

@ -209,7 +209,7 @@ namespace smt {
static void check_no_arithmetic(static_features const & st, char const * logic) { static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified logic does not support it."); throw default_exception("Benchmark constrains arithmetic, but specified logic does not support it.");
} }
void setup::setup_QF_UF() { void setup::setup_QF_UF() {

26
src/smt/theory_str.cpp
View file

@ -9424,15 +9424,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9451,15 +9451,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9471,15 +9471,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9500,15 +9500,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9762,7 +9762,7 @@ namespace smt {
expr_ref concatlenExpr (mk_strlen(concat), m) ; expr_ref concatlenExpr (mk_strlen(concat), m) ;
bool allLeafResolved = true; bool allLeafResolved = true;
if (! get_arith_value(concatlenExpr, lenValue)) { if (! get_arith_value(concatlenExpr, lenValue)) {
// the length fo concat is unresolved yet // the length of concat is unresolved yet
if (get_len_value(concat, lenValue)) { if (get_len_value(concat, lenValue)) {
// but all leaf nodes have length information // but all leaf nodes have length information
TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;);

2
src/tactic/sls/sls_engine.cpp
View file

@ -492,7 +492,7 @@ lbool sls_engine::search() {
score = m_tracker.get_top_sum(); score = m_tracker.get_top_sum();
// update assertion weights if a weigthing is enabled (sp < 1024) // update assertion weights if a weighting is enabled (sp < 1024)
if (m_paws) if (m_paws)
{ {
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz; i++)

4
src/test/lp/smt_reader.h
View file

@ -193,14 +193,14 @@ namespace lp {
} }
} }
void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
// lp_assert(el.m_head == "0"); // do nothing for the time being // lp_assert(el.m_head == "0"); // do nothing for the time being
} }
void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
lp_assert(el.m_elems.size() == 2); lp_assert(el.m_elems.size() == 2);
set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
adjust_rigth_side(c, el.m_elems[1]); adjust_right_side(c, el.m_elems[1]);
} }