mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-02 13:02:00 -07:00
parent 54a75d6a91
commit 4b22434739
1 changed files with 20 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/sat/smt/sat_th.h
View file

@ -29,6 +29,12 @@ namespace euf {
virtual ~th_internalizer() {} virtual ~th_internalizer() {}
virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0; virtual sat::literal internalize(expr* e, bool sign, bool root, bool redundant) = 0;
/**
\brief Apply (interpreted) sort constraints on the given enode.
*/
virtual void apply_sort_cnstr(enode * n, sort * s) {}
}; };
class th_decompile { class th_decompile {
@ -63,13 +69,22 @@ namespace euf {
class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_internalizer { class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_internalizer {
protected: protected:
ast_manager & m; ast_manager & m;
euf::theory_id m_id; theory_id m_id;
public: public:
th_solver(ast_manager& m, euf::theory_id id): m(m), m_id(id) {} th_solver(ast_manager& m, euf::theory_id id): m(m), m_id(id) {}
unsigned get_id() const override { return m_id; }
virtual th_solver* fresh(sat::solver* s, euf::solver& ctx) = 0; virtual th_solver* fresh(sat::solver* s, euf::solver& ctx) = 0;
virtual void new_eq_eh(euf::th_eq const& eq) {} virtual void new_eq_eh(euf::th_eq const& eq) {}
/**
\brief Parametric theories (e.g. Arrays) should implement this method.
*/
virtual bool is_shared(theory_var v) const { return false; }
}; };
class th_euf_solver : public th_solver { class th_euf_solver : public th_solver {
@ -89,13 +104,11 @@ namespace euf {
return v; return v;
} }
unsigned get_num_vars() const { return m_var2enode.size();}
enode* get_enode(theory_var v) const { return m_var2enode[v]; } enode* get_enode(theory_var v) const { return m_var2enode[v]; }
expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); }
euf::theory_var get_th_var(expr* e) const; theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
theory_var get_th_var(expr* e) const;
euf::theory_var get_th_var(euf::enode* n) const {
return n->get_th_var(get_id());
}
bool is_attached_to_var(enode* n) const { bool is_attached_to_var(enode* n) const {
theory_var v = n->get_th_var(get_id()); theory_var v = n->get_th_var(get_id());