Age | Commit message (Collapse) | Author |
|
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
|
|
allows linearization of div,mod,/ by a constant.
|
|
unknown key.
|
|
This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion. That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope. This is strange, and would likely lead to problems, so it's now
disabled.
Thanks to David Cok for inquiring about this.
|
|
|
|
|
|
|
|
* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression
|
|
|
|
* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|