| Age | Commit message (Collapse) | Author |
|---|
|
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.
It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
|
|
|
|
`TheoryProofEngine` now uses the `expectedType` optional argument.
* When printing terms, it sets this for theories that it dispatches too
* It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
* It is mindful of `expectedType` when using the let map.
I also moved to hpp function implementations into the cpp.
|
|
* expectedType in proof-printing code
To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.
This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.
Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.
* TypeNode, Don't mix default args & virtual
* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
be dynamically overriden during a dynamic dispatch.
* Since we don't want them to be overidable anyway, we use two
functions: one that is non-virtual and has a default, the other that
is virtual but has no default. The former just calls the latter.
* clang-format after signature changes
|
|
* Bugfix: convert ifte arms to formulas for printing
We have two kinds of ITEs in our LFSC proofs:
* ite: for sort-typed expressions
* ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.
Fixed now.
* Test the lifting of ITEs from arithmetic.
This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.
It used to fail, but now passes.
* clang-format
* Typos.
* Add test to CMake
* Set --check-proofs in test
* Address Yoni
* Expand printsAsBool documentation
* Assert ITE typing soundness
* Assert a subtype relation for ITEs, not equality
* Update src/proof/arith_proof.h
Thanks Yoni!
Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
|
|
Adds missing override keywords.
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
|
|
new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
|
|
|
|
|
|
Fix warning due to `ProofLetCount` being defined as `struct` in
`proof_utils.h` and `class` in `proof.h`. Fix warnings due to different
number of arguments of `printConstantDisequalityProof()` and
`printTheoryLemmaProof()` in subclasses.
|
|
|
|
the global let map before the aliasing part)
|
|
flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
|
|
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
|
|
Added support for the BV case
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
|
|
|
|
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
|
|
|
|
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
