mirror of
https://github.com/Z3Prover/z3
synced 2026-04-26 13:53:33 +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.
208 lines
7.9 KiB
C++
208 lines
7.9 KiB
C++
/*++
|
|
Copyright (c) 2015 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
theory_special_relations.h
|
|
|
|
Abstract:
|
|
|
|
Special Relations theory plugin.
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2015-9-16
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
#include "ast/special_relations_decl_plugin.h"
|
|
#include "smt/smt_theory.h"
|
|
#include "smt/theory_diff_logic.h"
|
|
#include "util/union_find.h"
|
|
#include "util/rational.h"
|
|
|
|
namespace smt {
|
|
class theory_special_relations : public theory {
|
|
|
|
|
|
struct relation;
|
|
|
|
class atom {
|
|
bool_var m_bvar;
|
|
relation& m_relation;
|
|
bool m_phase;
|
|
theory_var m_v1;
|
|
theory_var m_v2;
|
|
edge_id m_pos;
|
|
edge_id m_neg;
|
|
public:
|
|
atom(bool_var b, relation& r, theory_var v1, theory_var v2):
|
|
m_bvar(b),
|
|
m_relation(r),
|
|
m_phase(true),
|
|
m_v1(v1),
|
|
m_v2(v2)
|
|
{
|
|
r.ensure_var(v1);
|
|
r.ensure_var(v2);
|
|
literal_vector ls;
|
|
ls.push_back(literal(b, false));
|
|
m_pos = r.m_graph.add_edge(v1, v2, s_integer(0), ls); // v1 <= v2
|
|
ls[0] = literal(b, true);
|
|
m_neg = r.m_graph.add_edge(v2, v1, s_integer(-1), ls); // v2 + 1 <= v1
|
|
}
|
|
bool_var var() const { return m_bvar;}
|
|
relation& get_relation() const { return m_relation; }
|
|
bool phase() const { return m_phase; }
|
|
void set_phase(bool b) { m_phase = b; }
|
|
theory_var v1() const { return m_v1; }
|
|
theory_var v2() const { return m_v2; }
|
|
literal explanation() const { return literal(m_bvar, !m_phase); }
|
|
bool enable() {
|
|
edge_id edge = m_phase?m_pos:m_neg;
|
|
return m_relation.m_graph.enable_edge(edge);
|
|
}
|
|
};
|
|
typedef ptr_vector<atom> atoms;
|
|
|
|
struct scope {
|
|
unsigned m_asserted_atoms_lim;
|
|
unsigned m_asserted_qhead_old;
|
|
};
|
|
|
|
struct int_ext : public sidl_ext {
|
|
typedef literal_vector explanation;
|
|
};
|
|
struct graph : public dl_graph<int_ext> {
|
|
bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) {
|
|
// v1 + 1 <= v2
|
|
return enable_edge(add_edge(v1, v2, s_integer(-1), j));
|
|
}
|
|
bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) {
|
|
// v1 <= v2
|
|
return enable_edge(add_edge(v1, v2, s_integer(0), j));
|
|
}
|
|
};
|
|
|
|
typedef union_find<union_find_default_ctx> union_find_t;
|
|
|
|
struct relation {
|
|
ast_manager& m;
|
|
func_decl_ref m_next;
|
|
sr_property m_property;
|
|
func_decl* m_decl;
|
|
atoms m_asserted_atoms; // set of asserted atoms
|
|
unsigned m_asserted_qhead;
|
|
svector<scope> m_scopes;
|
|
graph m_graph;
|
|
union_find_default_ctx m_ufctx;
|
|
union_find_t m_uf;
|
|
literal_vector m_explanation;
|
|
|
|
relation(sr_property p, func_decl* d, ast_manager& m): m(m), m_next(m), m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {}
|
|
|
|
func_decl* decl() { return m_decl; }
|
|
|
|
app_ref next(expr* a, expr* b) { return app_ref(m.mk_app(next(), a, b), m); }
|
|
bool is_next(expr* n) { return is_app(n) && next() == to_app(n)->get_decl(); }
|
|
func_decl* next();
|
|
|
|
void push();
|
|
void pop(unsigned num_scopes);
|
|
void ensure_var(theory_var v);
|
|
bool new_eq_eh(literal l, theory_var v1, theory_var v2);
|
|
void operator()(literal_vector const & ex) {
|
|
m_explanation.append(ex);
|
|
}
|
|
void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {}
|
|
|
|
bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j);
|
|
bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j);
|
|
|
|
std::ostream& display(theory_special_relations const& sr, std::ostream& out) const;
|
|
};
|
|
|
|
typedef u_map<atom*> bool_var2atom;
|
|
|
|
special_relations_util m_util;
|
|
atoms m_atoms;
|
|
unsigned_vector m_atoms_lim;
|
|
ptr_vector<app> m_terms;
|
|
obj_map<func_decl, relation*> m_relations;
|
|
bool_var2atom m_bool_var2atom;
|
|
bool m_can_propagate;
|
|
|
|
|
|
void del_atoms(unsigned old_size);
|
|
lbool final_check(relation& r);
|
|
lbool final_check_po(relation& r);
|
|
lbool final_check_lo(relation& r);
|
|
lbool final_check_plo(relation& r);
|
|
lbool final_check_to(relation& r);
|
|
lbool final_check_tc(relation& r);
|
|
lbool propagate(relation& r);
|
|
lbool enable(atom& a);
|
|
bool extract_equalities(relation& r);
|
|
void set_neg_cycle_conflict(relation& r);
|
|
void set_conflict(relation& r);
|
|
lbool propagate_plo(atom& a);
|
|
lbool propagate_po(atom& a);
|
|
lbool propagate_tc(atom& a);
|
|
theory_var mk_var(expr* e);
|
|
void count_children(graph const& g, unsigned_vector& num_children);
|
|
void ensure_strict(graph& g);
|
|
void ensure_tree(graph& g);
|
|
void assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi);
|
|
expr_ref mk_inj(relation& r, model_generator& m);
|
|
expr_ref mk_class(relation& r, model_generator& m);
|
|
expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi);
|
|
void init_model_lo(relation& r, model_generator& m);
|
|
void init_model_to(relation& r, model_generator& m);
|
|
void init_model_po(relation& r, model_generator& m, bool is_reflexive);
|
|
void init_model_plo(relation& r, model_generator& m);
|
|
bool is_neighbour_edge(graph const& g, edge_id id) const;
|
|
bool is_strict_neighbour_edge(graph const& g, edge_id id) const;
|
|
bool disconnected(graph const& g, dl_var u, dl_var v) const;
|
|
|
|
literal mk_literal(expr* _e);
|
|
enode* ensure_enode(expr* e);
|
|
theory_var mk_var(enode* n) override;
|
|
|
|
void collect_asserted_po_atoms(vector< std::pair<bool_var,bool> >& atoms) const;
|
|
void display_atom(std::ostream & out, atom& a) const;
|
|
void internalize_next(func_decl* f, app * term);
|
|
|
|
public:
|
|
theory_special_relations(context& ctx, ast_manager& m);
|
|
~theory_special_relations() override;
|
|
|
|
theory * mk_fresh(context * new_ctx) override;
|
|
bool internalize_atom(app * atom, bool gate_ctx) override;
|
|
bool internalize_term(app * term) override;
|
|
void new_eq_eh(theory_var v1, theory_var v2) override;
|
|
void new_diseq_eh(theory_var v1, theory_var v2) override {}
|
|
bool use_diseqs() const override { return false; }
|
|
bool build_models() const override { return true; }
|
|
final_check_status final_check_eh(unsigned) override;
|
|
void reset_eh() override;
|
|
void assign_eh(bool_var v, bool is_true) override;
|
|
void init_search_eh() override {}
|
|
void push_scope_eh() override;
|
|
void pop_scope_eh(unsigned num_scopes) override;
|
|
void restart_eh() override {}
|
|
void collect_statistics(::statistics & st) const override;
|
|
model_value_proc * mk_value(enode * n, model_generator & mg) override;
|
|
void init_model(model_generator & m) override;
|
|
bool can_propagate() override { return m_can_propagate; }
|
|
void propagate() override;
|
|
void display(std::ostream & out) const override;
|
|
|
|
void get_specrels(func_decl_set& rels) const;
|
|
|
|
};
|
|
}
|
|
|