Constructor
new CNFProp(op, …kids) → {CNFProp}
Create a new CNFProp object.
Parameters
-
op
'and'|'or'The operator of the CNFProp. Either 'and' or 'or'.
-
kids
CNFProp|integer<repeatable>
The children of the CNFProp that the operator applies to. An array of CNFProps or integers.
Returns
-
CNFProp- The newly created CNFProp object.
Source
Classes
Members
signature
Compute Address Signature
When we have an array of LC's in a document it is convenient to have a signature for that array obtained by concatenating the addresses of all of the LCs. This routine computes that signature. This is useful for the 'ignore' arrays of let-scopes when checking preemies.
Source
switchVarSymbol
Represents the symbol used for displaying switch variables in Algebraic form. The switch variable symbol is currently '𝒵', which is represented by the unicode \u{1D4B5}.
Source
Methods
hasCNFform() → {boolean}
Check if the logical expression is in Conjunctive Normal Form (CNF).
Returns
-
booleanTrue if the expression is in CNF, false otherwise.
Source
simplify()
Distribute all negatives by DeMorgan's law, and cancel double negatives that result on this CNFProp. See the Propositional Form tutorial for details.
Source
toAlgebraic()
Convert a CNFProp to algebraic form. The optional argument n tells it the
lower bound for switch variables. See the Propositional Form tutorial for details.
Source
toArray()
Convert this CNFProp to an array of integers.
Source
toEnglish()
Convert this CNFProp to human readable form using the supplied catalog. See the Propositional Form tutorial for details.
Source
fromLC(L, catalog, target, checkPreemies, ignoresopt, sigopt) → {CNFProp}
Make a CNFProp from an LC - this is the main purpose of this class.
The last two arguments are only passed internally by the recursion: the array of Lets to ignore and its address signature are constant for the entire conversion (they depend only on the target and checkPreemies), so they are computed once at the top-level call and passed down rather than being recomputed at every node.
Parameters
-
L
LogicConcept -
catalog
Array.<string> -
target
LogicConcept -
checkPreemies
booleanfalse -
ignores
Array.<LogicConcept><optional>
internal use only
-
sig
string<optional>
internal use only
Returns
-
CNFProp
Source
toCNF(Lprop, switchvar) → {CNFProp}
Convert this CNFProp to CNF form. Lprop should be a simplified CNFProp.
switchvar is an object containing the value to use for the next switch
var with key num, e.g. a typical use might be
CNFProp.toCNF(CNFProp.fromLC(L),{num:L.catalog().length})
Parameters
-
Lprop
CNFPropSimplified CNFProp
-
switchvar
numberObject with key
numwhose values if the value to use for the next switchvar
Returns
-
CNFProp- CNF form of this CNFProp
Source
toVar(x, nopt) → {string}
Converts an integer $x$ to a variable. If the optional argument $n$ is present, return a switch variable if $n<\left|x\right|$.
Parameters
-
x
numberThe integer to be converted.
-
n
number<optional>
An optional argument that indicates the value after which a switch variables should be returned.
Returns
-
stringThe variable name corresponding to the integer $x$.