mirror of
https://github.com/Z3Prover/z3
synced 2025-08-19 09:40:20 +00:00
Wrap polysat tests in class
This commit is contained in:
Jakob Rath
parent
5886a8873c
commit
e0e03b3fc5
2 changed files with 105 additions and 93 deletions
|
|
@ -76,6 +76,7 @@ namespace polysat {
|
||||||
friend class inf_saturate;
|
friend class inf_saturate;
|
||||||
friend class constraint_manager;
|
friend class constraint_manager;
|
||||||
friend class scoped_solverv;
|
friend class scoped_solverv;
|
||||||
|
friend class test_polysat;
|
||||||
|
|
||||||
reslimit& m_lim;
|
reslimit& m_lim;
|
||||||
params_ref m_params;
|
params_ref m_params;
|
||||||
|
|
|
||||||
|
|
@ -4,7 +4,58 @@
|
||||||
#include "parsers/smt2/smt2parser.h"
|
#include "parsers/smt2/smt2parser.h"
|
||||||
#include <vector>
|
#include <vector>
|
||||||
|
|
||||||
|
namespace {
|
||||||
|
using namespace dd;
|
||||||
|
|
||||||
|
void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
|
||||||
|
SASSERT(k < 6);
|
||||||
|
unsigned i = k % 3;
|
||||||
|
unsigned j = k % 2;
|
||||||
|
if (i == 1)
|
||||||
|
std::swap(a, b);
|
||||||
|
else if (i == 2)
|
||||||
|
std::swap(a, c);
|
||||||
|
if (j == 1)
|
||||||
|
std::swap(b, c);
|
||||||
|
}
|
||||||
|
|
||||||
|
void permute_args(unsigned n, pdd& a, pdd& b, pdd& c, pdd& d) {
|
||||||
|
SASSERT(n < 24);
|
||||||
|
switch (n % 4) {
|
||||||
|
case 1:
|
||||||
|
std::swap(a, b);
|
||||||
|
break;
|
||||||
|
case 2:
|
||||||
|
std::swap(a, c);
|
||||||
|
break;
|
||||||
|
case 3:
|
||||||
|
std::swap(a, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
switch (n % 3) {
|
||||||
|
case 1:
|
||||||
|
std::swap(b, c);
|
||||||
|
break;
|
||||||
|
case 2:
|
||||||
|
std::swap(b, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
switch (n % 2) {
|
||||||
|
case 1:
|
||||||
|
std::swap(c, d);
|
||||||
|
break;
|
||||||
|
default:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
namespace polysat {
|
namespace polysat {
|
||||||
|
|
||||||
// test resolve, factoring routines
|
// test resolve, factoring routines
|
||||||
// auxiliary
|
// auxiliary
|
||||||
|
|
||||||
|
|
@ -64,6 +115,9 @@ namespace polysat {
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
class test_polysat {
|
||||||
|
public:
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Testing the solver's internal state.
|
* Testing the solver's internal state.
|
||||||
*/
|
*/
|
||||||
|
|
@ -738,52 +792,6 @@ namespace polysat {
|
||||||
s.expect_unsat();
|
s.expect_unsat();
|
||||||
}
|
}
|
||||||
|
|
||||||
void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
|
|
||||||
SASSERT(k < 6);
|
|
||||||
unsigned i = k % 3;
|
|
||||||
unsigned j = k % 2;
|
|
||||||
if (i == 1)
|
|
||||||
std::swap(a, b);
|
|
||||||
else if (i == 2)
|
|
||||||
std::swap(a, c);
|
|
||||||
if (j == 1)
|
|
||||||
std::swap(b, c);
|
|
||||||
}
|
|
||||||
|
|
||||||
void permute_args(unsigned n, pdd& a, pdd& b, pdd& c, pdd& d) {
|
|
||||||
SASSERT(n < 24);
|
|
||||||
switch (n % 4) {
|
|
||||||
case 1:
|
|
||||||
std::swap(a, b);
|
|
||||||
break;
|
|
||||||
case 2:
|
|
||||||
std::swap(a, c);
|
|
||||||
break;
|
|
||||||
case 3:
|
|
||||||
std::swap(a, d);
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
switch (n % 3) {
|
|
||||||
case 1:
|
|
||||||
std::swap(b, c);
|
|
||||||
break;
|
|
||||||
case 2:
|
|
||||||
std::swap(b, d);
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
switch (n % 2) {
|
|
||||||
case 1:
|
|
||||||
std::swap(c, d);
|
|
||||||
break;
|
|
||||||
default:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// xy < xz and !Omega(x*y) => y < z
|
// xy < xz and !Omega(x*y) => y < z
|
||||||
static void test_ineq_axiom1(unsigned bw = 32) {
|
static void test_ineq_axiom1(unsigned bw = 32) {
|
||||||
auto const bound = rational::power_of_two(bw/2);
|
auto const bound = rational::power_of_two(bw/2);
|
||||||
|
|
@ -1026,7 +1034,6 @@ namespace polysat {
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
|
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
|
||||||
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
|
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
|
||||||
// static void test_mixed_vars() {
|
// static void test_mixed_vars() {
|
||||||
|
|
@ -1040,9 +1047,11 @@ namespace polysat {
|
||||||
// // Expected result:
|
// // Expected result:
|
||||||
// }
|
// }
|
||||||
|
|
||||||
|
}; // class test_polysat
|
||||||
|
|
||||||
|
|
||||||
// convert assertions into internal solver state
|
// convert assertions into internal solver state
|
||||||
// support small grammar of formulas.
|
// support small grammar of formulas.
|
||||||
|
|
||||||
pdd to_pdd(ast_manager& m, solver& s, obj_map<expr, pdd*>& expr2pdd, expr* e) {
|
pdd to_pdd(ast_manager& m, solver& s, obj_map<expr, pdd*>& expr2pdd, expr* e) {
|
||||||
pdd* r = nullptr;
|
pdd* r = nullptr;
|
||||||
if (expr2pdd.find(e, r))
|
if (expr2pdd.find(e, r))
|
||||||
|
|
@ -1155,77 +1164,79 @@ namespace polysat {
|
||||||
for (auto const& [k,v] : expr2pdd)
|
for (auto const& [k,v] : expr2pdd)
|
||||||
dealloc(v);
|
dealloc(v);
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
} // namespace polysat
|
||||||
|
|
||||||
|
|
||||||
void tst_polysat() {
|
void tst_polysat() {
|
||||||
|
using namespace polysat;
|
||||||
|
|
||||||
polysat::test_band();
|
test_polysat::test_band();
|
||||||
return;
|
return;
|
||||||
|
|
||||||
polysat::test_quot_rem();
|
test_polysat::test_quot_rem();
|
||||||
return;
|
return;
|
||||||
|
|
||||||
polysat::test_ineq_axiom1();
|
test_polysat::test_ineq_axiom1();
|
||||||
polysat::test_ineq_axiom2();
|
test_polysat::test_ineq_axiom2();
|
||||||
polysat::test_ineq_axiom3();
|
test_polysat::test_ineq_axiom3();
|
||||||
polysat::test_ineq_axiom4();
|
test_polysat::test_ineq_axiom4();
|
||||||
polysat::test_ineq_axiom5();
|
test_polysat::test_ineq_axiom5();
|
||||||
polysat::test_ineq_axiom6();
|
test_polysat::test_ineq_axiom6();
|
||||||
return;
|
return;
|
||||||
|
|
||||||
polysat::test_ineq_basic4();
|
test_polysat::test_ineq_basic4();
|
||||||
//return;
|
//return;
|
||||||
|
|
||||||
polysat::test_ineq_basic6();
|
test_polysat::test_ineq_basic6();
|
||||||
|
|
||||||
// polysat::test_monot_bounds(8);
|
// test_polysat::test_monot_bounds(8);
|
||||||
|
|
||||||
polysat::test_add_conflicts();
|
test_polysat::test_add_conflicts();
|
||||||
polysat::test_wlist();
|
test_polysat::test_wlist();
|
||||||
polysat::test_l1();
|
test_polysat::test_l1();
|
||||||
polysat::test_l2();
|
test_polysat::test_l2();
|
||||||
polysat::test_l3();
|
test_polysat::test_l3();
|
||||||
polysat::test_l4();
|
test_polysat::test_l4();
|
||||||
polysat::test_l5();
|
test_polysat::test_l5();
|
||||||
polysat::test_p1();
|
test_polysat::test_p1();
|
||||||
polysat::test_p2();
|
test_polysat::test_p2();
|
||||||
polysat::test_p3();
|
test_polysat::test_p3();
|
||||||
|
|
||||||
polysat::test_ineq_basic1();
|
test_polysat::test_ineq_basic1();
|
||||||
polysat::test_ineq_basic2();
|
test_polysat::test_ineq_basic2();
|
||||||
polysat::test_ineq_basic3();
|
test_polysat::test_ineq_basic3();
|
||||||
polysat::test_ineq_basic4();
|
test_polysat::test_ineq_basic4();
|
||||||
polysat::test_ineq_basic5();
|
test_polysat::test_ineq_basic5();
|
||||||
polysat::test_ineq_basic6();
|
test_polysat::test_ineq_basic6();
|
||||||
|
|
||||||
polysat::test_cjust();
|
test_polysat::test_cjust();
|
||||||
polysat::test_subst();
|
test_polysat::test_subst();
|
||||||
polysat::test_monot_bounds(2);
|
test_polysat::test_monot_bounds(2);
|
||||||
|
|
||||||
polysat::test_var_minimize();
|
test_polysat::test_var_minimize();
|
||||||
|
|
||||||
polysat::test_ineq1();
|
test_polysat::test_ineq1();
|
||||||
polysat::test_ineq2();
|
test_polysat::test_ineq2();
|
||||||
polysat::test_monot();
|
test_polysat::test_monot();
|
||||||
|
|
||||||
return;
|
return;
|
||||||
|
|
||||||
polysat::test_ineq_axiom1();
|
test_polysat::test_ineq_axiom1();
|
||||||
polysat::test_ineq_axiom2();
|
test_polysat::test_ineq_axiom2();
|
||||||
polysat::test_ineq_axiom3();
|
test_polysat::test_ineq_axiom3();
|
||||||
polysat::test_ineq_axiom4();
|
test_polysat::test_ineq_axiom4();
|
||||||
polysat::test_ineq_axiom5();
|
test_polysat::test_ineq_axiom5();
|
||||||
polysat::test_ineq_axiom6();
|
test_polysat::test_ineq_axiom6();
|
||||||
#if 0
|
#if 0
|
||||||
polysat::test_ineq_non_axiom4(32, 5);
|
test_polysat::test_ineq_non_axiom4(32, 5);
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
// inefficient conflicts:
|
// inefficient conflicts:
|
||||||
// Takes time: polysat::test_monot_bounds_full();
|
// Takes time: test_polysat::test_monot_bounds_full();
|
||||||
|
|
||||||
polysat::test_monot_bounds_simple(8);
|
test_polysat::test_monot_bounds_simple(8);
|
||||||
polysat::test_fixed_point_arith_div_mul_inverse();
|
test_polysat::test_fixed_point_arith_div_mul_inverse();
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue