mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-06 18:34:28 -08:00
commit 55e91c099f
4 changed files with 587 additions and 217 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/card_decl_plugin.cpp
View file

@ -47,7 +47,7 @@ void card_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol con
app * card_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
parameter param(1);
parameter param(k);
return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
}

338
src/smt/theory_card.cpp
View file

@ -54,24 +54,22 @@ namespace smt {
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));
bool_var bv = ctx.mk_bool_var(atom);
card* c = alloc(card, bv, k);
add_card(c);
bool_var abv = ctx.mk_bool_var(atom);
if (k >= atom->get_num_args()) {
literal lit(abv);
ctx.mk_th_axiom(get_id(), 1, &lit);
return true;
}
card* c = alloc(card, abv, k);
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = atom->get_arg(i);
if (!ctx.b_internalized(arg)) {
ctx.internalize(arg, false);
}
bool_var bv;
bool has_bv = false;
if (!m.is_not(arg) && ctx.b_internalized(arg)) {
bv = ctx.get_bool_var(arg);
@ -100,7 +98,23 @@ namespace smt {
ctx.mark_as_relevant(tmp);
}
c->m_args.push_back(bv);
add_watch(bv, c);
if (0 < k) {
add_watch(bv, c);
}
}
if (0 < k) {
add_card(c);
}
else {
// bv <=> (and (not bv1) ... (not bv_n))
literal_vector& lits = get_lits();
lits.push_back(literal(abv));
for (unsigned i = 0; i < c->m_args.size(); ++i) {
ctx.mk_th_axiom(get_id(), ~literal(abv), ~literal(c->m_args[i]));
lits.push_back(literal(c->m_args[i]));
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
dealloc(c);
}
return true;
}
@ -309,7 +323,12 @@ namespace smt {
#if 0
class sorting {
class sorting_network {
ast_manager& m;
expr_ref_vector m_es;
expr_ref_vector* m_current;
expr_ref_vector* m_next;
void exchange(unsigned i, unsigned j, expr_ref_vector& es) {
SASSERT(i <= j);
if (i == j) {
@ -338,7 +357,7 @@ class sorting {
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) {
@ -346,7 +365,7 @@ class sorting {
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))));
}
@ -355,105 +374,99 @@ class sorting {
}
}
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;
expr_ref_vector merge(expr_ref_vector const& l1, expr_ref_vector& l2) {
if (l1.empty()) {
return l2;
}
if (l2.empty()) {
return l1;
}
expr_ref_vector result(m);
if (l1.size() == 1 && l2.size() == 1) {
result.push_back(l1[0]);
result.push_back(l2[0]);
exchange(0, 1, result);
return result;
}
unsigned l1o = l1.size()/2;
unsigned l2o = l2.size()/2;
unsigned l1e = (l1.size() % 2 == 1) ? l1o + 1 : l1o;
unsigned l2e = (l2.size() % 2 == 1) ? l2o + 1 : l2o;
expr_ref_vector evenl1(m, l1e);
expr_ref_vector oddl1(m, l1o);
expr_ref_vector evenl2(m, l2e);
expr_ref_vector oddl2(m, l2o);
for (unsigned i = 0; i < l1.size(); ++i) {
if (i % 2 == 0) {
evenl1[i/2] = l1[i];
}
else {
oddl1[i/2] = l1[i];
}
}
for (unsigned i = 0; i < l2.size(); ++i) {
if (i % 2 == 0) {
evenl2[i/2] = l2[i];
}
else {
oddl2[i/2] = l2[i];
}
}
expr_ref_vector even = merge(evenl1, evenl2);
expr_ref_vector odd = merge(oddl1, oddl2);
result.resize(l1.size() + l2.size());
for (unsigned i = 0; i < result.size(); ++i) {
if (i % 2 == 0) {
result[i] = even[i/2].get();
if (i > 0) {
exchange(i - 1, i, result);
}
}
else {
if (i /2 < odd.size()) {
result[i] = odd[i/2].get();
}
else {
result[i] = even[(i/2)+1].get();
}
}
}
return result;
}
public:
sorting_network(ast_manager& m):
m(m),
m_es(m),
m_current(0),
m_next(0)
{}
expr_ref_vector operator()(expr_ref_vector const& inputs) {
if (inputs.size() <= 1) {
return inputs;
}
m_es.reset();
m_es.append(inputs);
while (!is_power_of2(m_es.size())) {
m_es.push_back(m.mk_false());
}
m_es.reverse();
for (unsigned i = 0; i < m_es.size(); ++i) {
current(i) = i;
}
unsigned k = 2;
while (k <= m_es.size()) {
sort(k);
// TBD
k *= 2;
}
}
};
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);
@ -506,114 +519,7 @@ namespace Microsoft.Formula.Execution
}
}
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;
}
}
}

431
src/tactic/arith/lia2card_tactic.cpp Normal file
View file

@ -0,0 +1,431 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
lia2card_tactic.cpp
Abstract:
Convert 0-1 integer variables cardinality constraints to built-in cardinality operator.
Author:
Nikolaj Bjorner (nbjorner) 2013-11-5
Notes:
--*/
#include"tactical.h"
#include"cooperate.h"
#include"bound_manager.h"
#include"ast_pp.h"
#include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version.
#include"card_decl_plugin.h"
#include"arith_decl_plugin.h"
class lia2card_tactic : public tactic {
struct imp {
typedef obj_hashtable<expr> expr_set;
ast_manager & m;
arith_util a;
card_util m_card;
obj_map<expr, ptr_vector<expr> > m_uses;
obj_map<expr, expr*> m_converted;
expr_set m_01s;
imp(ast_manager & _m, params_ref const & p):
m(_m),
a(m),
m_card(m) {
}
void set_cancel(bool f) {
}
void updt_params(params_ref const & p) {
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
m_01s.reset();
m_uses.reset();
m_converted.reset();
tactic_report report("cardinality-intro", *g);
bound_manager bounds(m);
bounds(*g);
bound_manager::iterator bit = bounds.begin(), bend = bounds.end();
for (; bit != bend; ++bit) {
expr* x = *bit;
bool s1, s2;
rational lo, hi;
if (a.is_int(x) &&
bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() &&
bounds.has_upper(x, hi, s2) && !s2 && hi.is_one()) {
m_01s.insert(x);
TRACE("card", tout << "add bound " << mk_pp(x, m) << "\n";);
}
}
if (m_01s.empty()) {
result.push_back(g.get());
return;
}
expr_set::iterator it = m_01s.begin(), end = m_01s.end();
for (; it != end; ++it) {
m_uses.insert(*it, ptr_vector<expr>());
}
for (unsigned j = 0; j < g->size(); ++j) {
ast_mark mark;
collect_uses(mark, g->form(j));
}
it = m_01s.begin(), end = m_01s.end();
for (; it != end; ++it) {
if (!validate_uses(m_uses.find(*it))) {
m_uses.remove(*it);
m_01s.remove(*it);
it = m_01s.begin();
end = m_01s.end();
}
}
if (m_01s.empty()) {
result.push_back(g.get());
return;
}
expr_safe_replace sub(m);
extract_substitution(sub);
expr_ref new_curr(m);
proof_ref new_pr(m);
for (unsigned i = 0; i < g->size(); i++) {
expr * curr = g->form(i);
sub(curr, new_curr);
g->update(i, new_curr, new_pr, g->dep(i));
}
g->inc_depth();
result.push_back(g.get());
TRACE("card", g->display(tout););
SASSERT(g->is_well_sorted());
// TBD: convert models for 0-1 variables.
// TBD: support proof conversion (or not..)
}
void extract_substitution(expr_safe_replace& sub) {
expr_set::iterator it = m_01s.begin(), end = m_01s.end();
for (; it != end; ++it) {
extract_substitution(sub, *it);
}
}
void extract_substitution(expr_safe_replace& sub, expr* x) {
ptr_vector<expr> const& use_list = m_uses.find(x);
for (unsigned i = 0; i < use_list.size(); ++i) {
expr* u = use_list[i];
convert_01(sub, u);
}
}
expr_ref mk_le(expr* x, rational const& bound) {
if (bound.is_pos()) {
return expr_ref(m.mk_true(), m);
}
else if (bound.is_zero()) {
return expr_ref(m.mk_not(mk_01(x)), m);
}
else {
return expr_ref(m.mk_false(), m);
}
}
expr_ref mk_ge(expr* x, rational const& bound) {
if (bound.is_one()) {
return expr_ref(mk_01(x), m);
}
else if (bound.is_pos()) {
return expr_ref(m.mk_false(), m);
}
else {
return expr_ref(m.mk_true(), m);
}
}
bool is_01var(expr* x) const {
return m_01s.contains(x);
}
void convert_01(expr_safe_replace& sub, expr* fml) {
rational n;
unsigned k;
expr_ref_vector args(m);
expr_ref result(m);
expr* x, *y;
if (a.is_le(fml, x, y) || a.is_ge(fml, y, x)) {
if (is_01var(x) && a.is_numeral(y, n)) {
sub.insert(fml, mk_le(x, n));
return;
}
if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n));
return;
}
if (is_add(x, args) && is_unsigned(y, k)) { // x <= k
sub.insert(fml, m_card.mk_at_most_k(args.size(), args.c_ptr(), k));
return;
}
if (is_add(y, args) && is_unsigned(x, k)) { // k <= y <=> not (y <= k-1)
if (k == 0)
sub.insert(fml, m.mk_true());
else
sub.insert(fml, m.mk_not(m_card.mk_at_most_k(args.size(), args.c_ptr(), k-1)));
return;
}
UNREACHABLE();
}
if (a.is_lt(fml, x, y) || a.is_gt(fml, y, x)) {
if (is_01var(x) && a.is_numeral(y, n)) {
sub.insert(fml, mk_le(x, n-rational(1)));
return;
}
if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n+rational(1)));
return;
}
if (is_add(x, args) && is_unsigned(y, k)) { // x < k
if (k == 0)
sub.insert(fml, m.mk_false());
else
sub.insert(fml, m_card.mk_at_most_k(args.size(), args.c_ptr(), k-1));
return;
}
if (is_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k)
sub.insert(fml, m.mk_not(m_card.mk_at_most_k(args.size(), args.c_ptr(), k)));
return;
}
UNREACHABLE();
}
if (m.is_eq(fml, x, y)) {
if (!is_01var(x)) {
std::swap(x, y);
}
if (is_01var(x) && a.is_numeral(y, n)) {
if (n.is_one()) {
sub.insert(fml, mk_01(x));
}
else if (n.is_zero()) {
sub.insert(fml, m.mk_not(mk_01(x)));
}
else {
sub.insert(fml, m.mk_false());
}
return;
}
UNREACHABLE();
}
if (is_sum(fml)) {
SASSERT(m_uses.contains(fml));
ptr_vector<expr> const& u = m_uses.find(fml);
for (unsigned i = 0; i < u.size(); ++i) {
convert_01(sub, u[i]);
}
return;
}
UNREACHABLE();
}
expr_ref mk_01(expr* x) {
expr* r;
SASSERT(is_01var(x));
if (!m_converted.find(x, r)) {
symbol name = to_app(x)->get_decl()->get_name();
r = m.mk_fresh_const(name.str().c_str(), m.mk_bool_sort());
m_converted.insert(x, r);
}
return expr_ref(r, m);
}
bool is_add(expr* x, expr_ref_vector& args) {
if (a.is_add(x)) {
app* ap = to_app(x);
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
args.push_back(mk_01(ap->get_arg(i)));
}
return true;
}
else {
return false;
}
}
bool validate_uses(ptr_vector<expr> const& use_list) {
for (unsigned i = 0; i < use_list.size(); ++i) {
if (!validate_use(use_list[i])) {
return false;
}
}
return true;
}
bool validate_use(expr* fml) {
expr* x, *y;
if (a.is_le(fml, x, y) ||
a.is_ge(fml, x, y) ||
a.is_lt(fml, x, y) ||
a.is_gt(fml, x, y) ||
m.is_eq(fml, x, y)) {
if (a.is_numeral(x)) {
std::swap(x,y);
}
if ((is_one(y) || a.is_zero(y)) && is_01var(x))
return true;
if (a.is_numeral(y) && is_sum(x) && !m.is_eq(fml)) {
return true;
}
}
if (is_sum(fml)) {
SASSERT(m_uses.contains(fml));
ptr_vector<expr> const& u = m_uses.find(fml);
for (unsigned i = 0; i < u.size(); ++i) {
if (!validate_use(u[i])) {
return false;
}
}
return true;
}
TRACE("card", tout << "Use not validated: " << mk_pp(fml, m) << "\n";);
return false;
}
bool is_sum(expr* x) const {
if (a.is_add(x)) {
app* ap = to_app(x);
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
if (!is_01var(ap->get_arg(i))) {
return false;
}
}
return true;
}
return false;
}
bool is_unsigned(expr* x, unsigned& k) {
rational r;
if (a.is_numeral(x, r) && r.is_unsigned()) {
k = r.get_unsigned();
SASSERT(rational(k) == r);
return true;
}
else {
return false;
}
}
bool is_one(expr* x) {
rational r;
return a.is_numeral(x, r) && r.is_one();
}
void collect_uses(ast_mark& mark, expr* f) {
ptr_vector<expr> todo;
todo.push_back(f);
while (!todo.empty()) {
f = todo.back();
todo.pop_back();
if (mark.is_marked(f)) {
continue;
}
mark.mark(f, true);
if (is_var(f)) {
continue;
}
if (is_quantifier(f)) {
todo.push_back(to_quantifier(f)->get_expr());
continue;
}
app* a = to_app(f);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* arg = a->get_arg(i);
if (!m_uses.contains(arg)) {
m_uses.insert(arg, ptr_vector<expr>());
}
m_uses.find(arg).push_back(a);
todo.push_back(arg);
}
}
}
};
imp * m_imp;
params_ref m_params;
public:
lia2card_tactic(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(lia2card_tactic, m, m_params);
}
virtual ~lia2card_tactic() {
dealloc(m_imp);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
};
tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(lia2card_tactic, m, p));
}

33
src/tactic/arith/lia2card_tactic.h Normal file
View file

@ -0,0 +1,33 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
lia2card_tactic.h
Abstract:
Extract 0-1 integer variables used in
cardinality constraints and replace them by Booleans.
Author:
Nikolaj Bjorner (nbjorner) 2013-11-5
Notes:
--*/
#ifndef _LIA2CARD_TACTIC_H_
#define _LIA2CARD_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("lia2card", "introduce cardinality constraints from 0-1 integer.", "mk_lia2card_tactic(m, p)")
*/
#endif