Merge pull request #16 from Azumabashi/feat/export-generateAtomicProp…

…WithGivenId

export `generateAtomicPropWithGivenId`

src/propositionalLogic.nim

@@ -28,7 +28,7 @@ import
 # List of types/procs/iterators to be exported
 export
   TruthValue, TOP, BOTTOM, `==`, `and`, `or`, `not`,
-  PropLogicFormula, generateAtomicProp, `&`, `|`, `=>`, `!`, `$`, recByStructure,
+  PropLogicFormula, generateAtomicProp, generateAtomicPropWithGivenId, `&`, `|`, `=>`, `!`, `$`, recByStructure,
   isSat, getModels, isTautology, isContradiction,
   Interpretation, interpretations, getModels,
   simplification

src/propositionalLogic/formulae.nim

@@ -34,6 +34,21 @@ proc generateAtomicProp*(): PropLogicFormula =
   existingAtomicProps += 1
 
 proc generateAtomicPropWithGivenId*(id: int): PropLogicFormula = 
+  ## Returns atomic propositions with given id.
+  ## If the atomic propositions which id is given `id` does not exist, this proc raises `AssertionDefect`.
+  ## 
+  ## This procedure is defined to generate new `PropLogicFormula` objects correspond to an existing atomic proposition.
+  ## **Use proc `generateAtomicProp` to generate new atomic propositions**.
+  runnableExamples:
+    import propositionalLogic
+
+    let
+      P = generateAtomicProp()
+      Q = generateAtomicPropWithGivenId(P.id)
+    echo P == Q
+    ## Output:
+    ##   true
+  doAssert 0 <= id and id < existingAtomicProps
   result = PropLogicFormula(
     formulaType: PropFormulaType.atomicProp,
     id: id

tests/testEquivalance.nim

@@ -24,4 +24,8 @@ suite "check formula equivalance":
     check (P => Q) == (P => Q)
 
   test "logical equivalence but different formula":
-    check not ((P => Q) == ((!P) | Q))
+    check not ((P => Q) == ((!P) | Q))
+
+  test "an atomic propositions generated by generateAtomicProp and generateAtomicPropWithGivenId is considered as same":
+    let R = generateAtomicPropWithGivenId(P.id)
+    check P == R