From 16af539938b6fc83dae023a8876a5b55a49441c2 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 12:41:03 +0000 Subject: [PATCH] Improvement. Fix the difficulty score for subtraction. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1272 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/DifficultyScore.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h index a7e550f..5392a8e 100644 --- a/src/STPManager/DifficultyScore.h +++ b/src/STPManager/DifficultyScore.h @@ -50,6 +50,11 @@ private: // without getting the width of the child it'd always be 2. score = std::max(b[0].GetValueWidth(),1u) * (b.Degree()); } + else if (k == BVSUB) + { + // We convert subtract to a + (-b), we want the difficulty scores to be same. + score = std::max(b[0].GetValueWidth(),1u) * 3; + } else { score = std::max(b.GetValueWidth(),1u) * (b.Degree()); -- 2.47.3