Last active
April 11, 2021 06:46
-
-
Save tamarinvs19/bc8f489e593fac2ce38f613a06f6734d to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Строка 22:
(clauseToPropFormula $ Set.empty) == FTrue-- должно бытьFFalse(пустую клаузу невозможно удовлетворить)Тест в 89 строке, кажется, некорректный. Должно получиться
CNF $ Set.fromList [ Set.fromList [Pos "p", Pos "t"], Set.fromList [Pos "p", Neg "q"] ].Правило резолюции должно включать отбрасывание тавтологий, поэтому тест в строке 92 некорректный, должно получиться пустое множество.