summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2019-09-26Fix commentAndres Noetzli
2019-09-26Merge branch 'master' into splitEqRewAndres Noetzli
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-18Add support for creating constant arrays to the new C++ API (#3296)makaimann
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-16Avoid computing cardinality when constructing models (#3268)Andrew Reynolds
2019-09-16Fix spurious meta-info in regression (#3294)Andrew Reynolds
2019-09-16Remove equality inference option for quantifiers (#3282)Andrew Reynolds
2019-09-16 Fix HO model construction for functions having Boolean arguments (#3158)Andrew Reynolds
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...Andrew Reynolds
2019-09-12 Fix default grammar construction for arrays when no free variables are prese...Andrew Reynolds
2019-09-11Fix constructor type printing (#3246)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-08-29Better heuristic for str.code/re.range (#3220)Andres Noetzli
2019-08-29Infer conflicts based on regular expression inclusion (#3234)Andres Noetzli
2019-08-23 Infer emptiness instead of splitting when a string equality rewrites to a co...Andrew Reynolds
2019-08-23Exclude redundant lemmas when tracking inst lemmas. (#3210)Andrew Reynolds
2019-08-23Update dynamic splitting strategy for quantifiers (#3162)Andrew Reynolds
2019-08-22 Local substitutions for context-depdendent simplification in strings (#3204)Andrew Reynolds
2019-08-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-19New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming...Aina Niemetz
2019-08-18Context-independent regular expression unfolding (#3168)Andrew Reynolds
2019-08-14 Update to standard implementation of getting free variables (#3175)Andrew Reynolds
2019-08-13New C++ API: Add checks and tests for Solver::simplify. (#3170)Aina Niemetz
2019-08-13New C++ API: Fix test names of solver_black unit test. (#3170)Aina Niemetz
2019-08-13Add string rewrite involving allchar stars (#3167)Andrew Reynolds
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-11New C++ API: Add templated getIndices method for OpTerm (#3073)makaimann
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-08-04Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)Mathias Preiner
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-02Remove simplification specialized for sygus si solution reconstruction (#3147)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-08-02Fix solution filtering for streaming abducts (#3143)Andrew Reynolds
2019-08-01Fix BVGauss unit tests. (#3142)Mathias Preiner
2019-08-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-31adding bv_gauss unit test to build files (#3135)yoni206
2019-07-30Minor improvement for rewriter for str.replace (#3124)Andrew Reynolds
2019-07-30 Handle RE intersections modulo equality (#3120)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback