mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

move model_evaluator from pdr to model, call it model_implicant

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-23 21:33:35 +01:00
parent b35088f7e5
commit 2ff51e9a60
11 changed files with 1514 additions and 1341 deletions
Download patch file Download diff file Expand all files Collapse all files

917
src/model/model_implicant.cpp Normal file
View file

@ -0,0 +1,917 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
model_implicant.cpp
Abstract:
Facility to extract prime implicant from model.
Author:
Krystof Hoder (t-khoder) 2011-8-19.
Revision History:
Notes:
--*/
#include <sstream>
#include "array_decl_plugin.h"
#include "ast_pp.h"
#include "bool_rewriter.h"
#include "for_each_expr.h"
#include "model.h"
#include "ref_vector.h"
#include "rewriter.h"
#include "rewriter_def.h"
#include "util.h"
#include "model_implicant.h"
#include "arith_decl_plugin.h"
#include "expr_replacer.h"
#include "model_smt2_pp.h"
#include "poly_rewriter.h"
#include "poly_rewriter_def.h"
#include "arith_rewriter.h"
#include "scoped_proof.h"
/////////////////////////
// model_implicant
//
void model_implicant::assign_value(expr* e, expr* val) {
rational r;
if (m.is_true(val)) {
set_true(e);
}
else if (m.is_false(val)) {
set_false(e);
}
else if (m_arith.is_numeral(val, r)) {
set_number(e, r);
}
else if (m.is_value(val)) {
set_value(e, val);
}
else {
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
set_x(e);
}
}
void model_implicant::setup_model(model_ref& model) {
m_numbers.reset();
m_values.reset();
m_model = model;
rational r;
unsigned sz = model->get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * d = model->get_constant(i);
expr* val = model->get_const_interp(d);
expr* e = m.mk_const(d);
m_refs.push_back(e);
assign_value(e, val);
}
}
void model_implicant::reset() {
m1.reset();
m2.reset();
m_values.reset();
m_visited.reset();
m_numbers.reset();
m_refs.reset();
m_model = 0;
}
expr_ref_vector model_implicant::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
setup_model(mdl);
TRACE("pdr_verbose",
tout << "formulas:\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
expr_ref_vector model = prune_by_cone_of_influence(formulas);
TRACE("pdr_verbose",
tout << "pruned model:\n";
for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";);
reset();
DEBUG_CODE(
setup_model(mdl);
VERIFY(check_model(formulas));
reset(););
return model;
}
expr_ref_vector model_implicant::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
TRACE("pdr",
tout << "formulas:\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
expr_ref_vector result(m);
expr_ref tmp(m);
ptr_vector<expr> tocollect;
setup_model(mdl);
collect(formulas, tocollect);
for (unsigned i = 0; i < tocollect.size(); ++i) {
expr* e = tocollect[i];
expr* e1, *e2;
SASSERT(m.is_bool(e));
SASSERT(is_true(e) || is_false(e));
if (is_true(e)) {
result.push_back(e);
}
// hack to break disequalities for arithmetic variables.
else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) {
if (get_number(e1) < get_number(e2)) {
result.push_back(m_arith.mk_lt(e1,e2));
}
else {
result.push_back(m_arith.mk_lt(e2,e1));
}
}
else {
result.push_back(m.mk_not(e));
}
}
reset();
TRACE("pdr",
tout << "minimized model:\n";
for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n";
);
return result;
}
void model_implicant::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect) {
SASSERT(m.is_bool(e));
SASSERT(is_true(e) || is_false(e));
unsigned v = is_true(e);
unsigned sz = e->get_num_args();
expr* const* args = e->get_args();
if (e->get_family_id() == m.get_basic_family_id()) {
switch(e->get_decl_kind()) {
case OP_TRUE:
break;
case OP_FALSE:
break;
case OP_EQ:
case OP_IFF:
if (args[0] == args[1]) {
SASSERT(v);
// no-op
}
else if (m.is_bool(args[0])) {
todo.append(sz, args);
}
else {
tocollect.push_back(e);
}
break;
case OP_DISTINCT:
tocollect.push_back(e);
break;
case OP_ITE:
if (args[1] == args[2]) {
tocollect.push_back(args[1]);
}
else if (is_true(args[1]) && is_true(args[2])) {
todo.append(2, args+1);
}
else if (is_false(args[1]) && is_false(args[2])) {
todo.append(2, args+1);
}
else if (is_true(args[0])) {
todo.append(2, args);
}
else {
SASSERT(is_false(args[0]));
todo.push_back(args[0]);
todo.push_back(args[2]);
}
break;
case OP_AND:
if (v) {
todo.append(sz, args);
}
else {
unsigned i = 0;
for (; !is_false(args[i]) && i < sz; ++i);
if (i == sz) {
fatal_error(1);
}
VERIFY(i < sz);
todo.push_back(args[i]);
}
break;
case OP_OR:
if (v) {
unsigned i = 0;
for (; !is_true(args[i]) && i < sz; ++i);
if (i == sz) {
fatal_error(1);
}
VERIFY(i < sz);
todo.push_back(args[i]);
}
else {
todo.append(sz, args);
}
break;
case OP_XOR:
case OP_NOT:
todo.append(sz, args);
break;
case OP_IMPLIES:
if (v) {
if (is_true(args[1])) {
todo.push_back(args[1]);
}
else if (is_false(args[0])) {
todo.push_back(args[0]);
}
else {
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
else {
todo.append(sz, args);
}
break;
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
else {
tocollect.push_back(e);
}
}
void model_implicant::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect) {
ptr_vector<expr> todo;
todo.append(formulas);
m_visited.reset();
VERIFY(check_model(formulas));
while (!todo.empty()) {
app* e = to_app(todo.back());
todo.pop_back();
if (!m_visited.is_marked(e)) {
process_formula(e, todo, tocollect);
m_visited.mark(e, true);
}
}
m_visited.reset();
}
expr_ref_vector model_implicant::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
ptr_vector<expr> tocollect;
collect(formulas, tocollect);
m1.reset();
m2.reset();
for (unsigned i = 0; i < tocollect.size(); ++i) {
TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";);
for_each_expr(*this, m_visited, tocollect[i]);
}
unsigned sz = m_model->get_num_constants();
expr_ref e(m), eq(m), val(m);
expr_ref_vector model(m);
for (unsigned i = 0; i < sz; i++) {
e = m.mk_const(m_model->get_constant(i));
if (m_visited.is_marked(e)) {
val = eval(m_model, e);
eq = m.mk_eq(e, val);
model.push_back(eq);
}
}
m_visited.reset();
TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";);
return model;
}
void model_implicant::eval_arith(app* e) {
rational r, r2;
#define ARG1 e->get_arg(0)
#define ARG2 e->get_arg(1)
unsigned arity = e->get_num_args();
for (unsigned i = 0; i < arity; ++i) {
expr* arg = e->get_arg(i);
if (is_x(arg)) {
set_x(e);
return;
}
SASSERT(!is_unknown(arg));
}
switch(e->get_decl_kind()) {
case OP_NUM:
VERIFY(m_arith.is_numeral(e, r));
set_number(e, r);
break;
case OP_IRRATIONAL_ALGEBRAIC_NUM:
set_x(e);
break;
case OP_LE:
set_bool(e, get_number(ARG1) <= get_number(ARG2));
break;
case OP_GE:
set_bool(e, get_number(ARG1) >= get_number(ARG2));
break;
case OP_LT:
set_bool(e, get_number(ARG1) < get_number(ARG2));
break;
case OP_GT:
set_bool(e, get_number(ARG1) > get_number(ARG2));
break;
case OP_ADD:
r = rational::zero();
for (unsigned i = 0; i < arity; ++i) {
r += get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_SUB:
r = get_number(e->get_arg(0));
for (unsigned i = 1; i < arity; ++i) {
r -= get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_UMINUS:
SASSERT(arity == 1);
set_number(e, get_number(e->get_arg(0)));
break;
case OP_MUL:
r = rational::one();
for (unsigned i = 0; i < arity; ++i) {
r *= get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_DIV:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, get_number(ARG1) / r);
}
break;
case OP_IDIV:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, div(get_number(ARG1), r));
}
break;
case OP_REM:
// rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
r2 = mod(get_number(ARG1), r);
if (r.is_neg()) r2.neg();
set_number(e, r2);
}
break;
case OP_MOD:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, mod(get_number(ARG1), r));
}
break;
case OP_TO_REAL:
SASSERT(arity == 1);
set_number(e, get_number(ARG1));
break;
case OP_TO_INT:
SASSERT(arity == 1);
set_number(e, floor(get_number(ARG1)));
break;
case OP_IS_INT:
SASSERT(arity == 1);
set_bool(e, get_number(ARG1).is_int());
break;
case OP_POWER:
set_x(e);
break;
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
break;
}
}
void model_implicant::inherit_value(expr* e, expr* v) {
expr* w;
SASSERT(!is_unknown(v));
SASSERT(m.get_sort(e) == m.get_sort(v));
if (is_x(v)) {
set_x(e);
}
else if (m.is_bool(e)) {
SASSERT(m.is_bool(v));
if (is_true(v)) set_true(e);
else if (is_false(v)) set_false(e);
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
else if (m_arith.is_int_real(e)) {
set_number(e, get_number(v));
}
else if (m.is_value(v)) {
set_value(e, v);
}
else if (m_values.find(v, w)) {
set_value(e, w);
}
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
void model_implicant::eval_exprs(expr_ref_vector& es) {
model_ref mr(m_model);
for (unsigned j = 0; j < es.size(); ++j) {
if (m_array.is_as_array(es[j].get())) {
es[j] = eval(mr, es[j].get());
}
}
}
bool model_implicant::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
SASSERT(m_array.is_array(a));
TRACE("pdr", tout << mk_pp(a, m) << "\n";);
while (m_array.is_store(a)) {
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
eval_exprs(store);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_array.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
while (m_array.is_as_array(a)) {
func_decl* f = m_array.get_as_array_func_decl(to_app(a));
func_interp* g = m_model->get_func_interp(f);
unsigned sz = g->num_entries();
unsigned arity = f->get_arity();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m);
func_entry const* fe = g->get_entry(i);
store.append(arity, fe->get_args());
store.push_back(fe->get_result());
for (unsigned j = 0; j < store.size(); ++j) {
if (!is_ground(store[j].get())) {
TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
return false;
}
}
eval_exprs(store);
stores.push_back(store);
}
else_case = g->get_else();
if (!else_case) {
TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";);
return false;
}
if (!is_ground(else_case)) {
TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";);
return false;
}
if (m_array.is_as_array(else_case)) {
model_ref mr(m_model);
else_case = eval(mr, else_case);
}
TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";);
return true;
}
TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";);
return false;
}
/**
best effort evaluator of extensional array equality.
*/
void model_implicant::eval_array_eq(app* e, expr* arg1, expr* arg2) {
TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";);
expr_ref v1(m), v2(m);
m_model->eval(arg1, v1);
m_model->eval(arg2, v2);
if (v1 == v2) {
set_true(e);
return;
}
sort* s = m.get_sort(arg1);
sort* r = get_array_range(s);
// give up evaluating finite domain/range arrays
if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
return;
}
vector<expr_ref_vector> store;
expr_ref else1(m), else2(m);
if (!extract_array_func_interp(v1, store, else1) ||
!extract_array_func_interp(v2, store, else2)) {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
return;
}
if (else1 != else2) {
if (m.is_value(else1) && m.is_value(else2)) {
TRACE("pdr", tout
<< "defaults are different: " << mk_pp(e, m) << " "
<< mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
set_false(e);
}
else if (m_array.is_array(else1)) {
eval_array_eq(e, else1, else2);
}
else {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
}
return;
}
expr_ref s1(m), s2(m), w1(m), w2(m);
expr_ref_vector args1(m), args2(m);
args1.push_back(v1);
args2.push_back(v2);
for (unsigned i = 0; i < store.size(); ++i) {
args1.resize(1);
args2.resize(1);
args1.append(store[i].size()-1, store[i].c_ptr());
args2.append(store[i].size()-1, store[i].c_ptr());
s1 = m_array.mk_select(args1.size(), args1.c_ptr());
s2 = m_array.mk_select(args2.size(), args2.c_ptr());
m_model->eval(s1, w1);
m_model->eval(s2, w2);
if (w1 == w2) {
continue;
}
if (m.is_value(w1) && m.is_value(w2)) {
TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n";
tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
set_false(e);
}
else if (m_array.is_array(w1)) {
eval_array_eq(e, w1, w2);
if (is_true(e)) {
continue;
}
}
else {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
}
return;
}
set_true(e);
}
void model_implicant::eval_eq(app* e, expr* arg1, expr* arg2) {
if (arg1 == arg2) {
set_true(e);
}
else if (m_array.is_array(arg1)) {
eval_array_eq(e, arg1, arg2);
}
else if (is_x(arg1) || is_x(arg2)) {
expr_ref eq(m), vl(m);
eq = m.mk_eq(arg1, arg2);
m_model->eval(eq, vl);
if (m.is_true(vl)) {
set_bool(e, true);
}
else if (m.is_false(vl)) {
set_bool(e, false);
}
else {
TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";);
set_x(e);
}
}
else if (m.is_bool(arg1)) {
bool val = is_true(arg1) == is_true(arg2);
SASSERT(val == (is_false(arg1) == is_false(arg2)));
if (val) {
set_true(e);
}
else {
set_false(e);
}
}
else if (m_arith.is_int_real(arg1)) {
set_bool(e, get_number(arg1) == get_number(arg2));
}
else {
expr* e1 = get_value(arg1);
expr* e2 = get_value(arg2);
if (m.is_value(e1) && m.is_value(e2)) {
set_bool(e, e1 == e2);
}
else if (e1 == e2) {
set_bool(e, true);
}
else {
TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
set_x(e);
}
}
}
void model_implicant::eval_basic(app* e) {
expr* arg1, *arg2;
expr *argCond, *argThen, *argElse, *arg;
bool has_x = false;
unsigned arity = e->get_num_args();
switch(e->get_decl_kind()) {
case OP_AND:
for (unsigned j = 0; j < arity; ++j) {
expr * arg = e->get_arg(j);
if (is_false(arg)) {
set_false(e);
return;
}
else if (is_x(arg)) {
has_x = true;
}
else {
SASSERT(is_true(arg));
}
}
if (has_x) {
set_x(e);
}
else {
set_true(e);
}
break;
case OP_OR:
for (unsigned j = 0; j < arity; ++j) {
expr * arg = e->get_arg(j);
if (is_true(arg)) {
set_true(e);
return;
}
else if (is_x(arg)) {
has_x = true;
}
else {
SASSERT(is_false(arg));
}
}
if (has_x) {
set_x(e);
}
else {
set_false(e);
}
break;
case OP_NOT:
VERIFY(m.is_not(e, arg));
if (is_true(arg)) {
set_false(e);
}
else if (is_false(arg)) {
set_true(e);
}
else {
SASSERT(is_x(arg));
set_x(e);
}
break;
case OP_IMPLIES:
VERIFY(m.is_implies(e, arg1, arg2));
if (is_false(arg1) || is_true(arg2)) {
set_true(e);
}
else if (arg1 == arg2) {
set_true(e);
}
else if (is_true(arg1) && is_false(arg2)) {
set_false(e);
}
else {
SASSERT(is_x(arg1) || is_x(arg2));
set_x(e);
}
break;
case OP_IFF:
VERIFY(m.is_iff(e, arg1, arg2));
eval_eq(e, arg1, arg2);
break;
case OP_ITE:
VERIFY(m.is_ite(e, argCond, argThen, argElse));
if (is_true(argCond)) {
inherit_value(e, argThen);
}
else if (is_false(argCond)) {
inherit_value(e, argElse);
}
else if (argThen == argElse) {
inherit_value(e, argThen);
}
else if (m.is_bool(e)) {
SASSERT(is_x(argCond));
if (is_x(argThen) || is_x(argElse)) {
set_x(e);
}
else if (is_true(argThen) == is_true(argElse)) {
inherit_value(e, argThen);
}
else {
set_x(e);
}
}
else {
set_x(e);
}
break;
case OP_TRUE:
set_true(e);
break;
case OP_FALSE:
set_false(e);
break;
case OP_EQ:
VERIFY(m.is_eq(e, arg1, arg2));
eval_eq(e, arg1, arg2);
break;
case OP_DISTINCT: {
vector<rational> values;
for (unsigned i = 0; i < arity; ++i) {
expr* arg = e->get_arg(i);
if (is_x(arg)) {
set_x(e);
return;
}
values.push_back(get_number(arg));
}
std::sort(values.begin(), values.end());
for (unsigned i = 0; i + 1 < values.size(); ++i) {
if (values[i] == values[i+1]) {
set_false(e);
return;
}
}
set_true(e);
break;
}
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
bool model_implicant::check_model(ptr_vector<expr> const& formulas) {
ptr_vector<expr> todo(formulas);
while (!todo.empty()) {
expr * curr_e = todo.back();
if (!is_app(curr_e)) {
todo.pop_back();
continue;
}
app * curr = to_app(curr_e);
if (!is_unknown(curr)) {
todo.pop_back();
continue;
}
unsigned arity = curr->get_num_args();
for (unsigned i = 0; i < arity; ++i) {
if (is_unknown(curr->get_arg(i))) {
todo.push_back(curr->get_arg(i));
}
}
if (todo.back() != curr) {
continue;
}
todo.pop_back();
if (curr->get_family_id() == m_arith.get_family_id()) {
eval_arith(curr);
}
else if (curr->get_family_id() == m.get_basic_family_id()) {
eval_basic(curr);
}
else {
expr_ref vl(m);
m_model->eval(curr, vl);
assign_value(curr, vl);
}
IF_VERBOSE(35,verbose_stream() << "assigned "<<mk_pp(curr_e,m)
<<(is_true(curr_e) ? "true" : is_false(curr_e) ? "false" : "unknown") << "\n";);
SASSERT(!is_unknown(curr));
}
bool has_x = false;
for (unsigned i = 0; i < formulas.size(); ++i) {
expr * form = formulas[i];
SASSERT(!is_unknown(form));
TRACE("pdr_verbose",
tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" <<mk_pp(form, m)<< "\n";);
if (is_false(form)) {
IF_VERBOSE(0, verbose_stream() << "formula false in model: " << mk_pp(form, m) << "\n";);
UNREACHABLE();
}
if (is_x(form)) {
IF_VERBOSE(0, verbose_stream() << "formula undetermined in model: " << mk_pp(form, m) << "\n";);
TRACE("pdr", model_smt2_pp(tout, m, *m_model, 0););
has_x = true;
}
}
return !has_x;
}
expr_ref model_implicant::eval(model_ref& model, func_decl* d) {
SASSERT(d->get_arity() == 0);
expr_ref result(m);
if (m_array.is_array(d->get_range())) {
expr_ref e(m);
e = m.mk_const(d);
result = eval(model, e);
}
else {
result = model->get_const_interp(d);
}
return result;
}
expr_ref model_implicant::eval(model_ref& model, expr* e) {
expr_ref result(m);
m_model = model;
VERIFY(m_model->eval(e, result, true));
if (m_array.is_array(e)) {
vector<expr_ref_vector> stores;
expr_ref_vector args(m);
expr_ref else_case(m);
if (extract_array_func_interp(result, stores, else_case)) {
result = m_array.mk_const_array(m.get_sort(e), else_case);
while (!stores.empty() && stores.back().back() == else_case) {
stores.pop_back();
}
for (unsigned i = stores.size(); i > 0; ) {
--i;
args.resize(1);
args[0] = result;
args.append(stores[i]);
result = m_array.mk_store(args.size(), args.c_ptr());
}
return result;
}
}
return result;
}

118
src/model/model_implicant.h Normal file
View file

@ -0,0 +1,118 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
model_implicant.h
Abstract:
Facility to extract prime implicant from model.
Author:
Krystof Hoder (t-khoder) 2011-8-19.
Revision History:
--*/
#ifndef _MODEL_IMPLICANT_H_
#define _MODEL_IMPLICANT_H_
#include "ast.h"
#include "ast_pp.h"
#include "obj_hashtable.h"
#include "ref_vector.h"
#include "trace.h"
#include "vector.h"
#include "arith_decl_plugin.h"
#include "array_decl_plugin.h"
class model;
class model_core;
class model_implicant {
ast_manager& m;
arith_util m_arith;
array_util m_array;
obj_map<expr,rational> m_numbers;
expr_ref_vector m_refs;
obj_map<expr, expr*> m_values;
model_ref m_model;
//00 -- non-visited
//01 -- X
//10 -- false
//11 -- true
expr_mark m1;
expr_mark m2;
expr_mark m_visited;
void reset();
void setup_model(model_ref& model);
void assign_value(expr* e, expr* v);
void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
void eval_arith(app* e);
void eval_basic(app* e);
void eval_eq(app* e, expr* arg1, expr* arg2);
void eval_array_eq(app* e, expr* arg1, expr* arg2);
void inherit_value(expr* e, expr* v);
inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); }
inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); }
inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); }
inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); }
inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); }
inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
inline void set_number(expr* x, rational const& v) {
set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v);
}
inline expr* get_value(expr* x) { return m_values.find(x); }
inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
bool check_model(ptr_vector<expr> const & formulas);
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
void eval_exprs(expr_ref_vector& es);
public:
model_implicant(ast_manager& m) :
m(m), m_arith(m), m_array(m), m_refs(m) {}
/**
\brief extract equalities from model that suffice to satisfy formula.
\pre model satisfies formulas
*/
expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
\brief extract literals from formulas that satisfy formulas.
\pre model satisfies formulas
*/
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
for_each_expr visitor.
*/
void operator()(expr* e) {}
expr_ref eval(model_ref& mdl, expr* e);
expr_ref eval(model_ref& mdl, func_decl* d);
};
#endif

3
src/muz/pdr/pdr_context.cpp
View file

@ -48,6 +48,7 @@ Notes:
#include "qe_util.h"
#include "scoped_proof.h"
#include "blast_term_ite_tactic.h"
#include "model_implicant.h"
namespace pdr {
@ -1978,7 +1979,7 @@ namespace pdr {
tout << "Transition:\n" << mk_pp(T, m) << "\n";
tout << "Phi:\n" << mk_pp(phi, m) << "\n";);
model_evaluator mev(m);
model_implicant mev(m);
expr_ref_vector mdl(m), forms(m), Phi(m);
forms.push_back(T);
forms.push_back(phi);

873
src/muz/pdr/pdr_util.cpp
View file

@ -90,879 +90,6 @@ namespace pdr {
return res.str();
}
/////////////////////////
// model_evaluator
//
void model_evaluator::assign_value(expr* e, expr* val) {
rational r;
if (m.is_true(val)) {
set_true(e);
}
else if (m.is_false(val)) {
set_false(e);
}
else if (m_arith.is_numeral(val, r)) {
set_number(e, r);
}
else if (m.is_value(val)) {
set_value(e, val);
}
else {
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
set_x(e);
}
}
void model_evaluator::setup_model(model_ref& model) {
m_numbers.reset();
m_values.reset();
m_model = model;
rational r;
unsigned sz = model->get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * d = model->get_constant(i);
expr* val = model->get_const_interp(d);
expr* e = m.mk_const(d);
m_refs.push_back(e);
assign_value(e, val);
}
}
void model_evaluator::reset() {
m1.reset();
m2.reset();
m_values.reset();
m_visited.reset();
m_numbers.reset();
m_refs.reset();
m_model = 0;
}
expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
setup_model(mdl);
TRACE("pdr_verbose",
tout << "formulas:\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
expr_ref_vector model = prune_by_cone_of_influence(formulas);
TRACE("pdr_verbose",
tout << "pruned model:\n";
for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";);
reset();
DEBUG_CODE(
setup_model(mdl);
VERIFY(check_model(formulas));
reset(););
return model;
}
expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
TRACE("pdr",
tout << "formulas:\n";
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
expr_ref_vector result(m);
expr_ref tmp(m);
ptr_vector<expr> tocollect;
setup_model(mdl);
collect(formulas, tocollect);
for (unsigned i = 0; i < tocollect.size(); ++i) {
expr* e = tocollect[i];
expr* e1, *e2;
SASSERT(m.is_bool(e));
SASSERT(is_true(e) || is_false(e));
if (is_true(e)) {
result.push_back(e);
}
// hack to break disequalities for arithmetic variables.
else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) {
if (get_number(e1) < get_number(e2)) {
result.push_back(m_arith.mk_lt(e1,e2));
}
else {
result.push_back(m_arith.mk_lt(e2,e1));
}
}
else {
result.push_back(m.mk_not(e));
}
}
reset();
TRACE("pdr",
tout << "minimized model:\n";
for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n";
);
return result;
}
void model_evaluator::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect) {
SASSERT(m.is_bool(e));
SASSERT(is_true(e) || is_false(e));
unsigned v = is_true(e);
unsigned sz = e->get_num_args();
expr* const* args = e->get_args();
if (e->get_family_id() == m.get_basic_family_id()) {
switch(e->get_decl_kind()) {
case OP_TRUE:
break;
case OP_FALSE:
break;
case OP_EQ:
case OP_IFF:
if (args[0] == args[1]) {
SASSERT(v);
// no-op
}
else if (m.is_bool(args[0])) {
todo.append(sz, args);
}
else {
tocollect.push_back(e);
}
break;
case OP_DISTINCT:
tocollect.push_back(e);
break;
case OP_ITE:
if (args[1] == args[2]) {
tocollect.push_back(args[1]);
}
else if (is_true(args[1]) && is_true(args[2])) {
todo.append(2, args+1);
}
else if (is_false(args[1]) && is_false(args[2])) {
todo.append(2, args+1);
}
else if (is_true(args[0])) {
todo.append(2, args);
}
else {
SASSERT(is_false(args[0]));
todo.push_back(args[0]);
todo.push_back(args[2]);
}
break;
case OP_AND:
if (v) {
todo.append(sz, args);
}
else {
unsigned i = 0;
for (; !is_false(args[i]) && i < sz; ++i);
if (i == sz) {
fatal_error(1);
}
VERIFY(i < sz);
todo.push_back(args[i]);
}
break;
case OP_OR:
if (v) {
unsigned i = 0;
for (; !is_true(args[i]) && i < sz; ++i);
if (i == sz) {
fatal_error(1);
}
VERIFY(i < sz);
todo.push_back(args[i]);
}
else {
todo.append(sz, args);
}
break;
case OP_XOR:
case OP_NOT:
todo.append(sz, args);
break;
case OP_IMPLIES:
if (v) {
if (is_true(args[1])) {
todo.push_back(args[1]);
}
else if (is_false(args[0])) {
todo.push_back(args[0]);
}
else {
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
else {
todo.append(sz, args);
}
break;
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
else {
tocollect.push_back(e);
}
}
void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect) {
ptr_vector<expr> todo;
todo.append(formulas);
m_visited.reset();
VERIFY(check_model(formulas));
while (!todo.empty()) {
app* e = to_app(todo.back());
todo.pop_back();
if (!m_visited.is_marked(e)) {
process_formula(e, todo, tocollect);
m_visited.mark(e, true);
}
}
m_visited.reset();
}
expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
ptr_vector<expr> tocollect;
collect(formulas, tocollect);
m1.reset();
m2.reset();
for (unsigned i = 0; i < tocollect.size(); ++i) {
TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";);
for_each_expr(*this, m_visited, tocollect[i]);
}
unsigned sz = m_model->get_num_constants();
expr_ref e(m), eq(m), val(m);
expr_ref_vector model(m);
for (unsigned i = 0; i < sz; i++) {
e = m.mk_const(m_model->get_constant(i));
if (m_visited.is_marked(e)) {
val = eval(m_model, e);
eq = m.mk_eq(e, val);
model.push_back(eq);
}
}
m_visited.reset();
TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";);
return model;
}
void model_evaluator::eval_arith(app* e) {
rational r, r2;
#define ARG1 e->get_arg(0)
#define ARG2 e->get_arg(1)
unsigned arity = e->get_num_args();
for (unsigned i = 0; i < arity; ++i) {
expr* arg = e->get_arg(i);
if (is_x(arg)) {
set_x(e);
return;
}
SASSERT(!is_unknown(arg));
}
switch(e->get_decl_kind()) {
case OP_NUM:
VERIFY(m_arith.is_numeral(e, r));
set_number(e, r);
break;
case OP_IRRATIONAL_ALGEBRAIC_NUM:
set_x(e);
break;
case OP_LE:
set_bool(e, get_number(ARG1) <= get_number(ARG2));
break;
case OP_GE:
set_bool(e, get_number(ARG1) >= get_number(ARG2));
break;
case OP_LT:
set_bool(e, get_number(ARG1) < get_number(ARG2));
break;
case OP_GT:
set_bool(e, get_number(ARG1) > get_number(ARG2));
break;
case OP_ADD:
r = rational::zero();
for (unsigned i = 0; i < arity; ++i) {
r += get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_SUB:
r = get_number(e->get_arg(0));
for (unsigned i = 1; i < arity; ++i) {
r -= get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_UMINUS:
SASSERT(arity == 1);
set_number(e, get_number(e->get_arg(0)));
break;
case OP_MUL:
r = rational::one();
for (unsigned i = 0; i < arity; ++i) {
r *= get_number(e->get_arg(i));
}
set_number(e, r);
break;
case OP_DIV:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, get_number(ARG1) / r);
}
break;
case OP_IDIV:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, div(get_number(ARG1), r));
}
break;
case OP_REM:
// rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
r2 = mod(get_number(ARG1), r);
if (r.is_neg()) r2.neg();
set_number(e, r2);
}
break;
case OP_MOD:
SASSERT(arity == 2);
r = get_number(ARG2);
if (r.is_zero()) {
set_x(e);
}
else {
set_number(e, mod(get_number(ARG1), r));
}
break;
case OP_TO_REAL:
SASSERT(arity == 1);
set_number(e, get_number(ARG1));
break;
case OP_TO_INT:
SASSERT(arity == 1);
set_number(e, floor(get_number(ARG1)));
break;
case OP_IS_INT:
SASSERT(arity == 1);
set_bool(e, get_number(ARG1).is_int());
break;
case OP_POWER:
set_x(e);
break;
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
break;
}
}
void model_evaluator::inherit_value(expr* e, expr* v) {
expr* w;
SASSERT(!is_unknown(v));
SASSERT(m.get_sort(e) == m.get_sort(v));
if (is_x(v)) {
set_x(e);
}
else if (m.is_bool(e)) {
SASSERT(m.is_bool(v));
if (is_true(v)) set_true(e);
else if (is_false(v)) set_false(e);
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
else if (m_arith.is_int_real(e)) {
set_number(e, get_number(v));
}
else if (m.is_value(v)) {
set_value(e, v);
}
else if (m_values.find(v, w)) {
set_value(e, w);
}
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
void model_evaluator::eval_exprs(expr_ref_vector& es) {
model_ref mr(m_model);
for (unsigned j = 0; j < es.size(); ++j) {
if (m_array.is_as_array(es[j].get())) {
es[j] = eval(mr, es[j].get());
}
}
}
bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
SASSERT(m_array.is_array(a));
TRACE("pdr", tout << mk_pp(a, m) << "\n";);
while (m_array.is_store(a)) {
expr_ref_vector store(m);
store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
eval_exprs(store);
stores.push_back(store);
a = to_app(a)->get_arg(0);
}
if (m_array.is_const(a)) {
else_case = to_app(a)->get_arg(0);
return true;
}
while (m_array.is_as_array(a)) {
func_decl* f = m_array.get_as_array_func_decl(to_app(a));
func_interp* g = m_model->get_func_interp(f);
unsigned sz = g->num_entries();
unsigned arity = f->get_arity();
for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m);
func_entry const* fe = g->get_entry(i);
store.append(arity, fe->get_args());
store.push_back(fe->get_result());
for (unsigned j = 0; j < store.size(); ++j) {
if (!is_ground(store[j].get())) {
TRACE("pdr", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
return false;
}
}
eval_exprs(store);
stores.push_back(store);
}
else_case = g->get_else();
if (!else_case) {
TRACE("pdr", tout << "no else case " << mk_pp(a, m) << "\n";);
return false;
}
if (!is_ground(else_case)) {
TRACE("pdr", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";);
return false;
}
if (m_array.is_as_array(else_case)) {
model_ref mr(m_model);
else_case = eval(mr, else_case);
}
TRACE("pdr", tout << "else case: " << mk_pp(else_case, m) << "\n";);
return true;
}
TRACE("pdr", tout << "no translation: " << mk_pp(a, m) << "\n";);
return false;
}
/**
best effort evaluator of extensional array equality.
*/
void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) {
TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";);
expr_ref v1(m), v2(m);
m_model->eval(arg1, v1);
m_model->eval(arg2, v2);
if (v1 == v2) {
set_true(e);
return;
}
sort* s = m.get_sort(arg1);
sort* r = get_array_range(s);
// give up evaluating finite domain/range arrays
if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
return;
}
vector<expr_ref_vector> store;
expr_ref else1(m), else2(m);
if (!extract_array_func_interp(v1, store, else1) ||
!extract_array_func_interp(v2, store, else2)) {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
return;
}
if (else1 != else2) {
if (m.is_value(else1) && m.is_value(else2)) {
TRACE("pdr", tout
<< "defaults are different: " << mk_pp(e, m) << " "
<< mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
set_false(e);
}
else if (m_array.is_array(else1)) {
eval_array_eq(e, else1, else2);
}
else {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
}
return;
}
expr_ref s1(m), s2(m), w1(m), w2(m);
expr_ref_vector args1(m), args2(m);
args1.push_back(v1);
args2.push_back(v2);
for (unsigned i = 0; i < store.size(); ++i) {
args1.resize(1);
args2.resize(1);
args1.append(store[i].size()-1, store[i].c_ptr());
args2.append(store[i].size()-1, store[i].c_ptr());
s1 = m_array.mk_select(args1.size(), args1.c_ptr());
s2 = m_array.mk_select(args2.size(), args2.c_ptr());
m_model->eval(s1, w1);
m_model->eval(s2, w2);
if (w1 == w2) {
continue;
}
if (m.is_value(w1) && m.is_value(w2)) {
TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n";
tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
set_false(e);
}
else if (m_array.is_array(w1)) {
eval_array_eq(e, w1, w2);
if (is_true(e)) {
continue;
}
}
else {
TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
set_x(e);
}
return;
}
set_true(e);
}
void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) {
if (arg1 == arg2) {
set_true(e);
}
else if (m_array.is_array(arg1)) {
eval_array_eq(e, arg1, arg2);
}
else if (is_x(arg1) || is_x(arg2)) {
expr_ref eq(m), vl(m);
eq = m.mk_eq(arg1, arg2);
m_model->eval(eq, vl);
if (m.is_true(vl)) {
set_bool(e, true);
}
else if (m.is_false(vl)) {
set_bool(e, false);
}
else {
TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";);
set_x(e);
}
}
else if (m.is_bool(arg1)) {
bool val = is_true(arg1) == is_true(arg2);
SASSERT(val == (is_false(arg1) == is_false(arg2)));
if (val) {
set_true(e);
}
else {
set_false(e);
}
}
else if (m_arith.is_int_real(arg1)) {
set_bool(e, get_number(arg1) == get_number(arg2));
}
else {
expr* e1 = get_value(arg1);
expr* e2 = get_value(arg2);
if (m.is_value(e1) && m.is_value(e2)) {
set_bool(e, e1 == e2);
}
else if (e1 == e2) {
set_bool(e, true);
}
else {
TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
set_x(e);
}
}
}
void model_evaluator::eval_basic(app* e) {
expr* arg1, *arg2;
expr *argCond, *argThen, *argElse, *arg;
bool has_x = false;
unsigned arity = e->get_num_args();
switch(e->get_decl_kind()) {
case OP_AND:
for (unsigned j = 0; j < arity; ++j) {
expr * arg = e->get_arg(j);
if (is_false(arg)) {
set_false(e);
return;
}
else if (is_x(arg)) {
has_x = true;
}
else {
SASSERT(is_true(arg));
}
}
if (has_x) {
set_x(e);
}
else {
set_true(e);
}
break;
case OP_OR:
for (unsigned j = 0; j < arity; ++j) {
expr * arg = e->get_arg(j);
if (is_true(arg)) {
set_true(e);
return;
}
else if (is_x(arg)) {
has_x = true;
}
else {
SASSERT(is_false(arg));
}
}
if (has_x) {
set_x(e);
}
else {
set_false(e);
}
break;
case OP_NOT:
VERIFY(m.is_not(e, arg));
if (is_true(arg)) {
set_false(e);
}
else if (is_false(arg)) {
set_true(e);
}
else {
SASSERT(is_x(arg));
set_x(e);
}
break;
case OP_IMPLIES:
VERIFY(m.is_implies(e, arg1, arg2));
if (is_false(arg1) || is_true(arg2)) {
set_true(e);
}
else if (arg1 == arg2) {
set_true(e);
}
else if (is_true(arg1) && is_false(arg2)) {
set_false(e);
}
else {
SASSERT(is_x(arg1) || is_x(arg2));
set_x(e);
}
break;
case OP_IFF:
VERIFY(m.is_iff(e, arg1, arg2));
eval_eq(e, arg1, arg2);
break;
case OP_ITE:
VERIFY(m.is_ite(e, argCond, argThen, argElse));
if (is_true(argCond)) {
inherit_value(e, argThen);
}
else if (is_false(argCond)) {
inherit_value(e, argElse);
}
else if (argThen == argElse) {
inherit_value(e, argThen);
}
else if (m.is_bool(e)) {
SASSERT(is_x(argCond));
if (is_x(argThen) || is_x(argElse)) {
set_x(e);
}
else if (is_true(argThen) == is_true(argElse)) {
inherit_value(e, argThen);
}
else {
set_x(e);
}
}
else {
set_x(e);
}
break;
case OP_TRUE:
set_true(e);
break;
case OP_FALSE:
set_false(e);
break;
case OP_EQ:
VERIFY(m.is_eq(e, arg1, arg2));
eval_eq(e, arg1, arg2);
break;
case OP_DISTINCT: {
vector<rational> values;
for (unsigned i = 0; i < arity; ++i) {
expr* arg = e->get_arg(i);
if (is_x(arg)) {
set_x(e);
return;
}
values.push_back(get_number(arg));
}
std::sort(values.begin(), values.end());
for (unsigned i = 0; i + 1 < values.size(); ++i) {
if (values[i] == values[i+1]) {
set_false(e);
return;
}
}
set_true(e);
break;
}
default:
IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}
bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
ptr_vector<expr> todo(formulas);
while (!todo.empty()) {
expr * curr_e = todo.back();
if (!is_app(curr_e)) {
todo.pop_back();
continue;
}
app * curr = to_app(curr_e);
if (!is_unknown(curr)) {
todo.pop_back();
continue;
}
unsigned arity = curr->get_num_args();
for (unsigned i = 0; i < arity; ++i) {
if (is_unknown(curr->get_arg(i))) {
todo.push_back(curr->get_arg(i));
}
}
if (todo.back() != curr) {
continue;
}
todo.pop_back();
if (curr->get_family_id() == m_arith.get_family_id()) {
eval_arith(curr);
}
else if (curr->get_family_id() == m.get_basic_family_id()) {
eval_basic(curr);
}
else {
expr_ref vl(m);
m_model->eval(curr, vl);
assign_value(curr, vl);
}
IF_VERBOSE(35,verbose_stream() << "assigned "<<mk_pp(curr_e,m)
<<(is_true(curr_e) ? "true" : is_false(curr_e) ? "false" : "unknown") << "\n";);
SASSERT(!is_unknown(curr));
}
bool has_x = false;
for (unsigned i = 0; i < formulas.size(); ++i) {
expr * form = formulas[i];
SASSERT(!is_unknown(form));
TRACE("pdr_verbose",
tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" <<mk_pp(form, m)<< "\n";);
if (is_false(form)) {
IF_VERBOSE(0, verbose_stream() << "formula false in model: " << mk_pp(form, m) << "\n";);
UNREACHABLE();
}
if (is_x(form)) {
IF_VERBOSE(0, verbose_stream() << "formula undetermined in model: " << mk_pp(form, m) << "\n";);
TRACE("pdr", model_smt2_pp(tout, m, *m_model, 0););
has_x = true;
}
}
return !has_x;
}
expr_ref model_evaluator::eval(model_ref& model, func_decl* d) {
SASSERT(d->get_arity() == 0);
expr_ref result(m);
if (m_array.is_array(d->get_range())) {
expr_ref e(m);
e = m.mk_const(d);
result = eval(model, e);
}
else {
result = model->get_const_interp(d);
}
return result;
}
expr_ref model_evaluator::eval(model_ref& model, expr* e) {
expr_ref result(m);
m_model = model;
VERIFY(m_model->eval(e, result, true));
if (m_array.is_array(e)) {
vector<expr_ref_vector> stores;
expr_ref_vector args(m);
expr_ref else_case(m);
if (extract_array_func_interp(result, stores, else_case)) {
result = m_array.mk_const_array(m.get_sort(e), else_case);
while (!stores.empty() && stores.back().back() == else_case) {
stores.pop_back();
}
for (unsigned i = stores.size(); i > 0; ) {
--i;
args.resize(1);
args[0] = result;
args.append(stores[i]);
result = m_array.mk_store(args.size(), args.c_ptr());
}
return result;
}
}
return result;
}
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
ast_manager& m = fml.get_manager();
expr_ref_vector conjs(m);

80
src/muz/pdr/pdr_util.h
View file

@ -54,86 +54,6 @@ namespace pdr {
std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager);
std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager);
class model_evaluator {
ast_manager& m;
arith_util m_arith;
array_util m_array;
obj_map<expr,rational> m_numbers;
expr_ref_vector m_refs;
obj_map<expr, expr*> m_values;
model_ref m_model;
//00 -- non-visited
//01 -- X
//10 -- false
//11 -- true
expr_mark m1;
expr_mark m2;
expr_mark m_visited;
void reset();
void setup_model(model_ref& model);
void assign_value(expr* e, expr* v);
void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
void eval_arith(app* e);
void eval_basic(app* e);
void eval_eq(app* e, expr* arg1, expr* arg2);
void eval_array_eq(app* e, expr* arg1, expr* arg2);
void inherit_value(expr* e, expr* v);
inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); }
inline void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); }
inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); }
inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); }
inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); }
inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
inline void set_number(expr* x, rational const& v) {
set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v);
}
inline expr* get_value(expr* x) { return m_values.find(x); }
inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
bool check_model(ptr_vector<expr> const & formulas);
bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
void eval_exprs(expr_ref_vector& es);
public:
model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}
/**
\brief extract equalities from model that suffice to satisfy formula.
\pre model satisfies formulas
*/
expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
\brief extract literals from formulas that satisfy formulas.
\pre model satisfies formulas
*/
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
for_each_expr visitor.
*/
void operator()(expr* e) {}
expr_ref eval(model_ref& mdl, expr* e);
expr_ref eval(model_ref& mdl, func_decl* d);
};
/**
\brief replace variables that are used in many disequalities by

2
src/opt/fu_malik.cpp
View file

@ -243,7 +243,7 @@ namespace opt {
void set_solver() {
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
if (opt_s.is_dumping_benchmark())
if (opt_s.dump_benchmarks())
return;
solver& current_solver = s();

19
src/opt/opt_solver.cpp
View file

@ -35,7 +35,8 @@ namespace opt {
m_context(mgr, m_params),
m(mgr),
m_objective_enabled(false),
m_is_dump(false) {
m_dump_benchmarks(false),
m_dump_count(0) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
@ -45,7 +46,7 @@ namespace opt {
}
void opt_solver::updt_params(params_ref const & p) {
m_is_dump = p.get_bool("dump_benchmarks", false);
m_dump_benchmarks = p.get_bool("dump_benchmarks", false);
m_params.updt_params(p);
m_context.updt_params(p);
}
@ -105,22 +106,22 @@ namespace opt {
static unsigned g_checksat_count = 0;
bool opt_solver::is_dumping_benchmark() {
return m_is_dump;
bool opt_solver::dump_benchmarks() {
return m_dump_benchmarks;
}
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt_solver_na2as", {
tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n";
TRACE("opt", {
tout << "context size: " << m_context.size() << "\n";
for (unsigned i = 0; i < m_context.size(); ++i) {
tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
}
});
lbool r = m_context.check(num_assumptions, assumptions);
if (m_is_dump) {
if (dump_benchmarks()) {
std::stringstream file_name;
file_name << "opt_solver" << ++g_checksat_count << ".smt2";
file_name << "opt_solver" << ++m_dump_count << ".smt2";
std::ofstream buffer(file_name.str().c_str());
to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
buffer.close();

5
src/opt/opt_solver.h
View file

@ -46,7 +46,8 @@ namespace opt {
bool m_objective_enabled;
svector<smt::theory_var> m_objective_vars;
vector<inf_eps> m_objective_values;
bool m_is_dump;
bool m_dump_benchmarks;
unsigned m_dump_count;
statistics m_stats;
public:
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
@ -79,7 +80,7 @@ namespace opt {
static opt_solver& to_opt(solver& s);
void set_interim_stats(statistics & st);
bool is_dumping_benchmark();
bool dump_benchmarks();
class toggle_objective {
opt_solver& s;

260
src/smt/theory_pb.cpp
View file

@ -26,8 +26,6 @@ Notes:
namespace smt {
bool theory_pb::s_debug_conflict = true; // false; // true; //
void theory_pb::ineq::negate() {
m_lit.neg();
numeral sum(0);
@ -205,10 +203,54 @@ namespace smt {
}
k = k_new;
}
//
// normalize coefficients that fall within a range
// k/n <= ... < k/(n-1) for some n = 1,2,...
//
// e.g, k/n <= min <= max < k/(n-1)
// k/min <= n, n-1 < k/max
// . floor(k/max) = ceil(k/min) - 1
// . floor(k/max) < k/max
//
// example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2
// replace all coefficients by 1, and k by 2.
//
if (!k.is_one()) {
numeral min = coeff(0), max = coeff(0);
for (unsigned i = 1; i < size(); ++i) {
if (coeff(i) < min) min = coeff(i);
if (coeff(i) > max) max = coeff(i);
}
numeral n0 = k/max;
numeral n1 = floor(n0);
numeral n2 = ceil(k/min) - numeral::one();
if (n1 == n2 && !n0.is_int()) {
for (unsigned i = 0; i < size(); ++i) {
args[i].second = numeral::one();
}
k = n1 + numeral::one();
}
}
SASSERT(well_formed());
return l_undef;
}
app_ref theory_pb::ineq::to_expr(context& ctx, ast_manager& m) {
expr_ref tmp(m);
app_ref result(m);
svector<rational> coeffs;
expr_ref_vector args(m);
for (unsigned i = 0; i < size(); ++i) {
ctx.literal2expr(lit(i), tmp);
args.push_back(tmp);
coeffs.push_back(coeff(i));
}
pb_util pb(m);
result = pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k());
return result;
}
bool theory_pb::ineq::well_formed() const {
SASSERT(k().is_pos());
uint_set vars;
@ -406,12 +448,20 @@ namespace smt {
}
--c.m_watch_sz;
c.m_max_sum -= coeff;
if (c.max_coeff() == coeff) {
coeff = c.coeff(0);
for (unsigned i = 1; coeff != c.max_coeff() && i < c.m_watch_sz; ++i) {
if (coeff < c.coeff(i)) coeff = c.coeff(i);
}
c.set_max_coeff(coeff);
}
// current index of unwatched literal is c.watch_size().
}
void theory_pb::add_watch(ineq& c, unsigned i) {
bool_var v = c.lit(i).var();
literal lit = c.lit(i);
bool_var v = lit.var();
c.m_max_sum += c.coeff(i);
SASSERT(i >= c.watch_size());
if (i > c.watch_size()) {
@ -419,9 +469,9 @@ namespace smt {
}
++c.m_watch_sz;
ptr_vector<ineq>* ineqs;
if (!m_watch.find(v, ineqs)) {
if (!m_watch.find(lit.index(), ineqs)) {
ineqs = alloc(ptr_vector<ineq>);
m_watch.insert(v, ineqs);
m_watch.insert(lit.index(), ineqs);
}
ineqs->push_back(&c);
}
@ -500,8 +550,8 @@ namespace smt {
void theory_pb::assign_eh(bool_var v, bool is_true) {
context& ctx = get_context();
ptr_vector<ineq>* ineqs = 0;
if (m_watch.find(v, ineqs)) {
literal lit(v, !is_true);
if (m_watch.find(lit.index(), ineqs)) {
for (unsigned i = 0; i < ineqs->size(); ++i) {
if (assign_watch(v, is_true, *ineqs, i)) {
// i was removed from watch list.
@ -572,7 +622,7 @@ namespace smt {
if (maxsum < c.k()) {
literal_vector& lits = get_unhelpful_literals(c, false);
lits.push_back(~c.lit());
add_clause(c, ~lits[0], lits);
add_clause(c, lits);
}
else {
c.m_max_sum = numeral::zero();
@ -601,68 +651,63 @@ namespace smt {
unsigned w = c.find_lit(v, 0, c.watch_size());
SASSERT(ctx.get_assignment(c.lit()) == l_true);
SASSERT(is_true == c.lit(w).sign());
if (is_true == c.lit(w).sign()) {
//
// max_sum is decreased.
// Adjust set of watched literals.
//
numeral k = c.k();
numeral coeff = c.coeff(w);
for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) != l_false) {
add_watch(c, i);
}
}
//
// max_sum is decreased.
// Adjust set of watched literals.
//
if (c.max_sum() - coeff < k) {
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0
// create clause x1 or x2 or ~L
//
literal_vector& lits = get_unhelpful_literals(c, false);
lits.push_back(~c.lit());
add_clause(c, literal(v, !is_true), lits);
numeral k = c.k();
numeral coeff = c.coeff(w);
for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) {
if (ctx.get_assignment(c.lit(i)) != l_false) {
add_watch(c, i);
}
else {
del_watch(watch, watch_index, c, w);
removed = true;
if (c.max_sum() - coeff < k + c.max_coeff()) {
//
// opportunities for unit propagation for unassigned
// literals whose coefficients satisfy
// c.max_sum() - coeff < k
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0
// Create clauses x1 or ~L or x2
// x1 or ~L or x4
//
literal_vector& lits = get_unhelpful_literals(c, true);
lits.push_back(c.lit());
for (unsigned i = 0; i < c.size(); ++i) {
if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
add_assign(c, lits, c.lit(i));
}
}
if (c.max_sum() - coeff < k) {
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0
// create clause x1 or x2 or ~L
//
literal_vector& lits = get_unhelpful_literals(c, false);
lits.push_back(~c.lit());
add_clause(c, lits);
}
else {
del_watch(watch, watch_index, c, w);
removed = true;
if (c.max_sum() - coeff < k + c.max_coeff()) {
//
// opportunities for unit propagation for unassigned
// literals whose coefficients satisfy
// c.max_sum() - coeff < k
//
// L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0
// Create clauses x1 or ~L or x2
// x1 or ~L or x4
//
literal_vector& lits = get_unhelpful_literals(c, true);
lits.push_back(c.lit());
for (unsigned i = 0; i < c.size(); ++i) {
if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) {
add_assign(c, lits, c.lit(i));
}
}
//
// else: c.max_sum() >= k + c.max_coeff()
// we might miss opportunities for unit propagation if
// max_coeff is not the maximal coefficient
// of the current unassigned literal, but we can
// rely on eventually learning this from propagations.
//
}
//
// else: c.max_sum() >= k + c.max_coeff()
// we might miss opportunities for unit propagation if
// max_coeff is not the maximal coefficient
// of the current unassigned literal, but we can
// rely on eventually learning this from propagations.
//
}
//
// else: the current set of watch remain a potentially feasible assignment.
//
TRACE("pb",
tout << "assign: " << literal(v) << " <- " << is_true << "\n";
display(tout, c); );
@ -872,9 +917,9 @@ namespace smt {
while (m_assign_ineqs_trail.size() > sz) {
ineq* c = m_assign_ineqs_trail.back();
for (unsigned i = 0; i < c->watch_size(); ++i) {
bool_var w = c->lit(i).var();
literal w = c->lit(i);
ptr_vector<ineq>* ineqs = 0;
VERIFY(m_watch.find(w, ineqs));
VERIFY(m_watch.find(w.index(), ineqs));
for (unsigned j = 0; j < ineqs->size(); ++j) {
if ((*ineqs)[j] == c) {
std::swap((*ineqs)[j],(*ineqs)[ineqs->size()-1]);
@ -904,7 +949,7 @@ namespace smt {
void theory_pb::display(std::ostream& out) const {
u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
for (; it != end; ++it) {
out << "watch: " << literal(it->m_key) << " |-> ";
out << "watch: " << to_literal(it->m_key) << " |-> ";
watch_list const& wl = *it->m_value;
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
@ -988,7 +1033,7 @@ namespace smt {
void theory_pb::add_clause(ineq& c, literal conseq, literal_vector const& lits) {
void theory_pb::add_clause(ineq& c, literal_vector const& lits) {
inc_propagations(c);
m_stats.m_num_conflicts++;
context& ctx = get_context();
@ -999,21 +1044,16 @@ namespace smt {
tout << "\n";
display(tout, c, true););
#if 0
DEBUG_CODE(
if (s_debug_conflict) {
resolve_conflict(conseq, c);
});
#else
resolve_conflict(conseq, c);
#endif
resolve_conflict(c);
#if 1
justification* js = 0;
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(),
lits.size(), lits.c_ptr());
verbose_stream() << "\n";);
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
#endif
}
void theory_pb::set_mark(bool_var v, unsigned idx) {
@ -1022,9 +1062,7 @@ namespace smt {
m_conseq_index.resize(v+1, null_index);
}
SASSERT(!is_marked(v) || m_conseq_index[v] == idx);
if (m_conseq_index[v] == null_index) {
m_conseq_index[v] = idx;
}
m_conseq_index[v] = idx;
}
bool theory_pb::is_marked(bool_var v) const {
@ -1115,11 +1153,12 @@ namespace smt {
//
// modeled after sat_solver/smt_context
//
void theory_pb::resolve_conflict(literal conseq, ineq& c) {
bool theory_pb::resolve_conflict(ineq& c) {
TRACE("pb", tout << "RESOLVE: " << conseq << "\n"; display(tout, c, true););
TRACE("pb", display(tout, c, true););
bool_var v;
literal conseq;
context& ctx = get_context();
unsigned& lvl = m_conflict_lvl = 0;
for (unsigned i = 0; i < c.size(); ++i) {
@ -1127,12 +1166,8 @@ namespace smt {
lvl = std::max(lvl, ctx.get_assign_level(c.lit(i)));
}
}
SASSERT(lvl >= ctx.get_assign_level(c.lit()));
SASSERT(ctx.get_assignment(conseq) == l_true);
if (lvl == ctx.get_base_level()) {
return;
if (lvl < ctx.get_assign_level(c.lit()) || lvl == ctx.get_base_level()) {
return false;
}
m_num_marks = 0;
@ -1229,52 +1264,37 @@ namespace smt {
default:
UNREACHABLE();
}
m_lemma.normalize();
}
for (unsigned i = 0; i < m_lemma.size(); ++i) {
unset_mark(m_lemma.lit(i));
}
TRACE("pb", display(tout << "lemma: ", m_lemma););
// TBD:
// create clause m_ineq_literals => m_lemma;
//
#if 1
hoist_maximal_values();
IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
ast_manager& m = get_manager();
svector<rational> coeffs;
expr_ref_vector args(m);
expr_ref tmp(m);
for (unsigned i = 0; i < m_lemma.size(); ++i) {
ctx.literal2expr(m_lemma.lit(i), tmp);
args.push_back(tmp);
coeffs.push_back(m_lemma.coeff(i));
lbool is_true = m_lemma.normalize();
IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma););
switch(is_true) {
case l_true:
UNREACHABLE();
return false;
case l_false:
add_assign(c, m_ineq_literals, false_literal);
break;
default: {
app_ref tmp = m_lemma.to_expr(ctx, get_manager());
internalize_atom(tmp, false);
ctx.mark_as_relevant(tmp);
literal l(ctx.get_bool_var(tmp));
add_assign(c, m_ineq_literals, l);
break;
}
numeral k = m_lemma.k();
tmp = m_util.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k);
internalize_atom(to_app(tmp), false);
//m_ineq_literals.push_back(literal(ctx.get_bool_var(tmp)));
ctx.mark_as_relevant(tmp);
//justification* mjs = 0;
//ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), mjs, CLS_AUX_LEMMA, 0);
literal l(ctx.get_bool_var(tmp));
ineq* cc = 0;
if (m_ineqs.find(l.var(), cc)) {
add_assign(*cc, m_ineq_literals, l);
}
else {
ctx.assign(l, ctx.mk_justification(
theory_propagation_justification(
get_id(), ctx.get_region(),
m_ineq_literals.size(), m_ineq_literals.c_ptr(), l)));
// IF_VERBOSE(0, verbose_stream() << "Did not compile " << tmp << "\n";);
}
#endif
return true;
}
void theory_pb::hoist_maximal_values() {

9
src/smt/theory_pb.h
View file

@ -71,6 +71,7 @@ namespace smt {
numeral const& max_sum() const { return m_max_sum; }
numeral const& max_coeff() const { return m_max_coeff; }
void set_max_coeff(numeral const& n) { m_max_coeff = n; }
unsigned watch_size() const { return m_watch_sz; }
@ -91,8 +92,7 @@ namespace smt {
bool well_formed() const;
//static numeral gcd(numeral a, numeral b);
//static numeral lcm(numeral a, numeral b);
app_ref to_expr(context& ctx, ast_manager& m);
};
@ -119,7 +119,7 @@ namespace smt {
std::ostream& display(std::ostream& out, ineq& c, bool values = false) const;
virtual void display(std::ostream& out) const;
void add_clause(ineq& c, literal conseq, literal_vector const& lits);
void add_clause(ineq& c, literal_vector const& lits);
void add_assign(ineq& c, literal_vector const& lits, literal l);
literal_vector& get_lits();
@ -149,7 +149,7 @@ namespace smt {
void set_mark(bool_var v, unsigned idx);
void unset_mark(literal l);
void resolve_conflict(literal conseq, ineq& c);
bool resolve_conflict(ineq& c);
void process_antecedent(literal l, numeral coeff);
void process_ineq(ineq& c, literal conseq, numeral coeff);
@ -179,6 +179,5 @@ namespace smt {
virtual void restart_eh();
virtual void collect_statistics(::statistics & st) const;
static bool s_debug_conflict;
};
};

569
src/tactic/arith/lia2card_tactic.cpp
View file

@ -21,7 +21,6 @@ Notes:
#include"bound_manager.h"
#include"ast_pp.h"
#include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version.
#include"pb_decl_plugin.h"
#include"arith_decl_plugin.h"
@ -31,10 +30,10 @@ class lia2card_tactic : public tactic {
typedef obj_hashtable<expr> expr_set;
ast_manager & m;
arith_util a;
pb_util m_pb;
obj_map<expr, ptr_vector<expr> > m_uses;
obj_map<expr, expr*> m_converted;
pb_util m_pb;
mutable ptr_vector<expr> m_todo;
expr_set m_01s;
imp(ast_manager & _m, params_ref const & p):
m(_m),
@ -56,8 +55,6 @@ class lia2card_tactic : public tactic {
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);
@ -76,36 +73,9 @@ class lia2card_tactic : public tactic {
TRACE("pb", 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))) {
std::cout << "did not validate: " << mk_pp(*it, m) << "\n";
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);
extract_pb_substitution(g, sub);
expr_ref new_curr(m);
proof_ref new_pr(m);
@ -124,248 +94,110 @@ class lia2card_tactic : public tactic {
// 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_pb_substitution(goal_ref const& g, expr_safe_replace& sub) {
ast_mark mark;
for (unsigned i = 0; i < g->size(); i++) {
extract_pb_substitution(mark, g->form(i), sub);
}
}
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);
void extract_pb_substitution(ast_mark& mark, expr* fml, expr_safe_replace& sub) {
expr_ref tmp(m);
m_todo.reset();
m_todo.push_back(fml);
while (!m_todo.empty()) {
expr* e = m_todo.back();
m_todo.pop_back();
if (mark.is_marked(e) || !is_app(e)) {
continue;
}
mark.mark(e, true);
if (get_pb_relation(sub, e, tmp)) {
sub.insert(e, tmp);
continue;
}
app* ap = to_app(e);
m_todo.append(ap->get_num_args(), ap->get_args());
}
}
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));
}
else if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n));
}
else if (is_add(x, args) && is_unsigned(y, k)) { // x <= k
sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k));
}
else 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_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1)));
}
else {
UNREACHABLE();
}
}
else 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)));
}
else if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n+rational(1)));
}
else 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_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1));
}
else if (is_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k)
sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k)));
}
else {
UNREACHABLE();
}
}
else if (m.is_eq(fml, x, y)) {
if (!is_01var(x)) {
std::swap(x, y);
}
else 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());
}
}
else {
UNREACHABLE();
}
}
else 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]);
}
}
else {
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);
}
expr* r = m.mk_eq(x, a.mk_numeral(rational(1), m.get_sort(x)));
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) {
bool get_pb_relation(expr_safe_replace& sub, expr* fml, expr_ref& result) {
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;
}
}
expr_ref_vector args(m);
vector<rational> coeffs;
rational coeff;
if ((a.is_le(fml, x, y) || a.is_ge(fml, y, x)) &&
get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
get_pb_sum(y, -rational::one(), args, coeffs, coeff)) {
result = m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff);
return true;
}
TRACE("pb", tout << "Use not validated: " << mk_pp(fml, m) << "\n";);
else if ((a.is_lt(fml, y, x) || a.is_gt(fml, x, y)) &&
get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
get_pb_sum(y, -rational::one(), args, coeffs, coeff)) {
result = m.mk_not(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff));
return true;
}
else if (m.is_eq(fml, x, y) &&
get_pb_sum(x, rational::one(), args, coeffs, coeff) &&
get_pb_sum(y, -rational::one(), args, coeffs, coeff)) {
result = m.mk_and(m_pb.mk_le(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff),
m_pb.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), -coeff));
return true;
}
return false;
}
bool is_sum(expr* x) const {
bool get_pb_sum(expr* x, rational const& mul, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
expr *y, *z, *u;
rational r, q;
app* f = to_app(x);
bool ok = true;
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;
}
for (unsigned i = 0; ok && i < f->get_num_args(); ++i) {
ok = get_pb_sum(f->get_arg(i), mul, args, coeffs, coeff);
}
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 if (a.is_sub(x, y, z)) {
ok = get_pb_sum(y, mul, args, coeffs, coeff);
ok = ok && get_pb_sum(z, -mul, args, coeffs, coeff);
}
else if (a.is_uminus(x, y)) {
ok = get_pb_sum(y, -mul, args, coeffs, coeff);
}
else if (a.is_mul(x, y, z) && a.is_numeral(y, r)) {
ok = get_pb_sum(z, r*mul, args, coeffs, coeff);
}
else if (a.is_mul(x, z, y) && a.is_numeral(y, r)) {
ok = get_pb_sum(z, r*mul, args, coeffs, coeff);
}
else if (m.is_ite(x, y, z, u) && a.is_numeral(z, r) && a.is_numeral(u, q)) {
args.push_back(y);
coeffs.push_back(r*mul);
args.push_back(m.mk_not(y));
coeffs.push_back(q*mul);
}
else if (is_01var(x)) {
args.push_back(mk_01(x));
coeffs.push_back(mul);
}
else if (a.is_numeral(x, r)) {
coeff += mul*r;
}
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);
}
ok = false;
}
return ok;
}
};
@ -426,3 +258,240 @@ tactic * mk_lia2card_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(lia2card_tactic, m, p));
}
#if 0
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);
}
}
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));
}
else if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n));
}
else if (is_01_add(x, args) && is_unsigned(y, k)) { // x <= k
sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k));
}
else if (is_01_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_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1)));
}
else {
UNREACHABLE();
}
}
else 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)));
}
else if (is_01var(y) && a.is_numeral(x, n)) {
sub.insert(fml, mk_ge(y, n+rational(1)));
}
else if (is_01_add(x, args) && is_unsigned(y, k)) { // x < k
if (k == 0)
sub.insert(fml, m.mk_false());
else
sub.insert(fml, m_pb.mk_at_most_k(args.size(), args.c_ptr(), k-1));
}
else if (is_01_add(y, args) && is_unsigned(x, k)) { // k < y <=> not (y <= k)
sub.insert(fml, m.mk_not(m_pb.mk_at_most_k(args.size(), args.c_ptr(), k)));
}
else {
UNREACHABLE();
}
}
else 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());
}
}
else {
UNREACHABLE();
}
}
else if (is_01_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]);
}
}
else {
UNREACHABLE();
}
}
bool is_01_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) {
if (!is_01var(ap->get_arg(i))) {
return false;
}
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_01_sum(x) && !m.is_eq(fml)) {
return true;
}
}
if (is_01_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("pb", tout << "Use not validated: " << mk_pp(fml, m) << "\n";);
return false;
}
bool is_01_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;
}
void collect_uses(ast_mark& mark, expr* f) {
m_todo.reset();
m_todo.push_back(f);
while (!m_todo.empty()) {
f = m_todo.back();
m_todo.pop_back();
if (mark.is_marked(f)) {
continue;
}
mark.mark(f, true);
if (is_var(f)) {
continue;
}
if (is_quantifier(f)) {
m_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);
m_todo.push_back(arg);
}
}
}
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();
}
};
#endif