From c683e624bcde40592bab095460c9e754adb675bc Mon Sep 17 00:00:00 2001 From: Dimitri Lozeve Date: Wed, 3 Aug 2016 20:33:25 +0100 Subject: [PATCH] Changed arguments order to match other functions --- Sat.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Sat.hs b/Sat.hs index 44c4854..8f76a0a 100644 --- a/Sat.hs +++ b/Sat.hs @@ -195,13 +195,13 @@ resolveAll f = case findMatchingPair f of -- applies resolveAll and the unit propagation and pure literals -- rules, until it reaches the empty formula (therefore SAT) or an -- empty clause (therefore UNSAT). -resolutionSolve :: Assignment -> CNF -> Result -resolutionSolve asst [] = SAT asst -resolutionSolve asst f +resolutionSolve :: (CNF, Assignment) -> Result +resolutionSolve ([], asst) = SAT asst +resolutionSolve (f, asst) | [] `elem` f = UNSAT | otherwise = let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in - resolutionSolve asst' (resolveAll f') + resolutionSolve (resolveAll f', asst')