mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
add sr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
deb48bffe1
commit
876aa01167
|
@ -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
|
||||
|
|
79
src/ast/special_relations_decl_plugin.cpp
Normal file
79
src/ast/special_relations_decl_plugin.cpp
Normal file
|
@ -0,0 +1,79 @@
|
|||
/*++
|
||||
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.h"
|
||||
#include"special_relations_decl_plugin.h"
|
||||
|
||||
|
||||
|
||||
special_relations_decl_plugin::special_relations_decl_plugin():
|
||||
m_lo("linear-order"),
|
||||
m_po("partial-order"),
|
||||
m_po_ao("partial-order-already-ordered"),
|
||||
m_plo("piecewise-linear-order"),
|
||||
m_to("tree-order")
|
||||
{}
|
||||
|
||||
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 0;
|
||||
}
|
||||
if (domain[0] != domain[1]) {
|
||||
m_manager->raise_exception("argument sort missmatch");
|
||||
return 0;
|
||||
}
|
||||
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_PO_AO: name = m_po_ao; break;
|
||||
case OP_SPECIAL_RELATION_LO: name = m_lo; break;
|
||||
case OP_SPECIAL_RELATION_PLO: name = m_plo; break;
|
||||
case OP_SPECIAL_RELATION_TO: name = m_to; break;
|
||||
}
|
||||
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_po_ao.bare_str(), OP_SPECIAL_RELATION_PO_AO));
|
||||
op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
|
||||
op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
|
||||
op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
|
||||
}
|
||||
}
|
||||
|
||||
sr_property special_relations_util::get_property(func_decl* f) const {
|
||||
switch (f->get_decl_kind()) {
|
||||
case OP_SPECIAL_RELATION_PO: return sr_po;
|
||||
case OP_SPECIAL_RELATION_PO_AO: return sr_po; // still partial ordered
|
||||
case OP_SPECIAL_RELATION_LO: return sr_lo;
|
||||
case OP_SPECIAL_RELATION_PLO: return sr_plo;
|
||||
case OP_SPECIAL_RELATION_TO: return sr_to;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return sr_po;
|
||||
}
|
||||
}
|
97
src/ast/special_relations_decl_plugin.h
Normal file
97
src/ast/special_relations_decl_plugin.h
Normal file
|
@ -0,0 +1,97 @@
|
|||
/*++
|
||||
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.h"
|
||||
|
||||
|
||||
|
||||
enum special_relations_op_kind {
|
||||
OP_SPECIAL_RELATION_LO,
|
||||
OP_SPECIAL_RELATION_PO,
|
||||
OP_SPECIAL_RELATION_PO_AO,
|
||||
OP_SPECIAL_RELATION_PLO,
|
||||
OP_SPECIAL_RELATION_TO,
|
||||
LAST_SPECIAL_RELATIONS_OP
|
||||
};
|
||||
|
||||
class special_relations_decl_plugin : public decl_plugin {
|
||||
symbol m_lo;
|
||||
symbol m_po;
|
||||
symbol m_po_ao;
|
||||
symbol m_plo;
|
||||
symbol m_to;
|
||||
public:
|
||||
special_relations_decl_plugin();
|
||||
virtual ~special_relations_decl_plugin() {}
|
||||
|
||||
virtual decl_plugin * mk_fresh() {
|
||||
return alloc(special_relations_decl_plugin);
|
||||
}
|
||||
|
||||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
||||
|
||||
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { return 0; }
|
||||
};
|
||||
|
||||
enum sr_property {
|
||||
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_po = 0x01 | 0x02 | 0x04, // partial order
|
||||
sr_lo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // linear order
|
||||
sr_plo = 0x01 | 0x02 | 0x04 | 0x20, // piecewise linear order
|
||||
sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree
|
||||
};
|
||||
|
||||
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()); }
|
||||
|
||||
bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); }
|
||||
bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); }
|
||||
bool is_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); }
|
||||
bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); }
|
||||
bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); }
|
||||
|
||||
app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); }
|
||||
app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); }
|
||||
app * mk_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, arg1, arg2); }
|
||||
app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); }
|
||||
app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); }
|
||||
|
||||
};
|
||||
|
||||
|
||||
#endif /* SPECIAL_RELATIONS_DECL_PLUGIN_H_ */
|
|
@ -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
|
||||
|
|
|
@ -296,6 +296,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.
|
||||
|
@ -661,6 +664,113 @@ 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;
|
||||
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;
|
||||
int_vector bfs_todo;
|
||||
int_vector dfs_todo;
|
||||
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 ((gamma.is_one() || (!zero_edge && gamma.is_neg()))
|
||||
&& e.get_timestamp() < timestamp) {
|
||||
dl_var curr_target = e.get_target();
|
||||
if (curr_target == target) {
|
||||
f(e.get_explanation());
|
||||
m_freq_hybrid[e_id]++;
|
||||
for (;;) {
|
||||
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.
|
||||
|
@ -1274,8 +1384,22 @@ 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_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
|
||||
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;
|
||||
bfs_mark.resize(m_assignment.size(), false);
|
||||
|
@ -1292,10 +1416,7 @@ public:
|
|||
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()) {
|
||||
|
@ -1303,7 +1424,8 @@ public:
|
|||
}
|
||||
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) {
|
||||
if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp) {
|
||||
// if (gamma.is_zero() && e.get_timestamp() < 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";);
|
||||
|
@ -1477,11 +1599,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 +1687,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());
|
||||
|
|
905
src/smt/theory_special_relations.cpp
Normal file
905
src/smt/theory_special_relations.cpp
Normal file
|
@ -0,0 +1,905 @@
|
|||
/*++
|
||||
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/ast_pp.h"
|
||||
|
||||
static constexpr bool KVEC = false;
|
||||
static constexpr bool HYBRID_SEARCH = false;
|
||||
|
||||
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;
|
||||
if (!KVEC) {
|
||||
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);
|
||||
if (!KVEC) {
|
||||
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.enable_edge(m_graph.add_edge(v1, v2, s_integer(1), ls)) &&
|
||||
m_graph.enable_edge(m_graph.add_edge(v2, v1, s_integer(1), ls));
|
||||
}
|
||||
|
||||
theory_special_relations::theory_special_relations(ast_manager& m):
|
||||
theory(m.mk_family_id("special_relations")),
|
||||
m_util(m), m_autil(m) {
|
||||
params_ref params;
|
||||
params.set_bool("model", true);
|
||||
params.set_bool("unsat_core", true);
|
||||
m_nested_solver = mk_smt_solver(m, params, symbol("QF_LRA"));
|
||||
m_int_sort = m_autil.mk_real();
|
||||
}
|
||||
|
||||
theory_special_relations::~theory_special_relations() {
|
||||
reset_eh();
|
||||
m_nested_solver = nullptr;
|
||||
}
|
||||
|
||||
theory * theory_special_relations::mk_fresh(context * new_ctx) {
|
||||
return alloc(theory_special_relations, new_ctx->get_manager());
|
||||
}
|
||||
|
||||
static void populate_k_vars(int v, int k, u_map<ptr_vector<expr>>& map, int& curr_id, ast_manager& m, sort** int_sort) {
|
||||
int need = !map.contains(v) ? k : k - map[v].size();
|
||||
for (auto i = 0; i < need; ++i) {
|
||||
auto *fd = m.mk_func_decl(symbol(curr_id++), 0, int_sort, *int_sort);
|
||||
map[v].push_back(m.mk_app(fd, unsigned(0), nullptr));
|
||||
}
|
||||
}
|
||||
|
||||
bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) {
|
||||
TRACE("special_relations", tout << mk_pp(atm, get_manager()) << "\n";);
|
||||
SASSERT(m_util.is_special_relation(atm));
|
||||
relation* r = 0;
|
||||
if (!m_relations.find(atm->get_decl(), r)) {
|
||||
//todo: push pop may get misaligned if the following alloc happens after push
|
||||
r = alloc(relation, m_util.get_property(atm), atm->get_decl());
|
||||
m_relations.insert(atm->get_decl(), r);
|
||||
}
|
||||
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);
|
||||
//std::cerr << "INTER : " << a->v1() << ' ' << 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_ref eq(get_manager());
|
||||
app* t1 = get_enode(v1)->get_owner();
|
||||
app* t2 = get_enode(v2)->get_owner();
|
||||
eq = get_manager().mk_eq(t1, t2);
|
||||
VERIFY(internalize_atom(eq, false));
|
||||
literal l(ctx.get_literal(eq));
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; !ctx.inconsistent() && it != end; ++it) {
|
||||
relation& r = *it->m_value;
|
||||
if (!r.new_eq_eh(l, v1, v2)) {
|
||||
set_neg_cycle_conflict(r);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
final_check_status theory_special_relations::final_check_eh() {
|
||||
TRACE("special_relations", tout << "\n";);
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
lbool r = l_true;
|
||||
for (; it != end && r == l_true; ++it) {
|
||||
r = final_check(*it->m_value);
|
||||
}
|
||||
switch (r) {
|
||||
case l_undef:
|
||||
return FC_GIVEUP;
|
||||
case l_false:
|
||||
return FC_CONTINUE;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
it = m_relations.begin();
|
||||
bool new_equality = false;
|
||||
for (; it != end; ++it) {
|
||||
if (extract_equalities(*it->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());
|
||||
context& ctx = get_context();
|
||||
ensure_enode(e);
|
||||
return ctx.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;
|
||||
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())) {
|
||||
target.reset();
|
||||
theory_var w;
|
||||
// v2 !<= v1 is asserted
|
||||
target.insert(a.v2());
|
||||
if (r.m_graph.reachable(a.v1(), visited, target, w)) {
|
||||
// we already have v1 <= v2
|
||||
continue;
|
||||
}
|
||||
target.reset();
|
||||
if (r.m_graph.reachable(a.v2(), target, visited, w)) {
|
||||
// there is a common successor
|
||||
// v1 <= w
|
||||
// v2 <= w
|
||||
// v1 !<= v2
|
||||
// -> 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.enable_edge(r.m_graph.add_edge(a.v2(), a.v1(), s_integer(0), lits))) {
|
||||
set_neg_cycle_conflict(r);
|
||||
res = l_false;
|
||||
}
|
||||
}
|
||||
// TODO: check if algorithm correctly produces all constraints.
|
||||
// e.g., if we add an edge, do we have to repeat the loop?
|
||||
//
|
||||
}
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
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) {
|
||||
// timer m_timer_fc; //for debugging
|
||||
// static unsigned call_count = 0;
|
||||
// static double total_call_times = 0.0;
|
||||
// m_timer_fc.start();
|
||||
// call_count++;
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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; 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) {
|
||||
if (!KVEC) {
|
||||
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())) {
|
||||
// v1 !-> v2
|
||||
// find v1 -> v3 -> v4 -> v2 path
|
||||
r.m_explanation.reset();
|
||||
unsigned timestamp = r.m_graph.get_timestamp();
|
||||
auto found_path = HYBRID_SEARCH ?
|
||||
r.m_graph.find_path(a.v1(), a.v2(), timestamp, r) :
|
||||
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);
|
||||
res = l_false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return res;
|
||||
}
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = ctx.get_manager();
|
||||
|
||||
ptr_vector<expr> assumptions;
|
||||
ptr_vector<expr> literals;
|
||||
|
||||
int k = 1;
|
||||
static int curr_id = 100000;
|
||||
|
||||
u_map<ptr_vector<expr>> map;
|
||||
lbool res = l_true;
|
||||
for (atom * ap : r.m_asserted_atoms) {
|
||||
if (res != l_true) break;
|
||||
atom a = *ap;
|
||||
if (a.phase()) {
|
||||
continue;
|
||||
// assumptions.push_back(b);
|
||||
r.m_uf.merge(a.v1(), a.v2());
|
||||
}
|
||||
}
|
||||
for (atom * ap : r.m_asserted_atoms) {
|
||||
if (res != l_true) break;
|
||||
atom a = *ap;
|
||||
if (a.phase())
|
||||
continue;
|
||||
if (r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) {
|
||||
continue;
|
||||
}
|
||||
populate_k_vars(a.v1(), k, map, curr_id, m, &m_int_sort);
|
||||
populate_k_vars(a.v2(), k, map, curr_id, m, &m_int_sort);
|
||||
|
||||
literals.push_back(m_autil.mk_lt(map[a.v1()][0], map[a.v2()][0]));
|
||||
|
||||
auto bool_sort = m.mk_bool_sort();
|
||||
auto b_func = m.mk_func_decl(symbol(curr_id++), 0, &bool_sort, bool_sort);
|
||||
auto b = m.mk_app(b_func, unsigned(0), nullptr);
|
||||
|
||||
auto f = m.mk_implies( b, m.mk_not(literals.back()) );
|
||||
m_nested_solver->assert_expr(f);
|
||||
atom_cache.insert(b->get_id(), &a);
|
||||
assumptions.push_back(b);
|
||||
r.m_explanation.reset();
|
||||
if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
|
||||
expr_ref_vector unsat_core(m);
|
||||
m_nested_solver->get_unsat_core(unsat_core);
|
||||
for (expr* e : unsat_core) {
|
||||
atom& a = *atom_cache[e->get_id()];
|
||||
r.m_explanation.push_back(a.explanation());
|
||||
}
|
||||
for (auto e : r.m_explanation) {
|
||||
std::cerr << "EX " << e.hash() << "\n";
|
||||
}
|
||||
set_conflict(r);
|
||||
res = l_false;
|
||||
}
|
||||
assumptions.pop_back();
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
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() {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->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 = 0;
|
||||
VERIFY(m_bool_var2atom.find(v, a));
|
||||
a->set_phase(is_true);
|
||||
a->get_relation().m_asserted_atoms.push_back(a);
|
||||
//std::cerr << "ASSIGN: " << a->v1() << ' ' << a->v2() << "\n";
|
||||
}
|
||||
|
||||
void theory_special_relations::push_scope_eh() {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
it->m_value->push();
|
||||
}
|
||||
m_atoms_lim.push_back(m_atoms.size());
|
||||
}
|
||||
|
||||
void theory_special_relations::pop_scope_eh(unsigned num_scopes) {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
it->m_value->pop(num_scopes);
|
||||
}
|
||||
unsigned new_lvl = m_atoms_lim.size() - num_scopes;
|
||||
del_atoms(m_atoms_lim[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 {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
it->m_value->m_graph.collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
model_value_proc * theory_special_relations::mk_value(enode * n, model_generator & mg) {
|
||||
UNREACHABLE();
|
||||
return 0;
|
||||
}
|
||||
|
||||
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.enable_edge(g.add_edge(src, dst, s_integer(-2), 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()) continue;
|
||||
if (!disconnected(g, src1, src2)) continue;
|
||||
VERIFY(g.enable_edge(g.add_edge(src1, src2, s_integer(-2), 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;
|
||||
}
|
||||
int_vector const& edges = g.get_out_edges(u);
|
||||
for (unsigned i = 0; i < edges.size(); ++i) {
|
||||
edge_id e = edges[i];
|
||||
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) {
|
||||
// context& ctx = get_context();
|
||||
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) {
|
||||
//context& ctx = get_context();
|
||||
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;
|
||||
//context& ctx = get_context();
|
||||
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& m) {
|
||||
expr_ref inj = mk_inj(r, m);
|
||||
expr_ref cls = mk_class(r, m);
|
||||
func_interp* fi = alloc(func_interp, get_manager(), 2);
|
||||
fi->set_else(get_manager().mk_and(inj, cls));
|
||||
m.get_model().register_decl(r.decl(), fi);
|
||||
}
|
||||
|
||||
void theory_special_relations::init_model_po(relation& r, model_generator& mg) {
|
||||
// NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
/**
|
||||
\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_source(edge)) - g.get_assignment(g.get_target(edge))) << "\n";);
|
||||
|
||||
return
|
||||
g.is_enabled(edge) &&
|
||||
g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge)) == s_integer(1);
|
||||
}
|
||||
|
||||
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;
|
||||
int_vector const& edges = g.get_out_edges(v);
|
||||
for (unsigned i = 0; i < edges.size(); ++i) {
|
||||
edge_id e = edges[i];
|
||||
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 (unsigned j = 0; is_root && j < edges.size(); ++j) {
|
||||
is_root = !g.is_enabled(edges[j]);
|
||||
}
|
||||
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) {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
switch (it->m_value->m_property) {
|
||||
case sr_lo:
|
||||
init_model_lo(*it->m_value, m);
|
||||
break;
|
||||
case sr_plo:
|
||||
init_model_plo(*it->m_value, m);
|
||||
break;
|
||||
case sr_to:
|
||||
init_model_to(*it->m_value, m);
|
||||
break;
|
||||
case sr_po:
|
||||
init_model_po(*it->m_value, m);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE(); //ASHU: added to remove warning! Should be supported!
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_special_relations::display(std::ostream & out) const {
|
||||
if (m_relations.empty()) return;
|
||||
out << "Theory Special Relations\n";
|
||||
display_var2enode(out);
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
out << mk_pp(it->m_value->decl(), get_manager()) << ":\n";
|
||||
it->m_value->m_graph.display(out);
|
||||
it->m_value->m_uf.display(out);
|
||||
for (unsigned i = 0; i < it->m_value->m_asserted_atoms.size(); ++i){
|
||||
atom& a = *it->m_value->m_asserted_atoms[i];
|
||||
display_atom( out, a );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_special_relations::collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const {
|
||||
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
|
||||
for (; it != end; ++it) {
|
||||
relation& r = *(it->m_value );
|
||||
if( r.m_property != sr_po ) continue;
|
||||
// SASSERT( r.m_asserted_qhead == r.m_asserted_atoms.size() );
|
||||
for (unsigned i = 0; i < r.m_asserted_atoms.size(); ++i) {
|
||||
atom& a = *r.m_asserted_atoms[i];
|
||||
atoms.push_back( std::make_pair(a.var(),a.phase()) );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_special_relations::display_atom( std::ostream & out, atom& a ) const {
|
||||
context& ctx = get_context();
|
||||
expr* e = ctx.bool_var2expr( a.var() );
|
||||
if( !a.phase() ) out << "(not ";
|
||||
out << mk_pp( e, get_manager());
|
||||
if( !a.phase() ) out << ")";
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
void theory_special_relations::display_atom( atom& a) const {
|
||||
display_atom( std::cerr, a);
|
||||
}
|
||||
|
||||
}
|
198
src/smt/theory_special_relations.h
Normal file
198
src/smt/theory_special_relations.h
Normal file
|
@ -0,0 +1,198 @@
|
|||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_special_relations.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Special Relations theory plugin.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2015-9-16
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast/special_relations_decl_plugin.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/theory_diff_logic.h"
|
||||
#include "util/union_find.h"
|
||||
#include "solver/solver.h"
|
||||
|
||||
#ifndef THEORY_SPECIAL_RELATIONS_H_
|
||||
#define THEORY_SPECIAL_RELATIONS_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(1), ls); // v2 <= v1
|
||||
ls[0] = literal(b, true);
|
||||
m_neg = r.m_graph.add_edge(v2, v1, s_integer(-2), ls); // v1 <= v2 - 1
|
||||
}
|
||||
bool_var var() const { return m_bvar;}
|
||||
relation& get_relation() const { return m_relation; }
|
||||
bool phase() { return m_phase; }
|
||||
void set_phase(bool b) { m_phase = b; }
|
||||
theory_var v1() { return m_v1; }
|
||||
theory_var v2() { return m_v2; }
|
||||
literal explanation() { 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;
|
||||
};
|
||||
typedef dl_graph<int_ext> graph;
|
||||
|
||||
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) {}
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
typedef u_map<atom*> bool_var2atom;
|
||||
|
||||
special_relations_util m_util;
|
||||
arith_util m_autil;
|
||||
|
||||
atoms m_atoms;
|
||||
unsigned_vector m_atoms_lim;
|
||||
obj_map<func_decl, relation*> m_relations;
|
||||
bool_var2atom m_bool_var2atom;
|
||||
|
||||
scoped_ptr<solver> m_nested_solver;
|
||||
struct atom_hash {
|
||||
size_t operator()(atom a) const {
|
||||
return std::hash<int>()(a.v1()) ^ std::hash<int>()(a.v2()) ^ std::hash<bool>()(a.phase());
|
||||
}
|
||||
};
|
||||
u_map<expr*> expr_cache;
|
||||
u_map<atom*> atom_cache;
|
||||
sort* m_int_sort;
|
||||
|
||||
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); //ASHU: added to modify po solving
|
||||
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;
|
||||
|
||||
public:
|
||||
theory_special_relations(ast_manager& m);
|
||||
virtual ~theory_special_relations();
|
||||
|
||||
virtual theory * mk_fresh(context * new_ctx);
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
virtual bool internalize_term(app * term) { UNREACHABLE(); return false; }
|
||||
virtual void new_eq_eh(theory_var v1, theory_var v2);
|
||||
virtual void new_diseq_eh(theory_var v1, theory_var v2) {}
|
||||
virtual bool use_diseqs() const { return false; }
|
||||
virtual bool build_models() const { return true; }
|
||||
virtual final_check_status final_check_eh();
|
||||
virtual void reset_eh();
|
||||
virtual void assign_eh(bool_var v, bool is_true);
|
||||
virtual void init_search_eh() {}
|
||||
virtual void push_scope_eh();
|
||||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
virtual void restart_eh() {}
|
||||
virtual void collect_statistics(::statistics & st) const;
|
||||
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
|
||||
virtual void init_model(model_generator & m);
|
||||
virtual bool can_propagate() { return false; }
|
||||
virtual void propagate() {}
|
||||
virtual void display(std::ostream & out) const;
|
||||
|
||||
literal mk_literal(expr* _e);
|
||||
enode* ensure_enode(expr* e);
|
||||
theory_var mk_var(enode* n);
|
||||
|
||||
//BEGIN: ASHU
|
||||
void collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const;
|
||||
void display_atom( std::ostream & out, atom& a) const;
|
||||
void display_atom( atom& a) const;
|
||||
//END: ASHU
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
Loading…
Reference in a new issue