Implement printSolution option for all tasks

src/Config.hs

@@ -11,7 +11,7 @@ import Formula.Util
 
 
 
-newtype Number = Number {value :: Maybe Int} deriving (Typeable, Generic)
+newtype Number = Number {value :: Maybe Int} deriving (Show,Typeable, Generic)
 
 
 newtype StepAnswer = StepAnswer {step :: Maybe (Literal, Clause)} deriving (Typeable, Generic)
@@ -26,6 +26,7 @@ data PickInst = PickInst {
                  cnfs    :: ![Cnf]
                , correct :: !Int
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -34,20 +35,23 @@ dPickInst =  PickInst
           { cnfs = [mkCnf [mkClause [Literal 'A', Not 'B']], mkCnf [mkClause [Not 'A', Literal 'B']]]
           , correct = 1
           , addText = Nothing
+          , showSolution = False
           }
 
 
 
 data MaxInst = MaxInst {
                  cnf     :: !Cnf
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
 dMaxInst :: MaxInst
 dMaxInst =  MaxInst
           { cnf = mkCnf [mkClause [Literal 'A', Not 'B']]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -56,13 +60,15 @@ dMaxInst =  MaxInst
 data MinInst = MinInst {
                  dnf     :: !Dnf
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
 dMinInst :: MinInst
 dMinInst =  MinInst
           { dnf = mkDnf [mkCon [Literal 'A', Not 'B']]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -71,6 +77,7 @@ data FillInst = FillInst {
                  cnf     :: !Cnf
                , missing :: ![Int]
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -79,6 +86,7 @@ dFillInst =  FillInst
           { cnf = mkCnf [mkClause [Literal 'A', Not 'B']]
           , missing = [1,4]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -87,6 +95,7 @@ data DecideInst = DecideInst {
                  cnf     :: !Cnf
                , changed :: ![Int]
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -95,6 +104,7 @@ dDecideInst =  DecideInst
           { cnf = mkCnf [mkClause [Literal 'A', Not 'B']]
           , changed = [1,4]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -103,6 +113,7 @@ data StepInst = StepInst {
                  clause1 :: !Clause
                , clause2 :: !Clause
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -111,13 +122,15 @@ dStepInst =  StepInst
           { clause1 = mkClause [Not 'A', Not 'C', Literal 'B']
           , clause2 = mkClause [Literal 'A', Not 'C']
           , addText = Nothing
+          , showSolution = False
           }
 
 
 
 data ResolutionInst = ResolutionInst {
                  clauses :: ![Clause]
                , addText    :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -130,6 +143,7 @@ dResInst =  ResolutionInst
               , mkClause [Not 'B']
               ]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -139,6 +153,7 @@ data PrologInst = PrologInst {
                  literals1 :: !PrologClause
                , literals2 :: !PrologClause
                , addText :: !(Maybe String)
+               , showSolution :: Bool
                }
                deriving (Typeable, Generic)
 
@@ -148,6 +163,7 @@ dPrologInst =  PrologInst
           { literals1 = mkPrologClause [PrologLiteral True "pred" ["fact"]]
           , literals2 = mkPrologClause [PrologLiteral False "pred" ["fact"]]
           , addText = Nothing
+          , showSolution = False
           }
 
 
@@ -190,6 +206,7 @@ data PickConfig = PickConfig {
      , amountOfOptions :: Int
      , pickCnf :: Bool
      , extraText :: Maybe String
+     , printSolution :: Bool
      }
      deriving (Typeable, Generic)
 
@@ -199,6 +216,7 @@ dPickConf = PickConfig
     , amountOfOptions = 3
     , pickCnf = False
     , extraText = Nothing
+    , printSolution = False
     }
 
 
@@ -208,6 +226,7 @@ data FillConfig = FillConfig {
     , percentageOfGaps :: Int
     , percentTrueEntries :: Maybe (Int,Int)
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
@@ -217,6 +236,7 @@ dFillConf = FillConfig
     , percentageOfGaps = 40
     , percentTrueEntries = Just (30,70)
     , extraText = Nothing
+    , printSolution = False
     }
 
 
@@ -225,6 +245,7 @@ data MinMaxConfig = MinMaxConfig {
       cnfConf :: CnfConfig
     , percentTrueEntries :: Maybe (Int,Int)
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
@@ -233,6 +254,7 @@ dMinMaxConf = MinMaxConfig
     { cnfConf = dCnfConf
     , percentTrueEntries = Just (50,70)
     , extraText = Nothing
+    , printSolution = False
     }
 
 
@@ -241,6 +263,7 @@ data DecideConfig = DecideConfig {
       cnfConf :: CnfConfig
     , percentageOfChanged :: Int
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
@@ -249,20 +272,23 @@ dDecideConf = DecideConfig
     { cnfConf = dCnfConf
     , percentageOfChanged = 40
     , extraText = Nothing
+    , printSolution = False
     }
 
 
 
 data StepConfig = StepConfig {
       baseConf :: BaseConfig
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
 dStepConf :: StepConfig
 dStepConf = StepConfig
     { baseConf = dBaseConf
     , extraText = Nothing
+    , printSolution = False
     }
 
 
@@ -272,6 +298,7 @@ data PrologConfig = PrologConfig {
     , maxClauseLength :: Int
     , usedPredicates :: [PrologLiteral]
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
@@ -281,13 +308,15 @@ dPrologConf = PrologConfig
     , maxClauseLength = 3
     , usedPredicates = [PrologLiteral True "f" ["a"], PrologLiteral True "f" ["b"], PrologLiteral True "g" ["a"]]
     , extraText = Nothing
+    , printSolution = False
     }
 
 
 data ResolutionConfig = ResolutionConfig {
       baseConf :: BaseConfig
     , minSteps :: Int
     , extraText :: Maybe String
+    , printSolution :: Bool
     }
     deriving (Typeable, Generic)
 
@@ -296,4 +325,5 @@ dResConf = ResolutionConfig
     { baseConf = dBaseConf
     , minSteps = 2
     , extraText = Nothing
+    , printSolution = False
     }

src/Formula/Parsing.hs

@@ -298,8 +298,9 @@ instance Parse PickInst where
         tokenSymbol ","
         index <- lexeme $ many1 digit
         text <- optionMaybe $ lexeme bonusText
+        printSol <- lexeme $ many1 digit
         char ')'
-        pure $ PickInst cs (read index) text
+        pure $ PickInst cs (read index) text ((read printSol :: Int) /= 0)
           where
             bonusText = between start (char '}') $ many1 $ satisfy ( /= '}')
             start = do

src/Formula/Resolution.hs

@@ -5,18 +5,21 @@ module Formula.Resolution
        , resolvable
        , resolvableWith
        , applySteps
+       , computeResSteps
+       , showResSteps
        ) where
 
 
 import qualified Data.Set as Set
 import qualified SAT.MiniSat as Sat
 
 import Data.Set (empty,Set)
-import Data.Maybe (isJust)
+import Data.Maybe (isJust, fromJust)
 import Test.QuickCheck (Gen,choose,elements,shuffle)
 
-import Formula.Types
+import Formula.Types hiding (Dnf(..), Con(..))
 import Formula.Util
+import Data.List (nub, find, elemIndex)
 
 
 
@@ -142,3 +145,52 @@ setElements :: Set a -> Gen a
 setElements set
     | null set = error "setElements used with empty set."
     | otherwise = (`Set.elemAt` set) `fmap` choose (0, Set.size set - 1)
+
+----------------------------------------------------------------------------------------------------------
+
+initResolution :: [Clause] -> [([Clause], Clause)]
+initResolution = foldr (\ x -> (:) ([], x)) []
+
+resolutions :: [([Clause], Clause)] -> [([Clause], Clause)]
+resolutions [] = []
+resolutions xss@((cs, r):xs) = nub $ (cs,r) : [ ([x,y], fromJust res) | x <- allClauses, l <- Set.toList (literalSet x), y <- allClauses, let res = resolve x y l, isJust res]  ++ resolutions xs
+  where allClauses = map snd xss
+
+solution' :: [([Clause], Clause)] -> [([Clause], Clause)]
+solution' xs = if any (\(_, Clause x) -> null x) xs then xs else solution' (resolutions xs)
+
+reconstructSolution :: Clause -> [([Clause], Clause)] -> [([Clause], Clause)]
+reconstructSolution c xs = if isJust rOrigin then [ fromJust rOrigin ] else reconstructSolution (head (fst (fromJust r))) xs ++ reconstructSolution (last (fst (fromJust r))) xs  ++ [(fst (fromJust r) ,c)]
+  where rOrigin = find (\(ps,x) -> x == c && null ps) xs
+        r = find (\(ps,x) -> x == c && not (null ps)) xs
+
+applyNum :: [Clause] -> [([Clause], Clause)] -> [([Clause], Clause, Int)]
+applyNum _ [] = []
+applyNum origs xs = map (\(ys, c) -> (ys, c, fromJust (elemIndex c correctedOrigs) +1)) old ++ zipWith (curry (\((ys, c),i) -> (ys, c,i))) new [length origs + 1..]
+  where
+    old = filter (\(ps, _) -> null ps) xs
+    new = filter (\(ps, _) -> not (null ps)) xs
+    correctedOrigs = Set.toList $ clauseSet $ mkCnf origs
+
+convertSteps :: [([Clause], Clause, Int)] -> [ResStep]
+convertSteps [] = []
+convertSteps xs = map mapFn new
+  where new = filter (\(a,_,_) -> not (null a)) xs
+        mapFn (ys,c,i) = let (_,_,l) = fromJust (find (\(_,b,_) -> b == head ys) xs)
+                             (_,_,r) = fromJust (find (\(_,b,_) -> b == last ys) xs)
+                          in Res (Right l, Right r, (c, Just i))
+
+pretty' :: ResStep -> Bool -> String
+pretty' (Res (a,b,(c,d))) isLast = "(" ++ showEither a ++ ", " ++ showEither b ++ ", " ++ show c ++ showNum ++ ")"
+  where showEither (Left x) = show x
+        showEither (Right y) = show y
+        showNum = if isJust d && not isLast then " = " ++ show (fromJust d) else ""
+
+showResSteps :: [ResStep] -> [String]
+showResSteps [] = []
+showResSteps [x] = [pretty' x True]
+showResSteps (x:xs) = pretty' x False : showResSteps xs
+
+computeResSteps :: [Clause] -> [ResStep]
+computeResSteps clauses = convertSteps (applyNum clauses (reconstructSolution (Clause empty) (solution' (initResolution clauses))))
+

src/Formula/Types.hs

@@ -43,9 +43,9 @@ import GHC.Generics
 import Test.QuickCheck
 import Numeric.SpecFunctions as Math (choose)
 
-newtype ResStep = Res {trip :: (Either Clause Int, Either Clause Int, (Clause, Maybe Int))}
+newtype ResStep = Res {trip :: (Either Clause Int, Either Clause Int, (Clause, Maybe Int))} deriving Show
 
-newtype TruthValue = TruthValue {truth :: Bool} deriving (Typeable, Generic)
+newtype TruthValue = TruthValue {truth :: Bool} deriving (Show, Typeable, Generic)
 
 
 

src/LogicTasks/Helpers.hs

@@ -55,6 +55,12 @@ example correct s = indent $ do
 reject :: OutputMonad m => State (Map Language String) () -> LangM m
 reject  = refuse . indent . translate
 
+applyForAll :: OutputMonad m => [a] -> (a -> LangM m) -> LangM m
+applyForAll [] _ = pure ()
+applyForAll (x:xs) m = do
+  m x
+  applyForAll xs m
+  pure ()
 
 
 clauseKey :: OutputMonad m => LangM m

src/LogicTasks/Semantics/Decide.hs

@@ -22,6 +22,8 @@ import Formula.Util (isEmptyCnf, hasEmptyClause)
 import Formula.Table (flipAt, readEntries)
 import Formula.Types (atomics, availableLetter, genCnf, getTable, literals)
 import Util (checkCnfConf, isOutside, preventWithHint, remove)
+import LogicTasks.Helpers (example)
+import Control.Monad (when)
 
 
 
@@ -33,7 +35,7 @@ genDecideInst DecideConfig{cnfConf = CnfConfig {baseConf = BaseConfig{..}, ..},
       tableLen = length $ readEntries $ getTable cnf
       mistakeCount = max (tableLen * percentageOfChanged `div` 100) 1
     mistakes <- remove (tableLen - mistakeCount) [1..tableLen]
-    pure $ DecideInst cnf mistakes extraText
+    pure $ DecideInst cnf mistakes extraText printSolution
   where
     getCnf = genCnf (minClauseAmount, maxClauseAmount) (minClauseLength, maxClauseLength) usedLiterals
 
@@ -148,9 +150,14 @@ completeGrade DecideInst{..} sol = do
       german "Lösung ist korrekt?"
       english "Solution is correct?"
     )
-    (translate $ do
-      german $ "Die Lösung beinhaltet " ++ display ++ " Fehler."
-      english $ "Your solution contains " ++ display ++ " mistakes."
+    (do
+      translate $ do
+        german $ "Die Lösung beinhaltet " ++ display ++ " Fehler."
+        english $ "Your solution contains " ++ display ++ " mistakes."
+      when showSolution $ example (show changed) $ do
+        english "One possible solutions for this task is:"
+        german "Eine mögliche Lösung für die Aufgabe ist:"
+      pure ()
     )
   where
     nubSol = nub sol