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

Age	Commit message (Collapse)	Author
2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-15	Merge branch '1.0.x'	Tim King

2013-02-14	Removing BVDebug and replacing with Debug.	Tim King

2013-02-13	repairs a bug in rewriterule engine: constructor cannot be used as a pattern	Tianyi Liang

2013-02-12	Fix a preprocessing performance issue.	Morgan Deters

2013-02-07	Merge branch '1.0.x'	Morgan Deters
	Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07	Only put quantifier assertions in model equality engine if fullModel==true	Morgan Deters

2013-02-07	Significant work on bug #491 (not yet closed).	Morgan Deters

2013-02-07	More complete fix for bug 484 (includes fixes for records and tuples).	Morgan Deters

2013-02-07	Fix error in tuple type-checking.	Morgan Deters

2013-02-06	make datatypes enumerator behavior clearer (no exceptions in normal operation)	Morgan Deters

2013-02-06	make datatypes enumerator behavior clearer (no exceptions in normal operation)	Morgan Deters

2013-02-05	dos2unix conversion for a number of files; this avoids spurious conflicts ↵	Morgan Deters
	when merging to master
2013-02-05	More improvements for E-matching	Andrew Reynolds

2013-02-04	fixed files with DOS newlines; fixed contrib/ scripts to use git	Morgan Deters

2013-02-04	Some fixes for the miplib preprocessing pass.	Morgan Deters
	* TNode violation bug fix (thanks to Tim King for discovery & fix) * change Boolean miplib-trick substitution option into a threshold * ppAssert() the generated miplib constraints to arithmetic
2013-02-04	Model no longer adds subterms of quantifiers to equality engine, this fixed ↵	Morgan Deters
	bug 492 and resolves previous issue for bug 486. (cherry picked from part of commit e54c0f73712b25f1d6d49a3817c923eea077da81) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-02-04	Model no longer adds subterms of quantifiers to equality engine, this fixed ↵	Andrew Reynolds
	bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2013-02-03	Some cleanup of miplib regressions and options	Morgan Deters

2013-02-03	new option for doing top-level miplib substitutions (or not)	Morgan Deters

2013-02-03	new miplib pass, works for 1 or 2 vars	Morgan Deters

2013-02-03	Remove old miplibtrick from arith static learner	Morgan Deters

2013-01-31	Adding a heuristic to more eagerly split bounded integer variables.	Tim King

2013-01-28	fix for finite model finding caused by new collectModelInfo code	Andrew Reynolds

2013-01-28	made QuantifiersEngine::d_inst_match_trie and ↵	Andrew Reynolds
	QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486 (cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)
2013-01-28	made QuantifiersEngine::d_inst_match_trie and ↵	Andrew Reynolds
	QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
2013-01-27	some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵	Andrew Reynolds
	datatypes theory still crashes for datatypes with boolean subfields (cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
2013-01-27	some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵	Andrew Reynolds
	datatypes theory still crashes for datatypes with boolean subfields
2013-01-26	Merge branch '1.0.x'	Morgan Deters

2013-01-26	another fix for quantifier models (related to bug 486)	Morgan Deters

2013-01-25	fix --check-model --finite-model-find when used together (related to bug 486)	Morgan Deters

2013-01-25	Fix errors and reduce warnings on clang (merge from mdeters/clang)	Morgan Deters

2013-01-25	fix --check-model --finite-model-find when used together (related to bug 486)	Morgan Deters

2013-01-24	Add win32 support (merge from mdeters/win32, with some cleanup).	Morgan Deters

2013-01-23	Adding miplibtrick option.	Tim King

2013-01-23	Adding substitution size cap.	Tim King

2013-01-23	partially address bug 486: allow some model inspection of quantifiers	Morgan Deters

2013-01-23	partially address bug 486: allow some model inspection of quantifiers	Morgan Deters

2013-01-22	Merge branch '1.0.x'	Morgan Deters

2013-01-22	fix for theory preprocessing cache on clang, perhaps others.	Morgan Deters

2012-12-21	Merge branch '1.0.x'	Dejan Jovanović

2012-12-21	adding copy constructor for the datatype enumerator	Dejan Jovanović
	fixes bug 484
2012-12-14	Merging in patch from branch '1.0.x'.	Tim King

2012-12-14	Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x	Tim King

2012-12-14	Changing the rewriter to use Boute's Euclidean definition of division.	Tim King

2012-12-12	Merge pull request #2 from CVC4/1.0.x	Dejan Jovanović
	1.0.x
2012-12-12	* fixed bug 481 by adding check for division by 0 in bit-vector division circuit	lianah
	* added printing for total bit-vector division kinds for debugging purposes
2012-12-11	adding cache for preprocessing datatypes terms to fix bug 475, fix for ↵	Andrew Reynolds
	handling user attributes in quantifiers (was broken) (cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)
2012-12-11	adding cache for preprocessing datatypes terms to fix bug 475, fix for ↵	Andrew Reynolds
	handling user attributes in quantifiers (was broken)
2012-12-06	* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues	Morgan Deters
	* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches. (cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)