mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

remove trc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-17 10:47:46 -07:00
parent 502b29c424
commit 86b98e3477
9 changed files with 28 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_ast.cpp
View file

@ -1059,7 +1059,6 @@ extern "C" {
case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC;
case OP_SPECIAL_RELATION_TRC : return Z3_OP_SPECIAL_RELATION_TRC;
default: UNREACHABLE();
}
}

1
src/api/api_special_relations.cpp
View file

@ -62,5 +62,4 @@ extern "C" {
}
MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC);
MK_DECL(Z3_mk_transitive_reflexive_closure, OP_SPECIAL_RELATION_TRC);
};

11
src/api/z3_api.h
View file

@ -3671,17 +3671,6 @@ extern "C" {
*/
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f);
/**
\brief create transitive reflexive closure of binary relation.
\pre f is a binary relation, such that the two arguments have the same sorts.
The resulting relation f* represents the transitive-reflexive closure of f.
def_API('Z3_mk_transitive_reflexive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL)))
*/
Z3_func_decl Z3_API Z3_mk_transitive_reflexive_closure(Z3_context c, Z3_func_decl f);
/*@}*/
/** @name Quantifiers */

6
src/ast/special_relations_decl_plugin.cpp
View file

@ -26,8 +26,7 @@ special_relations_decl_plugin::special_relations_decl_plugin():
m_po("partial-order"),
m_plo("piecewise-linear-order"),
m_to("tree-order"),
m_tc("transitive-closure"),
m_trc("transitive-reflexive-closure")
m_tc("transitive-closure")
{}
func_decl * special_relations_decl_plugin::mk_func_decl(
@ -56,7 +55,6 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
case OP_SPECIAL_RELATION_TO: name = m_to; break;
case OP_SPECIAL_RELATION_TC: name = m_tc; break;
case OP_SPECIAL_RELATION_TRC: name = m_trc; break;
}
return m_manager->mk_func_decl(name, arity, domain, range, info);
}
@ -68,7 +66,6 @@ void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_name
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));
op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC));
op_names.push_back(builtin_name(m_trc.bare_str(), OP_SPECIAL_RELATION_TRC));
}
}
@ -79,7 +76,6 @@ sr_property special_relations_util::get_property(func_decl* f) const {
case OP_SPECIAL_RELATION_PLO: return sr_plo;
case OP_SPECIAL_RELATION_TO: return sr_to;
case OP_SPECIAL_RELATION_TC: return sr_tc;
case OP_SPECIAL_RELATION_TRC: return sr_trc;
default:
UNREACHABLE();
return sr_po;

5
src/ast/special_relations_decl_plugin.h
View file

@ -29,7 +29,6 @@ enum special_relations_op_kind {
OP_SPECIAL_RELATION_PLO,
OP_SPECIAL_RELATION_TO,
OP_SPECIAL_RELATION_TC,
OP_SPECIAL_RELATION_TRC,
LAST_SPECIAL_RELATIONS_OP
};
@ -39,7 +38,6 @@ class special_relations_decl_plugin : public decl_plugin {
symbol m_plo;
symbol m_to;
symbol m_tc;
symbol m_trc;
public:
special_relations_decl_plugin();
@ -70,7 +68,6 @@ enum sr_property {
sr_plo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // piecewise linear order
sr_lo = 0x01 | 0x02 | 0x04 | 0x20, // linear order
sr_tc = 0x40, // transitive closure of relation
sr_trc = 0x42 // transitive reflexive closure of relation
};
class special_relations_util {
@ -93,14 +90,12 @@ public:
func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); }
func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); }
func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); }
func_decl* mk_trc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TRC); }
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_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); }
bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); }
bool is_trc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TRC); }
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); }

27
src/smt/theory_array_bapa.cpp
View file

@ -1,4 +1,19 @@
/**
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
theory_array_bapa.cpp
Abstract:
Saturation procedure for BAPA predicates.
Assume there is a predicate
Size(S, n) for S : Array(T, Bool) and n : Int
The predicate is true if S is a set of size n.
Size(S, n), Size(T, m)
S, T are intersecting. n != m or S != T
@ -54,6 +69,12 @@ Finite domains:
Model construction for infinite domains when all Size(S, m) are negative for S.
Author:
Nikolaj Bjorner 2019-04-13
Revision History:
*/
#include "ast/ast_util.h"
@ -470,8 +491,12 @@ namespace smt {
};
theory_array_bapa::theory_array_bapa(theory_array_full& th) { m_imp = alloc(imp, th); }
theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); }
void theory_array_bapa::internalize_size(app* term) { m_imp->internalize_size(term); }
final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); }
void theory_array_bapa::init_model() { m_imp->init_model(); }
}

2
src/smt/theory_array_bapa.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2019 Microsoft Corporation
Module Name:

44
src/smt/theory_special_relations.cpp
View file

@ -322,9 +322,6 @@ namespace smt {
// we need reachability in the R graph not R* graph
theory_var r1 = get_representative(a.v1());
theory_var r2 = get_representative(a.v2());
if (r.m_property == sr_trc && r1 == r2) {
continue;
}
if (r_graph.can_reach(r1, r2)) {
TRACE("special_relations",
tout << a.v1() << ": " << mk_pp(arg1, m) << " -> "
@ -397,13 +394,6 @@ namespace smt {
return final_check_po(r);
}
lbool theory_special_relations::final_check_trc(relation& r) {
//
// reflexivity is enforced from propagation.
// enforce transitivity.
//
return final_check_tc(r);
}
lbool theory_special_relations::final_check_to(relation& r) {
uint_set visited, target;
@ -510,9 +500,6 @@ namespace smt {
case sr_tc:
res = final_check_tc(r);
break;
case sr_trc:
res = final_check_trc(r);
break;
default:
UNREACHABLE();
res = l_undef;
@ -525,7 +512,6 @@ namespace smt {
bool theory_special_relations::extract_equalities(relation& r) {
switch (r.m_property) {
case sr_tc:
case sr_trc:
return false;
default:
break;
@ -593,30 +579,6 @@ namespace smt {
return res;
}
/**
\brief ensure that reflexivity is enforce for Transitive Reflexive closures
!TRC(R)xy => x != y
*/
lbool theory_special_relations::propagate_trc(atom& a) {
lbool res = l_true;
if (a.phase()) {
VERIFY(a.enable());
relation& r = a.get_relation();
r.m_uf.merge(a.v1(), a.v2());
}
else {
literal lit(a.var(), true);
context& ctx = get_context();
expr* arg1 = get_expr(a.v1());
expr* arg2 = get_expr(a.v2());
literal consequent = ~mk_eq(arg1, arg2, false);
justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), 1, &lit, consequent));
ctx.assign(consequent, j);
res = l_false;
}
return res;
}
lbool theory_special_relations::propagate_tc(atom& a) {
if (a.phase()) {
VERIFY(a.enable());
@ -670,9 +632,6 @@ namespace smt {
res = propagate_po(a);
break;
case sr_tc:
res = propagate_trc(a);
break;
case sr_trc:
res = propagate_tc(a);
break;
default:
@ -1165,9 +1124,6 @@ namespace smt {
case sr_tc:
init_model_po(*kv.m_value, m, true);
break;
case sr_trc:
init_model_po(*kv.m_value, m, true);
break;
default:
// other 28 combinations of 0x1F
NOT_IMPLEMENTED_YET();

2
src/smt/theory_special_relations.h
View file

@ -144,7 +144,6 @@ namespace smt {
lbool final_check_plo(relation& r);
lbool final_check_to(relation& r);
lbool final_check_tc(relation& r);
lbool final_check_trc(relation& r);
lbool propagate(relation& r);
lbool enable(atom& a);
bool extract_equalities(relation& r);
@ -153,7 +152,6 @@ namespace smt {
lbool propagate_plo(atom& a);
lbool propagate_po(atom& a);
lbool propagate_tc(atom& a);
lbool propagate_trc(atom& a);
theory_var mk_var(expr* e);
void count_children(graph const& g, unsigned_vector& num_children);
void ensure_strict(graph& g);