| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The following items will be added / adressed in subsequent PRs:
* migrate statistics tracking for variables and bound variables
* migrate adding of listeners when variables and bound variables
are created
* consistent and clean NodeManagerScope handling
(out of scope for this PR)
* clean up all interfaces to use const references when possible
|
|
Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.
|
|
This PR ensures that several optimizations are not performed in the reference implementation of skolem sharing (d_useOpts=false). This is to ensure that the many of the rules in the strings proof checker do not depend on the rewriter.
These errors were caught by the LFSC proof checker.
|
|
Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms.
Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms.
This PR changes arithmetic in preparation for this change.
Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94.
Note that the indentation of code in operator_elim.cpp changed.
|
|
Theory preprocessing now theory-preprocesses lemmas until fixed point. This eliminates the old code for rewriting them only, which is no longer necessary as theory-preprocessing subsumes rewriting.
|
|
This PR replaces all TNode types in datatypes by Node within justification heuristic.
Fixes #6073.
Unfortunately, the example from #6073 times out now, thus there is no new regression.
|
|
This changes things so we process inferences with AND conclusions as lemmas always.
This fixes #6056, that benchmark times out.
|
|
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
|
|
As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this.
Fixes #5034.
|
|
This disables the temporarily available internals of datatype classes.
|
|
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
|
|
This disables the temporarily available internals of Term.
Note: getExpr() is still available and will be disabled when the API is
fully converted to Nodes.
|
|
When adding libpoly, we forgot to add a proper define to cvc4autoconfig and included real_algebraic_number.h everywhere to get this define. This PR introduces the CVC4_POLY_IMP define and removes all obsolete includes to real_algebraic_number.h.
|
|
Right now, the inference manager infrastructure drops conflicts (and literal propagations) if the solver already is in a conflict.
This PR removes this behavior. The current setup in linear arithmetic requires adding conflicts, even when already in conflict, and experiments showed a small but beneficial effect of this change.
|
|
This disables the temporarily available internals of Sort.
|
|
This disables the temporarily available internals of Result.
It further changes the interface for getUnknownExplanation, which now
returns an enum value instead of a string.
|
|
This disables the temporarily available internals of Op.
|
|
preprocessing (#6040)
Due to refactoring in theory preprocessor, which does fixed point preprocessing on created lemmas, several things can be simplified in arithmetic operator elimination.
This is required for further simplification to witness forms in the internal proof calculus.
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
|
|
This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
|
|
Make collect_tags.py more robust for non-ASCII characters.
|
|
This PR fixes an issue where utf8 encoded inputs are incorrectly parsed into CVC4::String. We now use std::mbtowc to first turn the char sequence from the std::string input into a std::wstring and then process this std::wstring one charactor (wchar_t) at a time.
Fixes #5673
|
|
This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.
Fixes #1479 #5769.
|
|
Fixes warnings with CVC4_FALLTHROUGH and -Werror for debug/production with gcc/clang. Clang detects that a CVC4_FALLTHROUGH after an Assert(false); is unreachable and issues a warning, while gcc issues a warning about an implicit fall-through if CVC4_FALLTHROUGH is not present.
|
|
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.
|
|
This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.
|
|
Miscellaneous changes from proof-new.
|
|
This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
|
|
This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
|
|
The justification heuristic stores a "copy" of assertions as TNode. As witnessed by #5938, these TNodes may invalid.
This PR changes this to store Nodes instead.
Fixes #5938.
|
|
This case was previously unhandled and exercised by a recently added regression.
|
|
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
|
|
Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
|
|
|
|
The static-learning preprocessing sometimes added non-rewritten assertions, despite being used in a part of the preprocessor that assumes all assertions to be rewritten. This may then break other passes further down, in the case of #5729 the non-clausal simplification which explicitly asserts that assertions are rewritten. This PR rewrites the respective assertion properly in the static-learning pass.
Fixes #5729.
|
|
This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
|
|
In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
|
|
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
|
|
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
|
|
When a clause is being explained, the negation of each of its literals, other than the one it propagates, needs to be explained. This process may lead to the creation of new clauses in the SAT solver (because if a literal being explained was propagated and an explanation was not yet given, it will then be computed and added). This may lead to changes in the memory where clauses are, which may break the reference to the original clause being explained. To avoid this issue we store the literals in the reason before we start explaining their negations. We then iterate over them rather than over the clause, as before.
|
|
This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.
|
|
This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
|
|
Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.
|
