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

Age	Commit message (Collapse)	Author
2018-02-15	Refactor regressions (#1581)	Andrew Reynolds

2017-12-27	Rel smt parser (#1446)	Arjun Viswanathan

2017-09-10	Ensure that expand definitions is called on all non-variable expressi… (#1070)	Andrew Reynolds
	* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions. * Add comments concerning expandDefinitions * Expand comment, move to .h
2017-05-15	Fix minor bug in sets rewriter	Andres Noetzli
	As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit.
2017-04-21	Fix new relations regressions to use sets-ext.	ajreynol

2017-04-21	Handle subtypes in sets. Bug fixes for tuples with subtypes.	ajreynol

2017-04-20	Support for relational operators identity and join image	Paul Meng

2017-04-14	Actively split for upwards closusure intersection. Minor clean up, add ↵	ajreynol
	regressions.
2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.
2017-03-28	Refactor the standard effort of relational solver	Paul Meng

2016-11-17	Fix Makefiles in test	Andres Notzli
	With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-10-26	New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵	ajreynol
	as extension of sets solver, add regressions.