mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

Code simplifications for finite set plugin

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 02:08:04 +00:00
parent d0e9d68746
commit e5d7319670
2 changed files with 4 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/finite_set_decl_plugin.cpp
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#include<sstream>
#include <sstream>
#include "ast/finite_set_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/array_decl_plugin.h"
@ -24,8 +24,7 @@ Revision History:
#include "ast/ast_pp.h"
#include "util/warning.h"
finite_set_decl_plugin::finite_set_decl_plugin():
m_init(false) {
finite_set_decl_plugin::finite_set_decl_plugin() {
m_names.resize(LAST_FINITE_SET_OP, nullptr);
m_names[OP_FINITE_SET_EMPTY] = "set.empty";
m_names[OP_FINITE_SET_SINGLETON] = "set.singleton";
@ -279,11 +278,11 @@ bool finite_set_decl_plugin::is_value(app * e) const {
continue;
}
// Check if it's a union, intersection, or difference
bool is_setop =
is_app_of(a, m_family_id, OP_FINITE_SET_UNION)
|| is_app_of(a, m_family_id, OP_FINITE_SET_INTERSECT)
|| is_app_of(a, m_family_id, OP_FINITE_SET_DIFFERENCE);
// Check if it's a union
if (is_setop) {
// Add arguments to todo list
for (auto arg : *a)
@ -297,8 +296,6 @@ bool finite_set_decl_plugin::is_value(app * e) const {
return false;
continue;
}
// can add also ranges where lo and hi are values.
// If it's none of the above, it's not a value
return false;

2
src/ast/finite_set_decl_plugin.h
View file

@ -56,7 +56,7 @@ enum finite_set_op_kind {
class finite_set_decl_plugin : public decl_plugin {
ptr_vector<polymorphism::psig> m_sigs;
svector<char const*> m_names;
bool m_init = false;
bool m_init{false};
void init();
func_decl * mk_empty(sort* set_sort);