| Age | Commit message (Collapse) | Author |
|---|
|
This PR does another round of refactoring of the resource manager and related code.
- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager
Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.
|
|
|
|
|
|
|
|
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
|
|
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.
This is in preparation for the new unsat cores based on proofs.
|
|
|
|
|
|
This PR introduces the header file for a more modular bv-to-int module, that will be called from the preprocessing pass bv-to-int, and possibly from the bit-vector solver after preprocessing.
The header file is basically a copy of the bv_to_int.h header file from preprocessing, with some adjustments to increase modularity.
In addition to the header file we also introduce an empty unit test that #includes the header, in order to identify compilation errors. The unit test will be populated in subsequent PRs, that will also include implementations.
|
|
Creating BitVectors (and deleting them) is in general expensive because
of the underlying multi-precision Integer. If possible, unnecessary
constructions and desctructions of BitVectors should be avoided.
The most common use case for `setBit` is that for an existing BitVector,
a given bit should be set to a certain value. Not doing this in place
generates unnecessary constructions and destructions of BitVectors.
|
|
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.
|
|
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.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
|
|
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
|
|
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.
|
|
Make collect_tags.py more robust for non-ASCII characters.
|
|
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.
|
|
This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic.
|
|
This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
|
|
This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.
|
|
Theory BV now sets up the default equality engine for BV solvers that do not use their own equality engine like e.g. the BV bitblast solver. This commit also adds the missing equality engine pieces to the BV bitblast solver (getEqualityStatus, explain).
|
|
This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.
|
|
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
|
|
The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.
This merges the helper class TheoryRegistrar into TheoryProxy.
|
|
This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).
This will be required for SAT relevancy.
No behavior changes in this PR.
|
|
This is required to avoid failures in the planned refactoring of check-models.
This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.
It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.
FYI @barrettcw
|
|
|
|
|
|
This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.
This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.
This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.
The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).
|
|
|
|
Mostly in cardinality extension, which was cleaned in the previous PR.
|
|
The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.
This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.
This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
|
|
This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.
|
|
Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.
|
|
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
|
|
This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
|
|
For some reason, our ABC build was including cnf_stream.h in an
extern "C" block instead of outside of it, which made the build fail
because the header indirectly includes cdqueue.h, which uses
templates. This change is older
(e9bfbb2)
but only started causing problems with our nightly builds recently.
|
|
This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.
This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.
This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).
|
|
This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.
|
|
Motivated by #4936, this PR adds a new BV rewrite rule:
(bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false)
Fixes #4936.
|
|
This makes it so that ExtTheory uses a generic callback instead of relying on Theory.
The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.
It also refactors the use of ExtTheory in strings and arithmetic.
|
|
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).
|
|
This is a followup to #4945 which simplifies the contract for computeRelevantTerms.
|
|
Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.
This includes:
A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).
Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.
FYI @barrettcw
Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.
|
|
This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.
FYI @aniemetz @mpreiner
|
