| Age | Commit message (Collapse) | Author |
|---|
|
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
|
|
This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
(#6240)
This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned.
Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.
|
|
Towards having complete stats on inference ids for each lemma, fact, and conflict.
|
|
This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
|
|
engine (#6198)
Towards breaking dependencies on quantifers engine.
|
|
Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
|
|
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.
|
|
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 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 makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
|
|
Does not support InstMatch interfaces anymore, which are spurious.
|
|
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
|
|
This PR collects the InferenceId in the InferenceManagerBuffered class.
|
|
Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
|
|
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
|
|
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
|
|
In preparation for splitting trigger.h/cpp into multiple files.
This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.
|
|
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.
|
|
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
