mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
network update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
9467806a5c
commit
bd33e466c2
4 changed files with 578 additions and 137 deletions
|
|
@ -118,12 +118,16 @@ namespace smt {
|
|||
/**
|
||||
\brief find node that points to 'n' in m_thread
|
||||
*/
|
||||
node find_rev_thread(node n, node ancestor) const;
|
||||
node find_rev_thread(node n) const;
|
||||
|
||||
void fix_depth(node start, node end);
|
||||
|
||||
void swap_order(node q, node v);
|
||||
|
||||
bool check_well_formed();
|
||||
|
||||
bool is_preorder_traversal(node start, node end);
|
||||
|
||||
public:
|
||||
|
||||
network_flow(graph & g, vector<fin_numeral> const & balances);
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ Notes:
|
|||
#define _NETWORK_FLOW_DEF_H_
|
||||
|
||||
#include"network_flow.h"
|
||||
#include"uint_set.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -269,7 +270,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
template<typename Ext>
|
||||
dl_var network_flow<Ext>::find_rev_thread(node n, node ancestor) const {
|
||||
dl_var network_flow<Ext>::find_rev_thread(node n) const {
|
||||
node ancestor = m_pred[n];
|
||||
SASSERT(ancestor != -1);
|
||||
while (m_thread[ancestor] != n) {
|
||||
ancestor = m_thread[ancestor];
|
||||
}
|
||||
|
|
@ -279,21 +282,19 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void network_flow<Ext>::fix_depth(node start, node end) {
|
||||
SASSERT(m_pred[start] != -1);
|
||||
// Increase depths of all children in T_q by the same amount
|
||||
int d = 1 + m_depth[m_pred[start]] - m_depth[start];
|
||||
do {
|
||||
m_depth[start] += d;
|
||||
start = m_thread[start];
|
||||
m_depth[start] = m_depth[m_pred[start]]+1;
|
||||
while (start != end) {
|
||||
start = m_thread[start];
|
||||
m_depth[start] = m_depth[m_pred[start]]+1;
|
||||
}
|
||||
while (start != end);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief add entering_edge, remove leaving_edge from spanning tree.
|
||||
|
||||
Old tree:
|
||||
root
|
||||
/ \
|
||||
Old tree: New tree:
|
||||
root root
|
||||
/ \ / \
|
||||
x y
|
||||
/ \ / \
|
||||
u w'
|
||||
|
|
@ -304,9 +305,6 @@ namespace smt {
|
|||
\
|
||||
q
|
||||
|
||||
New tree:
|
||||
root
|
||||
/ \
|
||||
x y
|
||||
/ \ / \
|
||||
u w'
|
||||
|
|
@ -350,6 +348,7 @@ namespace smt {
|
|||
// Initialize m_upwards[q] = q_upwards
|
||||
|
||||
bool prev_upwards = q_upwards;
|
||||
#if 0
|
||||
for (node n = q, prev = p; n != u; ) {
|
||||
SASSERT(m_pred[n] != u || n == v); // the last processed node is v
|
||||
node next = m_pred[n];
|
||||
|
|
@ -360,96 +359,79 @@ namespace smt {
|
|||
n = next;
|
||||
SASSERT(n != -1);
|
||||
}
|
||||
#else
|
||||
node old_pred = m_pred[q];
|
||||
m_pred[q] = p;
|
||||
for (node n = q; n != u; ) {
|
||||
SASSERT(old_pred != u || n == v); // the last processed node is v
|
||||
SASSERT(-1 != m_pred[old_pred]);
|
||||
node next_old_pred = m_pred[old_pred];
|
||||
swap_order(n, old_pred);
|
||||
std::swap(m_upwards[n], prev_upwards);
|
||||
prev_upwards = !prev_upwards; // flip previous version of upwards.
|
||||
n = old_pred;
|
||||
old_pred = next_old_pred;
|
||||
}
|
||||
|
||||
// At this point m_pred and m_upwards have been updated.
|
||||
|
||||
TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards););
|
||||
#endif
|
||||
|
||||
|
||||
//
|
||||
node x = m_final[p];
|
||||
node y = m_thread[x];
|
||||
node z = m_final[q];
|
||||
|
||||
// ----
|
||||
// update m_final.
|
||||
|
||||
// Do this before updating data structures
|
||||
node gamma_p = m_pred[m_thread[m_final[p]]];
|
||||
node gamma_v = m_pred[m_thread[m_final[v]]];
|
||||
node theta = m_thread[m_final[v]];
|
||||
|
||||
// Check that f(u) is not in T_v
|
||||
bool found_final_u = false;
|
||||
for (node n = v; n != theta; n = m_thread[n]) {
|
||||
if (n == m_final[u]) {
|
||||
found_final_u = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
node phi = find_rev_thread(v, u);
|
||||
node delta = found_final_u ? phi : m_final[u];
|
||||
|
||||
TRACE("network_flow", tout << "Graft T_q and T_r'\n";);
|
||||
|
||||
for (node n = p; n != gamma_p && n != -1; n = m_pred[n]) {
|
||||
TRACE("network_flow", tout << "1: m_final[" << n << "] |-> " << z << "\n";);
|
||||
m_final[n] = z;
|
||||
}
|
||||
|
||||
//
|
||||
|
||||
m_thread[x] = q;
|
||||
m_thread[z] = y;
|
||||
// m_thread and m_final were updated.
|
||||
// update the depth.
|
||||
|
||||
fix_depth(q, m_final[q]);
|
||||
|
||||
TRACE("network_flow", tout << "Update T_r'\n";);
|
||||
|
||||
m_thread[phi] = theta;
|
||||
|
||||
for (node n = u; n != gamma_v && n != -1; n = m_pred[n]) {
|
||||
TRACE("network_flow", tout << "2: m_final[" << n << "] |-> " << delta << "\n";);
|
||||
m_final[n] = delta;
|
||||
}
|
||||
|
||||
TRACE("network_flow", tout << pp_vector("Last Successors", m_final, true) << pp_vector("Depths", m_depth););
|
||||
|
||||
if (v != q) {
|
||||
TRACE("network_flow", tout << "Reroot T_v at q\n";);
|
||||
|
||||
node alpha1, alpha2;
|
||||
node prev = q;
|
||||
for (node n = v; n != q && n != -1; n = m_pred[n]) {
|
||||
// Find all immediate successors of n
|
||||
node t1 = m_thread[n];
|
||||
node t2 = m_thread[m_final[t1]];
|
||||
node t3 = m_thread[m_final[t2]];
|
||||
if (t1 == m_pred[n]) {
|
||||
alpha1 = t2;
|
||||
alpha2 = t3;
|
||||
}
|
||||
else if (t2 == m_pred[n]) {
|
||||
alpha1 = t1;
|
||||
alpha2 = t3;
|
||||
}
|
||||
else {
|
||||
alpha1 = t1;
|
||||
alpha2 = t2;
|
||||
}
|
||||
m_thread[n] = alpha1;
|
||||
m_thread[m_final[alpha1]] = alpha2;
|
||||
m_thread[m_final[alpha2]] = prev;
|
||||
prev = n;
|
||||
}
|
||||
m_thread[m_final[q]] = prev;
|
||||
}
|
||||
|
||||
TRACE("network_flow", {
|
||||
tout << pp_vector("Threads", m_thread, true);
|
||||
});
|
||||
}
|
||||
|
||||
/**
|
||||
swap v and q in tree.
|
||||
- fixup m_final
|
||||
- fixup m_thread
|
||||
- fixup m_pred
|
||||
|
||||
Case 1: final(q) == final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next
|
||||
|
||||
Case 2: final(q) != final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next
|
||||
|
||||
*/
|
||||
|
||||
template<typename Ext>
|
||||
void network_flow<Ext>::swap_order(node q, node v) {
|
||||
SASSERT(q != v);
|
||||
SASSERT(m_pred[q] == v);
|
||||
SASSERT(is_preorder_traversal(v, m_final[v]));
|
||||
node prev = find_rev_thread(v);
|
||||
node final_q = m_final[q];
|
||||
node final_v = m_final[v];
|
||||
node next = m_thread[final_v];
|
||||
node alpha = find_rev_thread(q);
|
||||
|
||||
if (final_q == final_v) {
|
||||
m_thread[final_q] = v;
|
||||
m_thread[alpha] = next;
|
||||
m_final[q] = alpha;
|
||||
m_final[v] = alpha;
|
||||
}
|
||||
else {
|
||||
node beta = m_thread[final_q];
|
||||
m_thread[final_q] = v;
|
||||
m_thread[alpha] = beta;
|
||||
m_final[q] = final_v;
|
||||
}
|
||||
m_thread[prev] = q;
|
||||
m_pred[v] = q;
|
||||
SASSERT(is_preorder_traversal(q, m_final[q]));
|
||||
}
|
||||
|
||||
|
||||
template<typename Ext>
|
||||
std::string network_flow<Ext>::display_spanning_tree() {
|
||||
++m_step;;
|
||||
|
|
@ -595,7 +577,8 @@ namespace smt {
|
|||
Furthermore, the nodes linked in m_thread follows a
|
||||
depth-first traversal order.
|
||||
|
||||
m_final[n] is deepest most node in a sub-tree rooted at n.
|
||||
m_final[n] is the last node in depth-first traversal order,
|
||||
starting from n, that is still a child of n.
|
||||
|
||||
m_upwards direction of edge from i to m_pred[i] m_graph
|
||||
|
||||
|
|
@ -670,6 +653,118 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool network_flow<Ext>::is_preorder_traversal(node start, node end) {
|
||||
|
||||
// get children of start:
|
||||
uint_set children;
|
||||
children.insert(start);
|
||||
node root = m_pred.size()-1;
|
||||
for (int i = 0; i < root; ++i) {
|
||||
for (int j = 0; j < root; ++j) {
|
||||
if (children.contains(m_pred[j])) {
|
||||
children.insert(j);
|
||||
}
|
||||
}
|
||||
}
|
||||
// visit children using m_thread
|
||||
children.remove(start);
|
||||
do {
|
||||
start = m_thread[start];
|
||||
SASSERT(children.contains(start));
|
||||
children.remove(start);
|
||||
}
|
||||
while (start != end);
|
||||
SASSERT(children.empty());
|
||||
return true;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
|
||||
// At this point m_pred and m_upwards have been updated.
|
||||
|
||||
TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards););
|
||||
|
||||
|
||||
//
|
||||
node x = m_final[p];
|
||||
node y = m_thread[x];
|
||||
node z = m_final[q];
|
||||
|
||||
// ----
|
||||
// update m_final.
|
||||
|
||||
// Do this before updating data structures
|
||||
node gamma_p = m_pred[m_thread[m_final[p]]];
|
||||
node gamma_v = m_pred[m_thread[m_final[v]]];
|
||||
node theta = m_thread[m_final[v]];
|
||||
|
||||
// Check that f(u) is not in T_v
|
||||
bool found_final_u = false;
|
||||
for (node n = v; n != theta; n = m_thread[n]) {
|
||||
if (n == m_final[u]) {
|
||||
found_final_u = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
node phi = find_rev_thread(v);
|
||||
node delta = found_final_u ? phi : m_final[u];
|
||||
|
||||
TRACE("network_flow", tout << "Graft T_q and T_r'\n";);
|
||||
|
||||
for (node n = p; n != gamma_p && n != -1; n = m_pred[n]) {
|
||||
TRACE("network_flow", tout << "1: m_final[" << n << "] |-> " << z << "\n";);
|
||||
m_final[n] = z;
|
||||
}
|
||||
|
||||
//
|
||||
|
||||
m_thread[x] = q;
|
||||
m_thread[z] = y;
|
||||
|
||||
|
||||
TRACE("network_flow", tout << "Update T_r'\n";);
|
||||
|
||||
m_thread[phi] = theta;
|
||||
|
||||
for (node n = u; n != gamma_v && n != -1; n = m_pred[n]) {
|
||||
TRACE("network_flow", tout << "2: m_final[" << n << "] |-> " << delta << "\n";);
|
||||
m_final[n] = delta;
|
||||
}
|
||||
|
||||
TRACE("network_flow", tout << pp_vector("Last Successors", m_final, true) << pp_vector("Depths", m_depth););
|
||||
|
||||
if (v != q) {
|
||||
TRACE("network_flow", tout << "Reroot T_v at q\n";);
|
||||
|
||||
node alpha1, alpha2;
|
||||
node prev = q;
|
||||
for (node n = v; n != q && n != -1; n = m_pred[n]) {
|
||||
// Find all immediate successors of n
|
||||
node t1 = m_thread[n];
|
||||
node t2 = m_thread[m_final[t1]];
|
||||
node t3 = m_thread[m_final[t2]];
|
||||
if (t1 == m_pred[n]) {
|
||||
alpha1 = t2;
|
||||
alpha2 = t3;
|
||||
}
|
||||
else if (t2 == m_pred[n]) {
|
||||
alpha1 = t1;
|
||||
alpha2 = t3;
|
||||
}
|
||||
else {
|
||||
alpha1 = t1;
|
||||
alpha2 = t2;
|
||||
}
|
||||
m_thread[n] = alpha1;
|
||||
m_thread[m_final[alpha1]] = alpha2;
|
||||
m_thread[m_final[alpha2]] = prev;
|
||||
prev = n;
|
||||
}
|
||||
m_thread[m_final[q]] = prev;
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Notes:
|
|||
|
||||
#include "theory_card.h"
|
||||
#include "smt_context.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -46,33 +47,59 @@ namespace smt {
|
|||
unsigned num_args = atom->get_num_args();
|
||||
SASSERT(m_util.is_at_most_k(atom));
|
||||
unsigned k = m_util.get_k(atom);
|
||||
bool_var bv;
|
||||
|
||||
if (ctx.b_internalized(atom)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
TRACE("card", tout << "internalize: " << mk_pp(atom, m) << "\n";);
|
||||
|
||||
if (k >= atom->get_num_args()) {
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
if (k == 0) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
SASSERT(0 < k && k < atom->get_num_args());
|
||||
SASSERT(!ctx.b_internalized(atom));
|
||||
bv = ctx.mk_bool_var(atom);
|
||||
card* c = alloc(card, atom, bv, k);
|
||||
bool_var bv = ctx.mk_bool_var(atom);
|
||||
card* c = alloc(card, bv, k);
|
||||
add_card(c);
|
||||
//
|
||||
// TBD take repeated bv into account.
|
||||
// base case: throw exception.
|
||||
// refinement: adjust argument list and k for non-repeated values.
|
||||
//
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr* arg = atom->get_arg(i);
|
||||
if (!ctx.b_internalized(arg)) {
|
||||
bv = ctx.mk_bool_var(arg);
|
||||
ctx.internalize(arg, false);
|
||||
}
|
||||
else {
|
||||
|
||||
bool has_bv = false;
|
||||
if (!m.is_not(arg) && ctx.b_internalized(arg)) {
|
||||
bv = ctx.get_bool_var(arg);
|
||||
|
||||
if (null_theory_var == ctx.get_var_theory(bv)) {
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
has_bv = true;
|
||||
}
|
||||
else if (get_id() == ctx.get_var_theory(bv)) {
|
||||
has_bv = true;
|
||||
}
|
||||
}
|
||||
if (null_theory_var == ctx.get_var_theory(bv)) {
|
||||
// pre-processing should better remove negations under cardinality.
|
||||
// assumes relevancy level = 2 or 0.
|
||||
if (!has_bv) {
|
||||
expr_ref tmp(m), fml(m);
|
||||
tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort());
|
||||
fml = m.mk_iff(tmp, arg);
|
||||
ctx.internalize(fml, false);
|
||||
SASSERT(ctx.b_internalized(tmp));
|
||||
bv = ctx.get_bool_var(tmp);
|
||||
SASSERT(null_theory_var == ctx.get_var_theory(bv));
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
literal lit(ctx.get_bool_var(fml));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
ctx.mark_as_relevant(tmp);
|
||||
}
|
||||
else {
|
||||
SASSERT(ctx.get_var_theory(bv) == get_id()); // TBD, fishy
|
||||
}
|
||||
c->m_args.push_back(bv);
|
||||
add_watch(bv, c);
|
||||
}
|
||||
return true;
|
||||
|
|
@ -110,12 +137,15 @@ namespace smt {
|
|||
|
||||
void theory_card::assign_eh(bool_var v, bool is_true) {
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
ptr_vector<card>* cards = 0;
|
||||
card* c = 0;
|
||||
TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";);
|
||||
|
||||
if (m_watch.find(v, cards)) {
|
||||
for (unsigned i = 0; i < cards->size(); ++i) {
|
||||
c = (*cards)[i];
|
||||
app* atm = c->m_atom;
|
||||
svector<bool_var> const& args = c->m_args;
|
||||
//
|
||||
// is_true && m_t + 1 > k -> force false
|
||||
// !is_true && m_f + 1 >= arity - k -> force true
|
||||
|
|
@ -128,10 +158,9 @@ namespace smt {
|
|||
case l_undef: {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(c->m_bv));
|
||||
for (unsigned i = 0; i < atm->get_num_args() && lits.size() < k + 1; ++i) {
|
||||
expr* arg = atm->get_arg(i);
|
||||
if (ctx.get_assignment(arg) == l_true) {
|
||||
lits.push_back(~literal(ctx.get_bool_var(arg)));
|
||||
for (unsigned i = 0; i < args.size() && lits.size() < k + 1; ++i) {
|
||||
if (ctx.get_assignment(args[i]) == l_true) {
|
||||
lits.push_back(~literal(args[i]));
|
||||
}
|
||||
}
|
||||
SASSERT(lits.size() == k + 1);
|
||||
|
|
@ -142,17 +171,17 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
}
|
||||
else if (!is_true && c->m_k >= atm->get_num_args() - c->m_f) {
|
||||
else if (!is_true && c->m_k >= args.size() - c->m_f - 1) {
|
||||
// forced true
|
||||
switch (ctx.get_assignment(c->m_bv)) {
|
||||
case l_false:
|
||||
case l_undef: {
|
||||
unsigned deficit = args.size() - c->m_k;
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(c->m_bv));
|
||||
for (unsigned i = 0; i < atm->get_num_args(); ++i) {
|
||||
expr* arg = atm->get_arg(i);
|
||||
if (ctx.get_assignment(arg) == l_false) {
|
||||
lits.push_back(~literal(ctx.get_bool_var(arg)));
|
||||
lits.push_back(literal(c->m_bv));
|
||||
for (unsigned i = 0; i < args.size() && lits.size() <= deficit; ++i) {
|
||||
if (ctx.get_assignment(args[i]) == l_false) {
|
||||
lits.push_back(literal(args[i]));
|
||||
}
|
||||
}
|
||||
add_clause(lits);
|
||||
|
|
@ -173,10 +202,12 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
if (m_cards.find(v, c)) {
|
||||
app* atm = to_app(ctx.bool_var2expr(v));
|
||||
SASSERT(atm->get_num_args() >= c->m_f + c->m_t);
|
||||
svector<bool_var> const& args = c->m_args;
|
||||
SASSERT(args.size() >= c->m_f + c->m_t);
|
||||
bool_var bv;
|
||||
|
||||
TRACE("card", tout << " t:" << is_true << " k:" << c->m_k << " t:" << c->m_t << " f:" << c->m_f << "\n";);
|
||||
|
||||
// at most k
|
||||
// propagate false to children that are not yet assigned.
|
||||
// v & t1 & ... & tk => ~l_j
|
||||
|
|
@ -185,8 +216,8 @@ namespace smt {
|
|||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(v));
|
||||
bool done = false;
|
||||
for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) {
|
||||
bv = ctx.get_bool_var(atm->get_arg(i));
|
||||
for (unsigned i = 0; !done && i < args.size(); ++i) {
|
||||
bv = args[i];
|
||||
if (ctx.get_assignment(bv) == l_true) {
|
||||
lits.push_back(literal(bv));
|
||||
}
|
||||
|
|
@ -196,8 +227,8 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
SASSERT(done || lits.size() == c->m_k + 1);
|
||||
for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) {
|
||||
bv = ctx.get_bool_var(atm->get_arg(i));
|
||||
for (unsigned i = 0; !done && i < args.size(); ++i) {
|
||||
bv = args[i];
|
||||
if (ctx.get_assignment(bv) == l_undef) {
|
||||
lits.push_back(literal(bv));
|
||||
add_clause(lits);
|
||||
|
|
@ -208,23 +239,22 @@ namespace smt {
|
|||
// at least k+1:
|
||||
// !v & !f1 & .. & !f_m => l_j
|
||||
// for m + k + 1 = arity()
|
||||
if (!is_true && atm->get_num_args() == 1 + c->m_f + c->m_k) {
|
||||
if (!is_true && args.size() <= 1 + c->m_f + c->m_k) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(v));
|
||||
lits.push_back(literal(v));
|
||||
bool done = false;
|
||||
for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) {
|
||||
bv = ctx.get_bool_var(atm->get_arg(i));
|
||||
for (unsigned i = 0; !done && i < args.size(); ++i) {
|
||||
bv = args[i];
|
||||
if (ctx.get_assignment(bv) == l_false) {
|
||||
lits.push_back(~literal(bv));
|
||||
lits.push_back(literal(bv));
|
||||
}
|
||||
if (lits.size() > c->m_k + 1) {
|
||||
add_clause(lits);
|
||||
done = true;
|
||||
}
|
||||
}
|
||||
SASSERT(done || lits.size() == c->m_k + 1);
|
||||
for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) {
|
||||
bv = ctx.get_bool_var(atm->get_arg(i));
|
||||
for (unsigned i = 0; !done && i < args.size(); ++i) {
|
||||
bv = args[i];
|
||||
if (ctx.get_assignment(bv) != l_false) {
|
||||
lits.push_back(~literal(bv));
|
||||
add_clause(lits);
|
||||
|
|
@ -276,3 +306,315 @@ namespace smt {
|
|||
}
|
||||
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
||||
class sorting {
|
||||
void exchange(unsigned i, unsigned j, expr_ref_vector& es) {
|
||||
SASSERT(i <= j);
|
||||
if (i == j) {
|
||||
return;
|
||||
}
|
||||
expr* ei = es[i].get();
|
||||
expr* ej = es[j].get();
|
||||
es[i] = m.mk_ite(mk_le(ei,ej), ei, ej);
|
||||
es[j] = m.mk_ite(mk_le(ej,ei), ei, ej);
|
||||
}
|
||||
|
||||
void sort(unsigned k) {
|
||||
if (k == 2) {
|
||||
for (unsigned i = 0; i < m_es.size()/2; ++i) {
|
||||
exchange(current(2*i), current(2*i+1), m_es);
|
||||
next(2*i) = current(2*i);
|
||||
next(2*i+1) = current(2*i+1);
|
||||
}
|
||||
std::swap(m_current, m_next);
|
||||
}
|
||||
else {
|
||||
|
||||
for (unsigned i = 0; i < m_es.size()/k; ++i) {
|
||||
for (unsigned j = 0; j < k / 2; ++j) {
|
||||
next((k * i) + j) = current((k * i) + (2 * j));
|
||||
next((k * i) + (k / 2) + j) = current((k * i) + (2 * j) + 1);
|
||||
}
|
||||
}
|
||||
|
||||
std::swap(m_current, m_next);
|
||||
sort(k / 2);
|
||||
for (unsigned i = 0; i < m_es.size() / k; ++i) {
|
||||
for (unsigned j = 0; j < k / 2; ++j) {
|
||||
next((k * i) + (2 * j)) = current((k * i) + j);
|
||||
next((k * i) + (2 * j) + 1) = current((k * i) + (k / 2) + j);
|
||||
}
|
||||
|
||||
for (unsigned j = 0; j < (k / 2) - 1; ++j) {
|
||||
exchange(next((k * i) + (2 * j) + 1), next((k * i) + (2 * (j + 1))));
|
||||
}
|
||||
}
|
||||
std::swap(m_current, m_next);
|
||||
}
|
||||
}
|
||||
|
||||
private Term[] Merge(Term[] l1, Term[] l2)
|
||||
{
|
||||
if (l1.Length == 0)
|
||||
{
|
||||
return l2;
|
||||
}
|
||||
else if (l2.Length == 0)
|
||||
{
|
||||
return l1;
|
||||
}
|
||||
else if (l1.Length == 1 && l2.Length == 1)
|
||||
{
|
||||
var merged = new Term[2];
|
||||
merged[0] = l1[0];
|
||||
merged[1] = l2[0];
|
||||
Exchange(0, 1, merged);
|
||||
return merged;
|
||||
}
|
||||
|
||||
var l1o = l1.Length / 2;
|
||||
var l2o = l2.Length / 2;
|
||||
var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o;
|
||||
var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o;
|
||||
|
||||
Term[] evenl1 = new Term[l1e];
|
||||
Term[] oddl1 = new Term[l1o];
|
||||
for (int i = 0; i < l1.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
evenl1[i / 2] = l1[i];
|
||||
}
|
||||
else
|
||||
{
|
||||
oddl1[i / 2] = l1[i];
|
||||
}
|
||||
}
|
||||
|
||||
Term[] evenl2 = new Term[l2e];
|
||||
Term[] oddl2 = new Term[l2o];
|
||||
for (int i = 0; i < l2.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
evenl2[i / 2] = l2[i];
|
||||
}
|
||||
else
|
||||
{
|
||||
oddl2[i / 2] = l2[i];
|
||||
}
|
||||
}
|
||||
|
||||
var even = Merge(evenl1, evenl2);
|
||||
var odd = Merge(oddl1, oddl2);
|
||||
|
||||
Term[] merge = new Term[l1.Length + l2.Length];
|
||||
|
||||
for (int i = 0; i < merge.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
merge[i] = even[i / 2];
|
||||
if (i > 0)
|
||||
{
|
||||
Exchange(i - 1, i, merge);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (i / 2 < odd.Length)
|
||||
{
|
||||
merge[i] = odd[i / 2];
|
||||
}
|
||||
else
|
||||
{
|
||||
merge[i] = even[(i / 2) + 1];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return merge;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
Sorting networks used in Formula:
|
||||
|
||||
namespace Microsoft.Formula.Execution
|
||||
{
|
||||
using System;
|
||||
using System.Diagnostics.Contracts;
|
||||
using Microsoft.Z3;
|
||||
|
||||
internal class SortingNetwork
|
||||
{
|
||||
private Term[] elements;
|
||||
private int[] current;
|
||||
private int[] next;
|
||||
|
||||
public SortingNetwork(SymbolicState owner, Term[] inputs, Sort sortingDomain)
|
||||
{
|
||||
Contract.Requires(owner != null && inputs != null && sortingDomain != null);
|
||||
Contract.Requires(inputs.Length > 0);
|
||||
|
||||
Owner = owner;
|
||||
Size = (int)Math.Pow(2, (int)Math.Ceiling(Math.Log(inputs.Length, 2)));
|
||||
|
||||
if (Size == 1)
|
||||
{
|
||||
elements = new Term[1];
|
||||
elements[0] = inputs[0];
|
||||
}
|
||||
else if (Size > 1)
|
||||
{
|
||||
var defaultElement = owner.Context.MkNumeral(0, sortingDomain);
|
||||
|
||||
current = new int[Size];
|
||||
next = new int[Size];
|
||||
elements = new Term[Size];
|
||||
for (int i = 0; i < Size; ++i)
|
||||
{
|
||||
current[i] = i;
|
||||
elements[i] = (i < Size - inputs.Length) ? defaultElement : inputs[i - (Size - inputs.Length)];
|
||||
}
|
||||
|
||||
int k = 2;
|
||||
Term xi;
|
||||
while (k <= Size)
|
||||
{
|
||||
Sort(k);
|
||||
|
||||
for (int i = 0; i < Size; ++i)
|
||||
{
|
||||
xi = owner.Context.MkFreshConst("x", sortingDomain);
|
||||
owner.Context.AssertCnstr(owner.Context.MkEq(xi, elements[i]));
|
||||
elements[i] = xi;
|
||||
}
|
||||
|
||||
for (int i = 0; i < elements.Length / k; ++i)
|
||||
{
|
||||
for (int j = 0; j < k - 1; ++j)
|
||||
{
|
||||
owner.Context.AssertCnstr(owner.Context.MkBvUle(elements[(k * i) + j], elements[(k * i) + j + 1]));
|
||||
}
|
||||
}
|
||||
|
||||
k *= 2;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public Term[] Outputs
|
||||
{
|
||||
get { return elements; }
|
||||
}
|
||||
|
||||
public int Size
|
||||
{
|
||||
get;
|
||||
private set;
|
||||
}
|
||||
|
||||
public SymbolicState Owner
|
||||
{
|
||||
get;
|
||||
private set;
|
||||
}
|
||||
|
||||
|
||||
private void Swap()
|
||||
{
|
||||
var tmp = current;
|
||||
current = next;
|
||||
next = tmp;
|
||||
}
|
||||
|
||||
private Term[] Merge(Term[] l1, Term[] l2)
|
||||
{
|
||||
if (l1.Length == 0)
|
||||
{
|
||||
return l2;
|
||||
}
|
||||
else if (l2.Length == 0)
|
||||
{
|
||||
return l1;
|
||||
}
|
||||
else if (l1.Length == 1 && l2.Length == 1)
|
||||
{
|
||||
var merged = new Term[2];
|
||||
merged[0] = l1[0];
|
||||
merged[1] = l2[0];
|
||||
Exchange(0, 1, merged);
|
||||
return merged;
|
||||
}
|
||||
|
||||
var l1o = l1.Length / 2;
|
||||
var l2o = l2.Length / 2;
|
||||
var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o;
|
||||
var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o;
|
||||
|
||||
Term[] evenl1 = new Term[l1e];
|
||||
Term[] oddl1 = new Term[l1o];
|
||||
for (int i = 0; i < l1.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
evenl1[i / 2] = l1[i];
|
||||
}
|
||||
else
|
||||
{
|
||||
oddl1[i / 2] = l1[i];
|
||||
}
|
||||
}
|
||||
|
||||
Term[] evenl2 = new Term[l2e];
|
||||
Term[] oddl2 = new Term[l2o];
|
||||
for (int i = 0; i < l2.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
evenl2[i / 2] = l2[i];
|
||||
}
|
||||
else
|
||||
{
|
||||
oddl2[i / 2] = l2[i];
|
||||
}
|
||||
}
|
||||
|
||||
var even = Merge(evenl1, evenl2);
|
||||
var odd = Merge(oddl1, oddl2);
|
||||
|
||||
Term[] merge = new Term[l1.Length + l2.Length];
|
||||
|
||||
for (int i = 0; i < merge.Length; ++i)
|
||||
{
|
||||
if (i % 2 == 0)
|
||||
{
|
||||
merge[i] = even[i / 2];
|
||||
if (i > 0)
|
||||
{
|
||||
Exchange(i - 1, i, merge);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (i / 2 < odd.Length)
|
||||
{
|
||||
merge[i] = odd[i / 2];
|
||||
}
|
||||
else
|
||||
{
|
||||
merge[i] = even[(i / 2) + 1];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return merge;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -30,9 +30,9 @@ namespace smt {
|
|||
bool_var m_bv;
|
||||
unsigned m_t;
|
||||
unsigned m_f;
|
||||
app* m_atom;
|
||||
card(app* a, bool_var bv, unsigned k):
|
||||
m_k(k), m_bv(bv), m_atom(a), m_t(0), m_f(0)
|
||||
svector<bool_var> m_args;
|
||||
card(bool_var bv, unsigned k):
|
||||
m_k(k), m_bv(bv), m_t(0), m_f(0)
|
||||
{}
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue