mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

support indexed relations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-26 08:39:56 -07:00
parent 81b1338af6
commit f55e4ccc41
7 changed files with 45 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/special_relations_decl_plugin.cpp
View file

@ -26,7 +26,6 @@ Revision History:
special_relations_decl_plugin::special_relations_decl_plugin():
m_lo("linear-order"),
m_po("partial-order"),
m_po_ao("partial-order-already-ordered"),
m_plo("piecewise-linear-order"),
m_to("tree-order")
{}
@ -47,7 +46,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
symbol name;
switch(k) {
case OP_SPECIAL_RELATION_PO: name = m_po; break;
case OP_SPECIAL_RELATION_PO_AO: name = m_po_ao; break;
case OP_SPECIAL_RELATION_LO: name = m_lo; break;
case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
case OP_SPECIAL_RELATION_TO: name = m_to; break;
@ -58,7 +56,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null) {
op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO));
op_names.push_back(builtin_name(m_po_ao.bare_str(), OP_SPECIAL_RELATION_PO_AO));
op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
@ -68,7 +65,6 @@ void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_name
sr_property special_relations_util::get_property(func_decl* f) const {
switch (f->get_decl_kind()) {
case OP_SPECIAL_RELATION_PO: return sr_po;
case OP_SPECIAL_RELATION_PO_AO: return sr_po; // still partial ordered
case OP_SPECIAL_RELATION_LO: return sr_lo;
case OP_SPECIAL_RELATION_PLO: return sr_plo;
case OP_SPECIAL_RELATION_TO: return sr_to;

4
src/ast/special_relations_decl_plugin.h
View file

@ -26,7 +26,6 @@ Revision History:
enum special_relations_op_kind {
OP_SPECIAL_RELATION_LO,
OP_SPECIAL_RELATION_PO,
OP_SPECIAL_RELATION_PO_AO,
OP_SPECIAL_RELATION_PLO,
OP_SPECIAL_RELATION_TO,
LAST_SPECIAL_RELATIONS_OP
@ -35,7 +34,6 @@ enum special_relations_op_kind {
class special_relations_decl_plugin : public decl_plugin {
symbol m_lo;
symbol m_po;
symbol m_po_ao;
symbol m_plo;
symbol m_to;
public:
@ -80,13 +78,11 @@ public:
bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); }
bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); }
bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); }
bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); }
bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); }
app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); }
app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); }
app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); }
app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); }
app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); }