summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-09-01todobool-terms-with-skolemsDejan Jovanovic
2015-09-01theoryOf() -> uninterpreted sort ownerDejan Jovanovic
2015-09-01removing THEORY_BOOL as a special tag from equality engineDejan Jovanovic
2015-03-18Change datatypes preregister to addTerm on boolean terms.ajreynol
2015-03-17fix some regression failuresKshitij Bansal
2015-03-02Initial work on boolean term reorganization. IFF replaced by EQUAL. Boolean...ajreynol
2015-02-27Revert "dummy commit to force nightly builds"Kshitij Bansal
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-25Switch back to eager loop temporarily.Tianyi Liang
2015-02-24minor fix for internal string printTianyi Liang
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-02-18dummy commit to force nightly buildsKshitij Bansal
2015-02-16Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2015-02-16webget: curl follow redirectKshitij Bansal
2015-02-14Fix unit tests.ajreynol
2015-02-14attempt to fix win32 buildsKshitij Bansal
2015-02-13Minor cleanup, remove unused files.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2015-02-12try curl before wget, workaround for issue with FTP PASVKshitij Bansal
2015-02-12Changing CXXFLAGS for custom cln installation in configure.ac.Tim King
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other refactor...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...ajreynol
2015-02-05Minor clean upTianyi Liang
2015-02-05Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2015-02-05Working version of sygus solution reconstruction from single inv cegqi. Heur...ajreynol
2015-02-04Initial draft of solution reconstruction into syntax for single inv cegqi.ajreynol
2015-02-04Work on solution reconstruction for single inv. Fix compiler error found by ...ajreynol
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ...ajreynol
2015-02-04Start work on simplifying single inv solutions. Minor.ajreynol
2015-02-03Simple variable elimination for single inv properties. Relax conditions for ...ajreynol
2015-02-03Solutions for single invocation conjectures.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
2015-02-02Representative programs must be minimal size, minor fixes, improvements to IT...ajreynol
2015-02-01Generalization of sygus lemmas based on arguments and content.ajreynol
2015-01-31Bug fix fairness for commutative operators in sygus. Minor.ajreynol
2015-01-31Lemmas instead of conflicts in sygus sym break (do not expand explanations). ...ajreynol
2015-01-30Generalize conflict clauses in sygus sym break, merge caches, refactor. Prep...ajreynol
2015-01-29Apply sygus search space narrowing for all subprograms of current global state.ajreynol
2015-01-29Restrict LtePartialInst instantiations based on E-matching, promote to quanti...ajreynol
2015-01-29Apply global search space narrowing for multiple synth-fun, enable its confli...ajreynol
2015-01-29Add module for sygus search space narrowing based on global state.ajreynol
2015-01-28Minor refactor CEGQI.ajreynol
2015-01-27Always miniscope nested quantifiers. Disable miniscoping when cegqi enabled....ajreynol
2015-01-27Recognize when synthesis conjectures are in single invocation fragment.ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2015-01-26Generalize sygus search space narrowing to arbitrary theory rewriting.ajreynol
2015-01-24Variable patterns only look at eligible terms. Minor refactoring of quantifi...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback