| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
* Make QEffort an enum.
* Format
* Minor
* Fix
|
|
* Split explain utility, invariance tests.
* Split extended rewriter.
* Remove unused function.
* Minor
* Move generic term utilities to term_util.
* Documentation, minor.
* Make arguments private in eval invariance.
* Document
* More documentation.
* Clang format.
* Fix, improve.
* Format
* Address review.
* Address missed comment.
* Add line breaks
* Format
|
|
* Initial setup for preprocessing counterexample lemmas.
* Improve documentation.
* Improving documentation, infrastructure.
* Extraction -> concatentation as a preprocess step.
* Clang format
* Minor
* Make option, refactor effort levels.
* Format
* Clean
* Format
* Rename
* Format
* More
* Format
* Splitting changes.
* Format
* Revert option.
* Minor
* Format
|
|
1172284. (#1362)
|
|
* Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891.
* Initializing to false explicitly.
|
|
|
|
* Initializes TriggerInfo::polarity. Resolves CID 1172054.
* Initializing to false explicitly.
|
|
|
|
* Refactoring rep set iterator, does not modify rep set externally.
* Decouple quantifiers engine and rep set iterator.
* Documentation
* Clang format
* Minor
* Minor
* More
* Format
* Address review.
* Format
* Minor
|
|
|
|
* Disable qe preprocessing for sygus by default, add option.
* Fix bug
* Unnest one
* Format
|
|
* Implement enumerator for functions.
* Address review.
* Minor
* Format
* Improve comment.
* Format
|
|
* Initial work on conjecture-specific symmetry breaking.
* More infrastructure, working on process term.
* Flattening.
* Process defs
* More setup
* Fixes.
* Sketching
* Generalize to inference of argument definitions.
* More, separate conjunct processing per synth function.
* Single occurrence variables.
* Assign relevance.
* Document, connecting.
* Connecting to grammar construction.
* Enabled, add regressions.
* Fix regressions.
* Clang format.
* Add regress1, minor.
* Fix
* Two passes.
* Fix
* Note
* Improve check match, make single var occurrence more conservative.
* Add regression.
* Clang format
* Minor comments
* Update regression to new option.
* Undo grammar cons changes.
* Enable irrelevant args.
* Improvements.
* Format
* Minor
|
|
|
|
|
|
* Clean and document datatype.h.
* More, make TODOs.
* More documentation
* More
* Reference issue.
* Format
* Fixes and improvements.
* Minor
* Minor
* Minor
* Fix
* Minor
* Format
|
|
|
|
* Minor preparation for final higher-order merge.
* Format
|
|
* Decouple sygus term database and term database.
* Clang format
* Fix include
|
|
This adds functions on Integers to compute modular addition, multiplication and inverse.
This is required for the Gaussian Elimination preprocessing pass for BV.
|
|
|
|
|
|
|
|
* Initialize TimerStat::d_start.
* 0 initializing d_data.
|
