tests: add reloc 64bit

Signed-off-by: Norbert Manthey <[email protected]>

Author: conp-solutions

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;
+}