mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
218 lines
8.9 KiB
C++
218 lines
8.9 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
theory_array_base.h
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2008-06-02.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "smt/smt_theory.h"
|
|
#include "smt/theory_array_bapa.h"
|
|
#include "ast/array_decl_plugin.h"
|
|
#include "model/array_factory.h"
|
|
|
|
namespace smt {
|
|
|
|
class theory_array_base : public theory {
|
|
friend class theory_array_bapa;
|
|
protected:
|
|
bool m_found_unsupported_op;
|
|
unsigned m_array_weak_head;
|
|
svector<theory_var> m_array_weak_trail;
|
|
bool has_propagate_up_trail() const { return m_array_weak_head < m_array_weak_trail.size(); }
|
|
void add_weak_var(theory_var v);
|
|
virtual void set_prop_upward(theory_var v) {}
|
|
void found_unsupported_op(expr * n);
|
|
void found_unsupported_op(enode* n) { found_unsupported_op(n->get_expr()); }
|
|
void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_expr()); }
|
|
|
|
bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); }
|
|
bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); }
|
|
bool is_select(app const* n) const { return n->is_app_of(get_id(), OP_SELECT); }
|
|
bool is_default(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_DEFAULT); }
|
|
bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); }
|
|
bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
|
|
bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
|
|
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
|
|
bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
|
|
bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); }
|
|
bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); }
|
|
|
|
bool is_store(enode const * n) const { return is_store(n->get_expr()); }
|
|
bool is_map(enode const* n) const { return is_map(n->get_expr()); }
|
|
bool is_select(enode const* n) const { return is_select(n->get_expr()); }
|
|
bool is_const(enode const* n) const { return is_const(n->get_expr()); }
|
|
bool is_as_array(enode const * n) const { return is_as_array(n->get_expr()); }
|
|
bool is_default(enode const* n) const { return is_default(n->get_expr()); }
|
|
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_expr()); }
|
|
bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_expr()); }
|
|
bool is_set_carde(enode const* n) const { return is_set_card(n->get_expr()); }
|
|
bool is_select_arg(enode* r);
|
|
|
|
app * mk_select(unsigned num_args, expr * const * args);
|
|
app * mk_select_reduce(unsigned num_args, expr * * args);
|
|
app * mk_select(expr_ref_vector const& args) { return mk_select(args.size(), args.data()); }
|
|
app * mk_store(unsigned num_args, expr * const * args);
|
|
app * mk_default(expr* a);
|
|
|
|
|
|
unsigned get_dimension(sort* s) const;
|
|
|
|
ptr_vector<enode> m_axiom1_todo;
|
|
enode_pair_vector m_axiom2_todo;
|
|
enode_pair_vector m_extensionality_todo;
|
|
enode_pair_vector m_congruent_todo;
|
|
scoped_ptr<theory_array_bapa> m_bapa;
|
|
|
|
void assert_axiom(unsigned num_lits, literal * lits);
|
|
void assert_axiom(literal l1, literal l2);
|
|
void assert_axiom(literal l);
|
|
void assert_store_axiom1_core(enode * n);
|
|
void assert_store_axiom2_core(enode * store, enode * select);
|
|
void assert_store_axiom1(enode * n) { m_axiom1_todo.push_back(n); }
|
|
bool assert_store_axiom2(enode * store, enode * select);
|
|
|
|
void assert_extensionality_core(enode * a1, enode * a2);
|
|
bool assert_extensionality(enode * a1, enode * a2);
|
|
|
|
expr_ref instantiate_lambda(app* e);
|
|
void assert_congruent_core(enode * a1, enode * a2);
|
|
void assert_congruent(enode * a1, enode * a2);
|
|
|
|
// --------------------------------------------------
|
|
// Array sort -> extensionality skolems
|
|
//
|
|
// --------------------------------------------------
|
|
ptr_vector<sort> m_sorts_trail;
|
|
obj_map<sort, func_decl_ref_vector*> m_sort2skolem;
|
|
|
|
func_decl_ref_vector * register_sort(sort * s_array);
|
|
|
|
// --------------------------------------------------
|
|
// array_value table
|
|
//
|
|
// Use select(A, i) nodes to represent an assignment for A.
|
|
// This structure is used to minimize the number of times the
|
|
// extensionality axiom is applied.
|
|
//
|
|
// --------------------------------------------------
|
|
struct value_chasher {
|
|
unsigned operator()(enode const * n, unsigned idx) const {
|
|
return n->get_arg(idx+1)->get_root()->hash();
|
|
}
|
|
};
|
|
struct value_khasher { unsigned operator()(enode * n) const { return 17; } };
|
|
struct value_hash_proc {
|
|
unsigned operator()(enode * n) const {
|
|
return get_composite_hash<enode *, value_khasher, value_chasher>(n, n->get_num_args() - 1);
|
|
}
|
|
};
|
|
struct value_eq_proc { bool operator()(enode * n1, enode * n2) const; };
|
|
typedef ptr_hashtable<enode, value_hash_proc, value_eq_proc> array_value;
|
|
|
|
array_value m_array_value;
|
|
bool already_diseq(enode * v1, enode * v2);
|
|
|
|
// --------------------------------------------------
|
|
// Backtracking
|
|
//
|
|
//
|
|
// --------------------------------------------------
|
|
struct scope {
|
|
unsigned m_sorts_trail_lim;
|
|
scope(unsigned l):m_sorts_trail_lim(l) {}
|
|
};
|
|
svector<scope> m_scopes;
|
|
void restore_sorts(unsigned old_size);
|
|
|
|
// --------------------------------------------------
|
|
// Interface
|
|
//
|
|
//
|
|
// --------------------------------------------------
|
|
bool is_shared(theory_var v) const override;
|
|
bool is_beta_redex(enode* p, enode* n) const override;
|
|
void collect_shared_vars(sbuffer<theory_var> & result);
|
|
unsigned mk_interface_eqs();
|
|
|
|
bool can_propagate() override;
|
|
void propagate() override;
|
|
void push_scope_eh() override;
|
|
void pop_scope_eh(unsigned num_scopes) override;
|
|
void reset_eh() override;
|
|
|
|
void reset_queues();
|
|
// -----------------------------------
|
|
//
|
|
// Model generation
|
|
//
|
|
// -----------------------------------
|
|
|
|
|
|
// I need a set of select enodes where select(A,i) = select(B,j) if i->get_root() == j->get_root()
|
|
struct sel_khasher {
|
|
unsigned operator()(enode const * n) const { return 0; }
|
|
};
|
|
|
|
struct sel_chasher {
|
|
unsigned operator()(enode const * n, unsigned idx) const {
|
|
return n->get_arg(idx+1)->get_root()->hash();
|
|
}
|
|
};
|
|
|
|
struct sel_hash {
|
|
unsigned operator()(enode * n) const;
|
|
};
|
|
|
|
struct sel_eq {
|
|
bool operator()(enode * n1, enode * n2) const;
|
|
};
|
|
|
|
typedef ptr_hashtable<enode, sel_hash, sel_eq> select_set;
|
|
|
|
array_factory * m_factory;
|
|
ptr_vector<enode> m_defaults; // temporary field for model construction
|
|
ptr_vector<void> m_else_values; // tagged pointer: expr or extra_fresh_value
|
|
svector<int> m_parents; // temporary field for model construction
|
|
obj_map<enode, select_set*> m_selects; // mapping from array -> relevant selects
|
|
ptr_vector<enode> m_selects_domain;
|
|
ptr_vector<select_set> m_selects_range;
|
|
bool m_use_unspecified_default; // temporary field for model construction
|
|
|
|
theory_var mg_find(theory_var v);
|
|
void mg_merge(theory_var n, theory_var m);
|
|
|
|
void set_default(theory_var v, enode* n);
|
|
enode* get_default(theory_var v);
|
|
|
|
void init_model(model_generator & m) override;
|
|
bool is_unspecified_default_ok() const;
|
|
void collect_defaults();
|
|
void collect_selects();
|
|
void propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo);
|
|
void propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo);
|
|
void propagate_selects();
|
|
select_set * get_select_set(enode * n);
|
|
void finalize_model(model_generator & m) override;
|
|
model_value_proc * mk_value(enode * n, model_generator & m) override;
|
|
bool include_func_interp(func_decl* f) override;
|
|
public:
|
|
theory_array_base(context& ctx);
|
|
~theory_array_base() override { restore_sorts(0); }
|
|
};
|
|
|
|
};
|
|
|
|
|