mirror of
https://github.com/Z3Prover/z3
synced 2026-01-19 08:43:18 +00:00
62b3668beb
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation. To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
211 lines
8.5 KiB
C++
211 lines
8.5 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 "ast/array_decl_plugin.h"
|
|
#include "model/array_factory.h"
|
|
|
|
namespace smt {
|
|
|
|
class theory_array_base : public theory {
|
|
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_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_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;
|
|
|
|
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); }
|
|
};
|
|
|
|
};
|
|
|
|
|