|
22 | 22 | import java.util.Comparator; |
23 | 23 | import java.util.Deque; |
24 | 24 | import java.util.HashMap; |
25 | | -import java.util.Iterator; |
26 | 25 | import java.util.LinkedHashSet; |
27 | 26 | import java.util.List; |
28 | 27 | import java.util.Map; |
29 | | -import java.util.Map.Entry; |
30 | | -import java.util.Optional; |
31 | 28 | import java.util.Set; |
32 | 29 | import org.sosy_lab.java_smt.api.ArrayFormula; |
33 | 30 | import org.sosy_lab.java_smt.api.BitvectorFormula; |
@@ -580,26 +577,10 @@ public BooleanFormula encapsulateBoolean(Term pTerm) { |
580 | 577 | return new BitwuzlaBooleanFormula(pTerm); |
581 | 578 | } |
582 | 579 |
|
583 | | - protected Table<String, Sort, Term> getCache() { |
| 580 | + Table<String, Sort, Term> getCache() { |
584 | 581 | return formulaCache; |
585 | 582 | } |
586 | 583 |
|
587 | | - // True if the entered String has an existing variable in the cache. |
588 | | - protected boolean formulaCacheContains(String variable) { |
589 | | - // There is always only 1 type permitted per variable |
590 | | - return formulaCache.containsRow(variable); |
591 | | - } |
592 | | - |
593 | | - // Optional that contains the variable to the entered String if there is one. |
594 | | - protected Optional<Term> getFormulaFromCache(String variable) { |
595 | | - Iterator<Entry<Sort, Term>> entrySetIter = formulaCache.row(variable).entrySet().iterator(); |
596 | | - if (entrySetIter.hasNext()) { |
597 | | - // If there is a non-empty row for an entry, there is only one entry |
598 | | - return Optional.of(entrySetIter.next().getValue()); |
599 | | - } |
600 | | - return Optional.empty(); |
601 | | - } |
602 | | - |
603 | 584 | @Override |
604 | 585 | public Object convertValue(Term term) { |
605 | 586 | Preconditions.checkArgument(term.is_value(), "Term \"%s\" is not a value.", term); |
|
0 commit comments