| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
* 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
|
|
* Disable qe preprocessing for sygus by default, add option.
* Fix bug
* Unnest one
* 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
|
|
* Support SAT logic.
* Add lustre example.
* Add to smt1 as well.
* Fix.
* Fix.
* Fix for new option.
|
|
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
|
|
* Initial documentation and clean up of SyGuS PBE class, fix issue with concat strategy.
* More documentation, cleanup.
* Do not use concat strategy for 3+ arguments to concat, add regression.
* Minor
|
|
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.
* Minor
* Add case for reals, comment.
* Fix regress1.
|
|
* Refactor conjecture class in ce guided instantiation, move to own file. In preparation for sygus streaming mode.
* Infrastructure for streaming guards, more cleanup.
* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.
* More cleanup, add comments.
* Update comments
* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.
* Fix makefile.
* Cleanup.
* Remove unused includes.
* Minor
|
|
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.
|
|
sygus), update regressions.
|
|
|
|
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
|
|
Minor fixes for inst max level.
|
|
Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
|
|
|
|
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
|
|
universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.
|
|
unconstrained functions in sygus solver.
|
|
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
|
|
|
|
regressions.
|
|
liberal.
|
|
quantified formulas with non-constant polarity.
|
|
|
|
|
|
|
|
pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.
|
|
|
|
Start grammar. Add regression.
|
|
Add regression.
|
|
grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
|
|
within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions.
|
|
|
|
|
|
|
|
|
|
--fmf-fun.
|
|
|
|
regressions.
|
|
Add sygus regressions.
|
|
|
