added unit propagation for formula simplification

Author: Alexander Steen

js/inputoutput.js

@@ -244,18 +244,36 @@ iol = new function() { const lib = this;
     return result
   }
 
-  /* TODO: unit propagation etc. for simplication */
+  /* tries to reduce the complexity of the set of formulas, by:
+     - applying intra-formula simplification
+     - unit propagation
+     - subsumption 
+  */
   const semanticalInterreduce = function(A) {
+    /* simplification: */
     const Asimp = pltk.simpset(A)
     const Asimpcnf = pltk.conjs(pltk.cnfsimp(pltk.cnf(pltk.mkConjs(Asimp)))) 
+    /* do unit propagation */
+    let units = _.filter(Asimpcnf, pltk.isUnitFormula)
+    let nonUnits = _.without(Asimpcnf, ...units)
+    let newUnits = units
+    while (!_.isEmpty(newUnits)) {
+      let replacements = _.map(units, u => [pltk.getUnitFormulaBody(u), pltk.getUnitFormulaPolarity(u)])
+      let rewrittenNonUnits = _.map(nonUnits, f => pltk.simp(pltk.deepReplaceBys1(f, replacements)))
+      newUnits = _.filter(rewrittenNonUnits, pltk.isUnitFormula)
+      units = units.concat(newUnits)
+      nonUnits = _.without(rewrittenNonUnits, ...newUnits)
+    }
+    const formulas = units.concat(nonUnits)
+    /* do subsumption*/
     let result = []
-    _.forEach(Asimpcnf, function(a) {
-      if (!pltk.consequence(result,a)) {
-        result = _.reject(result, r => pltk.consequence([a],r))
+    _.forEach(formulas, function(a) {
+      if (!pltk.consequence(result,a)) { /* <- forward subsumption */
+        result = _.reject(result, r => pltk.consequence([a],r)) /* backward subsumption */
         result.push(a)
       }
     })
-    //console.log("Result: ", pltk.plprintset(result))
+    /* done */
     return result
   }
 

js/pltk.js

@@ -346,6 +346,26 @@ pltk = new function() { const lib = this;
     } else return it
   }
 
+  lib.deepReplaceBy = function(it, what, by) {
+    if (_.isEqual(it, what)) {
+      return by
+    } else {
+      if (lib.isAtom(it)) {
+        return it
+      } else return { op: it.op, args: _.map(it.args, arg => lib.deepReplaceBy(arg, what, by)) }
+    }
+  }
+  
+  /* deep replacement successively (it's NOT simultaneously)*/
+  lib.deepReplaceBys = function(it, whats, bys) {
+    const replacements = _.zip(whats, bys)
+    return _.reduce(replacements, function (acc, replacement) { return lib.deepReplaceBy(acc, replacement[0], replacement[1]) }, it)
+  }
+  
+  /* deep replacement successively (it's NOT simultaneously)*/
+  lib.deepReplaceBys1 = function(it, replacements) {
+    return _.reduce(replacements, function (acc, replacement) { return lib.deepReplaceBy(acc, replacement[0], replacement[1]) }, it)
+  }
 
   /* true if a subsumes b */
   lib.disjClauseSubsumes = function(a,b) {
@@ -365,6 +385,24 @@ pltk = new function() { const lib = this;
     } 
     return lib.isVariable(f)
   }
+  
+  /* pre: isUnitFormula */
+  lib.getUnitFormulaPolarity = function(f) {    
+    if (lib.isNeg(f)) {
+      return { op: 'LF', args: []}
+    } else {
+      return { op: 'LF', args: []}
+    }
+  }
+  
+  /* pre: isUnitFormula */
+  lib.getUnitFormulaBody = function(f) {    
+    if (lib.isNeg(f)) {
+      return f.args[0]
+    } else {
+      return f
+    }
+  }
 
   lib.isVariable = function(f) {
     return _.get(f, 'op', '') == 'Var'
@@ -397,6 +435,10 @@ pltk = new function() { const lib = this;
     return _.has(f,'op') && f.op == 'LF'
   }
 
+  lib.isAtom = function(f) {
+    return lib.isVariable(f) || lib.isT(f) || lib.isF(f)
+  }
+  
   // ###############################
   /* Export to dimacs */
   // ###############################