summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-12Move ss-combine rewrite to extended rewritersat2019pldi2019Andres Noetzli
2018-11-07Add str.code support in old string rewriterAndres Noetzli
2018-11-07Merge branch 'master' into pldi2019Andres Noetzli
2018-11-07Fix collectEmptyEqs in string rewriter (#2692)Andres Noetzli
2018-11-07 Fix for itos reduction (#2691)Andrew Reynolds
2018-11-06Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)Andrew Reynolds
2018-11-05Change default sygus enumeration mode to auto (#2689)Andrew Reynolds
2018-11-05Fix coverity warnings in sygus enumerator (#2687)Andrew Reynolds
2018-11-05New C++ API: Split unit tests. (#2688)Aina Niemetz
2018-11-05Increasing coverage (#2683)yoni206
2018-11-05API: Fix assignment operators (#2680)Andres Noetzli
2018-11-05configure.sh: Fix option parsing to match --help (#2611)Andres Noetzli
2018-11-05Allow partial models with optimized sygus enumeration (#2682)Andrew Reynolds
2018-11-04 Implement option to turn off symmetry breaking for basic enumerators (#2686)Andrew Reynolds
2018-11-03Refactor default grammars construction (#2681)Haniel Barbosa
2018-11-01fixes to regression docs (#2679)yoni206
2018-11-01Merge branch 'extRewBv' into pldi2019Andres Noetzli
2018-11-01Merge branch 'master' into pldi2019Andres Noetzli
2018-10-31Merge branch 'master' into pldi2019Andres Noetzli
2018-10-31Add optimized sygus enumeration (#2677)Andrew Reynolds
2018-10-31Merge branch 'master' of https://github.com/CVC4/CVC4 into extRewBvajreynol
2018-10-31Fixajreynol
2018-10-31Record assumption info in AssertionPipeline (#2678)Andres Noetzli
2018-10-24Minor improvement to sygus trace (#2675)Andrew Reynolds
2018-10-23CMake: Set RPATH on installed binary (#2671)Andres Noetzli
2018-10-22Do not use lazy trie for sygus-rr-verify (#2668)Andrew Reynolds
2018-10-22Fail for SWIG 3.0.8 (#2656)makaimann
2018-10-22CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)Andres Noetzli
2018-10-22Only build CryptoMiniSat library, no binary (#2657)Andres Noetzli
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
2018-10-20Remove antlr_undefines.h. (#2664)Mathias Preiner
2018-10-20Add substr, contains and equality rewrites (#2665)Andres Noetzli
2018-10-20Disable dumping test for non-dumping builds (#2662)Andres Noetzli
2018-10-20Travis: run examples and avoid building them twice (#2663)Andres Noetzli
2018-10-19BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2...Aina Niemetz
2018-10-19BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const...Aina Niemetz
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-19Fix util::Random for macOS builds (#2655)Andres Noetzli
2018-10-19Add helper to detect length one string terms (#2654)Andres Noetzli
2018-10-18Add OptionException handling during initialization (#2466)Andres Noetzli
2018-10-18cmake: Run regression level 2 for make check. (#2645)Mathias Preiner
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Non-contributing find replace rewrite (#2652)Andrew Reynolds
2018-10-18Improve reduction for str.to.int (#2636)Andrew Reynolds
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-18Constant length regular expression elimination (#2646)Andrew Reynolds
2018-10-17 Skip sygus-rr-synth-check regressions when ASAN on (#2651)Andres Noetzli
2018-10-17Show if ASAN build in --show-config (#2650)Andres Noetzli
2018-10-17Sygus query generator (#2465)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback