mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
200 lines
7.3 KiB
C++
200 lines
7.3 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:
|
|
|
|
--*/
|
|
|
|
#ifndef THEORY_SPECIAL_RELATIONS_H_
|
|
#define THEORY_SPECIAL_RELATIONS_H_
|
|
|
|
#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 {
|
|
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): m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {}
|
|
|
|
func_decl* decl() { return m_decl; }
|
|
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;
|
|
obj_map<func_decl, relation*> m_relations;
|
|
bool_var2atom m_bool_var2atom;
|
|
|
|
|
|
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 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);
|
|
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);
|
|
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);
|
|
|
|
void collect_asserted_po_atoms(vector< std::pair<bool_var,bool> >& atoms) const;
|
|
void display_atom(std::ostream & out, atom& a) const;
|
|
|
|
public:
|
|
theory_special_relations(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 { UNREACHABLE(); return false; }
|
|
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() 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 false; }
|
|
void propagate() override {}
|
|
void display(std::ostream & out) const override;
|
|
|
|
};
|
|
}
|
|
|
|
#endif
|