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

Age	Commit message (Collapse)	Author
2015-06-30	fix sets-translate	Kshitij Bansal

2014-08-24	fix type in sets_translate	Kshitij Bansal

2014-07-01	Update copyrights.	Morgan Deters

2014-06-25	rename subseteq to subset in smtlib, all kinds and smt operator names are ↵	Kshitij Bansal
	now consistent
2014-06-22	Renaming of SMT2 operator names, kinds for set theory	Kshitij Bansal
	* SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq".
2014-06-19	Fix make install-examples.	Morgan Deters

2014-06-19	basic fixes for sets translator, separate binaries	Kshitij Bansal

2014-06-08	sets translate: a different translation using axioms	Kshitij Bansal
	todo: set logic correctly, split the code for two translators
2014-06-06	sets translator: fix for dags	Kshitij Bansal

2014-06-06	Sets translate, and other short fixes	Kshitij Bansal
	- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine