Age | Commit message (Collapse) | Author |
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
|
|
driver except in interactive mode.
|
|
success, nonzero error
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
|
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(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.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
|
|
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)
* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).
* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
consistency, error-reporting, and documentation.
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
|