z3-src 503.3.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

/*++

  Module Name:

    mbp_tg_plugins.h

Abstract:

    Model Based Projection for a theory

Author:

    Hari Govind V K (hgvk94) 2022-07-12

Revision History:


--*/
#pragma once
#include "ast/ast.h"
#include "qe/mbp/mbp_qel_util.h"
#include "qe/mbp/mbp_term_graph.h"
#include "util/obj_hashtable.h"

class mbp_tg_plugin {
public:
    // iterate through all terms in m_tg and apply all theory MBP rules once
    // returns true if any rules were applied
    virtual bool apply() { return false; }
    virtual ~mbp_tg_plugin() = default;
    virtual void use_model() { }
    virtual void get_new_vars(app_ref_vector*&) { }
    virtual family_id get_family_id() const { return null_family_id; }
};