mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-04-01 12:10:17 -07:00
parent ebc4b93d52 b18864d4cc
commit a9c20c96ee
39 changed files with 2264 additions and 251 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/CMakeLists.txt
View file

@ -61,6 +61,7 @@ z3_add_component(api
api_rcf.cpp
api_seq.cpp
api_solver.cpp
api_special_relations.cpp
api_stats.cpp
api_tactic.cpp
z3_replayer.cpp

11
src/api/api_ast.cpp
View file

@ -1052,6 +1052,17 @@ extern "C" {
}
}
if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO;
case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO;
case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO;
case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO;
default: UNREACHABLE();
}
}
if (mk_c(c)->get_bv_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_BV_NUM: return Z3_OP_BNUM;

1
src/api/api_context.cpp
View file

@ -101,6 +101,7 @@ namespace api {
m_datalog_fid = m().mk_family_id("datalog_relation");
m_fpa_fid = m().mk_family_id("fpa");
m_seq_fid = m().mk_family_id("seq");
m_special_relations_fid = m().mk_family_id("special_relations");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
install_tactics(*this);

3
src/api/api_context.h
View file

@ -30,6 +30,7 @@ Revision History:
#include "ast/dl_decl_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#include "smt/smt_kernel.h"
#include "smt/params/smt_params.h"
#include "util/event_handler.h"
@ -106,6 +107,7 @@ namespace api {
family_id m_pb_fid;
family_id m_fpa_fid;
family_id m_seq_fid;
family_id m_special_relations_fid;
datatype_decl_plugin * m_dt_plugin;
std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world.
@ -162,6 +164,7 @@ namespace api {
family_id get_fpa_fid() const { return m_fpa_fid; }
family_id get_seq_fid() const { return m_seq_fid; }
datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
family_id get_special_relations_fid() const { return m_special_relations_fid; }
Z3_error_code get_error_code() const { return m_error_code; }
void reset_error_code();

65
src/api/api_datatype.cpp
View file

@ -160,69 +160,40 @@ extern "C" {
LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), head(m), tail(m);
datatype_util& dt_util = mk_c(c)->dtutil();
mk_c(c)->reset_last_result();
datatype_util data_util(m);
accessor_decl* head_tail[2] = {
mk_accessor_decl(m, symbol("head"), type_ref(to_sort(elem_sort))),
mk_accessor_decl(m, symbol("tail"), type_ref(0))
};
constructor_decl* constrs[2] = {
mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr),
// Leo: SMT 2.0 document uses 'insert' instead of cons
mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail)
};
sort_ref_vector sorts(m);
{
datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 2, constrs);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, nullptr, sorts);
del_datatype_decl(decl);
if (!is_ok) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
}
sort_ref s = dt_util.mk_list_datatype(to_sort(elem_sort), to_symbol(name), cons, is_cons, head, tail, nil, is_nil);
if (!s) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
}
sort * s = sorts.get(0);
mk_c(c)->save_multiple_ast_trail(s);
ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
SASSERT(cnstrs.size() == 2);
func_decl* f;
if (nil_decl) {
f = cnstrs[0];
mk_c(c)->save_multiple_ast_trail(f);
*nil_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(nil);
*nil_decl = of_func_decl(nil);
}
if (is_nil_decl) {
f = data_util.get_constructor_is(cnstrs[0]);
mk_c(c)->save_multiple_ast_trail(f);
*is_nil_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(is_nil);
*is_nil_decl = of_func_decl(is_nil);
}
if (cons_decl) {
f = cnstrs[1];
mk_c(c)->save_multiple_ast_trail(f);
*cons_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(cons);
*cons_decl = of_func_decl(cons);
}
if (is_cons_decl) {
f = data_util.get_constructor_is(cnstrs[1]);
mk_c(c)->save_multiple_ast_trail(f);
*is_cons_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(is_cons);
*is_cons_decl = of_func_decl(is_cons);
}
if (head_decl) {
ptr_vector<func_decl> const& acc = *data_util.get_constructor_accessors(cnstrs[1]);
SASSERT(acc.size() == 2);
f = (acc)[0];
mk_c(c)->save_multiple_ast_trail(f);
*head_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(head);
*head_decl = of_func_decl(head);
}
if (tail_decl) {
ptr_vector<func_decl> const& acc = *data_util.get_constructor_accessors(cnstrs[1]);
SASSERT(acc.size() == 2);
f = (acc)[1];
mk_c(c)->save_multiple_ast_trail(f);
*tail_decl = of_func_decl(f);
mk_c(c)->save_multiple_ast_trail(tail);
*tail_decl = of_func_decl(tail);
}
RETURN_Z3_mk_list_sort(of_sort(s));
Z3_CATCH_RETURN(nullptr);

88
src/api/api_special_relations.cpp Normal file
View file

@ -0,0 +1,88 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
api_special_relations.cpp
Abstract:
Basic API for Special relations
Author:
Nikolaj Bjorner (nbjorner) 2019-03-25
Ashutosh Gupta 2016
Revision History:
--*/
#include <iostream>
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/ast_pp.h"
#include "ast/special_relations_decl_plugin.h"
extern "C" {
#if 0
bool Z3_API Z3_is_sr_lo(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_sr_lo(c, s);
RESET_ERROR_CODE();
RETURN_Z3(mk_c(c)->sr_util().is_lo( to_expr(s) ));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_is_sr_po(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_sr_po(c, s);
RESET_ERROR_CODE();
RETURN_Z3(mk_c(c)->sr_util().is_po( to_expr(s) ));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_is_sr_po_ao(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_sr_po_ao(c, s);
RESET_ERROR_CODE();
RETURN_Z3(mk_c(c)->sr_util().is_po_ao( to_expr(s) ));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_is_sr_plo(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_sr_plo(c, s);
RESET_ERROR_CODE();
RETURN_Z3(mk_c(c)->sr_util().is_plo( to_expr(s) ));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_is_sr_to(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_sr_to(c, s);
RESET_ERROR_CODE();
RETURN_Z3(mk_c(c)->sr_util().is_to( to_expr(s) ));
Z3_CATCH_RETURN(false);
}
#endif
#define MK_TERN(NAME, FID) \
Z3_ast Z3_API NAME(Z3_context c, unsigned index, Z3_ast a, Z3_ast b) { \
LOG_ ##NAME(c, index, a, b); \
Z3_TRY; \
expr* args[2] = { to_expr(a), to_expr(b) }; \
parameter p(index); \
ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_special_relations_fid(), FID, 1, &p, 2, args); \
mk_c(c)->save_ast_trail(a); \
RETURN_Z3(of_ast(a)); \
Z3_CATCH_RETURN(nullptr); \
}
MK_TERN(Z3_mk_linear_order, OP_SPECIAL_RELATION_LO);
MK_TERN(Z3_mk_partial_order, OP_SPECIAL_RELATION_PO);
MK_TERN(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO);
MK_TERN(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO);
};

21
src/api/c++/z3++.h
View file

@ -1707,6 +1707,27 @@ namespace z3 {
*/
inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
typedef Z3_ast Z3_apply_order(Z3_context, unsigned, Z3_ast, Z3_ast);
inline expr apply_order(Z3_apply_order app, unsigned index, expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r = app(a.ctx(), index, a, b);
a.check_error();
return expr(a.ctx(), r);
}
inline expr linear_order(unsigned index, expr const& a, expr const& b) {
return apply_order(Z3_mk_linear_order, index, a, b);
}
inline expr partial_order(unsigned index, expr const& a, expr const& b) {
return apply_order(Z3_mk_partial_order, index, a, b);
}
inline expr piecewise_linear_order(unsigned index, expr const& a, expr const& b) {
return apply_order(Z3_mk_piecewise_linear_order, index, a, b);
}
inline expr tree_order(unsigned index, expr const& a, expr const& b) {
return apply_order(Z3_mk_tree_order, index, a, b);
}
template<typename T> class cast_ast;
template<> class cast_ast<ast> {

3
src/api/python/z3/z3.py
View file

@ -10353,3 +10353,6 @@ def Range(lo, hi, ctx = None):
lo = _coerce_seq(lo, ctx)
hi = _coerce_seq(hi, ctx)
return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
# Special Relations

48
src/api/z3_api.h
View file

@ -1101,6 +1101,12 @@ typedef enum {
Z3_OP_BUREM_I,
Z3_OP_BSMOD_I,
// Special relations
Z3_OP_SPECIAL_RELATION_LO,
Z3_OP_SPECIAL_RELATION_PO,
Z3_OP_SPECIAL_RELATION_PLO,
Z3_OP_SPECIAL_RELATION_TO,
// Proofs
Z3_OP_PR_UNDEF = 0x500,
Z3_OP_PR_TRUE,
@ -3595,10 +3601,50 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
/*@}*/
/** @name Special relations */
/*@{*/
/**
\brief declare \c a and \c b are in linear order over a relation indexed by \c id.
\pre a and b are of same type.
def_API('Z3_mk_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
/**
\brief declare \c a and \c b are in partial order over a relation indexed by \c id.
\pre a and b are of same type.
def_API('Z3_mk_partial_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_partial_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
/**
\brief declare \c a and \c b are in piecewise linear order indexed by relation \c id.
\pre a and b are of same type.
def_API('Z3_mk_piecewise_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_piecewise_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
/**
\brief declare \c a and \c b are in tree order indexed by \c id.
\pre a and b are of same type.
def_API('Z3_mk_tree_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_tree_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b);
/*@}*/
/** @name Quantifiers */
/*@{*/
/**

1
src/ast/CMakeLists.txt
View file

@ -41,6 +41,7 @@ z3_add_component(ast
reg_decl_plugins.cpp
seq_decl_plugin.cpp
shared_occs.cpp
special_relations_decl_plugin.cpp
static_features.cpp
used_vars.cpp
well_sorted.cpp

1
src/ast/ast.h
View file

@ -2122,6 +2122,7 @@ public:
app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); }
app * mk_and(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2); }
app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2, arg3); }
app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(m_basic_family_id, OP_OR, 4, args); }
app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); }
app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); }
app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); }

15
src/ast/ast_util.h
View file

@ -111,6 +111,17 @@ app * mk_and(ast_manager & m, unsigned num_args, app * const * args);
inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
inline app_ref operator&(expr_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
inline app_ref operator&(app_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
inline app_ref operator&(var_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
inline app_ref operator&(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); }
inline app_ref operator|(expr_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
inline app_ref operator|(app_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
inline app_ref operator|(var_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
inline app_ref operator|(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
/**
Return (or args[0] ... args[num_args-1]) if num_args >= 2
Return args[0] if num_args == 1
@ -129,6 +140,10 @@ expr * mk_not(ast_manager & m, expr * arg);
expr_ref mk_not(const expr_ref& e);
inline expr_ref not(const expr_ref& e) { return mk_not(e); }
inline app_ref not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); }
/**
Negate and push over conjunction or disjunction.
*/

79
src/ast/datatype_decl_plugin.cpp
View file

@ -1188,6 +1188,85 @@ namespace datatype {
}
}
}
sort_ref util::mk_list_datatype(sort* elem, symbol const& name,
func_decl_ref& cons, func_decl_ref& is_cons,
func_decl_ref& hd, func_decl_ref& tl,
func_decl_ref& nil, func_decl_ref& is_nil) {
accessor_decl* head_tail[2] = {
mk_accessor_decl(m, symbol("head"), type_ref(elem)),
mk_accessor_decl(m, symbol("tail"), type_ref(0))
};
constructor_decl* constrs[2] = {
mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr),
mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail)
};
decl::plugin& p = *get_plugin();
sort_ref_vector sorts(m);
datatype_decl * decl = mk_datatype_decl(*this, name, 0, nullptr, 2, constrs);
bool is_ok = p.mk_datatypes(1, &decl, 0, nullptr, sorts);
del_datatype_decl(decl);
if (!is_ok) {
return sort_ref(m);
}
sort* s = sorts.get(0);
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
SASSERT(cnstrs.size() == 2);
nil = cnstrs[0];
is_nil = get_constructor_is(cnstrs[0]);
cons = cnstrs[1];
is_cons = get_constructor_is(cnstrs[1]);
ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[1]);
SASSERT(acc.size() == 2);
hd = acc[0];
tl = acc[1];
return sort_ref(s, m);
}
sort_ref util::mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair) {
type_ref t1(a), t2(b);
accessor_decl* fstd = mk_accessor_decl(m, symbol("fst"), t1);
accessor_decl* sndd = mk_accessor_decl(m, symbol("snd"), t2);
accessor_decl* accd[2] = { fstd, sndd };
auto * p = mk_constructor_decl(symbol("pair"), symbol("is-pair"), 2, accd);
auto* dt = mk_datatype_decl(*this, symbol("pair"), 0, nullptr, 1, &p);
sort_ref_vector sorts(m);
VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
del_datatype_decl(dt);
sort* s = sorts.get(0);
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
SASSERT(cnstrs.size() == 1);
ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[0]);
SASSERT(acc.size() == 2);
fst = acc[0];
snd = acc[1];
pair = cnstrs[0];
return sort_ref(s, m);
}
sort_ref util::mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs) {
ptr_vector<accessor_decl> accd;
for (auto const& e : elems) {
type_ref t(e.second);
accd.push_back(mk_accessor_decl(m, e.first, t));
}
auto* tuple = mk_constructor_decl(name, test, accd.size(), accd.c_ptr());
auto* dt = mk_datatype_decl(*this, name, 0, nullptr, 1, &tuple);
sort_ref_vector sorts(m);
VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts));
del_datatype_decl(dt);
sort* s = sorts.get(0);
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
SASSERT(cnstrs.size() == 1);
ptr_vector<func_decl> const& acc = *get_constructor_accessors(cnstrs[0]);
for (auto* f : acc) accs.push_back(f);
tup = cnstrs[0];
return sort_ref(s, m);
}
}
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) {

6
src/ast/datatype_decl_plugin.h
View file

@ -364,6 +364,12 @@ namespace datatype {
decl::plugin* get_plugin() { return m_plugin; }
void get_defs(sort* s, ptr_vector<def>& defs);
def const& get_def(sort* s) const;
sort_ref mk_list_datatype(sort* elem, symbol const& name,
func_decl_ref& cons, func_decl_ref& is_cons,
func_decl_ref& hd, func_decl_ref& tl,
func_decl_ref& nil, func_decl_ref& is_nil);
sort_ref mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair);
sort_ref mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs);
};
};

80
src/ast/pattern/expr_pattern_match.cpp
View file

@ -52,35 +52,57 @@ expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, u
}
m_regs[0] = qf->get_expr();
for (unsigned i = 0; i < m_precompiled.size(); ++i) {
quantifier* qf2 = m_precompiled[i].get();
if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) {
continue;
}
if (qf2->get_num_decls() != qf->get_num_decls()) {
continue;
}
subst s;
if (match(qf->get_expr(), m_first_instrs[i], s)) {
for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) {
app* p = static_cast<app*>(qf2->get_pattern(j));
expr_ref p_result(m_manager);
instantiate(p, qf->get_num_decls(), s, p_result);
patterns.push_back(to_app(p_result.get()));
}
weight = qf2->get_weight();
return true;
if (match_quantifier(i, qf, patterns, weight))
return true;
}
return false;
}
bool
expr_pattern_match::match_quantifier(unsigned i, quantifier* qf, app_ref_vector& patterns, unsigned& weight) {
quantifier* qf2 = m_precompiled[i].get();
if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) {
return false;
}
if (qf2->get_num_decls() != qf->get_num_decls()) {
return false;
}
subst s;
if (match(qf->get_expr(), m_first_instrs[i], s)) {
for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) {
app* p = static_cast<app*>(qf2->get_pattern(j));
expr_ref p_result(m_manager);
instantiate(p, qf->get_num_decls(), s, p_result);
patterns.push_back(to_app(p_result.get()));
}
weight = qf2->get_weight();
return true;
}
return false;
}
bool expr_pattern_match::match_quantifier_index(quantifier* qf, app_ref_vector& patterns, unsigned& index) {
if (m_regs.empty()) return false;
m_regs[0] = qf->get_expr();
for (unsigned i = 0; i < m_precompiled.size(); ++i) {
unsigned weight = 0;
if (match_quantifier(i, qf, patterns, weight)) {
index = i;
return true;
}
}
return false;
}
void
expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) {
bound b;
for (unsigned i = 0; i < num_bound; ++i) {
b.insert(m_bound_dom[i], m_bound_rng[i]);
}
TRACE("expr_pattern_match", tout << mk_pp(a, m_manager) << " " << num_bound << "\n";);
inst_proc proc(m_manager, s, b, m_regs);
for_each_ast(proc, a);
expr* v = nullptr;
@ -251,11 +273,7 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s)
break;
}
case CHECK_BOUND:
TRACE("expr_pattern_match",
tout
<< "check bound "
<< pc.m_num_bound << " " << pc.m_reg;
);
TRACE("expr_pattern_match", tout << "check bound " << pc.m_num_bound << " " << pc.m_reg << "\n";);
ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg];
break;
case BIND:
@ -396,11 +414,18 @@ expr_pattern_match::initialize(char const * spec_string) {
for (expr * e : ctx.assertions()) {
compile(e);
}
TRACE("expr_pattern_match", display(tout); );
}
void
expr_pattern_match::display(std::ostream& out) const {
unsigned expr_pattern_match::initialize(quantifier* q) {
if (m_instrs.empty()) {
m_instrs.push_back(instr(BACKTRACK));
}
compile(q);
return m_precompiled.size() - 1;
}
void expr_pattern_match::display(std::ostream& out) const {
for (unsigned i = 0; i < m_instrs.size(); ++i) {
display(out, m_instrs[i]);
}
@ -414,7 +439,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND:
out << "bind ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
@ -422,7 +446,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND_AC:
out << "bind_ac ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";
@ -430,7 +453,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const {
break;
case BIND_C:
out << "bind_c ";
out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " ";
out << mk_pp(pc.m_pat, m_manager) << "\n";
out << "next: " << pc.m_next << "\n";
out << "offset: " << pc.m_offset << "\n";

28
src/ast/pattern/expr_pattern_match.h
View file

@ -80,13 +80,7 @@ class expr_pattern_match {
}
void operator()(var* v) {
var* b = nullptr;
if (m_bound.find(v, b)) {
m_memoize.insert(v, b);
}
else {
UNREACHABLE();
}
m_memoize.insert(v, m_bound[v]);
}
void operator()(app * n) {
@ -98,15 +92,9 @@ class expr_pattern_match {
if (m_subst.find(decl, r)) {
decl = to_app(m_regs[r])->get_decl();
}
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = nullptr;
if (m_memoize.find(n->get_arg(i), arg)) {
SASSERT(arg);
args.push_back(arg);
}
else {
UNREACHABLE();
}
for (expr* arg : *n) {
arg = m_memoize[arg];
args.push_back(arg);
}
if (m_manager.is_pattern(n)) {
result = m_manager.mk_pattern(num_args, reinterpret_cast<app**>(args.c_ptr()));
@ -116,7 +104,6 @@ class expr_pattern_match {
}
m_pinned.push_back(result);
m_memoize.insert(n, result);
return;
}
};
@ -131,11 +118,14 @@ class expr_pattern_match {
public:
expr_pattern_match(ast_manager & manager);
~expr_pattern_match();
virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
virtual void initialize(char const * database);
bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight);
bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index);
unsigned initialize(quantifier* qf);
void initialize(char const * database);
void display(std::ostream& out) const;
private:
bool match_quantifier(unsigned i, quantifier * qf, app_ref_vector & patterns, unsigned & weight);
void instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result);
void compile(expr* q);
bool match(expr* a, unsigned init, subst& s);

13
src/ast/recfun_decl_plugin.cpp
View file

@ -316,6 +316,7 @@ namespace recfun {
return alloc(def, m(), m_fid, name, n, domain, range);
}
void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
d.set_definition(subst, n_vars, vars, rhs);
}
@ -384,7 +385,17 @@ namespace recfun {
promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) {
def* d = u().decl_fun(name, n, params, range);
SASSERT(! m_defs.contains(d->get_decl()));
SASSERT(!m_defs.contains(d->get_decl()));
m_defs.insert(d->get_decl(), d);
return promise_def(&u(), d);
}
promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range) {
def* d = u().decl_fun(name, n, params, range);
def* d2 = nullptr;
if (m_defs.find(d->get_decl(), d2)) {
dealloc(d2);
}
m_defs.insert(d->get_decl(), d);
return promise_def(&u(), d);
}

3
src/ast/recfun_decl_plugin.h
View file

@ -172,6 +172,8 @@ namespace recfun {
unsigned arity, sort * const * domain, sort * range) override;
promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range);
void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
@ -223,7 +225,6 @@ namespace recfun {
//<! add a function declaration
def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);
def& get_def(func_decl* f) {
SASSERT(m_plugin->has_def(f));
return m_plugin->get_def(f);

1
src/ast/rewriter/CMakeLists.txt
View file

@ -19,6 +19,7 @@ z3_add_component(rewriter
factor_equivs.cpp
factor_rewriter.cpp
fpa_rewriter.cpp
func_decl_replace.cpp
hoist_rewriter.cpp
inj_axiom.cpp
label_rewriter.cpp

97
src/ast/rewriter/func_decl_replace.cpp Normal file
View file

@ -0,0 +1,97 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
func_decl_replace.cpp
Abstract:
Replace functions in expressions.
Author:
Nikolaj Bjorner (nbjorner) 2019-03-28
Revision History:
--*/
#include "ast/rewriter/func_decl_replace.h"
expr_ref func_decl_replace::operator()(expr* e) {
m_todo.push_back(e);
while (!m_todo.empty()) {
expr* a = m_todo.back(), *b;
if (m_cache.contains(a)) {
m_todo.pop_back();
}
else if (is_var(a)) {
m_cache.insert(a, a);
m_todo.pop_back();
}
else if (is_app(a)) {
app* c = to_app(a);
unsigned n = c->get_num_args();
m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) {
expr* d = nullptr, *arg = c->get_arg(i);
if (m_cache.find(arg, d)) {
m_args.push_back(d);
arg_differs |= arg != d;
SASSERT(m.get_sort(arg) == m.get_sort(d));
}
else {
m_todo.push_back(arg);
}
}
if (m_args.size() == n) {
if (arg_differs) {
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
m_refs.push_back(b);
SASSERT(m.get_sort(a) == m.get_sort(b));
} else {
b = a;
}
func_decl* f = nullptr;
if (m_subst.find(c->get_decl(), f)) {
b = m.mk_app(f, m_args.size(), m_args.c_ptr());
m_refs.push_back(b);
}
m_cache.insert(a, b);
m_todo.pop_back();
}
}
else {
quantifier* q = to_quantifier(a);
SASSERT(is_quantifier(a));
expr* body = q->get_expr(), *new_body;
if (m_cache.find(body, new_body)) {
if (new_body == body) {
b = a;
}
else {
b = m.update_quantifier(q, new_body);
m_refs.push_back(b);
}
m_cache.insert(a, b);
m_todo.pop_back();
}
else {
m_todo.push_back(body);
}
}
}
return expr_ref(m_cache.find(e), m);
}
void func_decl_replace::reset() {
m_cache.reset();
m_subst.reset();
m_refs.reset();
m_funs.reset();
}

46
src/ast/rewriter/func_decl_replace.h Normal file
View file

@ -0,0 +1,46 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
func_decl_replace.h
Abstract:
Replace functions in expressions.
Author:
Nikolaj Bjorner (nbjorner) 2019-03-28
Revision History:
--*/
#ifndef FUNC_DECL_REPLACE_H_
#define FUNC_DECL_REPLACE_H_
#include "ast/ast.h"
class func_decl_replace {
ast_manager& m;
obj_map<func_decl, func_decl*> m_subst;
obj_map<expr, expr*> m_cache;
ptr_vector<expr> m_todo, m_args;
expr_ref_vector m_refs;
func_decl_ref_vector m_funs;
public:
func_decl_replace(ast_manager& m): m(m), m_refs(m), m_funs(m) {}
void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); m_funs.push_back(src), m_funs.push_back(dst); }
expr_ref operator()(expr* e);
void reset();
bool empty() const { return m_subst.empty(); }
};
#endif /* FUNC_DECL_REPLACE_H_ */

75
src/ast/special_relations_decl_plugin.cpp Normal file
View file

@ -0,0 +1,75 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
special_relations_decl_plugin.cpp
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2015-15-9.
Revision History:
--*/
#include <sstream>
#include "ast/ast.h"
#include "ast/special_relations_decl_plugin.h"
special_relations_decl_plugin::special_relations_decl_plugin():
m_lo("linear-order"),
m_po("partial-order"),
m_plo("piecewise-linear-order"),
m_to("tree-order")
{}
func_decl * special_relations_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range)
{
if (arity != 2) {
m_manager->raise_exception("special relations should have arity 2");
return nullptr;
}
if (domain[0] != domain[1]) {
m_manager->raise_exception("argument sort missmatch");
return nullptr;
}
func_decl_info info(m_family_id, k, num_parameters, parameters);
symbol name;
switch(k) {
case OP_SPECIAL_RELATION_PO: name = m_po; 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;
}
return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), info);
}
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_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));
}
}
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_LO: return sr_lo;
case OP_SPECIAL_RELATION_PLO: return sr_plo;
case OP_SPECIAL_RELATION_TO: return sr_to;
default:
UNREACHABLE();
return sr_po;
}
}

99
src/ast/special_relations_decl_plugin.h Normal file
View file

@ -0,0 +1,99 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
special_relations_decl_plugin.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2015-15-9.
Ashutosh Gupta 2016
Revision History:
--*/
#ifndef SPECIAL_RELATIONS_DECL_PLUGIN_H_
#define SPECIAL_RELATIONS_DECL_PLUGIN_H_
#include "ast/ast.h"
enum special_relations_op_kind {
OP_SPECIAL_RELATION_LO,
OP_SPECIAL_RELATION_PO,
OP_SPECIAL_RELATION_PLO,
OP_SPECIAL_RELATION_TO,
LAST_SPECIAL_RELATIONS_OP
};
class special_relations_decl_plugin : public decl_plugin {
symbol m_lo;
symbol m_po;
symbol m_plo;
symbol m_to;
public:
special_relations_decl_plugin();
~special_relations_decl_plugin() override {}
decl_plugin * mk_fresh() override {
return alloc(special_relations_decl_plugin);
}
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; }
};
enum sr_property {
sr_none = 0x00,
sr_transitive = 0x01, // Rxy & Ryz -> Rxz
sr_reflexive = 0x02, // Rxx
sr_antisymmetric = 0x04, // Rxy & Ryx -> x = y
sr_lefttree = 0x08, // Ryx & Rzx -> Ryz | Rzy
sr_righttree = 0x10, // Rxy & Rxz -> Ryx | Rzy
sr_total = 0x20, // Rxy | Ryx
sr_po = 0x01 | 0x02 | 0x04, // partial order
sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree
sr_plo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // piecewise linear order
sr_lo = 0x01 | 0x02 | 0x04 | 0x20, // linear order
};
class special_relations_util {
ast_manager& m;
family_id m_fid;
public:
special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {}
bool is_special_relation(func_decl* f) const { return f->get_family_id() == m_fid; }
bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); }
sr_property get_property(func_decl* f) const;
sr_property get_property(app* e) const { return get_property(e->get_decl()); }
func_decl* mk_to_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_TO, 1, &p, 2, f->get_domain(), f->get_range()); }
func_decl* mk_po_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PO, 1, &p, 2, f->get_domain(), f->get_range()); }
func_decl* mk_plo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PLO, 1, &p, 2, f->get_domain(), f->get_range()); }
func_decl* mk_lo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_LO, 1, &p, 2, f->get_domain(), f->get_range()); }
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); }
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_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); }
};
#endif /* SPECIAL_RELATIONS_DECL_PLUGIN_H_ */

7
src/ast/static_features.cpp
View file

@ -30,6 +30,7 @@ static_features::static_features(ast_manager & m):
m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")),
m_arrfid(m.mk_family_id("array")),
m_srfid(m.mk_family_id("special_relations")),
m_label_sym("label"),
m_pattern_sym("pattern"),
m_expr_list_sym("expr-list") {
@ -78,6 +79,7 @@ void static_features::reset() {
m_has_real = false;
m_has_bv = false;
m_has_fpa = false;
m_has_sr = false;
m_has_str = false;
m_has_seq_non_str = false;
m_has_arrays = false;
@ -274,6 +276,8 @@ void static_features::update_core(expr * e) {
m_has_bv = true;
if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e)))
m_has_fpa = true;
if (is_app(e) && to_app(e)->get_family_id() == m_srfid)
m_has_sr = true;
if (!m_has_arrays && m_arrayutil.is_array(e))
m_has_arrays = true;
if (!m_has_ext_arrays && m_arrayutil.is_array(e) &&
@ -281,9 +285,8 @@ void static_features::update_core(expr * e) {
m_has_ext_arrays = true;
if (!m_has_str && m_sequtil.str.is_string_term(e))
m_has_str = true;
if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e))
m_has_seq_non_str = true;
}
if (is_app(e)) {
family_id fid = to_app(e)->get_family_id();
mark_theory(fid);

3
src/ast/static_features.h
View file

@ -25,6 +25,7 @@ Revision History:
#include "ast/array_decl_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#include "util/map.h"
struct static_features {
@ -38,6 +39,7 @@ struct static_features {
family_id m_afid;
family_id m_lfid;
family_id m_arrfid;
family_id m_srfid;
ast_mark m_already_visited;
bool m_cnf;
unsigned m_num_exprs; //
@ -79,6 +81,7 @@ struct static_features {
bool m_has_real; //
bool m_has_bv; //
bool m_has_fpa; //
bool m_has_sr; // has special relations
bool m_has_str; // has String-typed terms
bool m_has_seq_non_str; // has non-String-typed Sequence terms
bool m_has_arrays; //

3
src/cmd_context/cmd_context.cpp
View file

@ -31,6 +31,7 @@ Notes:
#include "ast/pb_decl_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/csp_decl_plugin.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/pp.h"
@ -687,6 +688,7 @@ void cmd_context::init_manager_core(bool new_manager) {
register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa());
register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic));
register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin), !has_logic());
}
else {
// the manager was created by an external module
@ -703,6 +705,7 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
load_plugin(symbol("pb"), logic_has_pb(), fids);
load_plugin(symbol("csp"), smt_logics::logic_is_csp(m_logic), fids);
for (family_id fid : fids) {
decl_plugin * p = m_manager->get_plugin(fid);
if (p) {

1
src/model/model.cpp
View file

@ -217,6 +217,7 @@ void model::compress() {
}
}
if (removed.empty()) break;
TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";);
remove_decls(m_decls, removed);
remove_decls(m_func_decls, removed);
remove_decls(m_const_decls, removed);

1
src/model/model_core.cpp
View file

@ -66,6 +66,7 @@ void model_core::register_decl(func_decl * d, expr * v) {
}
void model_core::register_decl(func_decl * d, func_interp * fi) {
TRACE("model", tout << "register " << d->get_name() << "\n";);
SASSERT(d->get_arity() > 0);
SASSERT(&fi->m() == &m);
decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr);

1
src/smt/CMakeLists.txt
View file

@ -62,6 +62,7 @@ z3_add_component(smt
theory_pb.cpp
theory_recfun.cpp
theory_seq.cpp
theory_special_relations.cpp
theory_str.cpp
theory_utvpi.cpp
theory_wmaxsat.cpp

341
src/smt/diff_logic.h
View file

@ -228,10 +228,7 @@ class dl_graph {
int n = m_out_edges.size();
for (dl_var id = 0; id < n; id++) {
const edge_id_vector & e_ids = m_out_edges[id];
edge_id_vector::const_iterator it = e_ids.begin();
edge_id_vector::const_iterator end = e_ids.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : e_ids) {
SASSERT(static_cast<unsigned>(e_id) <= m_edges.size());
const edge & e = m_edges[e_id];
SASSERT(e.get_source() == id);
@ -239,10 +236,7 @@ class dl_graph {
}
for (dl_var id = 0; id < n; id++) {
const edge_id_vector & e_ids = m_in_edges[id];
edge_id_vector::const_iterator it = e_ids.begin();
edge_id_vector::const_iterator end = e_ids.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : e_ids) {
SASSERT(static_cast<unsigned>(e_id) <= m_edges.size());
const edge & e = m_edges[e_id];
SASSERT(e.get_target() == id);
@ -296,6 +290,9 @@ public:
numeral const& get_weight(edge_id id) const { return m_edges[id].get_weight(); }
edge_id_vector const& get_out_edges(dl_var v) const { return m_out_edges[v]; }
edge_id_vector const& get_in_edges(dl_var v) const { return m_in_edges[v]; }
private:
// An assignment is almost feasible if all but edge with idt edge are feasible.
@ -327,17 +324,16 @@ private:
// Store in gamma the normalized weight. The normalized weight is given
// by the formula
// m_assignment[e.get_source()] - m_assignment[e.get_target()] + e.get_weight()
void set_gamma(const edge & e, numeral & gamma) {
numeral& set_gamma(const edge & e, numeral & gamma) {
gamma = m_assignment[e.get_source()];
gamma -= m_assignment[e.get_target()];
gamma += e.get_weight();
return gamma;
}
void reset_marks() {
dl_var_vector::iterator it = m_visited.begin();
dl_var_vector::iterator end = m_visited.end();
for (; it != end; ++it) {
m_mark[*it] = DL_UNMARKED;
for (dl_var v : m_visited) {
m_mark[v] = DL_UNMARKED;
}
m_visited.reset();
}
@ -378,7 +374,7 @@ private:
TRACE("arith", tout << id << "\n";);
dl_var source = target;
for(;;) {
while (true) {
++m_stats.m_propagation_cost;
if (m_mark[root] != DL_UNMARKED) {
// negative cycle was found
@ -389,10 +385,7 @@ private:
return false;
}
typename edge_id_vector::iterator it = m_out_edges[source].begin();
typename edge_id_vector::iterator end = m_out_edges[source].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : m_out_edges[source]) {
edge & e = m_edges[e_id];
SASSERT(e.get_source() == source);
if (!e.is_enabled()) {
@ -442,10 +435,7 @@ private:
dl_var src = e->get_source();
dl_var dst = e->get_target();
numeral w = e->get_weight();
typename edge_id_vector::iterator it = m_out_edges[src].begin();
typename edge_id_vector::iterator end = m_out_edges[src].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : m_out_edges[src]) {
edge const& e2 = m_edges[e_id];
if (e2.get_target() == dst &&
e2.is_enabled() && // or at least not be inconsistent with current choices
@ -595,10 +585,7 @@ public:
//
// search for edges that can reduce size of negative cycle.
//
typename edge_id_vector::iterator it = m_out_edges[src].begin();
typename edge_id_vector::iterator end = m_out_edges[src].end();
for (; it != end; ++it) {
edge_id e_id2 = *it;
for (edge_id e_id2 : m_out_edges[src]) {
edge const& e2 = m_edges[e_id2];
dl_var src2 = e2.get_target();
if (e_id2 == e_id || !e2.is_enabled()) {
@ -661,6 +648,121 @@ public:
}
}
bool can_reach(dl_var src, dl_var dst) {
uint_set target, visited;
target.insert(dst);
return reachable(src, target, visited, dst);
}
bool reachable(dl_var start, uint_set const& target, uint_set& visited, dl_var& dst) {
visited.reset();
svector<dl_var> nodes;
nodes.push_back(start);
for (dl_var n : nodes) {
if (visited.contains(n)) continue;
visited.insert(n);
edge_id_vector & edges = m_out_edges[n];
for (edge_id e_id : edges) {
edge & e = m_edges[e_id];
if (e.is_enabled()) {
dst = e.get_target();
if (target.contains(dst)) {
return true;
}
nodes.push_back(dst);
}
}
}
return false;
}
private:
svector<int> m_freq_hybrid;
int m_total_count = 0;
int m_run_counter = -1;
svector<int> m_hybrid_visited, m_hybrid_parent;
bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const {
return (gamma.is_zero() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp;
}
int_vector bfs_todo;
int_vector dfs_todo;
public:
template<typename Functor>
bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
auto zero_edge = true;
unsigned bfs_head = 0;
bfs_todo.reset();
dfs_todo.reset();
m_hybrid_visited.resize(m_assignment.size(), m_run_counter++);
m_hybrid_parent.resize(m_assignment.size(), -1);
bfs_todo.push_back(source);
m_hybrid_parent[source] = -1;
m_hybrid_visited[source] = m_run_counter;
numeral gamma;
while (bfs_head < bfs_todo.size() || !dfs_todo.empty()) {
m_total_count++;
dl_var v;
if (!dfs_todo.empty()) {
v = dfs_todo.back();
dfs_todo.pop_back();
}
else {
v = bfs_todo[bfs_head++];
}
edge_id_vector & edges = m_out_edges[v];
for (edge_id e_id : edges) {
edge & e = m_edges[e_id];
SASSERT(e.get_source() == v);
if (!e.is_enabled()) {
continue;
}
set_gamma(e, gamma);
if (is_connected(gamma, zero_edge, e, timestamp)) {
dl_var curr_target = e.get_target();
if (curr_target == target) {
f(e.get_explanation());
m_freq_hybrid[e_id]++;
while (true) {
int p = m_hybrid_parent[v];
if (p == -1)
return true;
edge_id eid;
bool ret = get_edge_id(p, v, eid);
if (eid == null_edge_id || !ret) {
return true;
}
else {
edge & e = m_edges[eid];
f(e.get_explanation());
m_freq_hybrid[eid]++;
v = p;
}
}
}
else if (m_hybrid_visited[curr_target] != m_run_counter) {
if (m_freq_hybrid[e_id] > 1) {
dfs_todo.push_back(curr_target);
}
else {
bfs_todo.push_back(curr_target);
}
m_hybrid_visited[curr_target] = m_run_counter;
m_hybrid_parent[curr_target] = v;
}
}
}
}
return false;
}
//
// Create fresh literals obtained by resolving a pair (or more)
// literals associated with the edges.
@ -795,10 +897,8 @@ public:
SASSERT(is_feasible());
if (!m_assignment[v].is_zero()) {
numeral k = m_assignment[v];
typename assignment::iterator it = m_assignment.begin();
typename assignment::iterator end = m_assignment.end();
for (; it != end; ++it) {
*it -= k;
for (auto& a : m_assignment) {
a -= k;
}
SASSERT(is_feasible());
}
@ -853,10 +953,7 @@ public:
void display_agl(std::ostream & out) const {
uint_set vars;
typename edges::const_iterator it = m_edges.begin();
typename edges::const_iterator end = m_edges.end();
for (; it != end; ++it) {
edge const& e = *it;
for (edge const& e : m_edges) {
if (e.is_enabled()) {
vars.insert(e.get_source());
vars.insert(e.get_target());
@ -870,9 +967,7 @@ public:
out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n";
}
}
it = m_edges.begin();
for (; it != end; ++it) {
edge const& e = *it;
for (edge const& e : m_edges) {
if (e.is_enabled()) {
out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n";
}
@ -888,22 +983,19 @@ public:
}
void display_edges(std::ostream & out) const {
typename edges::const_iterator it = m_edges.begin();
typename edges::const_iterator end = m_edges.end();
for (; it != end; ++it) {
edge const& e = *it;
for (edge const& e : m_edges) {
if (e.is_enabled()) {
display_edge(out, e);
}
}
}
void display_edge(std::ostream & out, edge_id id) const {
display_edge(out, m_edges[id]);
std::ostream& display_edge(std::ostream & out, edge_id id) const {
return display_edge(out, m_edges[id]);
}
void display_edge(std::ostream & out, const edge & e) const {
out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n";
std::ostream& display_edge(std::ostream & out, const edge & e) const {
return out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n";
}
template<typename FilterAssignmentProc>
@ -920,11 +1012,8 @@ public:
// If there is such edge, then the weight is stored in w and the explanation in ex.
bool get_edge_weight(dl_var source, dl_var target, numeral & w, explanation & ex) {
edge_id_vector & edges = m_out_edges[source];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
bool found = false;
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges) {
edge & e = m_edges[e_id];
if (e.is_enabled() && e.get_target() == target && (!found || e.get_weight() < w)) {
w = e.get_weight();
@ -939,12 +1028,10 @@ public:
// If there is such edge, return its edge_id in parameter id.
bool get_edge_id(dl_var source, dl_var target, edge_id & id) const {
edge_id_vector const & edges = m_out_edges[source];
typename edge_id_vector::const_iterator it = edges.begin();
typename edge_id_vector::const_iterator end = edges.end();
for (; it != end; ++it) {
id = *it;
edge const & e = m_edges[id];
for (edge_id e_id : edges) {
edge const & e = m_edges[e_id];
if (e.get_target() == target) {
id = e_id;
return true;
}
}
@ -958,18 +1045,14 @@ public:
void get_neighbours_undirected(dl_var current, svector<dl_var> & neighbours) {
neighbours.reset();
edge_id_vector & out_edges = m_out_edges[current];
typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : out_edges) {
edge & e = m_edges[e_id];
SASSERT(e.get_source() == current);
dl_var neighbour = e.get_target();
neighbours.push_back(neighbour);
}
edge_id_vector & in_edges = m_in_edges[current];
typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end();
for (; it2 != end2; ++it2) {
edge_id e_id = *it2;
for (edge_id e_id : in_edges) {
edge & e = m_edges[e_id];
SASSERT(e.get_target() == current);
dl_var neighbour = e.get_source();
@ -1052,10 +1135,7 @@ public:
template<typename Functor>
void enumerate_edges(dl_var source, dl_var target, Functor& f) {
edge_id_vector & edges = m_out_edges[source];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges) {
edge const& e = m_edges[e_id];
if (e.get_target() == target) {
f(e.get_weight(), e.get_explanation());
@ -1112,10 +1192,7 @@ public:
m_roots.push_back(v);
numeral gamma;
edge_id_vector & edges = m_out_edges[v];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges) {
edge & e = m_edges[e_id];
if (!e.is_enabled()) {
continue;
@ -1165,20 +1242,11 @@ public:
m_dfs_time[v] = 0;
succ.push_back(v);
numeral gamma;
for (unsigned i = 0; i < succ.size(); ++i) {
v = succ[i];
edge_id_vector & edges = m_out_edges[v];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
edge & e = m_edges[e_id];
if (!e.is_enabled()) {
continue;
}
SASSERT(e.get_source() == v);
set_gamma(e, gamma);
if (gamma.is_zero()) {
for (dl_var w : succ) {
for (edge_id e_id : m_out_edges[w]) {
edge & e = m_edges[e_id];
if (e.is_enabled() && set_gamma(e, gamma).is_zero()) {
SASSERT(e.get_source() == w);
dl_var target = e.get_target();
if (m_dfs_time[target] == -1) {
succ.push_back(target);
@ -1269,50 +1337,57 @@ private:
m_edge_id(e) {
}
};
public:
// Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp.
// The functor f is applied on every explanation attached to the edges in the shortest path.
// Return true if the path exists, false otherwise.
// Return true if the path exists, false otherwise.
template<typename Functor>
bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
return find_shortest_path_aux(source, target, timestamp, f, true);
}
template<typename Functor>
bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
return find_shortest_path_aux(source, target, timestamp, f, false);
}
template<typename Functor>
bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) {
svector<bfs_elem> bfs_todo;
svector<char> bfs_mark;
svector<bool> bfs_mark;
bfs_mark.resize(m_assignment.size(), false);
bfs_todo.push_back(bfs_elem(source, -1, null_edge_id));
bfs_mark[source] = true;
unsigned m_head = 0;
numeral gamma;
while (m_head < bfs_todo.size()) {
bfs_elem & curr = bfs_todo[m_head];
int parent_idx = m_head;
m_head++;
dl_var v = curr.m_var;
for (unsigned head = 0; head < bfs_todo.size(); ++head) {
bfs_elem & curr = bfs_todo[head];
int parent_idx = head;
dl_var v = curr.m_var;
TRACE("dl_bfs", tout << "processing: " << v << "\n";);
edge_id_vector & edges = m_out_edges[v];
typename edge_id_vector::iterator it = edges.begin();
typename edge_id_vector::iterator end = edges.end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges) {
edge & e = m_edges[e_id];
SASSERT(e.get_source() == v);
if (!e.is_enabled()) {
continue;
}
set_gamma(e, gamma);
TRACE("dl_bfs", tout << "processing edge: "; display_edge(tout, e); tout << "gamma: " << gamma << "\n";);
if (gamma.is_zero() && e.get_timestamp() < timestamp) {
TRACE("dl_bfs", display_edge(tout << "processing edge: ", e) << " gamma: " << gamma << "\n";);
if (is_connected(gamma, zero_edge, e, timestamp)) {
dl_var curr_target = e.get_target();
TRACE("dl_bfs", tout << "curr_target: " << curr_target <<
", mark: " << static_cast<int>(bfs_mark[curr_target]) << "\n";);
TRACE("dl_bfs", tout << "curr_target: " << curr_target << ", mark: " << bfs_mark[curr_target] << "\n";);
if (curr_target == target) {
TRACE("dl_bfs", tout << "found path\n";);
TRACE("dl_eq_bug", tout << "path: " << source << " --> " << target << "\n";
display_edge(tout, e);
int tmp_parent_idx = parent_idx;
for (;;) {
while (true) {
bfs_elem & curr = bfs_todo[tmp_parent_idx];
if (curr.m_edge_id == null_edge_id) {
break;
@ -1322,11 +1397,10 @@ public:
display_edge(tout, e);
tmp_parent_idx = curr.m_parent_idx;
}
tout.flush();
});
TRACE("dl_eq_bug", display_edge(tout, e););
f(e.get_explanation());
for (;;) {
while (true) {
SASSERT(parent_idx >= 0);
bfs_elem & curr = bfs_todo[parent_idx];
if (curr.m_edge_id == null_edge_id) {
@ -1340,11 +1414,9 @@ public:
}
}
}
else {
if (!bfs_mark[curr_target]) {
bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id));
bfs_mark[curr_target] = true;
}
else if (!bfs_mark[curr_target]) {
bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id));
bfs_mark[curr_target] = true;
}
}
}
@ -1430,8 +1502,7 @@ private:
numeral get_reduced_weight(dfs_state& state, dl_var n, edge const& e) {
numeral gamma;
set_gamma(e, gamma);
return state.m_delta[n] + gamma;
return state.m_delta[n] + set_gamma(e, gamma);
}
template<bool is_fw>
@ -1477,11 +1548,7 @@ private:
}
TRACE("diff_logic", tout << "source: " << source << "\n";);
typename edge_id_vector::const_iterator it = edges[source].begin();
typename edge_id_vector::const_iterator end = edges[source].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges[source]) {
edge const& e = m_edges[e_id];
if (&e == &e_init) {
@ -1569,11 +1636,9 @@ private:
tout << "\n";
});
typename heap<typename dfs_state::hp_lt>::const_iterator it = state.m_heap.begin();
typename heap<typename dfs_state::hp_lt>::const_iterator end = state.m_heap.end();
for (; it != end; ++it) {
SASSERT(m_mark[*it] != DL_PROP_UNMARKED);
m_mark[*it] = DL_PROP_UNMARKED;;
for (auto & s : state.m_heap) {
SASSERT(m_mark[s] != DL_PROP_UNMARKED);
m_mark[s] = DL_PROP_UNMARKED;;
}
state.m_heap.reset();
SASSERT(marks_are_clear());
@ -1592,11 +1657,8 @@ private:
for (unsigned i = 0; i < src.m_visited.size(); ++i) {
dl_var c = src.m_visited[i];
typename edge_id_vector::const_iterator it = edges[c].begin();
typename edge_id_vector::const_iterator end = edges[c].end();
numeral n1 = n0 + src.m_delta[c] - m_assignment[c];
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : edges[c]) {
edge const& e1 = m_edges[e_id];
SASSERT(c == e1.get_source());
if (e1.is_enabled()) {
@ -1644,13 +1706,10 @@ public:
edge_id_vector& out_edges = m_out_edges[src];
edge_id_vector& in_edges = m_in_edges[dst];
numeral w = e1.get_weight();
typename edge_id_vector::const_iterator it, end;
if (out_edges.size() < in_edges.size()) {
end = out_edges.end();
for (it = out_edges.begin(); it != end; ++it) {
for (edge_id e_id : out_edges) {
++m_stats.m_implied_literal_cost;
edge_id e_id = *it;
edge const& e2 = m_edges[e_id];
if (e_id != id && !e2.is_enabled() && e2.get_target() == dst && e2.get_weight() >= w) {
subsumed.push_back(e_id);
@ -1659,10 +1718,8 @@ public:
}
}
else {
end = in_edges.end();
for (it = in_edges.begin(); it != end; ++it) {
for (edge_id e_id : in_edges) {
++m_stats.m_implied_literal_cost;
edge_id e_id = *it;
edge const& e2 = m_edges[e_id];
if (e_id != id && !e2.is_enabled() && e2.get_source() == src && e2.get_weight() >= w) {
subsumed.push_back(e_id);
@ -1696,20 +1753,14 @@ public:
find_subsumed1(id, subsumed);
typename edge_id_vector::const_iterator it, end, it3, end3;
it = m_in_edges[src].begin();
end = m_in_edges[src].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : m_in_edges[src]) {
edge const& e2 = m_edges[e_id];
if (!e2.is_enabled() || e2.get_source() == dst) {
continue;
}
w2 = e2.get_weight() + w;
it3 = m_out_edges[e2.get_source()].begin();
end3 = m_out_edges[e2.get_source()].end();
for (; it3 != end3; ++it3) {
for (edge_id e_id3 : m_out_edges[e2.get_source()]) {
++m_stats.m_implied_literal_cost;
edge_id e_id3 = *it3;
edge const& e3 = m_edges[e_id3];
if (e3.is_enabled() || e3.get_target() != dst) {
continue;
@ -1720,21 +1771,15 @@ public:
}
}
}
it = m_out_edges[dst].begin();
end = m_out_edges[dst].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : m_out_edges[dst]) {
edge const& e2 = m_edges[e_id];
if (!e2.is_enabled() || e2.get_target() == src) {
continue;
}
w2 = e2.get_weight() + w;
it3 = m_in_edges[e2.get_target()].begin();
end3 = m_in_edges[e2.get_target()].end();
for (; it3 != end3; ++it3) {
for (edge_id e_id3 : m_in_edges[e2.get_target()]) {
++m_stats.m_implied_literal_cost;
edge_id e_id3 = *it3;
edge const& e3 = m_edges[e_id3];
if (e3.is_enabled() || e3.get_source() != src) {
continue;
@ -1783,11 +1828,7 @@ public:
m_mark[v] = DL_PROCESSED;
TRACE("diff_logic", tout << v << "\n";);
typename edge_id_vector::iterator it = m_out_edges[v].begin();
typename edge_id_vector::iterator end = m_out_edges[v].end();
for (; it != end; ++it) {
edge_id e_id = *it;
for (edge_id e_id : m_out_edges[v]) {
edge const& e = m_edges[e_id];
if (!e.is_enabled() || e.get_timestamp() > timestamp) {
continue;

1
src/smt/smt_context.cpp
View file

@ -4474,6 +4474,7 @@ namespace smt {
fi->set_else(bodyr);
m_model->register_decl(f, fi);
}
TRACE("model", tout << *m_model << "\n";);
}
};

7
src/smt/smt_setup.cpp
View file

@ -33,6 +33,7 @@ Revision History:
#include "smt/theory_dl.h"
#include "smt/theory_seq_empty.h"
#include "smt/theory_seq.h"
#include "smt/theory_special_relations.h"
#include "smt/theory_pb.h"
#include "smt/theory_fpa.h"
#include "smt/theory_str.h"
@ -935,6 +936,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager));
}
void setup::setup_special_relations() {
m_context.register_plugin(alloc(smt::theory_special_relations, m_manager));
}
void setup::setup_unknown() {
static_features st(m_manager);
ptr_vector<expr> fmls;
@ -950,6 +955,7 @@ namespace smt {
setup_seq_str(st);
setup_card();
setup_fpa();
if (st.m_has_sr) setup_special_relations();
}
void setup::setup_unknown(static_features & st) {
@ -966,6 +972,7 @@ namespace smt {
setup_card();
setup_fpa();
setup_recfuns();
if (st.m_has_sr) setup_special_relations();
return;
}

1
src/smt/smt_setup.h
View file

@ -82,6 +82,7 @@ namespace smt {
void setup_QF_S();
void setup_LRA();
void setup_CSP();
void setup_special_relations();
void setup_AUFLIA(bool simple_array = true);
void setup_AUFLIA(static_features const & st);
void setup_AUFLIRA(bool simple_array = true);

2
src/smt/theory_recfun.cpp
View file

@ -460,7 +460,7 @@ namespace smt {
}
void theory_recfun::display(std::ostream & out) const {
out << "recfun{}";
out << "recfun{}\n";
}
void theory_recfun::collect_statistics(::statistics & st) const {

907
src/smt/theory_special_relations.cpp Normal file
View file

@ -0,0 +1,907 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
theory_special_relations.cpp
Abstract:
Special Relations theory plugin.
Author:
Nikolaj Bjorner (nbjorner) 2015-9-16
Ashutosh Gupta 2016
Notes:
--*/
#include <fstream>
#include "smt/smt_context.h"
#include "smt/theory_arith.h"
#include "smt/theory_special_relations.h"
#include "smt/smt_solver.h"
#include "solver/solver.h"
#include "ast/reg_decl_plugins.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/recfun_replace.h"
namespace smt {
void theory_special_relations::relation::push() {
m_scopes.push_back(scope());
scope& s = m_scopes.back();
s.m_asserted_atoms_lim = m_asserted_atoms.size();
s.m_asserted_qhead_old = m_asserted_qhead;
m_graph.push();
m_ufctx.get_trail_stack().push_scope();
}
void theory_special_relations::relation::pop(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope& s = m_scopes[new_lvl];
m_asserted_atoms.shrink(s.m_asserted_atoms_lim);
m_asserted_qhead = s.m_asserted_qhead_old;
m_scopes.shrink(new_lvl);
m_graph.pop(num_scopes);
m_ufctx.get_trail_stack().pop_scope(num_scopes);
}
void theory_special_relations::relation::ensure_var(theory_var v) {
while ((unsigned)v > m_uf.mk_var());
if ((unsigned)v >= m_graph.get_num_nodes()) {
m_graph.init_var(v);
}
}
bool theory_special_relations::relation::new_eq_eh(literal l, theory_var v1, theory_var v2) {
ensure_var(v1);
ensure_var(v2);
literal_vector ls;
ls.push_back(l);
return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls);
}
std::ostream& theory_special_relations::relation::display(theory_special_relations const& th, std::ostream& out) const {
out << mk_pp(m_decl, th.get_manager());
for (unsigned i = 0; i < m_decl->get_num_parameters(); ++i) {
th.get_manager().display(out << " ", m_decl->get_parameter(i));
}
out << ":\n";
m_graph.display(out);
out << "explanation: " << m_explanation << "\n";
m_uf.display(out);
for (atom* ap : m_asserted_atoms) {
th.display_atom(out, *ap);
}
return out;
}
theory_special_relations::theory_special_relations(ast_manager& m):
theory(m.mk_family_id("special_relations")),
m_util(m) {
}
theory_special_relations::~theory_special_relations() {
reset_eh();
}
theory * theory_special_relations::mk_fresh(context * new_ctx) {
return alloc(theory_special_relations, new_ctx->get_manager());
}
bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) {
SASSERT(m_util.is_special_relation(atm));
relation* r = 0;
if (!m_relations.find(atm->get_decl(), r)) {
r = alloc(relation, m_util.get_property(atm), atm->get_decl());
m_relations.insert(atm->get_decl(), r);
for (unsigned i = 0; i < m_atoms_lim.size(); ++i) r->push();
}
context& ctx = get_context();
expr* arg0 = atm->get_arg(0);
expr* arg1 = atm->get_arg(1);
theory_var v0 = mk_var(arg0);
theory_var v1 = mk_var(arg1);
bool_var v = ctx.mk_bool_var(atm);
ctx.set_var_theory(v, get_id());
atom* a = alloc(atom, v, *r, v0, v1);
m_atoms.push_back(a);
TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : bv" << v << " v" << a->v1() << " v" << a->v2() << ' ' << gate_ctx << "\n";);
m_bool_var2atom.insert(v, a);
return true;
}
theory_var theory_special_relations::mk_var(expr* e) {
context& ctx = get_context();
if (!ctx.e_internalized(e)) {
ctx.internalize(e, false);
}
enode * n = ctx.get_enode(e);
theory_var v = n->get_th_var(get_id());
if (null_theory_var == v) {
v = theory::mk_var(n);
ctx.attach_th_var(n, this, v);
}
return v;
}
void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) {
context& ctx = get_context();
app* t1 = get_enode(v1)->get_owner();
app* t2 = get_enode(v2)->get_owner();
literal eq = mk_eq(t1, t2, false);
for (auto const& kv : m_relations) {
relation& r = *kv.m_value;
if (!r.new_eq_eh(eq, v1, v2)) {
set_neg_cycle_conflict(r);
break;
}
}
}
final_check_status theory_special_relations::final_check_eh() {
TRACE("special_relations", tout << "\n";);
for (auto const& kv : m_relations) {
lbool r = final_check(*kv.m_value);
switch (r) {
case l_undef:
return FC_GIVEUP;
case l_false:
return FC_CONTINUE;
default:
break;
}
}
bool new_equality = false;
for (auto const& kv : m_relations) {
if (extract_equalities(*kv.m_value)) {
new_equality = true;
}
}
if (new_equality) {
return FC_CONTINUE;
}
else {
return FC_DONE;
}
}
lbool theory_special_relations::final_check_lo(relation& r) {
// all constraints are saturated by propagation.
return l_true;
}
enode* theory_special_relations::ensure_enode(expr* e) {
context& ctx = get_context();
if (!ctx.e_internalized(e)) {
ctx.internalize(e, false);
}
enode* n = ctx.get_enode(e);
ctx.mark_as_relevant(n);
return n;
}
literal theory_special_relations::mk_literal(expr* _e) {
expr_ref e(_e, get_manager());
ensure_enode(e);
return get_context().get_literal(e);
}
theory_var theory_special_relations::mk_var(enode* n) {
if (is_attached_to_var(n)) {
return n->get_th_var(get_id());
}
else {
theory_var v = theory::mk_var(n);
get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n);
return v;
}
}
lbool theory_special_relations::final_check_plo(relation& r) {
//
// ensure that !Rxy -> Ryx between connected components
// (where Rzx & Rzy or Rxz & Ryz for some z)
//
lbool res = l_true;
for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) {
atom& a = *r.m_asserted_atoms[i];
if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) {
res = enable(a);
}
}
return res;
}
lbool theory_special_relations::final_check_to(relation& r) {
uint_set visited, target;
for (atom* ap : r.m_asserted_atoms) {
atom& a = *ap;
if (a.phase() || r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) {
continue;
}
target.reset();
theory_var w;
// v2 !<= v1 is asserted
target.insert(a.v2());
if (r.m_graph.reachable(a.v1(), target, visited, w)) {
// we already have v1 <= v2
continue;
}
// the nodes visited from v1 become target for v2
if (r.m_graph.reachable(a.v2(), visited, target, w)) {
// we have the following:
// v1 <= w
// v2 <= w
// v1 !<= v2
//
// enforce the assertion
//
// v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1
//
unsigned timestamp = r.m_graph.get_timestamp();
r.m_explanation.reset();
r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r);
r.m_graph.find_shortest_reachable_path(a.v2(), w, timestamp, r);
r.m_explanation.push_back(a.explanation());
literal_vector const& lits = r.m_explanation;
if (!r.m_graph.add_non_strict_edge(a.v2(), a.v1(), lits)) {
set_neg_cycle_conflict(r);
return l_false;
}
}
}
return l_true;
}
lbool theory_special_relations::enable(atom& a) {
if (!a.enable()) {
relation& r = a.get_relation();
set_neg_cycle_conflict(r);
return l_false;
}
else {
return l_true;
}
}
void theory_special_relations::set_neg_cycle_conflict(relation& r) {
r.m_explanation.reset();
r.m_graph.traverse_neg_cycle2(false, r);
set_conflict(r);
}
void theory_special_relations::set_conflict(relation& r) {
literal_vector const& lits = r.m_explanation;
context & ctx = get_context();
vector<parameter> params;
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
get_id(), ctx.get_region(),
lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr())));
}
lbool theory_special_relations::final_check(relation& r) {
lbool res = propagate(r);
if (res != l_true) return res;
switch (r.m_property) {
case sr_lo:
res = final_check_lo(r);
break;
case sr_po:
res = final_check_po(r);
break;
case sr_plo:
res = final_check_plo(r);
break;
case sr_to:
res = final_check_to(r);
break;
default:
UNREACHABLE();
res = l_undef;
}
TRACE("special_relations", r.display(*this, tout););
return res;
}
bool theory_special_relations::extract_equalities(relation& r) {
bool new_eq = false;
int_vector scc_id;
u_map<unsigned> roots;
context& ctx = get_context();
r.m_graph.compute_zero_edge_scc(scc_id);
for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) {
if (scc_id[i] == -1) {
continue;
}
enode* n = get_enode(i);
if (roots.find(scc_id[i], j)) {
enode* m = get_enode(j);
if (n->get_root() != m->get_root()) {
new_eq = true;
unsigned timestamp = r.m_graph.get_timestamp();
r.m_explanation.reset();
r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r);
r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r);
eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), r.m_explanation.size(), r.m_explanation.c_ptr())));
ctx.assign_eq(n, m, js);
}
}
else {
roots.insert(scc_id[i], i);
}
}
return new_eq;
}
/*
\brief Propagation for piecewise linear orders
*/
lbool theory_special_relations::propagate_plo(atom& a) {
lbool res = l_true;
relation& r = a.get_relation();
if (a.phase()) {
r.m_uf.merge(a.v1(), a.v2());
res = enable(a);
}
else if (r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) {
res = enable(a);
}
return res;
}
lbool theory_special_relations::propagate_po(atom& a) {
lbool res = l_true;
relation& r = a.get_relation();
if (a.phase()) {
r.m_uf.merge(a.v1(), a.v2());
res = enable(a);
}
return res;
}
lbool theory_special_relations::final_check_po(relation& r) {
for (atom* ap : r.m_asserted_atoms) {
atom& a = *ap;
if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) {
// v1 !-> v2
// find v1 -> v3 -> v4 -> v2 path
r.m_explanation.reset();
unsigned timestamp = r.m_graph.get_timestamp();
bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r);
if (found_path) {
r.m_explanation.push_back(a.explanation());
set_conflict(r);
return l_false;
}
}
}
return l_true;
}
lbool theory_special_relations::propagate(relation& r) {
lbool res = l_true;
while (res == l_true && r.m_asserted_qhead < r.m_asserted_atoms.size()) {
atom& a = *r.m_asserted_atoms[r.m_asserted_qhead];
switch (r.m_property) {
case sr_lo:
res = enable(a);
break;
case sr_plo:
res = propagate_plo(a);
break;
case sr_po:
res = propagate_po(a);
break;
default:
if (a.phase()) {
res = enable(a);
}
break;
}
++r.m_asserted_qhead;
}
return res;
}
void theory_special_relations::reset_eh() {
for (auto const& kv : m_relations) {
dealloc(kv.m_value);
}
m_relations.reset();
del_atoms(0);
}
void theory_special_relations::assign_eh(bool_var v, bool is_true) {
TRACE("special_relations", tout << "assign bv" << v << " " << (is_true?" <- true":" <- false") << "\n";);
atom* a = m_bool_var2atom[v];
a->set_phase(is_true);
a->get_relation().m_asserted_atoms.push_back(a);
}
void theory_special_relations::push_scope_eh() {
for (auto const& kv : m_relations) {
kv.m_value->push();
}
m_atoms_lim.push_back(m_atoms.size());
}
void theory_special_relations::pop_scope_eh(unsigned num_scopes) {
for (auto const& kv : m_relations) {
kv.m_value->pop(num_scopes);
}
unsigned new_lvl = m_atoms_lim.size() - num_scopes;
del_atoms(m_atoms_lim[new_lvl]);
m_atoms_lim.shrink(new_lvl);
}
void theory_special_relations::del_atoms(unsigned old_size) {
atoms::iterator begin = m_atoms.begin() + old_size;
atoms::iterator it = m_atoms.end();
while (it != begin) {
--it;
atom* a = *it;
m_bool_var2atom.erase(a->var());
dealloc(a);
}
m_atoms.shrink(old_size);
}
void theory_special_relations::collect_statistics(::statistics & st) const {
for (auto const& kv : m_relations) {
kv.m_value->m_graph.collect_statistics(st);
}
}
model_value_proc * theory_special_relations::mk_value(enode * n, model_generator & mg) {
UNREACHABLE();
return nullptr;
}
void theory_special_relations::ensure_strict(graph& g) {
unsigned sz = g.get_num_edges();
for (unsigned i = 0; i < sz; ++i) {
if (!g.is_enabled(i)) continue;
if (g.get_weight(i) != s_integer(0)) continue;
dl_var src = g.get_source(i);
dl_var dst = g.get_target(i);
if (get_enode(src)->get_root() == get_enode(dst)->get_root()) continue;
VERIFY(g.add_strict_edge(src, dst, literal_vector()));
}
TRACE("special_relations", g.display(tout););
}
void theory_special_relations::ensure_tree(graph& g) {
unsigned sz = g.get_num_nodes();
for (unsigned i = 0; i < sz; ++i) {
int_vector const& edges = g.get_in_edges(i);
for (unsigned j = 0; j < edges.size(); ++j) {
edge_id e1 = edges[j];
if (g.is_enabled(e1)) {
SASSERT (i == g.get_target(e1));
dl_var src1 = g.get_source(e1);
for (unsigned k = j + 1; k < edges.size(); ++k) {
edge_id e2 = edges[k];
if (g.is_enabled(e2)) {
dl_var src2 = g.get_source(e2);
if (get_enode(src1)->get_root() != get_enode(src2)->get_root() &&
disconnected(g, src1, src2)) {
VERIFY(g.add_strict_edge(src1, src2, literal_vector()));
}
}
}
}
}
}
TRACE("special_relations", g.display(tout););
}
bool theory_special_relations::disconnected(graph const& g, dl_var u, dl_var v) const {
s_integer val_u = g.get_assignment(u);
s_integer val_v = g.get_assignment(v);
if (val_u == val_v) return u != v;
if (val_u < val_v) {
std::swap(u, v);
std::swap(val_u, val_v);
}
SASSERT(val_u > val_v);
svector<dl_var> todo;
todo.push_back(u);
while (!todo.empty()) {
u = todo.back();
todo.pop_back();
if (u == v) {
return false;
}
SASSERT(g.get_assignment(u) <= val_u);
if (g.get_assignment(u) <= val_v) {
continue;
}
for (edge_id e : g.get_out_edges(u)) {
if (is_strict_neighbour_edge(g, e)) {
todo.push_back(g.get_target(e));
}
}
}
return true;
}
expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) {
ast_manager& m = get_manager();
r.push();
ensure_strict(r.m_graph);
func_decl_ref fn(m);
expr_ref result(m);
arith_util arith(m);
sort* const* ty = r.decl()->get_domain();
fn = m.mk_fresh_func_decl("inj", 1, ty, arith.mk_int());
unsigned sz = r.m_graph.get_num_nodes();
func_interp* fi = alloc(func_interp, m, 1);
for (unsigned i = 0; i < sz; ++i) {
s_integer val = r.m_graph.get_assignment(i);
expr* arg = get_enode(i)->get_owner();
fi->insert_new_entry(&arg, arith.mk_numeral(val.to_rational(), true));
}
TRACE("special_relations", r.m_graph.display(tout););
r.pop(1);
fi->set_else(arith.mk_numeral(rational(0), true));
mg.get_model().register_decl(fn, fi);
result = arith.mk_le(m.mk_app(fn,m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty)));
return result;
}
expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) {
ast_manager& m = get_manager();
expr_ref result(m);
func_decl_ref fn(m);
arith_util arith(m);
func_interp* fi = alloc(func_interp, m, 1);
sort* const* ty = r.decl()->get_domain();
fn = m.mk_fresh_func_decl("class", 1, ty, arith.mk_int());
unsigned sz = r.m_graph.get_num_nodes();
for (unsigned i = 0; i < sz; ++i) {
unsigned val = r.m_uf.find(i);
expr* arg = get_enode(i)->get_owner();
fi->insert_new_entry(&arg, arith.mk_numeral(rational(val), true));
}
fi->set_else(arith.mk_numeral(rational(0), true));
mg.get_model().register_decl(fn, fi);
result = m.mk_eq(m.mk_app(fn, m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty)));
return result;
}
expr_ref theory_special_relations::mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi) {
graph const& g = r.m_graph;
ast_manager& m = get_manager();
expr_ref result(m);
func_decl_ref lofn(m), hifn(m);
arith_util arith(m);
func_interp* lofi = alloc(func_interp, m, 1);
func_interp* hifi = alloc(func_interp, m, 1);
sort* const* ty = r.decl()->get_domain();
lofn = m.mk_fresh_func_decl("lo", 1, ty, arith.mk_int());
hifn = m.mk_fresh_func_decl("hi", 1, ty, arith.mk_int());
unsigned sz = g.get_num_nodes();
for (unsigned i = 0; i < sz; ++i) {
expr* arg = get_enode(i)->get_owner();
lofi->insert_new_entry(&arg, arith.mk_numeral(rational(lo[i]), true));
hifi->insert_new_entry(&arg, arith.mk_numeral(rational(hi[i]), true));
}
lofi->set_else(arith.mk_numeral(rational(0), true));
hifi->set_else(arith.mk_numeral(rational(0), true));
mg.get_model().register_decl(lofn, lofi);
mg.get_model().register_decl(hifn, hifi);
result = m.mk_and(arith.mk_le(m.mk_app(lofn, m.mk_var(0, *ty)), m.mk_app(lofn, m.mk_var(1, *ty))),
arith.mk_le(m.mk_app(hifn, m.mk_var(1, *ty)), m.mk_app(hifn, m.mk_var(0, *ty))));
return result;
}
void theory_special_relations::init_model_lo(relation& r, model_generator& m) {
expr_ref inj = mk_inj(r, m);
func_interp* fi = alloc(func_interp, get_manager(), 2);
fi->set_else(inj);
m.get_model().register_decl(r.decl(), fi);
}
void theory_special_relations::init_model_plo(relation& r, model_generator& mg) {
expr_ref inj = mk_inj(r, mg);
expr_ref cls = mk_class(r, mg);
func_interp* fi = alloc(func_interp, get_manager(), 2);
fi->set_else(get_manager().mk_and(inj, cls));
mg.get_model().register_decl(r.decl(), fi);
}
/**
\brief model for a partial order,
is a recursive function that evaluates membership in partial order over
a fixed set of edges. It runs in O(e*n^2) where n is the number of vertices and e
number of edges.
connected1(x, y, v, w, S) =
if x = v then
if y = w then (S, true) else
if w in S then (S, false) else
connected2(w, y, S u { w }, edges)
else (S, false)
connected2(x, y, S, []) = (S, false)
connected2(x, y, S, (u,w)::edges) =
let (S, c) = connected1(x, y, u, w, S)
if c then (S, true) else connected2(x, y, S, edges)
*/
void theory_special_relations::init_model_po(relation& r, model_generator& mg) {
ast_manager& m = get_manager();
sort* s = r.m_decl->get_domain(0);
context& ctx = get_context();
datatype_util dt(m);
recfun::util rf(m);
recfun::decl::plugin& p = rf.get_plugin();
func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), hd(m), tl(m);
sort_ref listS(dt.mk_list_datatype(s, symbol("List"), cons, is_cons, hd, tl, nil, is_nil), m);
func_decl_ref fst(m), snd(m), pair(m);
sort_ref tup(dt.mk_pair_datatype(listS, m.mk_bool_sort(), fst, snd, pair), m);
sort* dom1[5] = { s, s, listS, s, s };
recfun::promise_def c1 = p.ensure_def(symbol("connected1"), 5, dom1, tup);
sort* dom2[3] = { s, s, listS };
recfun::promise_def c2 = p.ensure_def(symbol("connected2"), 3, dom2, tup);
sort* dom3[2] = { s, listS };
recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom3, m.mk_bool_sort());
var_ref xV(m.mk_var(1, s), m);
var_ref SV(m.mk_var(0, listS), m);
var_ref yV(m), vV(m), wV(m);
expr* x = xV, *S = SV;
expr* T = m.mk_true();
expr* F = m.mk_false();
func_decl* memf = mem.get_def()->get_decl();
func_decl* conn1 = c1.get_def()->get_decl();
func_decl* conn2 = c2.get_def()->get_decl();
expr_ref mem_body(m);
mem_body = m.mk_ite(m.mk_app(is_nil, S),
F,
m.mk_ite(m.mk_eq(m.mk_app(hd, S), x),
T,
m.mk_app(memf, x, m.mk_app(tl, S))));
recfun_replace rep(m);
var* vars[2] = { xV, SV };
p.set_definition(rep, mem, 2, vars, mem_body);
xV = m.mk_var(4, s);
yV = m.mk_var(3, s);
SV = m.mk_var(2, listS);
vV = m.mk_var(1, s);
wV = m.mk_var(0, s);
expr* y = yV, *v = vV, *w = wV;
x = xV, S = SV;
expr_ref ST(m.mk_app(pair, S, T), m);
expr_ref SF(m.mk_app(pair, S, F), m);
expr_ref connected_body(m);
connected_body =
m.mk_ite(m.mk_not(m.mk_eq(x, v)),
SF,
m.mk_ite(m.mk_eq(y, w),
ST,
m.mk_ite(m.mk_app(memf, w, S),
SF,
m.mk_app(conn2, w, y, m.mk_app(cons, w, S)))));
var* vars2[5] = { xV, yV, SV, vV, wV };
p.set_definition(rep, c1, 5, vars2, connected_body);
xV = m.mk_var(2, s);
yV = m.mk_var(1, s);
SV = m.mk_var(0, listS);
x = xV, y = yV, S = SV;
ST = m.mk_app(pair, S, T);
SF = m.mk_app(pair, S, F);
expr_ref connected_rec_body(m);
connected_rec_body = SF;
for (atom* ap : r.m_asserted_atoms) {
atom& a = *ap;
if (!a.phase()) continue;
SASSERT(ctx.get_assignment(a.var()) == l_true);
expr* n1 = get_enode(a.v1())->get_root()->get_owner();
expr* n2 = get_enode(a.v2())->get_root()->get_owner();
expr* Sr = connected_rec_body;
expr* args[5] = { x, y, m.mk_app(fst, Sr), n1, n2};
expr* Sc = m.mk_app(conn1, 5, args);
connected_rec_body = m.mk_ite(m.mk_app(snd, Sr), ST, Sc);
}
var* vars3[3] = { xV, yV, SV };
p.set_definition(rep, c2, 3, vars3, connected_rec_body);
// r.m_decl(x,y) -> snd(connected2(x,y,nil))
xV = m.mk_var(0, s);
yV = m.mk_var(1, s);
x = xV, y = yV;
func_interp* fi = alloc(func_interp, m, 2);
fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, x, m.mk_const(nil)))));
mg.get_model().register_decl(r.decl(), fi);
}
/**
\brief map each node to an interval of numbers, such that
the children are proper sub-intervals.
Then the <= relation becomes interval containment.
1. For each vertex, count the number of nodes below it in the transitive closure.
Store the result in num_children.
2. Identify each root.
3. Process children, assigning unique (and disjoint) intervals.
4. Extract interpretation.
*/
void theory_special_relations::init_model_to(relation& r, model_generator& mg) {
unsigned_vector num_children, lo, hi;
graph const& g = r.m_graph;
r.push();
ensure_strict(r.m_graph);
ensure_tree(r.m_graph);
count_children(g, num_children);
assign_interval(g, num_children, lo, hi);
expr_ref iv = mk_interval(r, mg, lo, hi);
r.pop(1);
func_interp* fi = alloc(func_interp, get_manager(), 2);
fi->set_else(iv);
mg.get_model().register_decl(r.decl(), fi);
}
bool theory_special_relations::is_neighbour_edge(graph const& g, edge_id edge) const {
CTRACE("special_relations_verbose", g.is_enabled(edge),
tout << edge << ": " << g.get_source(edge) << " " << g.get_target(edge) << " ";
tout << (g.get_assignment(g.get_target(edge)) - g.get_assignment(g.get_source(edge))) << "\n";);
return
g.is_enabled(edge) &&
g.get_assignment(g.get_source(edge)) + s_integer(1) == g.get_assignment(g.get_target(edge));
}
bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const {
return is_neighbour_edge(g, e) && g.get_weight(e) != s_integer(0);
}
void theory_special_relations::count_children(graph const& g, unsigned_vector& num_children) {
unsigned sz = g.get_num_nodes();
svector<dl_var> nodes;
num_children.resize(sz, 0);
svector<bool> processed(sz, false);
for (unsigned i = 0; i < sz; ++i) nodes.push_back(i);
while (!nodes.empty()) {
dl_var v = nodes.back();
if (processed[v]) {
nodes.pop_back();
continue;
}
unsigned nc = 1;
bool all_p = true;
for (edge_id e : g.get_out_edges(v)) {
if (is_strict_neighbour_edge(g, e)) {
dl_var dst = g.get_target(e);
TRACE("special_relations", tout << v << " -> " << dst << "\n";);
if (!processed[dst]) {
all_p = false;
nodes.push_back(dst);
}
nc += num_children[dst];
}
}
if (all_p) {
nodes.pop_back();
num_children[v] = nc;
processed[v] = true;
}
}
TRACE("special_relations",
for (unsigned i = 0; i < sz; ++i) {
tout << i << ": " << num_children[i] << "\n";
});
}
void theory_special_relations::assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi) {
svector<dl_var> nodes;
unsigned sz = g.get_num_nodes();
lo.resize(sz, 0);
hi.resize(sz, 0);
unsigned offset = 0;
for (unsigned i = 0; i < sz; ++i) {
bool is_root = true;
int_vector const& edges = g.get_in_edges(i);
for (edge_id e_id : edges) {
is_root &= !g.is_enabled(e_id);
}
if (is_root) {
lo[i] = offset;
hi[i] = offset + num_children[i] - 1;
offset = hi[i] + 1;
nodes.push_back(i);
}
}
while (!nodes.empty()) {
dl_var v = nodes.back();
int_vector const& edges = g.get_out_edges(v);
unsigned l = lo[v];
unsigned h = hi[v];
(void)h;
nodes.pop_back();
for (unsigned i = 0; i < edges.size(); ++i) {
SASSERT(l <= h);
if (is_strict_neighbour_edge(g, edges[i])) {
dl_var dst = g.get_target(edges[i]);
lo[dst] = l;
hi[dst] = l + num_children[dst] - 1;
l = hi[dst] + 1;
nodes.push_back(dst);
}
}
SASSERT(l == h);
}
}
void theory_special_relations::init_model(model_generator & m) {
for (auto const& kv : m_relations) {
switch (kv.m_value->m_property) {
case sr_lo:
init_model_lo(*kv.m_value, m);
break;
case sr_plo:
init_model_plo(*kv.m_value, m);
break;
case sr_to:
init_model_to(*kv.m_value, m);
break;
case sr_po:
init_model_po(*kv.m_value, m);
break;
default:
// other 28 combinations of 0x1F
NOT_IMPLEMENTED_YET();
}
}
}
void theory_special_relations::display(std::ostream & out) const {
if (m_relations.empty()) return;
out << "Theory Special Relations\n";
display_var2enode(out);
for (auto const& kv : m_relations) {
kv.m_value->display(*this, out);
}
}
void theory_special_relations::collect_asserted_po_atoms(vector<std::pair<bool_var, bool>>& atoms) const {
for (auto const& kv : m_relations) {
relation& r = *kv.m_value;
if (r.m_property != sr_po) continue;
for (atom* ap : r.m_asserted_atoms) {
atoms.push_back(std::make_pair(ap->var(), ap->phase()));
}
}
}
void theory_special_relations::display_atom(std::ostream & out, atom& a) const {
context& ctx = get_context();
expr* e = ctx.bool_var2expr(a.var());
out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n";
}
}

199
src/smt/theory_special_relations.h Normal file
View file

@ -0,0 +1,199 @@
/*++
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

2
src/tactic/core/CMakeLists.txt
View file

@ -19,6 +19,7 @@ z3_add_component(core_tactics
reduce_invertible_tactic.cpp
simplify_tactic.cpp
solve_eqs_tactic.cpp
special_relations_tactic.cpp
split_clause_tactic.cpp
symmetry_reduce_tactic.cpp
tseitin_cnf_tactic.cpp
@ -46,6 +47,7 @@ z3_add_component(core_tactics
reduce_invertible_tactic.h
simplify_tactic.h
solve_eqs_tactic.h
special_relations_tactic.h
split_clause_tactic.h
symmetry_reduce_tactic.h
tseitin_cnf_tactic.h

182
src/tactic/core/special_relations_tactic.cpp Normal file
View file

@ -0,0 +1,182 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
special_relations_tactic.cpp
Abstract:
Detect special relations in an axiomatization,
rewrite goal using special relations.
Author:
Nikolaj Bjorner (nbjorner) 2019-03-28
Notes:
--*/
#include "tactic/core/special_relations_tactic.h"
#include "ast/rewriter/func_decl_replace.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
void special_relations_tactic::collect_feature(goal const& g, unsigned idx,
obj_map<func_decl, sp_axioms>& goal_features) {
expr* f = g.form(idx);
func_decl_ref p(m);
if (!is_quantifier(f)) return;
unsigned index = 0;
app_ref_vector patterns(m);
bool is_match = m_pm.match_quantifier_index(to_quantifier(f), patterns, index);
TRACE("special_relations", tout << "check " << is_match << " " << mk_pp(f, m) << "\n";
if (is_match) tout << patterns << " " << index << "\n";);
if (is_match) {
p = to_app(patterns.get(0)->get_arg(0))->get_decl();
insert(goal_features, p, idx, m_properties[index]);
}
}
void special_relations_tactic::insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* f, unsigned idx, sr_property p) {
sp_axioms ax;
goal_features.find(f, ax);
ax.m_goal_indices.push_back(idx);
ax.m_sp_features = (sr_property)(p | ax.m_sp_features);
goal_features.insert(f, ax);
}
void special_relations_tactic::initialize() {
if (!m_properties.empty()) return;
sort_ref A(m.mk_uninterpreted_sort(symbol("A")), m);
func_decl_ref R(m.mk_func_decl(symbol("?R"), A, A, m.mk_bool_sort()), m);
var_ref x(m.mk_var(0, A), m);
var_ref y(m.mk_var(1, A), m);
var_ref z(m.mk_var(2, A), m);
expr* _x = x, *_y = y, *_z = z;
expr_ref Rxy(m.mk_app(R, _x, y), m);
expr_ref Ryz(m.mk_app(R, _y, z), m);
expr_ref Rxz(m.mk_app(R, _x, z), m);
expr_ref Rxx(m.mk_app(R, _x, x), m);
expr_ref Ryx(m.mk_app(R, _y, x), m);
expr_ref Rzy(m.mk_app(R, _z, y), m);
expr_ref Rzx(m.mk_app(R, _z, x), m);
expr_ref nRxy(m.mk_not(Rxy), m);
expr_ref nRyx(m.mk_not(Ryx), m);
expr_ref nRzx(m.mk_not(Rzx), m);
expr_ref nRxz(m.mk_not(Rxz), m);
sort* As[3] = { A, A, A};
symbol xyz[3] = { symbol("x"), symbol("y"), symbol("z") };
expr_ref fml(m);
quantifier_ref q(m);
expr_ref pat(m.mk_pattern(to_app(Rxy)), m);
expr_ref pat0(m.mk_pattern(to_app(Rxx)), m);
expr* pats[1] = { pat };
expr* pats0[1] = { pat0 };
fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = m.mk_or(not(Rxy & Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = Rxx;
q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats0);
register_pattern(m_pm.initialize(q), sr_reflexive);
fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(not(Rxy & Ryx), m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(nRyx, nRzx, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(not (Ryx & Rzx), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_lefttree);
fml = m.mk_or(nRxy, nRxz, Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(not(Rxy & Rxz), Ryz, Rzy);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_righttree);
fml = m.mk_or(Rxy, Ryx);
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_total);
TRACE("special_relations", m_pm.display(tout););
}
void special_relations_tactic::register_pattern(unsigned index, sr_property p) {
SASSERT(index == m_properties.size());
m_properties.push_back(p);
}
void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) {
tactic_report report("special_relations", *g);
initialize();
obj_map<func_decl, sp_axioms> goal_features;
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
collect_feature(*g, idx, goal_features);
}
special_relations_util u(m);
func_decl_replace replace(m);
unsigned_vector to_delete;
for(auto const& kv : goal_features) {
func_decl* sp = nullptr;
sr_property feature = kv.m_value.m_sp_features;
switch (feature) {
case sr_po:
replace.insert(kv.m_key, u.mk_po_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_to:
replace.insert(kv.m_key, u.mk_to_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_plo:
replace.insert(kv.m_key, u.mk_plo_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
case sr_lo:
replace.insert(kv.m_key, u.mk_lo_decl(kv.m_key));
to_delete.append(kv.m_value.m_goal_indices);
break;
default:
TRACE("special_relations", tout << "unprocessed feature " << feature << "\n";);
break;
}
}
if (!replace.empty()) {
for (unsigned idx = 0; idx < size; idx++) {
if (to_delete.contains(idx)) {
g->update(idx, m.mk_true());
}
else {
expr_ref new_f = replace(g->form(idx));
g->update(idx, new_f);
}
}
g->elim_true();
}
g->inc_depth();
result.push_back(g.get());
}
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) {
return alloc(special_relations_tactic, m, p);
}

72
src/tactic/core/special_relations_tactic.h Normal file
View file

@ -0,0 +1,72 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
special_relations_tactic.h
Abstract:
Detect special relations in an axiomatization,
rewrite goal using special relations.
Author:
Nikolaj Bjorner (nbjorner) 2019-03-28
Notes:
--*/
#ifndef SPECIAL_RELATIONS_TACTIC_H_
#define SPECIAL_RELATIONS_TACTIC_H_
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/pattern/expr_pattern_match.h"
class special_relations_tactic : public tactic {
ast_manager& m;
params_ref m_params;
expr_pattern_match m_pm;
svector<sr_property> m_properties;
struct sp_axioms {
unsigned_vector m_goal_indices;
sr_property m_sp_features;
sp_axioms():m_sp_features(sr_none) {}
};
void collect_feature(goal const& g, unsigned idx, obj_map<func_decl, sp_axioms>& goal_features);
void insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* f, unsigned idx, sr_property p);
void initialize();
void register_pattern(unsigned index, sr_property);
public:
special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()):
m(m), m_params(ref), m_pm(m) {}
~special_relations_tactic() override {}
void updt_params(params_ref const & p) override { m_params = p; }
void collect_param_descrs(param_descrs & r) override { }
void operator()(goal_ref const & in, goal_ref_buffer & result) override;
void cleanup() override {}
tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }
};
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("special-relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)")
*/
#endif