mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Remove tst_polysat_argv

Browse source
This commit is contained in:
Jakob Rath 2022-11-17 15:23:50 +01:00
parent 81150f433a
commit 80a2ac64de
2 changed files with 0 additions and 180 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/test/main.cpp
View file

@ -264,7 +264,6 @@ int main(int argc, char ** argv) {
//TST_ARGV(hs);
TST(finder);
TST(polysat);
TST_ARGV(polysat_argv);
TST(fixplex);
TST(mod_interval);
TST(viable);

179
src/test/polysat.cpp
View file

@ -1427,136 +1427,6 @@ namespace polysat {
}; // class test_fi
// convert assertions into internal solver state
// support small grammar of formulas.
pdd to_pdd(ast_manager& m, solver& s, obj_map<expr, pdd*>& expr2pdd, expr* e) {
pdd* r = nullptr;
if (expr2pdd.find(e, r))
return *r;
bv_util bv(m);
rational n;
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)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
auto qr = s.quot_rem(pa, pb);
r = alloc(pdd, std::get<0>(qr));
}
else if (bv.is_bv_urem(e, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
auto qr = s.quot_rem(pa, pb);
r = alloc(pdd, std::get<1>(qr));
}
else if (bv.is_bv_lshr(e, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
r = alloc(pdd, s.lshr(pa, pb));
}
else if (bv.is_bv_and(e) && to_app(e)->get_num_args() == 2) {
a = to_app(e)->get_arg(0);
b = to_app(e)->get_arg(1);
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
r = alloc(pdd, s.band(pa, pb));
}
else if (bv.is_bv_neg(e)) {
a = to_app(e)->get_arg(0);
auto pa = to_pdd(m, s, expr2pdd, a);
r = alloc(pdd, -pa);
}
else if (bv.is_numeral(e, n, sz))
r = alloc(pdd, s.value(n, sz));
else if (is_uninterp(e))
r = alloc(pdd, s.var(s.add_var(sz)));
else {
std::cout << "UNKNOWN " << mk_pp(e, m) << "\n";
NOT_IMPLEMENTED_YET();
r = alloc(pdd, s.var(s.add_var(sz)));
}
expr2pdd.insert(e, r);
return *r;
}
void internalize(ast_manager& m, solver& s, ptr_vector<expr>& fmls) {
bv_util bv(m);
obj_map<expr, pdd*> expr2pdd;
for (expr* fm : fmls) {
bool is_not = m.is_not(fm, fm);
expr* a, *b;
if (m.is_eq(fm, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
if (is_not)
s.add_diseq(pa - pb);
else
s.add_eq(pa - pb);
}
else if (bv.is_ult(fm, a, b) || bv.is_ugt(fm, b, a)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
if (is_not)
s.add_ule(pb, pa);
else
s.add_ult(pa, pb);
}
else if (bv.is_ule(fm, a, b) || bv.is_uge(fm, b, a)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
if (is_not)
s.add_ult(pb, pa);
else
s.add_ule(pa, pb);
}
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);
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);
if (is_not)
s.add_slt(pb, pa);
else
s.add_sle(pa, pb);
}
else if (bv.is_bv_umul_no_ovfl(fm, a, b)) {
auto pa = to_pdd(m, s, expr2pdd, a);
auto pb = to_pdd(m, s, expr2pdd, b);
if (is_not)
s.add_umul_ovfl(pa, pb);
else
s.add_umul_noovfl(pa, pb);
}
else {
std::cout << "SKIP: " << mk_pp(fm, m) << "\n";
}
}
for (auto const& [k,v] : expr2pdd)
dealloc(v);
}
} // namespace polysat
@ -1657,52 +1527,3 @@ void tst_polysat() {
if (collect_test_records)
display_test_records(test_records, std::cout);
}
#include "ast/bv_decl_plugin.h"
polysat::scoped_solver* g_solver = nullptr;
static void display_statistics() {
if (g_solver) {
statistics st;
g_solver->collect_statistics(st);
std::cout << st << "\n";
}
}
static void STD_CALL polysat_argv_on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
display_statistics();
raise(SIGINT);
}
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.
signal(SIGINT, polysat_argv_on_ctrl_c);
if (argc < 3) {
std::cerr << "Usage: " << argv[0] << " FILE\n";
return;
}
std::cout << "processing " << argv[2] << "\n";
std::ifstream is(argv[2]);
if (is.bad() || is.fail()) {
std::cout << "failed to open " << argv[2] << "\n";
return;
}
cmd_context ctx(false);
ast_manager& m = ctx.m();
ctx.set_ignore_check(true);
VERIFY(parse_smt2_commands(ctx, is));
ptr_vector<expr> fmls = ctx.assertions();
polysat::scoped_solver s("polysat");
s.set_max_conflicts(1000);
g_solver = &s;
polysat::internalize(m, s, fmls);
std::cout << "checking\n";
s.check();
}