| Age | Commit message (Collapse) | Author |
|---|
|
Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.
|
|
This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
|
|
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 work towards a configurable approach to theory combination.
Setting the master equality engine in QuantifiersEngine mimics setting EqualityEngine in Theory.
|
|
This was an option that rejected instantiations that are true according to the current
model's equality engine.
This option was never helpful and will be burdensome to maintain with new updates
to equality engine infrastructure.
|
|
|
|
robust (#4034)
Fixes #4002 (that benchmark is now unknown).
The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.
The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.
A block of code changed indentation in this PR, which was updated to the new standards.
|
|
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* Make QEffort an enum.
* Format
* Minor
* Fix
|
|
* Initial draft of splitting quant util.
* Minor
* Document recursive term builder.
* Rename file, minor.
* Clang format
|
|
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
|
|
document (#1290)
* Move, document, and rename enumerative instantiation.
* Clang format.
|
|
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
|
|
Commit 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 introduced a memory leak
where d_quant_attr was not deleted when the QuantifiersEngine was
destroyed. This commit fixes the issue by turning d_quant_attr into an
std::unique_ptr.
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|
|
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
|
|
* 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.
|
|
|
|
|
|
master equality engine during term indexing, fixes bug 801.
|
