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> nexts = Sets.newSet(); for(Map 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 instantiatedDeletions = action.instantiateDeletions(binding);