| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
|
|
|
|
Does not support InstMatch interfaces anymore, which are spurious.
|
|
This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
|
|
Towards eliminating dependence on QuantifierEngine from inst_match_trie.
|
|
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.
|
|
(#5477)
This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.
The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.
Fixes #5365, fixes #5279, fixes #4849, fixes #4433.
This PR also required fixes related to how quantifier elimination is computed.
|
|
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 adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).
It also simplifies and improves printing of Instantiation Tries.
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
