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

Age	Commit message (Collapse)	Author
2014-10-17	Merge branch '1.4.x'	Morgan Deters

2014-10-17	Remove a bad (unstable, timing-dependent) test.	Morgan Deters

2014-10-14	Context-dependent expr attributes are now attached to a specific SmtEngine, ↵	Morgan Deters
	and the SAT context is owned by the SmtEngine.
2014-10-06	Fix unit test that was broken with last commit.	Morgan Deters

2014-10-03	Merge branch '1.4.x'	Morgan Deters

2014-10-03	Fix unit test for ArrayStoreAll.	Morgan Deters

2014-09-25	fix unit test for new fair datatype enumeration	Morgan Deters

2014-08-22	Unit test fix.	Morgan Deters

2014-08-04	Better support for resource-limiting when there aren't any actual conflicts.	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2014-06-25	BinaryHeap unit test and some usability/build fixes for the data structure ↵	Morgan Deters
	itself.
2014-06-21	Some minor cleanup and documentation.	Morgan Deters

2014-06-21	fixed build failure	lianah

2014-06-19	added model generation to eager bit-blasting and turned abc off by default	lianah

2014-06-19	disable unate lemmas when using incremental mode	Kshitij Bansal

2014-06-11	Merge pull request #31 from kbansal/sets	Kshitij Bansal
	Sets
2014-06-11	fixed unit tests failures	lianah

2014-06-11	disable failing test	Kshitij Bansal

2014-05-27	update stats_black	Kshitij Bansal

2014-04-01	Merge branch '1.3.x'	Tim King

2014-04-01	Fixing bug 552. There was a bug when integers are made using a string with ↵1.3.x	Tim King
	a lot of leading 0s on old versions of CLN.
2014-03-12	Fix LogicInfo unit test.	Morgan Deters

2014-03-04	Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵	Morgan Deters
	(resolves bug #548).
2014-02-21	add new theory (sets)	Kshitij Bansal
	Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-01-22	Delay QuantifiersEngine and UF strong solver initialization until after ↵	Morgan Deters
	final options/logic are set.
2013-12-24	Better automatic handling of output language setting.	Morgan Deters

2013-12-10	Fix timer statistics to report correct time even on process abort.	Morgan Deters

2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-12-02	Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a ↵	Morgan Deters
	subtype of (Pair Real Real). Resolves bug #541.
2013-11-20	Changing the number of bits allocated per field in node values.	Tim King

2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09	Add support for check-sat with argument.	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-04	Merge branch '1.2.x'	Morgan Deters

2013-06-04	Fix clang static initialization order issue; fixes bug 512.	Morgan Deters

2013-05-29	Merge branch '1.2.x'	Morgan Deters

2013-05-28	Standardize SMT-LIBv2 set of logics to use LogicInfo.	Morgan Deters
	Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics.
2013-05-09	Changing the integer normal form to increase matching.	Tim King

2013-05-03	Fixing compilation of unit tests. These problems were due to splitLemma() ↵	Tim King
	being pure virtual.
2013-04-05	Fix unit test (compile error) for new SatSolver interface	Morgan Deters

2013-04-03	Some final minor changes before cutting 1.1.	Morgan Deters
	* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-03-21	Some model and printing fixes for defined functions in input.	Morgan Deters

2013-03-20	Interactive mode support for multiline input	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2013-02-04	Fix NodeBuilder bug which could attempt to allocate beyond hard limit	Morgan Deters

2012-12-14	Adding unit test for different versions of division.	Tim King

2012-12-08	Fix bug 476: when CxxTest is not found, make the error less fatal-looking	Morgan Deters