summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-11-01Fix and refactor TheoryStrings::checkFlatForms() (#3326)Andres Noetzli
2019-11-01Eagerly beta reduce during sygus to builtin term conversion (#3418)Andrew Reynolds
2019-10-31Rename datatypes sygus solver (#3417)Andrew Reynolds
2019-10-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-27Fix collect model info for higher-order (#3409)Andrew Reynolds
2019-10-27Fix global-declarations support (#3403)Andres Noetzli
2019-10-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
2019-10-22Refactoring skolems for sets (#3381)Andrew Reynolds
2019-10-22NodeValue: Eliminate redundant NBITS macros. (#3400)Aina Niemetz
2019-10-20Cleaning-up the declaration of wrapped functions/methods, which have no defin...Andrew V. Jones
2019-10-18Update overflow check to handle negative numbers (#3396)makaimann
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-10-16Solver state for theory of strings (#3181)Andrew Reynolds
2019-10-15Fix line numbers in templates (#3391)Andres Noetzli
2019-10-15Remove remaining references to Boost and Autotools (#3390)Andres Noetzli
2019-10-15Fix OOB access (#3383)Andres Noetzli
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-14Minor refactor in strings rewriter (#3387)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-11Add support for UBSan instrumentation (#3382)Andres Noetzli
2019-10-10Make order of theories explicit in the source code. (#3379)Aina Niemetz
2019-10-10Warning instead of assertion for failing propagating instance (#3380)Andrew Reynolds
2019-10-09test: Add TS_UTILS_EXPECT_ABORT macro for unit tests. (#3378)Mathias Preiner
2019-10-09NodeValue: Use 'using' instead of 'typedef'. (#3374)Aina Niemetz
2019-10-09NodeValue: Use fixed width return type for getRefCount(). (#3374)Aina Niemetz
2019-10-09Reorder NodeValue class according to our code style guidelines. (#3374)Aina Niemetz
2019-10-08Avoid printing success for `--force-logic` (#3363)Andres Noetzli
2019-10-08cmake: Fix include of CVC4JavaTargets.cmake. (#3373)Mathias Preiner
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-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-10-08pass parameters by reference where it affects performancePiotr Trojanek
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-07Build system: Add build type for incremental competition builds. (#3365)Aina Niemetz
2019-10-07New C++ API: Add Term::getId(). (#3360)Aina Niemetz
2019-10-07[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)Andres Noetzli
2019-10-06Fix typo in regression (#3359)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback