mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
get_model_ptr to align naming
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2243bd3c4a
commit
82ca71e87f
|
@ -1660,7 +1660,7 @@ namespace pdr {
|
|||
bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
|
||||
|
||||
pred_transformer& pt = n.pt();
|
||||
model_ref M = n.model_ptr();
|
||||
model_ref M = n.get_model_ptr();
|
||||
datalog::rule const& r = pt.find_rule(*M);
|
||||
expr* T = pt.get_transition(r);
|
||||
expr* phi = n.state();
|
||||
|
|
|
@ -195,7 +195,7 @@ namespace pdr {
|
|||
ptr_vector<model_node> const& children() { return m_children; }
|
||||
pred_transformer& pt() const { return m_pt; }
|
||||
model_node* parent() const { return m_parent; }
|
||||
model* model_ptr() const { return m_model.get(); }
|
||||
model* get_model_ptr() const { return m_model.get(); }
|
||||
model const& get_model() const { return *m_model; }
|
||||
unsigned index() const;
|
||||
|
||||
|
|
|
@ -418,7 +418,7 @@ namespace pdr {
|
|||
// nodes from leaves that are repeated
|
||||
// inside the search tree don't have models.
|
||||
//
|
||||
if (!(&node.get_model())) {
|
||||
if (!node.get_model_ptr()) {
|
||||
return;
|
||||
}
|
||||
m_current_rule = &pt.find_rule(node.get_model());
|
||||
|
|
Loading…
Reference in a new issue