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

add handling of misc operations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-18 14:30:56 -07:00
parent 3da37f4fb5
commit 4405fa1156
2 changed files with 34 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/bv_decl_plugin.h
View file

@ -364,6 +364,7 @@ public:
MATCH_UNARY(is_bv_not);
MATCH_BINARY(is_bv_add);
MATCH_BINARY(is_bv_sub);
MATCH_BINARY(is_bv_mul);
MATCH_BINARY(is_bv_sle);
MATCH_BINARY(is_bv_ule);

52
src/test/polysat.cpp
View file

@ -727,33 +727,44 @@ namespace polysat {
return *r;
bv_util bv(m);
rational n;
unsigned sz;
unsigned sz = bv.get_bv_size(e);
expr* a, *b;
if (bv.is_bv_add(e, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
r = alloc(pdd, pa + pb);
}
else if (bv.is_bv_sub(e, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
r = alloc(pdd, pa - pb);
}
else if (bv.is_bv_mul(e, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
r = alloc(pdd, pa * pb);
}
else if (bv.is_bv_udiv(e, a, b)) {
std::cout << "TODO udiv\n";
// quot = udiv(a, b)
// quot*b + rem == a
// rem < b or b == 0
// quot*b does not overflow
auto quot = s.var(s.add_var(sz));
auto rem = s.var(s.add_var(sz));
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
s.add_eq(quot*pb + rem - pa);
s.add_ult(rem, pb);
// TODO:
// s.add_mul_noovfl(quot, pb);
r = alloc(pdd, quot);
}
else if (bv.is_numeral(e, n, sz)) {
else if (bv.is_numeral(e, n, sz))
r = alloc(pdd, s.value(n, sz));
}
else if (is_uninterp(e)) {
sz = bv.get_bv_size(e);
else if (is_uninterp(e))
r = alloc(pdd, s.var(s.add_var(sz)));
}
else
std::cout << "unknown " << mk_pp(e, m) << "\n";
if (!r) {
sz = bv.get_bv_size(e);
else {
std::cout << "UNKNOWN " << mk_pp(e, m) << "\n";
r = alloc(pdd, s.var(s.add_var(sz)));
}
expr2pdd.insert(e, r);
@ -793,15 +804,21 @@ namespace polysat {
else if (bv.is_slt(fm, a, b) || bv.is_sgt(fm, b, a)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
std::cout << "slt\n";
if (is_not)
s.add_sle(pb, pa);
else
s.add_slt(pa, pb);
}
else if (bv.is_sle(fm, a, b) || bv.is_sge(fm, b, a)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
std::cout << "sle\n";
if (is_not)
s.add_slt(pb, pa);
else
s.add_sle(pa, pb);
}
else {
std::cout << "formula: " << is_not << " " << mk_pp(fm, m) << "\n";
std::cout << "SKIP: " << mk_pp(fm, m) << "\n";
}
}
for (auto [k,v] : expr2pdd)
@ -842,19 +859,15 @@ void tst_polysat() {
#endif
}
// TBD also add test that loads from a file and runs the polysat engine.
// sketch follows below:
#include "ast/bv_decl_plugin.h"
void tst_polysat_argv(char** argv, int argc, int& i) {
// set up SMT2 parser to extract assertions
// assume they are simple bit-vector equations (and inequations)
// convert to solver state.
std::cout << "argc " << argc << "\n";
if (argc < 3) {
std::cerr << "Usage: " << argv[0] << " FILE\n";
return;
@ -872,5 +885,6 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
auto fmls = ctx.assertions();
polysat::scoped_solver s("polysat");
polysat::internalize(m, s, fmls);
std::cout << "checking\n";
s.check();
}