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

Age	Commit message (Collapse)	Author
2013-07-22	Allow BV and DT in either order in the logic string	Morgan Deters

2013-07-22	Add option --cbqi-recurse.	Andrew Reynolds

2013-07-22	Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added ↵	Andrew Reynolds
	infrastructure to BV collectModelInfo in preparation for bug fix.
2013-07-19	possible fix for bug 521	Dejan Jovanovic

2013-07-19	Minor fix for --no-condense-function-values	Morgan Deters

2013-07-18	Fix quantifier instantiation bug in cbqi, add default priorities in rewrite ↵	Andrew Reynolds
	engine.
2013-07-17	Fix bug 516; include some bug testcases.	Morgan Deters

2013-07-16	fixed seg fault when bv equality is turned off	Liana Hadarean

2013-07-16	fixed bug520	Liana Hadarean

2013-07-16	"Tabular"-style function definitions in models with ↵	Morgan Deters
	--no-condense-function-values
2013-07-16	Minor bugfixes to model-building	Morgan Deters

2013-07-13	Remove now-unused language bindings interface file.	Morgan Deters

2013-07-13	Fix language bindings and portfolio builds.	Morgan Deters

2013-07-12	Fix for curious GCC 4.8 translation with -O.	Morgan Deters

2013-07-11	Remove auto-aritization from TPTP parser	Morgan Deters

2013-07-11	Support for TPTP's TFF0 (with arithmetic)	Morgan Deters
	This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
2013-07-11	Fix for Boolean-term rewriting and LAMBDAs	Morgan Deters

2013-07-09	Fix for bug 519; don't involve ITESimplifier in model generation.	Morgan Deters

2013-07-09	add relevant domain computation	Andrew Reynolds

2013-07-06	Model output is now const; this related to bug 519	Morgan Deters

2013-07-05	Fix for a datatype parsing bug that Tim found.	Morgan Deters

2013-07-02	Make uf strong solver user-context dependent, fixes bug 522.	Andrew Reynolds

2013-07-02	Minor fixes for bounded integers, rewrite engine.	Andrew Reynolds

2013-06-28	More bug fixes for interval models.	Andrew Reynolds

2013-06-28	Fix portfolio builds after yesterday's commits.	Morgan Deters

2013-06-27	Better check-models output for some kinds of problems; add anassertion that ↵	Morgan Deters
	the master equality engine is consistent when it needs to be. This is intended to help root out some recent model-generation bugs.
2013-06-27	Fix minor warnings found by recent clang/gcc.	Morgan Deters

2013-06-27	Remove output.h from public space, to avoid clashes with symbols defined in ↵	Morgan Deters
	users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27	Small fix for IS_INTEGER.	Morgan Deters

2013-06-27	Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they ↵	Morgan Deters
	don't escape to user space Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27	Better user documentation for mkVar() and mkBoundVar().	Morgan Deters
	Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27	Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".	Morgan Deters
	Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-26	Add support for interval models in bounded integers MBQI (in progress).	Andrew Reynolds

2013-06-25	Merge branch '1.2.x'	Morgan Deters

2013-06-25	Proposed fix for bug #513	Morgan Deters

2013-06-25	Refactoring of model engine to separate individual implementations of model ↵	Andrew Reynolds
	builder. Begin work on interval models for integers. Other minor cleanup.
2013-06-24	Add files missing from last commit	Morgan Deters

2013-06-24	Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵	Morgan Deters
	allows linearization of div,mod,/ by a constant.
2013-06-24	Add options for symmetry breaking in uf+ss totality axiom approach, option ↵	Andrew Reynolds
	for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
2013-06-21	Fix failure in non-assertion builds on incorrect SmtEngine use.	Morgan Deters

2013-06-19	Workaround for suspected clang 3.0 codegen bug on Mac	Morgan Deters

2013-06-19	Fix to the "include" extended feature of the SMT-LIB parser	Morgan Deters

2013-06-19	Give a more useful parse error message for "undeclared variable -1".	Morgan Deters
	Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
2013-06-17	Make --var-elim-quant true by default. Add rewrite engine to quantifiers ↵	Andrew Reynolds
	module.
2013-06-15	Fix in SMT2 parser for parametric datatypes	Andrew Reynolds

2013-06-09	another fix for array-store-all printing	Morgan Deters

2013-06-09	Better array-store-all output for SMT-LIB.	Morgan Deters

2013-06-08	Fixes for Boolean terms in arrays (including fix for bug 517).	Morgan Deters

2013-06-07	One more case for arrays of Boolean.	Morgan Deters

2013-06-07	Fix for bug 517.	Morgan Deters