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

Age	Commit message (Expand)	Author
2016-05-26	Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in...	ajreynol
2016-05-17	Minor fix cbqi for constant monomials.	ajreynol
2016-04-10	More work on instantiation propagation. Enable external filtering of instanti...	ajreynol
2016-04-03	Updating the copyright headers and scripts.	Tim King
2016-03-02	Work towards complete instantiation for datatypes.	ajreynol
2016-02-02	Moving dump., command., model., and ite_removal. from smt_util/ to smt/. ...	Tim King
2015-12-22	Bug fix for cbqi, do not use model values for terms involving non-enumerable ...	ajreynol
2015-12-14	Refactoring Options Handler & Library Cycle Breaking	Tim King
2015-11-18	Option for midpoints in cbqi.	ajreynol
2015-11-11	Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.	ajreynol
2015-11-10	Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...	ajreynol
2015-11-04	Better combination of UF with cbqi, refactor quantifiers intialization.	ajreynol
2015-10-31	Improvements to handling of mixed Int/Real quantifiers.	ajreynol
2015-10-26	Extend counterexample-guided instantiation to extended theory of Int/Real, mi...	ajreynol
2015-10-22	Enable counterexample-guided quantifier instantiation by default for quantifi...	ajreynol