////////////////////////////////////////////////////////////
//
// CNFProp (for Global n-compact Validation)
//
// Imports
import CNF from '../validation/conjunctive-normal-form.js'
import { LogicConcept } from '../logic-concept.js'
import { Environment } from '../environment.js'
import Utilities from './utils.js'
const { tab, indent, subscript, profile } = Utilities
/**
* Represents the Propositional Form of any LC and the utilities to convert that
* to cnf form required by satSolve. It is needed because the PropositionalForm
* class does not support LCs, only sequents.
*/
export class CNFProp {
/**
* Create a new CNFProp object.
*
* @param {'and'|'or'} op - The operator of the CNFProp. Either 'and' or 'or'.
* @param {...(CNFProp|integer)} kids - The children of the CNFProp that the operator applies to. An array of CNFProps or integers.
* @returns {CNFProp} - The newly created CNFProp object.
*/
constructor ( op, ...kids ) {
this.op = op || 'and' // 'and' or 'or'
this.kids = kids || [ ] // Array of CNFProps or integers
this.negated = false // negated or not
}
/**
* 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.
*
* @param {LogicConcept} L
* @param {string[]} catalog
* @param {LogicConcept} target
* @param {boolean} checkPreemies
* @param {LogicConcept[]} [ignores] - internal use only
* @param {string} [sig] - internal use only
* @returns {CNFProp}
*/
static fromLC ( L , catalog = L.cat, target = L , checkPreemies = false ,
ignores , sig ) {
catalog = catalog || L.catalog()
// check if it should be negated
// propositions accessible to the target (nonreflexive) are treated as
// given when the target is present.
const negated = (L.isA('given') || L.isAccessibleTo(target))
const sign = negated ? -1 : 1
// Propositions have atomic prop form. ForSome declarations have an atomic
// propositional form with constants renamed by the body. A copy of the
// body is added afterwards, and treated like any other LC in the
// document. Note that .isAProposition ignores anything that is marked
// .ignore or in the supplied array 'ignores'.
if (ignores === undefined) {
ignores = (checkPreemies) ? target.letAncestors() : []
sig = CNFProp.signature(ignores)
}
if ( L.isAProposition( ignores ) ) {
let ans
// if its index is cached, use that
if (!L.propIndex) L.propIndex = new Map()
const lookup = L.propIndex.get(sig) ||
profile( () => L.lookup( catalog , ignores ) , 'catalog lookup' )
L.propIndex.set(sig,lookup)
ans = sign*lookup
return ans
// if it's an environment process the relevant children, skipping over
// anything irrelevant to the target and Declare's which have no prop form.
} else if (L instanceof Environment) {
// if it's a cached environment, return it
if (L.CNFProp && L.CNFProp.has(sig)) {
return L.CNFProp.get(sig)
}
// make the environment's CNFProp
let env = new CNFProp()
profile( () => {
let kids = L.children()
// remove trailing givens and anything irrelevantTo the target
while ( kids.length>0 &&
( kids.last().isA('given') ||
kids.last().irrelevantTo( target )
)
)
kids.pop()
// givens and claims accessible to the target other than itself, should be
// negated. Thus we don't pass the second argument to isAccessibleTo to
// say it should be reflexive.
env.negated = negated
while ( kids.length > 0 ) {
let A = kids.pop()
// skip it if it's a Declare, or an unnecessary declaration (the
// leading Let of a Rule or Theorem), which validation ignores as if
// it were deleted
if (A.isA('Declare') || A.isA('unnecessary')) continue
// skip it if it's a Comment or anything with .ignore. This eliminates
// entire subenvironments and everything inside them because of this
// recursion is top-down.
if (A.ignore) continue
// if doing a preemie check, ignore the let ancestors of the target
if (checkPreemies && ignores.includes(A)) continue
// otherwise get it's prop form
let Aprop = CNFProp.fromLC(A,catalog,target,checkPreemies,ignores,sig)
if ( Aprop === null ) continue
// check if it's given or accessible to the target
const isNegated = A.isA('given') || A.isAccessibleTo(target)
// check if we have to change the op based on this latest child
let newop = isNegated ? 'or' : 'and'
// if we do, and there's more than one kid, wrap the kids w/ previous
// op
if ( newop!==env.op && env.kids.length>1 ) {
env.kids = [ new CNFProp( env.op , ...env.kids ) ]
}
env.op = newop
// if the new guy has the same op and is not negated, unshift its
// children, otherwise just unshift the whole thing
if ( Aprop.op===env.op && !isNegated ) {
env.kids.unshift(...Aprop.kids)
} else {
env.kids.unshift(Aprop)
}
}
} , 'env to CNFProp' )
// compare what's cached to the new one
// if (L.CNFProp && L.isA('given') && L.parent()===L.root() && L.CNFProp!==env) {
// console.log(`These don't match: ${L.address()}`)
// console.log(L.root().cat)
// console.log(L.CNFProp)
// console.log(`and:`)
// console.log(env)
// console.log(`---------------------`)
// }
// given environments that are children of the root are typically instantiations,
// so we cache their CFProp because it is only a function of the ignore signature.
if (L.isA('given') && L.parent()===L.root()) {
if (!L.CNFProp) L.CNFProp = new Map()
L.CNFProp.set(sig,env)
}
return env
}
}
/**
* 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.
*
* @param {Array} A - The array of LCs
*/
static signature = A => {
return JSON.stringify(A.map( x => x.address()))
}
/**
* Converts an integer $x$ to a variable. If the optional argument $n$ is present,
* return a switch variable if $n<\left|x\right|$.
*
* @param {number} x The integer to be converted.
* @param {number} [n] An optional argument that indicates the value after
* which a switch variables should be returned.
* @returns {string} The variable name corresponding to the integer $x$.
*/
static toVar ( x , n = Infinity ) {
const A = 'A'.charCodeAt(0)
let prefix = (x<0) ? ':' : ''
x = Math.abs(x)
let name = (n<x) ? `𝒵${subscript(x-n)}` :
(x<27) ? String.fromCharCode(x+A-1) :
(x<53) ? String.fromCharCode(x+A+5) : `𝒳${subscript(x)}`
return prefix+name
}
/**
* Convert a CNFProp to algebraic form. The optional argument `n` tells it the
* lower bound for switch variables. See the [Propositional Form tutorial]{@tutorial
* Propositional Form} for details.
*/
toAlgebraic ( n = Infinity ) {
const A = 'A'.charCodeAt(0)
let ans = this.kids.map( x => {
// convert nonzero integers to variables
if ( Number.isInteger(x) ) { return CNFProp.toVar(x,n)
// x must be a CNFProp
} else { return x.toAlgebraic(n) }
} )
let joint = (this.op === 'and') ? '+' : ''
ans = ans.join(joint)
return (this.negated) ? `:(${ans})` :
(this.op==='and') ? `(${ans})` : ans
}
/**
* Convert this CNFProp to human readable form using the supplied catalog.
* See the [Propositional Form tutorial]{@tutorial Propositional Form} for details.
*/
toEnglish (catalog) {
let ans = this.kids.map( x => {
// lookup nonzero integers in the catalog
if ( Number.isInteger(x) ) { return ((x<0)?'¬':'')+catalog[Math.abs(x)-1]
// x must be a CNFProp
} else { return x.toEnglish(catalog) }
} )
let joint = (this.op === 'and') ? ' and ' : ' or '
ans = ans.join(joint)
return (this.negated) ? `¬(${ans})` :
(this.op==='and') ? `(${ans})` : ans
}
// convert this CNFProp to a legible human readable form using the supplied catalog
toNice (catalog, level = 0) {
// get the array of nice kids, indented by level+1
let ans = this.kids.map( x => {
// lookup nonzero integers in the catalog
if ( Number.isInteger(x) ) { // +`${Math.abs(x)}`
return indent(((x<0)?':':'')+catalog[Math.abs(x)-1],(level+1)*2)
// x must be a CNFProp
} else { return x.toNice(catalog, level+1) }
} )
// join them with newlines
ans = ans.join('\n')
// wrap the whole thing appropriately
// say(`This is negated? ${this.negated}`)
return (this.negated) ? tab(level*2)+`:{\n${ans}}` :
(this.op==='and') ? tab(level*2)+`{\n${ans}}` : tab(level*2)+`{\n${ans}}`
}
/**
* 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}.
*/
static get switchVarSymbol () { return '𝒵'}
/**
* Check if the logical expression is in Conjunctive Normal Form (CNF).
*
* @returns {boolean} True if the expression is in CNF, false otherwise.
*/
hasCNFform() {
// Check if the expression is not negated, has 'and' operator,
// and all subexpressions are instances of CNFProp
// with 'or' operator and contain only integer values.
return !this.negated &&
this.op === 'and' &&
this.kids.every(x => {
return (x instanceof this.constructor) &&
x.kids.every(Number.isInteger) &&
(x.op === 'or')
})
}
/**
* Distribute all negatives by DeMorgan's law, and cancel double negatives
* that result on this CNFProp. See the
* [Propositional Form tutorial]{@tutorial Propositional Form} for details.
*/
simplify ( toggle ) {
let ans = new CNFProp()
// distribute the nots
if ( (this.negated && !toggle) || (!this.negated && toggle) ) {
ans.op = (this.op==='and') ? 'or' : 'and'
ans.kids = this.kids.map( x => {
return ( Number.isInteger(x) ) ? -x : x.simplify(true)
} )
} else {
ans.op = this.op
ans.kids = this.kids.map( x => {
return ( Number.isInteger(x) ) ? x : x.simplify( )
} )
}
return ans
}
/**
* 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})`
*
* @param {CNFProp} Lprop - Simplified CNFProp
* @param {number} switchvar - Object with key `num` whose values if the value
* to use for the next switchvar
* @returns {CNFProp} - CNF form of this CNFProp
*/
static toCNF ( Lprop , switchvar ) {
if (Number.isInteger(Lprop)) { return [[Lprop]] }
if (Lprop.kids.length===0) { return (Lprop.op==='and') ? [] : [[]] }
if (Lprop.kids.length===1) { return CNFProp.toCNF(Lprop.kids[0]) }
// it's compound
if (Lprop.op==='and') {
return CNF.and(...Lprop.kids.map(x=>CNFProp.toCNF(x,switchvar)))
}
// the only remaining case is Lprop === 'or'
let kids = [...Lprop.kids]
let ans = CNFProp.toCNF(kids.pop(),switchvar)
while (kids.length>0) {
let P=CNFProp.toCNF(kids.pop(),switchvar)
ans = CNF.or( P, ans, () => {
++switchvar.num
return switchvar.num
} )
}
return ans
}
/**
* Convert this CNFProp to an array of integers.
*/
toArray () {
let unsigned = this.kids.map( x => ( Number.isInteger(x) ) ? x : x.toArray() )
return (this.negated) ? ['-',unsigned] : unsigned
}
// Convert a numerical CNF to an algebraic form with switch vars after n
// Don't really need this, but is good for debugging
static cnf2Algebraic ( C , n ) {
let ans = C.map( x => x.map( y => CNFProp.toVar(y,n)).join('') )
return ans.join('+')
}
// end CNFProp class
}source