mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-11-09 11:10:34 -05:00
Option to keep empty bindings. Default: keep.
This commit is contained in:
parent
14e418b37a
commit
1476d80eab
2 changed files with 5 additions and 3 deletions
|
@ -41,7 +41,7 @@
|
||||||
(snark:use-hyperresolution t)
|
(snark:use-hyperresolution t)
|
||||||
(snark:use-paramodulation t)
|
(snark:use-paramodulation t)
|
||||||
|
|
||||||
(snark:allow-skolem-symbols-in-answers nil))
|
(snark:allow-skolem-symbols-in-answers t))
|
||||||
|
|
||||||
(defun row-formula (name))
|
(defun row-formula (name))
|
||||||
|
|
||||||
|
|
|
@ -27,8 +27,10 @@ import static edu.rpi.rair.State.FALSE;
|
||||||
public class Operations {
|
public class Operations {
|
||||||
|
|
||||||
private static boolean DEEP_EQUIVALENCE = false;
|
private static boolean DEEP_EQUIVALENCE = false;
|
||||||
|
private static boolean THROW_AWAY_EMPTY_BINDINGS = false;
|
||||||
private static Prover prover;
|
private static Prover prover;
|
||||||
|
|
||||||
|
|
||||||
static{
|
static{
|
||||||
prover = new SnarkWrapper();
|
prover = new SnarkWrapper();
|
||||||
}
|
}
|
||||||
|
@ -93,9 +95,9 @@ public class Operations {
|
||||||
Set<Pair<State,Action>> nexts = Sets.newSet();
|
Set<Pair<State,Action>> nexts = Sets.newSet();
|
||||||
for(Map<Variable, Value> binding: bindingsOpt.get()){
|
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);
|
Set<Formula> instantiatedDeletions = action.instantiateDeletions(binding);
|
||||||
|
|
Loading…
Reference in a new issue