cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
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

2014-06-11	Some clean-up, post bv-merge.	Morgan Deters
	Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc.