summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-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-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-26Symmetry breaking for variable agnostic enumerators (#2527)Andrew Reynolds
2018-09-25Eagerly ensure literal on active guards for sygus enumerators (#2531)Andrew Reynolds
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-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-22cmake: Add python3 option.Mathias Preiner
2018-09-22cmake: Enable -Wall.Mathias Preiner
2018-09-22cmake: Build fully static binaries with option --static.Mathias Preiner
2018-09-22cmake: Add more documentation, some fixes and cleanup.Mathias Preiner
2018-09-22cmake: Guard GetGitRevisionDescription.Mathias Preiner
2018-09-22cmake: Add support for cross-compiling for Windows.Mathias Preiner
2018-09-22cmake: More documentation, clean up.Aina Niemetz
2018-09-22cmake: Move extracting git information to src/base cmake config file.Aina Niemetz
2018-09-22cmake: FindANTLR: Check if antlr3FileStreamNew is available.Mathias Preiner
2018-09-22cmake: Add make install rule.Mathias Preiner
2018-09-22cmake: Various CMakeLists.txt fixes/cleanup.Mathias Preiner
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
The sources of all previous libraries are now added to libcvc4 and built as libcvc4. This removes circular dependencies between libcvc4 and libexpr. Further, we now only have one parser library and don't build additional libraries for each language.
2018-09-22cmake: Move find_package to where it is actually needed.Mathias Preiner
2018-09-22cmake: Add convenience wrappers for tag generation.Mathias Preiner
2018-09-22cmake: Add library versioning for libcvc4.so.Mathias Preiner
2018-09-22cmake: Rebase with current master, add new tests/source files.Mathias Preiner
2018-09-22cmake: Use target specific includes for libcvc4.Mathias Preiner
Further, print definitions added with add_definitions(...).
2018-09-22cmake: Add missing dependency.Mathias Preiner
2018-09-22cmake: Add SWIG support + Python and Java bindings.Mathias Preiner
2018-09-22cmake: Add portfolio support.Mathias Preiner
2018-09-22cmake: Add support for CxxTest.Aina Niemetz
2018-09-22cmake: Do not set global output directories for binaries and libraries.Mathias Preiner
2018-09-22cmake: Fix some includes.Mathias Preiner
2018-09-22cmake: Add module finder for readline.Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback