mirror of
https://github.com/Z3Prover/z3
synced 2026-05-19 00:19:31 +00:00
daefb4ddfd
* Initial plan * Fix unused parameter warnings in empty override functions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Omit parameter names in empty override functions instead of casting to void 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>
61 lines
1.2 KiB
C++
61 lines
1.2 KiB
C++
/*++
|
|
Copyright (c) 2023 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
euf_arith_plugin.h
|
|
|
|
Abstract:
|
|
|
|
plugin structure for arithmetic
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2023-11-11
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "ast/euf/euf_plugin.h"
|
|
#include "ast/euf/euf_ac_plugin.h"
|
|
|
|
namespace euf {
|
|
|
|
class egraph;
|
|
|
|
class arith_plugin : public plugin {
|
|
enum class undo_t { undo_add, undo_mul };
|
|
arith_util a;
|
|
svector<undo_t> m_undo;
|
|
ac_plugin m_add, m_mul;
|
|
|
|
public:
|
|
arith_plugin(egraph& g);
|
|
|
|
theory_id get_id() const override { return a.get_family_id(); }
|
|
|
|
void register_node(enode* n) override;
|
|
|
|
void merge_eh(enode* n1, enode* n2) override;
|
|
|
|
void diseq_eh(enode*) override { }
|
|
|
|
void undo() override;
|
|
|
|
void push_scope_eh() override {
|
|
m_add.push_scope_eh();
|
|
m_mul.push_scope_eh();
|
|
}
|
|
|
|
void propagate() override;
|
|
|
|
std::ostream& display(std::ostream& out) const override;
|
|
|
|
void collect_statistics(statistics& st) const override {
|
|
m_add.collect_statistics(st);
|
|
m_mul.collect_statistics(st);
|
|
}
|
|
|
|
};
|
|
}
|