summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-27 Fix indexof range lemma (#3499)Andrew Reynolds
2019-11-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-22fixing stupid typo (#3488)Haniel Barbosa
2019-11-21hard limit for rec-fun eval (#3485)Haniel Barbosa
2019-11-20Lazy evaluation via rec-funs of ITE expressions (#3482)Haniel Barbosa
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-17Updates to the unit tests, api, and examples for datatypes (#3459)Andrew Reynolds
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-14Use Shebang in cxxtestgen when appropriate (#3458)Alex Ozdemir
2019-11-13Allow (set-logic ...) after (reset) (#3457)Andres Noetzli
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
2019-11-06[Regressions] Remove leading whitespace in output (#3444)Andres Noetzli
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-04[Regressions] Support for running w/ default args (#3436)Andres Noetzli
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-27Fix global-declarations support (#3403)Andres Noetzli
2019-10-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
2019-10-18Update overflow check to handle negative numbers (#3396)makaimann
2019-10-15Fix regression (#3393)Andres Noetzli
2019-10-14Disable regression test for competition build (#3388)Andres Noetzli
2019-10-14Remove benchmark (#3389)Andrew Reynolds
2019-10-14Support UF in default sygus grammars (#3319)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-14Ensure lemmas from sygus repair const are guarded (#3385)Andrew Reynolds
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-11Check that logic is set when synth-fun command is encountered (#3384)Andrew Reynolds
2019-10-09test: Add TS_UTILS_EXPECT_ABORT macro for unit tests. (#3378)Mathias Preiner
2019-10-08Avoid printing success for `--force-logic` (#3363)Andres Noetzli
2019-10-08New C++ API: Term: Add missing checks for null. (#3364)Aina Niemetz
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-10-08Fix method for getting arithmetic function definition body (#3371)Andrew Reynolds
2019-10-08[CVC Parser] Add support for regular expressions (#3346)Andres Noetzli
2019-10-08Disallow --proof and --incremental (#3332)Andres Noetzli
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-10-07New C++ API: Add Term::getId(). (#3360)Aina Niemetz
2019-10-06Fix typo in regression (#3359)Andrew Reynolds
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
2019-10-03Disable proofs for unsupported logics (#3327)yoni206
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback