| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This is so that we can use CI in master for proofs.
|
|
|
|
Fixes #6142.
|
|
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
Cryptominisat supports writing statistics to a sqlite3 database, and automatically enabled it when it can find sqlite bindings.
This disables sqlite3, as we don't need it anyway.
Fixes #6131.
|
|
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
|
|
|
|
This fixes a subtle bug with how quantifier bodies are letified.
It makes our letification more conservative so that let symbols are never pushed inside quantifier bodies, instead quantifier bodies are letified independently of the context.
|
|
This is in preparation for moving several utilities into the quantifiers inference manager.
This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine.
|
|
|
|
(#6141)
|
|
Adds a dot printer for proof nodes. Also adds an option to choose the proof format (as a mode).
Signed-off-by: Diego Della Rocca de Camargos <diegodellarocc@gmail.com>
|
|
|
|
|
|
Commit d47a8708171f1cf488fe9ce05f56f2566db53093 refactored the interface of
prop engine. In doing so, it changed the order in which preregistration lemmas
were asserted. Before the commit, they were asserted after all the user
assertions. After the commit, they were asserted after each user assertion that
generated them. This, however, seems to have a negative performance impact,
especially for string benchmarks because the justification heuristic tries to
justify the assertions in the order in which they appear. Intuitively, it makes
sense to first try to satisfy the user assertions before trying to satisfy the
preregistration lemmas.
Signed-off-by: Andres Noetzli <noetzli@amazon.com>
|
|
|
|
Towards having proofs working on master.
|
|
Broken in dc679ed.
|
|
|
|
|
|
|
|
This will help reduce the CI times and ccache sizes.
|
|
This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
|
|
Preparation for making ARITH_SCALE_SUM_UB a macro.
Adds a proof rule for summing upper bounds: ARITH_SUM_UB.
Moves ARITH_MULT_* rules from the non-linear extension to the main
arithmetic checker, since they will be needed for all of arith now.
Aligns the ARITH_SCALE_SUM_UB documentation with its checker.
|
|
This makes quantifiers use standard inference ids.
This eliminates the need to track ad-hoc statistics, per instantiation type.
This makes minor modifications to a few interfaces in quantifiers to enable this.
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
Refactoring out the code from `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.
Signed-off-by: mikolas <mikolas.janota@gmail.com>
|
|
This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.
It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
|
|
This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.
|
|
Fixes -Wshadow and -Wsuggest-override wranings.
|
|
This test shouldn't be an API test and is not portable to the new API
right now statistics are not retrievable via the API. When we add
methods for retrieving statistics to the new API, we'll need thorough
unit tests this, which makes this test obsolete.
|
|
This is in preparation for deleting the Expr layer.
This further fixes incorrect handling of ownership for the datatypes
owned by the NodeManager.
|
|
|
|
Ensures that all checks are performed in production builds with enabled assertions.
|
|
|
|
This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
|
|
This adds missing checks to guard that Term and Sort arguments are
associated with the solver object that is called.
|
|
This class contains all globally available utilities for internal code.
|
|
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
|
|
This also renames metakind::getLowerBoundForKind and
metakind::getUpperBoundForKind for consistency.
Note that the NodeManager class needs to be reordered to comply to our
style guidelines. This PR does not reorder but introduces a public block
at the top (where the rest of the public interface of the class should
go eventually).
|
|
The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.
|
|
Further cleans up some unused variables and moves the configuration of
best to configure.sh.
|
|
This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.
As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:
(P (witness ((x T)) (A x)))
now we return:
(P k), with skolem lemma ( (A k), k )
Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.
|
|
Fixes #6075.
|
|
This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.
To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.
These two fixes are required to fix #6071.
Note: we should performance test this on SMT-LIB.
|
|
Fixes #5658.
This was fixed by recent refactoring to quantifier elimination, adding the regression to close the issue.
|
