From f6c720fc056082b7b3605bff74bf1b2d588b57f7 Mon Sep 17 00:00:00 2001 From: msoos Date: Wed, 2 Dec 2009 16:34:56 +0000 Subject: [PATCH] Disabling var-replacer feature of CryptoMiniSat to allow for programmable solver git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@449 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat2/Solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index e8d4186..bcf6931 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -175,7 +175,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + //ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); xor_clause_inverted ^= ps[i].sign(); ps[i] ^= ps[i].sign(); @@ -251,7 +251,7 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + //ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); if (value(ps[i]) == l_True || ps[i] == ~p) return true; else if (value(ps[i]) != l_False && ps[i] != p) -- 2.47.3