Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
also have SMT solvers alternate fact filter
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
use the right filter in each slice
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned slices
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
store fact filter along with ATP slice
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
simplified SMT solver code in Sledgehammer
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
changeset |
files
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
changeset |
files
|