Skip to content

Commit

Permalink
remove stale assertions due to lambda #2446
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jul 30, 2019
1 parent 902c683 commit 7463126
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 19 deletions.
17 changes: 9 additions & 8 deletions scripts/update_api.py
View file
Expand Up @@ -54,6 +54,7 @@
ERROR_CODE = 11
DOUBLE = 12
FLOAT = 13
CHAR = 14

FIRST_OBJ_ID = 100

Expand All @@ -62,33 +63,33 @@ def is_obj(ty):

Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double',
FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'bool', SYMBOL : 'Z3_symbol',
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code'
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char'
}

Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong',
UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float',
STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol',
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint'
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char'
}

# Mapping to .NET types
Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char' }

# Mapping to Java types
Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'}
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' }

Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar'}

# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char' }

next_type_id = FIRST_OBJ_ID

Expand Down Expand Up @@ -751,7 +752,7 @@ def mk_java(java_dir, package_name):

Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number',
FLOAT : 'number', STRING : 'string', STRING_PTR : 'array',
BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number' }
BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number', CHAR : 'number' }

def type2napi(t):
try:
Expand All @@ -761,7 +762,7 @@ def type2napi(t):

Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'array',
BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32' }
BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32', CHAR : 'char' }

def type2napibuilder(t):
try:
Expand Down
1 change: 1 addition & 0 deletions src/qe/qsat.cpp
View file
Expand Up @@ -1278,6 +1278,7 @@ namespace qe {
in->reset();
in->inc_depth();
result.push_back(in.get());
std::cout << in->models_enabled() << " " << m_model_save.get() << "\n";
if (in->models_enabled()) {
model_converter_ref mc;
mc = model2model_converter(m_model_save.get());
Expand Down
17 changes: 6 additions & 11 deletions src/smt/smt_model_finder.cpp
View file
Expand Up @@ -522,7 +522,7 @@ namespace smt {
}

instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const {
SASSERT(!has_quantifiers(q->get_expr()));
//SASSERT(!has_quantifiers(q->get_expr()));
ast_idx_pair k(q, i);
node * r = nullptr;
if (m_uvars.find(k, r))
Expand Down Expand Up @@ -1735,12 +1735,6 @@ namespace smt {
m_the_one(nullptr),
m_uvar_inst_sets(nullptr) {
if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) {
static bool displayed_flat_msg = false;
if (!displayed_flat_msg) {
// [Leo]: This warning message is not useful.
// warning_msg("For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.");
displayed_flat_msg = true;
}
proof_ref pr(m);
expr_ref new_q(m);
pull_quant pull(m);
Expand All @@ -1753,7 +1747,7 @@ namespace smt {
}
CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()),
tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";);
SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr()));
// SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr()));
}

~quantifier_info() {
Expand Down Expand Up @@ -2200,7 +2194,7 @@ namespace smt {
}
else {
SASSERT(is_quantifier(curr)); // no nested quantifiers
UNREACHABLE();
//UNREACHABLE();
}
}
}
Expand Down Expand Up @@ -2332,7 +2326,8 @@ namespace smt {
}
else {
SASSERT(is_quantifier(curr));
UNREACHABLE(); // can't happen, the quantifier is supposed to be flat.
SASSERT(is_lambda(curr));
//UNREACHABLE(); // can't happen, the quantifier is supposed to be flat.
}
}
}
Expand Down Expand Up @@ -2385,7 +2380,7 @@ namespace smt {
quantifier * q = d->get_flat_q();
if (m.is_lambda_def(q)) return;
expr * e = q->get_expr();
SASSERT(!has_quantifiers(e));
//SASSERT(!has_quantifiers(e));
reset_cache();
SASSERT(m_ttodo.empty());
SASSERT(m_ftodo.empty());
Expand Down

0 comments on commit 7463126

Please sign in to comment.