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

Age	Commit message (Collapse)	Author
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	Printing commands as they're executed now requires verbosity 3+	Morgan Deters

2013-02-04	Merge branch '1.0.x'	Morgan Deters

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	Merge from mdeters/miplib branch (commit ↵	Morgan Deters
	'ce7c485182902ae43871057185095f71f74a8a58')
2013-02-03	new option for doing top-level miplib substitutions (or not)	Morgan Deters

2013-02-03	extended miplib trick to 6 vars, should work on pp miplib examples now	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-02-03	correct output language bug with --dump-to	Morgan Deters

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

2013-02-01	Fix a tuple attribute bug that was causing model-generation problems for tuples	Morgan Deters

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

2013-01-31	Fix a small problem in clang builds due to namespaces and symbol lookup	Morgan Deters

2013-01-31	Fix a small problem in clang builds due to namespaces and symbol lookup	Morgan Deters

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

2013-01-30	correct output language bug with --dump-to	Morgan Deters

2013-01-29	currently disabling bug486 regression. we need to discuss ↵	Andrew Reynolds
	getValue/collectModelInfo for quantifiers more.
2013-01-28	fix for finite model finding caused by new collectModelInfo code	Andrew Reynolds

2013-01-28	Updated NEWS for recent changes.	Morgan Deters

2013-01-28	Fixes for Win32 (closes bugs 488 and 489)	Morgan Deters
	* timer statistics now supported (closes bug 488) * use of --mmap doesn't crash anymore (closes bug 489)
2013-01-28	Merge branch '1.0.x'	Morgan Deters

2013-01-28	Fix the regression test for bug 486, and enable it	Morgan Deters
	(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
2013-01-28	Fix the regression test for bug 486, and enable it	Morgan Deters

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	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

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	Merge branch '1.0.x'	Morgan Deters
	Conflicts: NEWS
2013-01-23	fix to workaround ANTLR 3.2 issue with initialization	Morgan Deters

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-23	update NEWS file	Morgan Deters

2013-01-23	add user patterns to the Smt1 parser; update NEWS file	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

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

2013-01-22	update ANTLR URLs (antlr.org -> antlr3.org)	Morgan Deters