Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Formula type refactoring #251

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Formula type refactoring #251

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
896ae32
rename Literal constructors
nimec01 Jan 31, 2025
e57f1cd
change type of + turn some 'literal' to 'atomic'
nimec01 Jan 31, 2025
af0c5a3
fix accidental replacement
nimec01 Jan 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions src/Config.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ data PickInst = PickInst {

dPickInst :: PickInst
dPickInst = PickInst
{ formulas = [InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']], InstCnf $ mkCnf [mkClause [Not 'A', Literal 'B']]]
{ formulas = [InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']], InstCnf $ mkCnf [mkClause [Neg 'A', Pos 'B']]]
, correct = 1
, showSolution = False
, addText = Nothing
Expand All @@ -89,7 +89,7 @@ data MaxInst = MaxInst {

dMaxInst :: MaxInst
dMaxInst = MaxInst
{ cnf = mkCnf [mkClause [Literal 'A', Not 'B']]
{ cnf = mkCnf [mkClause [Pos 'A', Neg 'B']]
, showSolution = False
, addText = Nothing
, unicodeAllowed = False
Expand All @@ -108,7 +108,7 @@ data MinInst = MinInst {

dMinInst :: MinInst
dMinInst = MinInst
{ dnf = mkDnf [mkCon [Literal 'A', Not 'B']]
{ dnf = mkDnf [mkCon [Pos 'A', Neg 'B']]
, showSolution = False
, addText = Nothing
, unicodeAllowed = False
Expand All @@ -127,7 +127,7 @@ data FillInst = FillInst {

dFillInst :: FillInst
dFillInst = FillInst
{ formula = InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']]
{ formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
, missing = [1,4]
, missingValues = [True, True]
, showSolution = False
Expand All @@ -146,7 +146,7 @@ data DecideInst = DecideInst {

dDecideInst :: DecideInst
dDecideInst = DecideInst
{ formula = InstCnf $ mkCnf [mkClause [Literal 'A', Not 'B']]
{ formula = InstCnf $ mkCnf [mkClause [Pos 'A', Neg 'B']]
, changed = [1,4]
, showSolution = False
, addText = Nothing
Expand All @@ -167,9 +167,9 @@ data StepInst = StepInst {

dStepInst :: StepInst
dStepInst = StepInst
{ clause1 = mkClause [Not 'A', Not 'C', Literal 'B']
, clause2 = mkClause [Literal 'A', Not 'C']
, solution = (Literal 'A', mkClause [Not 'C', Literal 'B'])
{ clause1 = mkClause [Neg 'A', Neg 'C', Pos 'B']
, clause2 = mkClause [Pos 'A', Neg 'C']
, solution = (Pos 'A', mkClause [Neg 'C', Pos 'B'])
, usesSetNotation = False
, showSolution = False
, addText = Nothing
Expand All @@ -191,13 +191,13 @@ data ResolutionInst = ResolutionInst {

dResInst :: ResolutionInst
dResInst = let
nAnCpB = mkClause [Not 'A', Not 'C', Literal 'B']
pAnC = mkClause [Literal 'A', Not 'C']
pC = mkClause [Literal 'C']
nB = mkClause [Not 'B']
pA = mkClause [Literal 'A']
nC = mkClause [Not 'C']
nCpB = mkClause [Not 'C', Literal 'B']
nAnCpB = mkClause [Neg 'A', Neg 'C', Pos 'B']
pAnC = mkClause [Pos 'A', Neg 'C']
pC = mkClause [Pos 'C']
nB = mkClause [Neg 'B']
pA = mkClause [Pos 'A']
nC = mkClause [Neg 'C']
nCpB = mkClause [Neg 'C', Pos 'B']
in ResolutionInst
{ clauses =
[ nAnCpB
Expand Down
31 changes: 16 additions & 15 deletions src/Formula/Parsing.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,8 @@ module Formula.Parsing (
import Config
import Formula.Util
import ParsingHelpers (caseInsensitive, lexeme, tokenSymbol)
import Formula.Types
import Formula.Types hiding (Literal(..))
import qualified Formula.Types as Lit (Literal(..))

import Control.Monad (void)
import Data.Map (fromList)
Expand Down Expand Up @@ -174,8 +175,8 @@ instance Parse TruthValue where



instance Parse Literal
instance FromGrammar Literal where
instance Parse Lit.Literal
instance FromGrammar Lit.Literal where
topLevelSpec = LevelSpec
{ allowOr = False
, allowAnd = False
Expand All @@ -188,8 +189,8 @@ instance FromGrammar Literal where
, nextLevelSpec = Nothing
}

fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Literal x
fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Not x
fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (OfAtom (Atom x)))))) = Just $ Lit.Pos x
fromGrammar (WithPrecedence (NoArrows (NoOrs (NoAnds (NegAtom (Atom x)))))) = Just $ Lit.Neg x
fromGrammar _ = Nothing

clauseSetParser :: Parser Clause
Expand Down Expand Up @@ -222,9 +223,9 @@ instance FromGrammar Clause where
fromGrammar (WithPrecedence TopLevelBackImpl) = Nothing
fromGrammar (WithPrecedence (NoArrows f)) = mkClause <$> foldlOrs phi (Just []) f
where
phi :: Maybe [Literal] -> Ands -> Maybe [Literal]
phi xs (NoAnds (OfAtom (Atom x))) = (Literal x :) <$> xs
phi xs (NoAnds ((NegAtom (Atom x)))) = (Not x :) <$> xs
phi :: Maybe [Lit.Literal] -> Ands -> Maybe [Lit.Literal]
phi xs (NoAnds (OfAtom (Atom x))) = (Lit.Pos x :) <$> xs
phi xs (NoAnds ((NegAtom (Atom x)))) = (Lit.Neg x :) <$> xs
phi _ (NoAnds (Neg{})) = Nothing
phi _ (NoAnds (OfNested{})) = Nothing
phi _ Ands{} = Nothing
Expand All @@ -247,9 +248,9 @@ instance FromGrammar Con where
fromGrammar OfNoFixity{} = Nothing
fromGrammar (WithPrecedence (NoArrows (OfAnds f))) = mkCon <$> foldlAnds phi (Just []) f
where
phi :: Maybe [Literal] -> Neg -> Maybe [Literal]
phi xs (OfAtom (Atom x)) = (Literal x :) <$> xs
phi xs (NegAtom (Atom x)) = (Not x :) <$> xs
phi :: Maybe [Lit.Literal] -> Neg -> Maybe [Lit.Literal]
phi xs (OfAtom (Atom x)) = (Lit.Pos x :) <$> xs
phi xs (NegAtom (Atom x)) = (Lit.Neg x :) <$> xs
phi _ Neg{} = Nothing
phi _ OfNested{} = Nothing
fromGrammar _ = Nothing
Expand All @@ -269,8 +270,8 @@ instance FromGrammar Cnf where
go (WithPrecedence TopLevelBackImpl) = Nothing
phi :: Maybe [Clause] -> Neg -> Maybe [Clause]
phi xs (OfNested (Nested f)) = (:) <$> fromGrammar f <*> xs
phi xs (OfAtom (Atom x)) = (mkClause [Literal x] :) <$> xs
phi xs (NegAtom (Atom x)) = (mkClause [Not x] :) <$> xs
phi xs (OfAtom (Atom x)) = (mkClause [Lit.Pos x] :) <$> xs
phi xs (NegAtom (Atom x)) = (mkClause [Lit.Neg x] :) <$> xs
phi _ Neg{} = Nothing

instance Parse Dnf
Expand All @@ -285,8 +286,8 @@ instance FromGrammar Dnf where
where
phi :: Maybe [Con] -> Ands -> Maybe [Con]
phi xs (NoAnds (OfNested (Nested x))) = (:) <$> fromGrammar x <*> xs
phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Literal x] :) <$> xs
phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Not x] :) <$> xs
phi xs (NoAnds (OfAtom (Atom x))) = (mkCon [Lit.Pos x] :) <$> xs
phi xs (NoAnds (NegAtom (Atom x))) = (mkCon [Lit.Neg x] :) <$> xs
phi _ (NoAnds Neg{}) = Nothing
phi _ (Ands{}) = Nothing

Expand Down
4 changes: 2 additions & 2 deletions src/Formula/Printing.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ instance Pretty ResStep where


instance Pretty Literal where
pretty (Literal x) = char x
pretty (Not x) = myText ['¬', x]
pretty (Pos x) = char x
pretty (Neg x) = myText ['¬', x]



Expand Down
12 changes: 6 additions & 6 deletions src/Formula/Resolution.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ resolvableWith c1 c2
| length possible == 1 = Just (head possible)
| otherwise = Nothing
where
lits = atomics c1
lits = map Pos $ atomics c1 -- TODO: Should `literals` be used here?
possible = filter (isJust . resolve c1 c2) lits


Expand Down Expand Up @@ -100,8 +100,8 @@ genRes (minLen,maxLen) steps lits = do
then do
chosenChar <- elements xs
let
pos = Set.singleton $ Literal chosenChar
neg = Set.singleton $ Not chosenChar
pos = Set.singleton $ Pos chosenChar
neg = Set.singleton $ Neg chosenChar
startSet = Set.fromList [pos,neg]
buildClauses xs (startSet,[Res (Left (toClause pos),Left (toClause neg), (toClause empty,Nothing))]) 0
else do
Expand All @@ -111,7 +111,7 @@ genRes (minLen,maxLen) steps lits = do
chosenClause <- setElements (if Set.null underMin then underMax else underMin)
let
chooseableLits = filter (\lit ->
Literal lit `Set.notMember` chosenClause && Not lit `Set.notMember` chosenClause) xs
Pos lit `Set.notMember` chosenClause && Neg lit `Set.notMember` chosenClause) xs
if null chooseableLits
then buildClauses xs (ys,rs) (runs+1)
else do
Expand All @@ -124,10 +124,10 @@ genRes (minLen,maxLen) steps lits = do
else choose (1,2)
chosenChar <- elements chooseableLits
if choice == 1
then checkValidAndInsert (Literal chosenChar) chosenClause rs clauseSize 0
then checkValidAndInsert (Pos chosenChar) chosenClause rs clauseSize 0
else do
firstAmount <- choose (1, clauseSize-1)
chosenSign <- elements [Literal chosenChar, Not chosenChar]
chosenSign <- elements [Pos chosenChar, Neg chosenChar]
checkValidAndInsert chosenSign chosenClause rs firstAmount firstAmount
where
checkValidAndInsert :: Literal -> Set Literal -> [ResStep] -> Int -> Int -> Gen (Set (Set Literal),[ResStep])
Expand Down
11 changes: 6 additions & 5 deletions src/Formula/Table.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
module Formula.Table
(
readEntries
, readLiterals
, readAtomics
, flipAt
, gapsAt
) where
Expand All @@ -20,13 +20,14 @@ import qualified Data.Set as Set (fromList)
readEntries :: Table -> [Maybe Bool]
readEntries = getEntries

readLiterals :: Table -> Set Literal
readLiterals = Set.fromList . getLiterals
-- Used in Autotool
readAtomics :: Table -> Set Char
readAtomics = Set.fromList . getAtomics



gapsAt :: Table -> [Int] -> Table
gapsAt table gaps = Table (getLiterals table) newEntries
gapsAt table gaps = Table (getAtomics table) newEntries
where
entries = getEntries table
newEntries = [ if x+1 `elem` gaps then Nothing else entries !! x
Expand All @@ -38,7 +39,7 @@ gapsAt table gaps = Table (getLiterals table) newEntries


flipAt :: Table -> [Int] -> Table
flipAt table indices = Table (getLiterals table) newEntries
flipAt table indices = Table (getAtomics table) newEntries
where
entries = getEntries table
newEntries = [ let value = entries !! x in
Expand Down
Loading
Loading