Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-04-27 | Disambiguate namespaces in options, fix permissions | Clark Barrett | |
2015-03-31 | fix echo command in --tear-down-incremental | Kshitij Bansal | |
2015-01-30 | Generalize conflict clauses in sygus sym break, merge caches, refactor. ↵ | ajreynol | |
Preparation for single invocation properties. Set output lang to SMT2 for sygus. | |||
2015-01-26 | Output solutions for synthesis conjectures with --dump-synth. Minor ↵ | ajreynol | |
refactor of previous commit. | |||
2015-01-14 | sygus input language and benchmark | Morgan Deters | |
2014-11-17 | Resource-limiting work. | Liana Hadarean | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2014-11-12 | Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5. | Morgan Deters | |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
2014-10-08 | Merge branch '1.4.x' | Morgan Deters | |
2014-10-08 | Some minor cleanup. | Morgan Deters | |
2014-10-08 | Remove private header from public driver. | Morgan Deters | |
2014-09-30 | Merge branch '1.4.x' | Morgan Deters | |
2014-09-30 | Fix improper #inclusion of private header outside library. | Morgan Deters | |
2014-09-30 | Fix a command-replay bug in tear-down-incremental mode. Thanks to Christoph ↵ | Morgan Deters | |
Sticksel for the report. | |||
2014-09-30 | Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵ | Morgan Deters | |
Christoph Sticksel for reporting these. | |||
2014-09-18 | cvc4terminate infinite loop fix | Kshitij Bansal | |
2014-09-18 | cvc4terminate infinite loop fix | Kshitij Bansal | |
2014-09-04 | Update command_executor_portfolio.cpp | Kshitij Bansal | |
2014-09-03 | Work on conjecture generator : do not generalize subterms with concrete ↵ | ajreynol | |
values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation. Print --dump-instantiations on sat/unknown. | |||
2014-08-26 | Improved SMT-LIBv2 language support for unsat cores. | Morgan Deters | |
2014-08-23 | Unsat core printing. | Morgan Deters | |
2014-08-23 | Some fixes for dump- and get-unsat-core. | Morgan Deters | |
2014-07-11 | fix for windows build | Kshitij Bansal | |
2014-07-10 | Merge remote-tracking branch 'origin/master' into segfaultfix | Kshitij Bansal | |
2014-07-04 | initialize variables | Kshitij Bansal | |
2014-07-01 | Update portfolio_util.cpp | Kshitij Bansal | |
2014-07-01 | Update copyrights. | Morgan Deters | |
2014-07-01 | chat about thread creation | Kshitij Bansal | |
2014-06-27 | Another fix for 32-bit (amends commit b825605). | Morgan Deters | |
2014-06-26 | Merge pull request #46 from mdeters/bug573 | Kshitij Bansal | |
Potential fix for bug 573. | |||
2014-06-26 | Fix for 32-bit (esp. win32 failing build). | Morgan Deters | |
2014-06-26 | Potential fix for bug 573. | Morgan Deters | |
2014-06-26 | Ignore error result when an error is squelched via command verbosity. | Morgan Deters | |
2014-06-25 | Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now ↵ | Morgan Deters | |
supported. | |||
2014-06-24 | stack-size portfolio fix. boost 1.50 now required | Morgan Deters | |
2014-06-22 | Merge tag 'smtcomp2014-application' | Morgan Deters | |
Conflicts: contrib/run-script-smtcomp2014-application src/main/driver_unified.cpp | |||
2014-06-22 | QuitCommand needs "success" output for trace executor. :-(smtcomp2014-application | Morgan Deters | |
2014-06-22 | Final fixes for smtcomp2014-application. | Morgan Deters | |
2014-06-21 | Add some missing functions in configuration and compat library. | Morgan Deters | |
2014-06-19 | Better --segv-spin messages. | Morgan Deters | |
2014-06-19 | Fix for mac readline. | Morgan Deters | |
2014-06-19 | Some reversions of recent commits re: portfolio failure. | Morgan Deters | |
* Partial reversion of b8e28a7, do it a different way. * Revert "Test portfolio with --no-wait-to-join." This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c. | |||
2014-06-19 | More application-track fixes for use with trace executor. | Morgan Deters | |
2014-06-19 | Some fixes for tear-down-incremental and "success" output. | Morgan Deters | |
2014-06-17 | Some reversions of recent commits re: portfolio failure. | Morgan Deters | |
* Partial reversion of b8e28a7, do it a different way. * Revert "Test portfolio with --no-wait-to-join." This reverts commit 8b56004ee8bf6c34aaf045bec12bf0e4401a044c. | |||
2014-06-17 | More application-track fixes for use with trace executor. | Morgan Deters | |
2014-06-17 | Some fixes for tear-down-incremental and "success" output. | Morgan Deters | |
2014-06-15 | Careful there aren't too many "success" messages with ↵ | Morgan Deters | |
--tear-down-incremental (can confuse trace runner). | |||
2014-06-11 | Flush output stream after result printed in portfolio. | Morgan Deters | |
2014-06-11 | Fix for competition mode + parallel. | Morgan Deters | |