projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Support ackermannization on uninterpreted sorts in BV (#3372)
[cvc5.git]
/
test
/
regress
/
regress0
/
sygus
/
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
tree
|
commitdiff
2019-11-30
Andres Noetzli
Competition build: Skip parsing error regression (...
tree
|
commitdiff
2019-11-25
Andrew Reynolds
Better front-end type checking for SyGuS (#3496)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Avoid non-well-founded sygus grammars (#3434)
tree
|
commitdiff
2019-10-15
Andres Noetzli
Fix regression (#3393)
tree
|
commitdiff
2019-10-14
Andres Noetzli
Disable regression test for competition build (#3388)
tree
|
commitdiff
2019-10-11
Andrew Reynolds
Check that logic is set when synth-fun command is encou...
tree
|
commitdiff
2019-10-08
Andrew Reynolds
Limit cases of sygus inference based on type (#3370)
tree
|
commitdiff
2019-10-01
Andrew Reynolds
Trivial solve method for single invocation sygus (...
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix sygus datatype parsing in sygus v1 format (#3113)
tree
|
commitdiff
2018-11-21
Andrew Reynolds
Quickly recognize when PBE conjectures are infeasible...
tree
|
commitdiff
2018-11-07
Haniel Barbosa
Adding default SyGuS grammar construction for arrays...
tree
|
commitdiff
2018-10-05
Andrew Reynolds
Update default options for sygus (#2586)
tree
|
commitdiff
2018-09-26
Haniel Barbosa
Makes SyGuS parsing more robust in invariant problems...
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added regression tests and target make regress.
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-08-22
Haniel Barbosa
Adds regression test for automatic generation of SyGuS...
tree
|
commitdiff
2018-07-23
Andrew Reynolds
sygusComp2018: add regressions (#2191)
tree
|
commitdiff
2018-05-21
Caleb Donovick
Fix file extension (#1919)
tree
|
commitdiff
2018-05-18
Andrew Reynolds
Cegis unif defaults to cegis when no unif (#1942)
tree
|
commitdiff
2018-03-21
Andres Noetzli
Move regression tests to single Makefile.am (#1658)
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Refactor regressions (#1581)
tree
|
commitdiff
2018-02-06
Andrew Reynolds
Statically eliminate redundant sygus constructors ...
tree
|
commitdiff
2018-02-02
Andrew Reynolds
Fix remaining synthesis solution regressions (#1557)
tree
|
commitdiff
2018-02-02
Haniel Barbosa
Option to check solutions produced by SyGuS solver...
tree
|
commitdiff
2018-01-22
Aina Niemetz
Refactor and fix solveBvLit for CBQI BV. (#1526)
tree
|
commitdiff
2018-01-12
Andrew Reynolds
Improvements for CBQI BV (#1504)
tree
|
commitdiff
2017-12-07
Andrew Reynolds
Fixes related to SyGuS + real arithmetic (#1432)
tree
|
commitdiff
2017-12-01
Andrew Reynolds
Refactor and generalize PBE strategies (#1410)
tree
|
commitdiff
2017-11-21
Andrew Reynolds
Cegqi bv remove extract terms preprocess pass (#1376)
tree
|
commitdiff
2017-11-13
Andrew Reynolds
Disable sygus qe preprocessing by default (#1353)
tree
|
commitdiff
2017-11-13
Andrew Reynolds
Argument Relevance for Synthesis Conjectures (#1311)
tree
|
commitdiff
2017-11-04
Andrew Reynolds
Suppport SAT logic (#1310)
tree
|
commitdiff
2017-11-03
Andrew Reynolds
Sygus clean main (#1297)
tree
|
commitdiff
2017-10-23
Andrew Reynolds
Document sygus programming-by-examples utility (#1260)
tree
|
commitdiff
2017-10-12
Andrew Reynolds
Sygus logics (#1226)
tree
|
commitdiff
2017-09-30
Andrew Reynolds
SyGuS streaming solution mode (#1131)
tree
|
commitdiff
2017-09-21
Andrew Reynolds
Sygus inv templ refactor (#1110)
tree
|
commitdiff
2017-08-24
Andrew Reynolds
Merge pull request #191 from timothy-king/cleanup-regexp
tree
|
commitdiff
2017-08-04
ajreynol
Set default language to smt lib 2.6 (including as a...
tree
|
commitdiff
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
tree
|
commitdiff
2017-07-20
ajreynol
Fix a few bugs related to sygus.
tree
|
commitdiff
2017-07-10
ajreynol
Merge datatype shared selectors/sygus comp 2017 branch...
tree
|
commitdiff
2016-11-18
Clark Barrett
Merge pull request #110 from 4tXJ7f/fix_makefiles
tree
|
commitdiff
2016-11-18
Andres Notzli
Fix Makefiles in test
tree
|
commitdiff
2016-10-21
ajreynol
Move slow regress0 benchmarks to regress1, increment...
tree
|
commitdiff
2016-07-05
PaulMeng
Merge branch 'master' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-05-18
ajreynol
Refactor modes for sygus+single invocation. Add option...
tree
|
commitdiff
2016-05-16
ajreynol
Enable --sygus-direct-eval by default, limit to terms...
tree
|
commitdiff
2016-05-06
ajreynol
Minor clean up, fixes related to sygus.
tree
|
commitdiff
2016-05-05
ajreynol
Compute term indices lazily in TermDb. Optimization...
tree
|
commitdiff
2016-04-20
PaulMeng
update from the master
tree
|
commitdiff
2016-03-08
ajreynol
Extend synthesis solver to handle single invocation...
tree
|
commitdiff
2015-11-25
ajreynol
Infrastructure for partially single invocation properti...
tree
|
commitdiff
2015-11-10
ajreynol
Fix infinite loop in datatype enumerator. Minor fixes...
tree
|
commitdiff
2015-11-07
Tim King
Changing file permissions to add or remove executable...
tree
|
commitdiff
2015-09-29
ajreynol
Fix for fmf+incremental. Restrict cbqi to literals...
tree
|
commitdiff
2015-09-24
ajreynol
Counterexample-guided instantiation for datatypes....
tree
|
commitdiff
2015-09-17
ajreynol
Allow most smt2 commands as sygus commands. Fix bug...
tree
|
commitdiff
2015-09-02
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
tree
|
commitdiff
2015-08-27
ajreynol
Modify slow regressions.
tree
|
commitdiff
2015-08-01
ajreynol
Support for default grammar for datatypes in sygus...
tree
|
commitdiff
2015-07-31
ajreynol
Sygus support for inductive datatypes.
tree
|
commitdiff
2015-07-28
Tianyi Liang
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2015-07-25
ajreynol
Add option --sygus-inv-templ for synthesizing strengthe...
tree
|
commitdiff
2015-07-20
ajreynol
Squashed merge of SygusComp 2015 branch.
tree
|
commitdiff
2015-06-11
ajreynol
Avoid naming conflicts in sygus, refactor. Add missing...
tree
|
commitdiff
2015-06-11
ajreynol
Handle duplicate operators in sygus grammars. Parse...
tree
|
commitdiff
2015-06-11
ajreynol
Update experimental scripts. Support top-level non...
tree
|
commitdiff
2015-06-10
ajreynol
Support for printing solutions involving LetGTerm sygus...
tree
|
commitdiff
2015-06-02
ajreynol
Flatten sygus grammars during parsing. Remove duplicate...
tree
|
commitdiff
2015-05-12
barrettcw
Merge pull request #74 from finnhaedicke/namespace_minisat
tree
|
commitdiff
2015-05-11
ajreynol
Allow sygus with no syntactic restrictions for LIA...
tree
|
commitdiff
2015-05-11
ajreynol
Add missing regression.
tree
|
commitdiff
2015-05-11
ajreynol
Support for arbitrary constants/variables in Sygus...
tree
|
commitdiff
2015-04-24
ajreynol
Fix sygus parser for non-tokenized operators, reenable...
tree
|
commitdiff
2015-04-23
Clark Barrett
Merge branch 'master' into google
tree
|
commitdiff
2015-04-22
Kshitij Bansal
Merge pull request #73 from kbansal/parser-dont-tokenize
tree
|
commitdiff
2015-04-16
Kshitij Bansal
disable failing sygus tests
tree
|
commitdiff
2015-02-26
ajreynol
Robust strategy for single invocation LIA synthesis...
tree
|
commitdiff
2015-02-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
tree
|
commitdiff
2015-01-20
ajreynol
Mark datatypes as sygus. Add option to normalize sygus...
tree
|
commitdiff
2015-01-14
Morgan Deters
sygus input language and benchmark
tree
|
commitdiff