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

start update with expr-inverter to handle PB

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-22 18:17:07 -08:00
parent b592ce4707
commit 4f4cafbc98
1 changed files with 80 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

80
src/ast/converters/expr_inverter.cpp
View file

@ -20,6 +20,7 @@ Author:
#include "ast/ast_util.h"
#include "ast/arith_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/pb_decl_plugin.h"
#include "ast/converters/expr_inverter.h"
class basic_expr_inverter : public iexpr_inverter {
@ -743,6 +744,84 @@ public:
}
};
#if 0
class pb_expr_inverter : public iexpr_inverter {
pb_util pb;
public:
pb_expr_inverter(ast_manager& m) : iexpr_inverter(m), pb(m) {}
family_id get_fid() const override { return pb.get_family_id(); }
bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r) override {
rational k, c;
unsigned new_k = 0;
expr_ref_vector new_args(m), uncnstr_args(m);
vector<rational> coeffs;
switch (f->get_decl_kind()) {
case OP_AT_MOST_K:
// a' + b' + c + d <= 3 -> r := c + d <= 1
// a' + b' + c + d <= 1 -> r := c + d <= 1
// a' + b' + c' + d <= 2 -> r := fresh
// a', b', c' := ~r
k = pb.get_k(f);
if (!k.is_unsigned())
return false;
for (unsigned i = 0; i < num; ++i)
if (uncnstr(args[i]))
uncnstr_args.push_back(args[i]);
else
new_args.push_back(args[i]);
if (uncnstr_args.empty())
return false;
if (new_args.size() <= k && uncnstr_args.size() > k)
mk_fresh_uncnstr_var_for(f, r);
else if (new_args.size() <= k) // k >= uncnstr_args.size()
r = pb.mk_at_most_k(new_args, k.get_unsigned() - uncnstr_args.size());
else // |new_args| > k
r = pb.mk_at_most_k(new_args, k.get_unsigned());
if (m_mc) {
for (unsigned i = 0; i < uncnstr_args.size(); ++i)
add_def(uncnstr_args.get(i), m.mk_not(r));
}
return true;
case OP_AT_LEAST_K:
k = pb.get_k(f);
if (!k.is_unsigned())
return false;
for (unsigned i = 0; i < num; ++i)
if (uncnstr(args[i]))
uncnstr_args.push_back(args[i]);
else
new_args.push_back(args[i]);
if (uncnstr_args.empty())
return false;
// cases k <= uncstr_args.size()
// k > uncstr_args.size()
return false;
case OP_PB_LE:
// 2*x + 3*y + z + 2*u <= k -> r
// r := z + 2u <=
//
k = pb.get_k(f);
for (unsigned i = 0; i < num; ++i)
if (uncnstr(args[i]))
uncnstr_args.push_back(args[i]), c += pb.get_coeff(f, i);
else
new_args.push_back(args[i]), coeffs.push_back(pb.get_coeff(f, i));
if (uncnstr_args.empty())
return false;
return false;
default:
return false;
}
}
bool mk_diff(expr* t, expr_ref& r) override {
return false;
}
};
#endif
class seq_expr_inverter : public iexpr_inverter {
seq_util seq;
@ -870,6 +949,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
add(alloc(dt_expr_inverter, m));
add(alloc(basic_expr_inverter, m, *this));
add(alloc(seq_expr_inverter, m));
//add(alloc(pb_expr_inverter, m));
}