Commit 7352f9a6 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

Testing cadical bind

parent ecd8cbb0
......@@ -75,23 +75,22 @@ SUBool::TestCadical::TestSimple() const
return (val == PartialValue::TRUE);
}
#if 0
bool
SUBool::TestGlucose::TestLearntsRandom(const unsigned nrounds,
SUBool::TestCadical::TestLearntsRandom(const unsigned nrounds,
const unsigned nclauses, const unsigned clause_size,
const unsigned nvars) const
{
std::cout << "Testing glucose learnts" << std::endl;
std::cout << "Testing cadical learnts" << std::endl;
for (unsigned round = 0; round < nrounds; ++round)
{
CNF cnf = random_k_cnf(nclauses, clause_size, nvars);
std::cout << "Round " << round + 1 << std::endl;
//<<", cnf:"<<std::endl; std::cout<<cnf;
SimpSolverWrapper wrap;
CadicalWrapper wrap(true);
auto &g = wrap.Solver();
if (!g.AddCnf(cnf))
{
std::cout << "Glucose returned false when adding CNF [FAILED]"
std::cout << "Cadical returned false when adding CNF [FAILED]"
<< std::endl;
return false;
}
......@@ -104,9 +103,9 @@ SUBool::TestGlucose::TestLearntsRandom(const unsigned nrounds,
}
std::cout << std::endl;
bool result = g.Solve(assump);
std::cout << "Glucose solve result: " << (result ? "SAT" : "UNSAT")
std::cout << "Cadical solve result: " << (result ? "SAT" : "UNSAT")
<< std::endl;
auto learnts = g.Learnts();
auto learnts = g.ExtractLearnts();
std::cout << "...nLearnts=" << learnts.size() << std::endl;
bool all_implicates = true;
for (const auto &clause : learnts)
......@@ -133,16 +132,16 @@ SUBool::TestGlucose::TestLearntsRandom(const unsigned nrounds,
}
bool
SUBool::TestGlucose::TestConflict(
SUBool::TestCadical::TestConflict(
const CNF &cnf, const std::vector<Literal> &assumptions) const
{
std::cout << "Testing glucose conflict clause with assumptions: ";
std::cout << "Testing cadical conflict clause with assumptions: ";
for (unsigned i = 0; i < assumptions.size(); ++i)
{
std::cout << " " << assumptions[i];
}
std::cout << std::endl;
SimpSolverWrapper wrap;
CadicalWrapper wrap(false);
auto &g = wrap.Solver();
g.AddCnf(cnf);
if (g.Solve(assumptions))
......@@ -169,11 +168,11 @@ SUBool::TestGlucose::TestConflict(
}
bool
SUBool::TestGlucose::TestConflicts(const unsigned nrounds,
SUBool::TestCadical::TestConflicts(const unsigned nrounds,
const unsigned nconflicts_per_round, const unsigned nvars,
const unsigned nclauses) const
{
std::cout << "Testing glucose conflict clause" << std::endl;
std::cout << "Testing cadical conflict clause" << std::endl;
for (unsigned round = 0; round < nrounds; ++round)
{
auto sat_cnf = random_sat_cnf(nclauses, nvars);
......@@ -193,11 +192,11 @@ SUBool::TestGlucose::TestConflicts(const unsigned nrounds,
}
bool
SUBool::TestGlucose::TestIncrementalSimple() const
SUBool::TestCadical::TestIncrementalSimple() const
{
std::cout << "Testing glucose incremental capabilities on a simple CNF"
std::cout << "Testing cadical incremental capabilities on a simple CNF"
<< std::endl;
IncSolverWrapper wrap;
CadicalWrapper wrap(false);
auto &g = wrap.Solver();
auto cnf = Dimacs::parse_cnf(dimacs);
std::cout << cnf << std::endl;
......@@ -216,12 +215,12 @@ SUBool::TestGlucose::TestIncrementalSimple() const
}
bool
SUBool::TestGlucose::TestIncremental(const unsigned n_rounds,
SUBool::TestCadical::TestIncremental(const unsigned n_rounds,
const unsigned n_clauses, const unsigned n_vars,
const unsigned assump_length) const
{
std::cout << "Testing glucose incremental capabilities" << std::endl;
IncSolverWrapper wrap;
std::cout << "Testing cadical incremental capabilities" << std::endl;
CadicalWrapper wrap(false);
auto &g = wrap.Solver();
auto sat_cnf = random_sat_cnf(n_clauses, n_vars);
g.AddCnf(sat_cnf.first);
......@@ -235,7 +234,7 @@ SUBool::TestGlucose::TestIncremental(const unsigned n_rounds,
std::cout << "Trying assumptions: " << VectorPrinter(assump) << std::endl;
auto b = g.Solve(assump);
std::cout << "Result: " << (b ? "SAT" : "UNSAT") << std::endl;
SimpSolverWrapper wrap2;
CadicalWrapper wrap2(false);
auto &g2 = wrap2.Solver();
g2.AddCnf(sat_cnf.first);
auto b2 = g2.Solve(assump);
......@@ -250,18 +249,15 @@ SUBool::TestGlucose::TestIncremental(const unsigned n_rounds,
std::cout << "[OK]" << std::endl;
return true;
}
#endif
bool
SUBool::TestCadical::RunTests() const
{
bool success = TestSimple();
#if 0
success = TestLearntsRandom(100, 150, 3, 30) && success;
success = TestConflicts(10, 10, 30, 50) && success;
success = TestIncrementalSimple() && success;
success = TestIncremental(100, 1000, 500, 50) && success;
#endif
return success;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment