diff --git a/minisat/tests/reloc64.cc b/minisat/tests/reloc64.cc new file mode 100644 index 00000000..7f7c9c01 --- /dev/null +++ b/minisat/tests/reloc64.cc @@ -0,0 +1,60 @@ +/**************************************************************************************[reloc64.cc] +Copyright (c) 2021, Norbert Manthey + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "tests/TestSolver.h" + +using namespace MERGESAT_NSPACE; + +bool TestSolver::test_entrypoint() +{ + /* Make sure the values are as expected after solving */ + test_assert(okay(), "solver has to be okay"); + + test_assert(clauses.size() == 1, "there is a clause to work with"); + + CRef r = clauses[0]; + Clause &c = ca[r]; + + CRef new_ref = (1UL << 33) + 3UL; + c.relocate(new_ref); + CRef c_ref = c.relocation(); + + test_assert(new_ref == c_ref, "stored ref should be working"); + + return true; +} + +int main(int argc, char **argv) +{ + TestSolver solver; + + solver.verbosity = 0; + + while (solver.nVars() < 2) solver.newVar(); + + solver.addClause(mkLit(1), mkLit(2)); + + bool status = solver.solve(); + + test_assert(status == true, "The given formula has to be satisfiable"); + + status = solver.test_entrypoint(); + test_assert(status == true, "Relocation should be successful."); + return 0; +}