cvc5.git
2015-02-14 ajreynolFix unit tests.
2015-02-14 Kshitij Bansalattempt to fix win32 builds
2015-02-13 ajreynolMinor cleanup, remove unused files.
2015-02-13 ajreynolHandle recursive singleton case for codatatypes, add...
2015-02-12 Kshitij Bansaltry curl before wget, workaround for issue with FTP...
2015-02-12 Tim KingChanging CXXFLAGS for custom cln installation in config...
2015-02-11 ajreynolBetter support for solving multiple functions with...
2015-02-11 ajreynolMove si solution reconstruction to own file, make more...
2015-02-06 ajreynolHandle missing cases for single inv solution reconstruc...
2015-02-06 Tianyi LiangMinor clean up
2015-02-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2015-02-06 Tianyi LiangImproved string performance, thanks to Peter's benchmarks.
2015-02-06 Tianyi LiangImproved string performance, thanks to Peter's benchmarks.
2015-02-05 ajreynolWorking version of sygus solution reconstruction from...
2015-02-04 ajreynolInitial draft of solution reconstruction into syntax...
2015-02-04 ajreynolWork on solution reconstruction for single inv. Fix...
2015-02-04 ajreynolRefactor sygus_util to TermDb. Initial work on solutio...
2015-02-04 ajreynolStart work on simplifying single inv solutions. Minor.
2015-02-03 ajreynolSimple variable elimination for single inv properties...
2015-02-02 ajreynolSolutions for single invocation conjectures.
2015-02-02 ajreynolSingle invocation module for counterexample guided...
2015-02-02 ajreynolRepresentative programs must be minimal size, minor...
2015-02-01 ajreynolGeneralization of sygus lemmas based on arguments and...
2015-01-31 ajreynolBug fix fairness for commutative operators in sygus...
2015-01-31 ajreynolLemmas instead of conflicts in sygus sym break (do...
2015-01-30 ajreynolGeneralize conflict clauses in sygus sym break, merge...
2015-01-29 ajreynolApply sygus search space narrowing for all subprograms...
2015-01-29 ajreynolRestrict LtePartialInst instantiations based on E-match...
2015-01-29 ajreynolApply global search space narrowing for multiple synth...
2015-01-29 ajreynolAdd module for sygus search space narrowing based on...
2015-01-28 ajreynolMinor refactor CEGQI.
2015-01-27 ajreynolAlways miniscope nested quantifiers. Disable miniscopi...
2015-01-27 ajreynolRecognize when synthesis conjectures are in single...
2015-01-26 ajreynolOutput solutions for synthesis conjectures with --dump...
2015-01-26 ajreynolGeneralize sygus search space narrowing to arbitrary...
2015-01-24 ajreynolVariable patterns only look at eligible terms. Minor...
2015-01-24 ajreynolAdd --lte-restrict-inst-closure option. Push dt.size...
2015-01-23 ajreynolRefactor sygus arg nf. Minor improvements.
2015-01-23 ajreynolCEGQI fairness based on term height. Fix sygus-nf...
2015-01-23 ajreynolRework inst-closure.
2015-01-22 ajreynolNarrow sygus search space based on NNF and rewriting...
2015-01-22 ajreynolAdd option --lte-partial-inst. Remove inst-closure.
2015-01-22 ajreynolDo not drop patterns during boolean term rewriting...
2015-01-21 ajreynolAvoid redundant constant arguments for SygusNormalForm...
2015-01-21 ajreynolInitial work on sygusNormalForm.
2015-01-20 ajreynolMark datatypes as sygus. Add option to normalize sygus...
2015-01-20 ajreynolHandle miniscoping of conjunctions in synthesis propert...
2015-01-19 Tim KingAdding tests for get-value output for arithmetic.
2015-01-19 Tim KingAdding an additional search path to configure.ac for...
2015-01-17 ajreynolAvoid name conflicts for multiple synth-fun.
2015-01-16 ajreynolLinearize multiplication by constants in sygus grammars...
2015-01-16 ajreynolAllow uninterpreted/defined functions in Sygus grammars...
2015-01-16 ajreynolMinor: Ensure indexed terms are in EE. Add support...
2015-01-14 Morgan Deterssygus input language and benchmark
2015-01-13 Morgan DetersFix #line numbering.
2015-01-13 Morgan DetersFix a memory issue in ResourceManager on 32-bit (resolv...
2015-01-13 Morgan DetersRemove private #include.
2015-01-13 Morgan DetersFix typo.
2015-01-13 Morgan DetersRemove old .orig files that were added to the repository.
2015-01-11 Tianyi Liangadjusted to both v2.0 and v2.5 string literals
2015-01-09 Tianyi Liangblocked unprintable characters in string literals;
2015-01-08 Tianyi Liangswitch ascii encoding to unsigned char
2015-01-07 Tianyi Liangpatch to the last commit
2015-01-07 Tianyi Liangbug fix, thanks to Pierre's report
2015-01-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2015-01-07 Tianyi Liangadded initial AX rules;
2015-01-07 Tianyi Liangadded initial AX rules;
2014-12-28 ajreynolDisable prenex by default when using fmf bound int...
2014-12-27 Dejan JovanovicAdding an option to the equality engine constructor...
2014-12-22 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-12-22 Tianyi Liangbug fix for constant regular expression model building
2014-12-22 Tianyi Liangbug fix for constant regular expression model building
2014-12-22 ajreynolDo not collapse wrongly applied selectors for non-well...
2014-12-21 ajreynolAdd misc trigger options.
2014-12-16 Morgan DetersFix oversight in dumping assertions in preprocessing.
2014-12-12 ajreynolAdd cvc parsing support for cardinality constraints...
2014-12-11 Morgan DetersMinor fixes to language bindings. (Resolves #607.)
2014-12-11 ajreynolOption to enable/disable cyclicity check in datatypes.
2014-12-11 Tianyi Liangbug fix, thanks to Guy's example.
2014-12-09 Morgan DetersBetter error description (related to bug 605).
2014-12-09 Morgan DetersCleanup.
2014-12-06 Tianyi LiangAdded string constant in java api example.
2014-12-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-12-06 Tianyi LiangAdded C++/Java api examples;
2014-12-06 Tianyi LiangAdded C++/Java api examples;
2014-12-06 ajreynolFix dt.size care graph.
2014-12-05 Tianyi LiangRelaxed the constant requirement for regular expression...
2014-12-04 Tianyi Liangclean up and improve intersection
2014-12-04 Morgan DetersFix valgrind-flagged error about uninitialized value.
2014-12-04 Morgan DetersFix segfault in lambdas when constructed via API.
2014-12-04 Morgan DetersFix UnsatCore in language bindings.
2014-12-04 Martin BrainFloating point infrastructure.
2014-12-03 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2014-12-03 Kshitij BansalRevert "Disable constants sharing in eq engine, disable...
2014-12-03 Tianyi Liangdisable inter cache
2014-11-28 ajreynolSynchronize conjecture generation with E-matching....
2014-11-27 Tianyi Liangadd intersection rewriting
2014-11-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-11-27 Tianyi Liangadd more regexp rewriting
2014-11-27 Tianyi Liangadd more functions for regular expressions
next