From 1476d80eab1c12f478ed5a9c257d25ba94669722 Mon Sep 17 00:00:00 2001
From: Naveen Sundar Govindarajulu <naveensundarg@gmail.com>
Date: Thu, 19 Jan 2017 15:12:10 -0500
Subject: [PATCH] Option to keep empty bindings. Default: keep.

---
 snark-20120808r02/snark-interface.lisp     | 2 +-
 src/main/java/edu/rpi/rair/Operations.java | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp
index d505964..e987a27 100644
--- a/snark-20120808r02/snark-interface.lisp
+++ b/snark-20120808r02/snark-interface.lisp
@@ -41,7 +41,7 @@
   (snark:use-hyperresolution t)
   (snark:use-paramodulation t)
 
-  (snark:allow-skolem-symbols-in-answers nil))
+  (snark:allow-skolem-symbols-in-answers t))
 
 (defun row-formula (name))
 
diff --git a/src/main/java/edu/rpi/rair/Operations.java b/src/main/java/edu/rpi/rair/Operations.java
index 81575cf..c1a1bdf 100644
--- a/src/main/java/edu/rpi/rair/Operations.java
+++ b/src/main/java/edu/rpi/rair/Operations.java
@@ -27,8 +27,10 @@ import static edu.rpi.rair.State.FALSE;
 public class Operations {
 
     private static boolean DEEP_EQUIVALENCE = false;
+    private static boolean THROW_AWAY_EMPTY_BINDINGS = false;
     private static Prover prover;
 
+
     static{
         prover = new SnarkWrapper();
     }
@@ -93,9 +95,9 @@ public class Operations {
         Set<Pair<State,Action>> nexts = Sets.newSet();
         for(Map<Variable, Value> binding: bindingsOpt.get()){
 
-            if(binding.values().stream().anyMatch(x-> x instanceof Variable)){
+            if(THROW_AWAY_EMPTY_BINDINGS && binding.values().stream().anyMatch(x-> x instanceof Variable)){
 
-                continue;
+               continue;
             }
 
         Set<Formula> instantiatedDeletions =  action.instantiateDeletions(binding);