mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

remove stale assertions due to lambda #2446

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-30 14:32:06 +08:00
parent 902c683b92
commit 74631265b9
3 changed files with 16 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

17
scripts/update_api.py
View file

@ -54,6 +54,7 @@ PRINT_MODE = 10
ERROR_CODE = 11
DOUBLE = 12
FLOAT = 13
CHAR = 14
FIRST_OBJ_ID = 100
@ -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
@ -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:
@ -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:

1
src/qe/qsat.cpp
View file

@ -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());

17
src/smt/smt_model_finder.cpp
View file

@ -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))
@ -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);
@ -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() {
@ -2200,7 +2194,7 @@ namespace smt {
}
else {
SASSERT(is_quantifier(curr)); // no nested quantifiers
UNREACHABLE();
//UNREACHABLE();
}
}
}
@ -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.
}
}
}
@ -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());