summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-26quick testeatmydataAndres Noetzli
2018-09-26styleanwu1219
2018-09-26fix buganwu1219
2018-09-26space issueanwu1219
2018-09-26fix styleanwu1219
2018-09-26fix styleanwu1219
2018-09-26fix styleanwu1219
2018-09-26add documentations, fix space issuesanwu1219
2018-09-26merge two filesanwu1219
2018-09-26merge two filesanwu1219
2018-09-25Merge branch 'master' of https://github.com/CVC4/CVC4anwu1219
2018-09-25cmake: New INSTALL.md for build and testing instructions. (#2536)Aina Niemetz
2018-09-25cmake: Exclude examples for coverage target. (#2535)Mathias Preiner
2018-09-25Eagerly ensure literal on active guards for sygus enumerators (#2531)Andrew Reynolds
2018-09-25cmake: Add check for GCC 4.5.1 and warn user. (#2533)Mathias Preiner
2018-09-25examples/hashsmt/sha1_inversion: Fix includes for newer Boost version. (#2534)Aina Niemetz
2018-09-25cmake: configure.sh wrapper: Removed unused option --gmp.Aina Niemetz
2018-09-25carefully printing trusted assertions in proofs (#2505)yoni206
2018-09-25update CMakeListsanwu1219
2018-09-25Merge branch 'master' of https://github.com/CVC4/CVC4anwu1219
2018-09-25 revert whiute spaceanwu1219
2018-09-25revert whitespaceanwu1219
2018-09-25clean upanwu1219
2018-09-25revert spaceanwu1219
2018-09-25fix styleanwu1219
2018-09-25add space backanwu1219
2018-09-25clean upanwu1219
2018-09-25cmake: Fix tag code generation dependencies. (#2529)Mathias Preiner
2018-09-25Fix warnings uncovered by cmake build (#2521)Andrew Reynolds
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in. After the change, we are +61-7 on SMT LIB: https://www.starexec.org/starexec/secure/details/job.jsp?id=30581
2018-09-24Allow partial models for multiple sygus enumerators (#2499)Andrew Reynolds
2018-09-24Infrastructure for variable agnostic sygus enumerators (#2511)Andrew Reynolds
2018-09-24 Improve non-linear check model error handling (#2497)Andrew Reynolds
2018-09-24Refactor strings equality rewriting (#2513)Andrew Reynolds
This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
2018-09-24cmake: Fix dependencies for code generation. (#2524)Mathias Preiner
2018-09-24Fix wiki urls. (#2504)Mathias Preiner
2018-09-24cmake: Fix git version info (again). (#2523)Aina Niemetz
2018-09-24cmake: Fix theory order #2. (#2522)Mathias Preiner
2018-09-24Unify rewrites related to (str.contains x y) --> (= x y) (#2512)Andres Noetzli
2018-09-24cmake: Fix theory order. (#2518)Mathias Preiner
2018-09-24Make string rewriter unit tests more robust (#2520)Andres Noetzli
This commit changes the unit test for the string rewriter to use the extended rewriter instead of the regular rewriter to make it more robust, e.g. to different orderings in conjunctions.
2018-09-24cmake: Fix and simplify git version info. (#2516)Aina Niemetz
2018-09-24cmake: Add program prefix option. (#2515)Mathias Preiner
2018-09-24Fix generating debug/trace tags.Mathias Preiner
2018-09-23 New C++ API: Add checks for Terms/OpTerms. (#2455)Aina Niemetz
2018-09-23Fix regress2. (#2502)Andrew Reynolds
2018-09-22cmake: Add python3 option.Mathias Preiner
2018-09-22cmake: Enable -Wall.Mathias Preiner
2018-09-22cmake: Fix systemtests dependency.Mathias Preiner
2018-09-22cmake: Build fully static binaries with option --static.Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback