| Age | Commit message (Collapse) | Author |
|---|
|
* 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.
|
|
Logic enum with an UNSET value. (#1329)
|
|
|
|
* Removing an unused member from Tptp. Initializing members of Tptp.
* Removing delcaration for myPopCharStream.
|
|
enum. Always initializing VarInfo::d_type. (#1333)
|
|
* Allow FORALL passed as an argument to get-qe.
* Document
* Format
* Minor
|
|
|
|
|
|
|
|
* Updates to interface for grammar construction.
* Minor
* Format
|
|
* Unrecursify rewrite assertion for cbqi bv.
* Format
|
|
Returns a copy of d_value to enable public access of GMP and CLN data.
|
|
* Generalize component contains, some infrastructure.
* Length entailment, substr for component contains, int.to.str for constant can contain concat.
* Disable rewrite.
* Fix, reenable length entailment for contains.
* Clang format, minor.
* Comment
* Minor fixes and improvements for comments.
* Improvements
* Clang format
* Fixes
* Clang format
* Fix, improve.
* Format
* Fix assertion
|
|
* Make higher-order a flag in logic info.
* Format
* Minor
* Format
|
|
* Support SAT logic.
* Add lustre example.
* Add to smt1 as well.
* Fix.
* Fix.
* Fix for new option.
|
|
|
