Skip to content

Instantly share code, notes, and snippets.

@tamarinvs19

tamarinvs19/Task2Tests.hs

Last active April 11, 2021 06:46
Show Gist options
  • Save tamarinvs19/bc8f489e593fac2ce38f613a06f6734d to your computer and use it in GitHub Desktop.
Save tamarinvs19/bc8f489e593fac2ce38f613a06f6734d to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. tamarinvs19 renamed this gist Apr 6, 2021. 1 changed file with 0 additions and 0 deletions.
    0 hs → Task2Tests.hs
    View file
    File renamed without changes.
  2. tamarinvs19 created this gist Apr 6, 2021.
    97 changes: 97 additions & 0 deletions hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,97 @@
    equivCNF :: CNF -> CNF -> Bool
    equivCNF cnf1 cnf2 = equiv (toPropFormula cnf1) (toPropFormula cnf2)

    -- Тесты промежуточных функций CNF
    testAccessoryFunctions :: Spec
    testAccessoryFunctions = describe "testing accessory functions:" $ do
    it "test toPropLit Pos" $
    (toPropLit (Atom "p")) == (Just $ Pos "p")
    it "test toPropLit Neg" $
    (toPropLit (Not $ Atom "p")) == (Just $ Neg "p")
    it "test toPropLit error And" $
    (toPropLit [pf| p /\ ~q |]) == Nothing
    it "test toPropLit error Or" $
    (toPropLit [pf| p \/ q |]) == Nothing

    it "test PropLitToPropFormula Pos" $
    (propLitToPropFormula $ Pos "a") == Atom "a"
    it "testPropLitToPropFormula Neg" $
    (propLitToPropFormula $ Neg "a") == (Not $ Atom "a")

    it "test ClauseToPropFormula empty" $
    (clauseToPropFormula $ Set.empty) == FTrue
    it "test ClauseToPropFormula size = 1" $
    (clauseToPropFormula $ Set.fromList [Pos "a"]) == Atom "a"
    it "test ClauseToPropFormula size = 5" $
    equiv (clauseToPropFormula $ Set.fromList [Pos "a", Neg "b", Pos "c", Pos "d", Neg "e"]) [pf| a \/ ~b \/ c \/ d \/ ~e |] `shouldBe` True

    it "test toPropFormula empty" $
    (toPropFormula $ (CNF Set.empty)) == FTrue
    it "test toPropFormula size = 1x2" $
    equiv (toPropFormula $ (CNF $ Set.fromList [Set.fromList [Pos "a", Neg "b"] ])) [pf| a \/ ~b |] `shouldBe` True
    it "test toPropFormula size = 3x3" $
    equiv (toPropFormula $ (CNF $ Set.fromList [
    Set.fromList [Pos "a", Neg "b", Pos "c"],
    Set.fromList [Neg "a", Neg "b", Neg "c"],
    Set.fromList [Pos "a", Neg "b", Pos "d"]
    ])) [pf| (a \/ ~b \/ c) /\ (~a \/ ~b \/ ~c) /\ (a \/ ~b \/ d) |] `shouldBe` True

    it "test isTrivial: trivial And" $
    isTrivial [pf| p /\ q |] `shouldBe` True
    it "test isTrivial: trivial Or" $
    isTrivial [pf| p \/ q |] `shouldBe` True
    it "test isTrivial: non trivial" $
    isTrivial [pf| p \/ q \/ r |] `shouldBe` False
    it "test isTrivial: non trivial 2" $
    isTrivial [pf| (p \/ q \/ r) /\ p \/ q |] `shouldBe` False

    it "test trivialCNF: trivial Or" $
    equiv (toPropFormula $ trivialCNF ("p_100", [pf| p \/ q |])) [pf| p_100 <-> p \/ q |] `shouldBe` True
    it "test trivialCNF: trivial And" $
    equiv (toPropFormula $ trivialCNF ("p_100", [pf| p /\ q |])) [pf| p_100 <-> p /\ q |] `shouldBe` True

    it "test maxVarIndex: without name_N" $
    maxVarIndex "p" [pf| p \/ q \/ r /\ (p /\ q) |] == 0
    it "test maxVarIndex: name_1" $
    maxVarIndex "p" [pf| p_1 \/ q \/ r /\ (p /\ q) |] == 1
    it "test maxVarIndex: name_1 inner" $
    maxVarIndex "p" [pf| p \/ q \/ r /\ (p_1 /\ q) |] == 1
    it "test maxVarIndex: name_4" $
    maxVarIndex "p" [pf| p_1 \/ q \/ r /\ (p_4 /\ q \/ (p_3 \/ p_2)) |] == 4

    it "test mainCNF 1" $
    mainCNF ([pf| p /\ (p \/ q) |], M.empty, 1) == ([pf| p /\ p_1 |], M.fromList [("p_1", [pf| p \/ q |])], 2)
    it "test mainCNF 2" $
    mainCNF ([pf| p /\ q |], M.empty, 1) == ([pf| p_1 |], M.fromList [("p_1", [pf| p /\ q |])], 2)
    it "test mainCNF 3" $
    mainCNF ([pf| p_100 /\ q |], M.empty, 101) == ([pf| p_101 |], M.fromList [("p_101", [pf| p_100 /\ q |])], 102)

    it "test unsat mainCNF" $
    mainCNF ([pf| p /\ ~p |], M.empty, 1) `shouldBe` ([pf| p_1 |], M.fromList [("p_1", [pf| p /\ ~p |])], 2)
    it "test unsat eqsatCNF" $
    eqsatCNF [pf| p /\ ~p |] `equivCNF` CNF (Set.fromList ([Set.fromList [Pos "p_1"]] ++ (Set.toList $ clauses $ trivialCNF ("p_1", [pf| p /\ ~p |]))))


    -- Тесты для преобразований DP и DPLL
    instance Eq CNF where
    (CNF a) == (CNF b) = a == b

    testRulesDP :: Spec
    testRulesDP = describe "testing DP rules:" $ do
    it "test unitFoldingRule: no singeElement" $
    unitFoldingRule (CNF $ Set.fromList [ Set.fromList [Pos "p", Pos "q"], Set.fromList [Neg "p", Pos "r"]]) `shouldBe` Nothing
    it "test unitFoldingRule" $
    unitFoldingRule (CNF $ Set.fromList [ Set.fromList [Pos "r", Pos "q"], Set.fromList [Pos "p"], Set.fromList [Pos "p", Pos "q"], Set.fromList [Neg "p", Pos "r"]]) `shouldBe` Just (CNF $ Set.fromList [ Set.fromList [Pos "r", Pos "q"], Set.fromList [Pos "r"]])

    it "test pureLiteralRule: no pureLit" $
    pureLiteralRule (CNF $ Set.fromList [ Set.fromList [Pos "p", Pos "q"], Set.fromList [Neg "p", Neg "q"]]) `shouldBe` Nothing
    it "test pureLiteralRule" $
    pureLiteralRule (CNF $ Set.fromList [ Set.fromList [Pos "r", Neg "q", Neg "t"], Set.fromList [Pos "p", Pos "t"], Set.fromList [Pos "p", Neg "q"], Set.fromList [Neg "p", Pos "r"]]) `shouldBe` Just (CNF $ Set.fromList [ Set.fromList [Pos "p", Pos "t"] ])

    it "test resolutionRule 1" $
    resolutionRule (CNF $ Set.fromList [ Set.fromList [Pos "p", Pos "q"], Set.fromList [Neg "p", Neg "q"]]) `shouldBe` (CNF $ Set.fromList [Set.fromList [Pos "q", Neg "q"]])
    it "test pureLiteralRule 2" $
    resolutionRule (CNF $ Set.fromList [ Set.fromList [Neg "r", Pos "q", Neg "t"], Set.fromList [Pos "p", Pos "t"], Set.fromList [Pos "p", Neg "q"], Set.fromList [Neg "p", Pos "r"]]) `shouldBe` (CNF $ Set.fromList [ Set.fromList [Neg "q", Pos "r"], Set.fromList [Pos "t", Pos "r"], Set.fromList [Neg "r", Pos "q", Neg "t"] ])
    it "test resolutionRule 3" $
    resolutionRule (CNF $ Set.fromList [ Set.fromList [Pos "p", Neg "p"] ]) `shouldBe` (CNF $ Set.empty)