summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-28Merge branch 'master' into emptyEqemptyEqAndrew Reynolds
2018-09-28cmake: Only do Java tests when unit testing on (#2551)Andres Noetzli
Right now, we are adding the Java tests even when we are not building unit tests. This commit changes the build system to only add the Java tests when unit tests are enabled. There are two reasons for this change: - building a production version of CVC4 should not require JUnit - it seems more intuitive (to me at least) to disable JUnit tests when unit tests are disabled This change also simplifies building the Java bindings in our homebrew formula.
2018-09-27cmake: Add CxxTest finder module to allow custom paths. (#2542)Mathias Preiner
2018-09-27address review, fix oobAndres Noetzli
2018-09-27Remove assertion. (#2549)Andrew Reynolds
2018-09-27Infrastructure for using active enumerators in sygus modules (#2547)Andrew Reynolds
2018-09-27Incorporate all unification enumerators into getTermList. (#2541)Andrew Reynolds
2018-09-27Rewrites for (= "" _) and (= (str.replace _) _)Andres Noetzli
This commit adds rewrites for string equalities, specifically equalities with empty strings and replacements.
2018-09-27Fix Taylor overapproximation for large exponentials (#2538)Andrew Reynolds
2018-09-26 Fix homogeneous string constant rewrite (#2545)Andrew Reynolds
2018-09-26Fix bug in getSymbols. (#2544)Andrew Reynolds
2018-09-26cmake: Only print dumping warning if not disabled by user. (#2543)Mathias Preiner
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-26cmake: Fix test target dependency issues. (#2540)Mathias Preiner
2018-09-26Enable quantified array regression. (#2539)Andrew Reynolds
2018-09-26Symmetry breaking for variable agnostic enumerators (#2527)Andrew Reynolds
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-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
2018-09-22cmake: Run make coverage in parallel by default.Mathias Preiner
2018-09-22cmake: Add more documentation, some fixes and cleanup.Mathias Preiner
2018-09-22cmake: configure.sh wrapper: Use explicit build directory structure.Aina Niemetz
We don't create build directories for every build type (and configuration) anymore. The default build directory is now 'build' (created where you call the wrapper script from). Option --name allows to configure an individual name (and path) for the build directory.
2018-09-22cmake: configure wrapper: Modify next steps message after configuration.Mathias Preiner
Since configure.sh is only a wrapper for cmake it prints all the messages from cmake. At the end we print the next steps after configuration. If configure.sh is used we add the info to also change into the build directory before calling make.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback