mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 03:25:43 +00:00
Remove unused defined_names and simplify contains return
- Remove unused 'defined_names dn(m)' variable in smt_model_checker.cpp, a leftover from the 'remove side definitions' refactoring - Remove corresponding unused #include of defined_names.h from smt_model_checker.h - Simplify redundant if/return pattern in fingerprint_set::contains to a direct return statement Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
parent
a0a3047e36
commit
bc4e26233d
3 changed files with 2 additions and 6 deletions
|
|
@ -100,13 +100,11 @@ namespace smt {
|
|||
|
||||
bool fingerprint_set::contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
|
||||
fingerprint * d = mk_dummy(data, data_hash, num_args, args);
|
||||
if (m_set.contains(d))
|
||||
if (m_set.contains(d))
|
||||
return true;
|
||||
for (unsigned i = 0; i < num_args; ++i)
|
||||
d->m_args[i] = d->m_args[i]->get_root();
|
||||
if (m_set.contains(d))
|
||||
return true;
|
||||
return false;
|
||||
return m_set.contains(d);
|
||||
}
|
||||
|
||||
void fingerprint_set::reset() {
|
||||
|
|
|
|||
|
|
@ -258,7 +258,6 @@ namespace smt {
|
|||
svector<symbol> names;
|
||||
for (unsigned i = 0; i < f->get_arity(); ++i)
|
||||
names.push_back(symbol(i));
|
||||
defined_names dn(m);
|
||||
body = replace_value_from_ctx(body);
|
||||
body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body);
|
||||
sk_term = body;
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ Revision History:
|
|||
#include "util/obj_hashtable.h"
|
||||
#include "ast/ast.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/normal_forms/defined_names.h"
|
||||
#include "params/qi_params.h"
|
||||
#include "params/smt_params.h"
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue