mirror of
https://github.com/Z3Prover/z3
synced 2026-02-19 23:14:40 +00:00
df4052ec69
* Initial plan * Implement finite_sets_decl_plugin with all specified operations Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add tests for finite_sets_decl_plugin Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add set.singleton operator to finite_sets_decl_plugin Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Refactor finite_sets_decl_plugin to use polymorphic signatures and Array sorts Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Rename finite_sets to finite_set everywhere including file names Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Rename set.filter to set.select Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Refactor finite_set_decl_plugin to use polymorphism_util Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Move psig and match method to polymorphism_util Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add MATCH macros and fix is_fully_interp return value Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add is_finite_set helper and parameter count validation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
71 lines
2.4 KiB
C++
71 lines
2.4 KiB
C++
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
reg_decl_plugins
|
|
|
|
Abstract:
|
|
|
|
Goodie for installing all available declarations
|
|
plugins in an ast_manager
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2012-10-24.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "ast/ast.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "ast/array_decl_plugin.h"
|
|
#include "ast/bv_decl_plugin.h"
|
|
#include "ast/datatype_decl_plugin.h"
|
|
#include "ast/recfun_decl_plugin.h"
|
|
#include "ast/dl_decl_plugin.h"
|
|
#include "ast/char_decl_plugin.h"
|
|
#include "ast/seq_decl_plugin.h"
|
|
#include "ast/pb_decl_plugin.h"
|
|
#include "ast/fpa_decl_plugin.h"
|
|
#include "ast/special_relations_decl_plugin.h"
|
|
#include "ast/finite_set_decl_plugin.h"
|
|
|
|
void reg_decl_plugins(ast_manager & m) {
|
|
if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
|
|
m.register_plugin(symbol("arith"), alloc(arith_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("bv")))) {
|
|
m.register_plugin(symbol("bv"), alloc(bv_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("array")))) {
|
|
m.register_plugin(symbol("array"), alloc(array_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) {
|
|
m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) {
|
|
m.register_plugin(symbol("recfun"), alloc(recfun::decl::plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) {
|
|
m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("char")))) {
|
|
m.register_plugin(symbol("char"), alloc(char_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("seq")))) {
|
|
m.register_plugin(symbol("seq"), alloc(seq_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
|
|
m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
|
|
m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) {
|
|
m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin));
|
|
}
|
|
if (!m.get_plugin(m.mk_family_id(symbol("finite_set")))) {
|
|
m.register_plugin(symbol("finite_set"), alloc(finite_set_decl_plugin));
|
|
}
|
|
}
|