Age | Commit message (Collapse) | Author |
|
|
|
|
|
Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.
|
|
|
|
Now prints each tag in a separate line.
|
|
|
|
|
|
|
|
|
|
This is another step towards addressing #1304 and #1344. This pull request:
- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback
This lays the basis for more general linearizations.
|
|
|
|
|
|
This commit fixes two issues with reset-assertions:
- pending pops were not done in SmtEngine, resulting in the following
assertion failure:
d_userLevels.size() == 0 && d_userContext->getLevel() == 1
- all definitions were erased on reset-assertion in an SMT2 file,
leading to errors about undefined types
|
|
|
|
|
|
My last commit for the Valgrind instrumentation contained a typo that
made the nightlies fail. This commit fixes the issue.
|
|
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
|
|
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
|
|
|
|
|
|
This
makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.
Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default
Allows cbqiNestedQE to be used in the BV logic.
Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
lambdas (#1403)
This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.
The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
|
|
|
|
|
|
* minor
Using string previously computed
* adding option
* starting module for simplifying grammars
* more
* more
* fix
* fix
* fix
* fix
* fix
* removing unused command
* removing unused command
* removing unnecessary quantifier engine
* adding lambda support
* transient
* reverting changes
* starting normalization of integers
* removing unnecessary objects
* using for_each
* rebuilding given datatypes
* recrating types as given
* bug fixing
* minor
* reverting space changes
* addressing review
* addressing review
|
|
* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
|
|
|
|
|
|
* Higher-order instantiation.
* Add missing files.
* Document inst match generators, make collectHoVarApplyTerms iterative.
* More documentation.
* More documentation.
* More documentation.
* More documentation
* Refactoring, documentation.
* More documentation.
* Fix comment, reference issue.
* More documentation. Fix ho trigger for the changes from master.
* Minor
* More documentation.
* More documentation.
* More
* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.
* More
* Minor improvements to comments.
* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.
* Improve documentation for ho_trigger.
* Update ho trigger to not access now private member of TermDb.
* Address comments.
* Address
* Clang format
|
|
* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043.
* Fixing a missed assertion. Fixing a few compiler warnings.
* Switching back to an enum from an enum class.
|
|
* Documenting single invocation partiion.
* More
* More encapsulation.
* More, documentation complete.
* Split to own file.
* Format
* Fully encapsulate.
* Format
* Improvements to doc.
* Format
* Address
* Format
* Missed comment
* Newline
* Address
* Format
|
|
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
|
|
* Add arithmetic monomial sum utility.
* Clang format
* Fix
* Address review.
* Fix missed comment.
* Format
* Fix
|
|
(#1374)
|
|
* Initial infrastructure for sygus printing.
* Minor
* Minor improvements
* Format
* Minor
* Empty constructor printer.
* Format
* Minor
* Format
* Address.
|
|
|
|
and 1362931. (#1373)
|
|
|