mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

simplify model_core.h: remove unused typedef, fix trailing whitespace, simplify get_some_const_interp

Browse source 
- Remove unused i_interp typedef (was never referenced outside of its definition)
- Remove trailing whitespace on m_const_decls, m_func_decls lines
- Simplify get_some_const_interp body using ternary operator

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-06-02 05:55:22 +00:00 • committed by GitHub
parent 78a7b4d3a6
commit 156bf81349
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/model/model_core.h
View file

@ -25,7 +25,6 @@ Revision History:
class model_core {
protected:
typedef std::pair<unsigned, expr*> i_expr;
typedef std::pair<unsigned, func_interp*> i_interp;
typedef obj_map<func_decl, i_expr> decl2expr;
typedef obj_map<func_decl, func_interp*> decl2finterp;
ast_manager & m;
@ -33,9 +32,9 @@ protected:
decl2expr m_interp; //!< interpretation for uninterpreted constants
decl2finterp m_finterp; //!< interpretation for uninterpreted functions
ptr_vector<func_decl> m_decls; //!< domain of m_interp
ptr_vector<func_decl> m_const_decls;
ptr_vector<func_decl> m_func_decls;
ptr_vector<func_decl> m_const_decls;
ptr_vector<func_decl> m_func_decls;
public:
model_core(ast_manager & m):m(m), m_ref_count(0) { }
virtual ~model_core();
@ -78,10 +77,9 @@ public:
virtual expr * get_fresh_value(sort * s) = 0;
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
expr * get_some_const_interp(func_decl * d) {
expr * r = get_const_interp(d);
if (r) return r;
return get_some_value(d->get_range());
expr * get_some_const_interp(func_decl * d) {
expr * r = get_const_interp(d);
return r ? r : get_some_value(d->get_range());
}
//
// Reference counting