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

Age	Commit message (Collapse)	Author
2013-03-27	some Java bindings fixes (fixes Debian build problems)	Morgan Deters

2013-03-27	Merge branch 'master' into bv-core	lianah

2013-03-26	added model generation for bv subtheories and bv-inequality solver option	lianah

2013-03-26	Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac	Morgan Deters

2013-03-25	java input stream adapters working	Morgan Deters

2013-03-23	Merge remote-tracking branch 'dddejan/c++11'	Dejan Jovanović
	Conflicts: src/smt/boolean_terms.cpp
2013-03-23	changing string hash function to use the gnu namespace	Dejan Jovanović
	due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
2013-03-22	Support for Boolean term conversion in datatypes.	Morgan Deters

2013-03-22	compiles with	Dejan Jovanović
	export CXXFLAGS='-std=gnu++0x' before configure fails all regressions in the parser
2013-03-21	Merge branch 'master' into bv-core	lianah

2013-03-20	Better reporting of detached git state in --version and --show-config	Morgan Deters

2013-03-19	merged master with dejan's constant evaluating equality engine	Liana Hadarean

2013-03-19	Remove PropositionalQuery class and all CUDD-related build stuff (and ↵	Morgan Deters
	references)
2013-03-14	Merge branch '1.0.x'	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2013-03-13	post failed attempts at getting the incremental solver to work	lianah

2013-03-11	ite removal option for quantifiers --ite-remove-quant, e-matching for ↵	Andrew Reynolds
	boolean terms, improvement for pre skolemization
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-16	Fix version identification for new git repository.	Morgan Deters

2013-02-05	dos2unix conversion for a number of files; this avoids spurious conflicts ↵	Morgan Deters
	when merging to master
2013-02-04	fixed files with DOS newlines; fixed contrib/ scripts to use git	Morgan Deters

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-01	merged master into branch	lianah

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

2013-01-28	compiling implementation of new slicer finished; need to add debugging ↵	lianah
	information and debug.
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	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

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

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

2013-01-10	fixed most bugs and added paranoid assertions	lianah

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-10	ported my bv-core branch from svn to git	Liana Hadarean

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)
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.
2012-12-05	Improved garbage collection for TheoryArith. The merges all of the code ↵	Tim King
	over from branches/arithmetic/converge except for the new code for simplex.
2012-12-01	Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and ↵	Tim King
	Integer((long int)((1<<29)+1)) gave different values. This was confirmed on vm-int1.cims.nyu.edu. See http://www.ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.
2012-11-30	Changes to SExpr to accept autoconversion from bool and const char*. Adding ↵	Tim King
	an example for combination.
2012-11-29	fixes bug 438, incorporate subtypes into type unification when typechecking ↵	Andrew Reynolds
	parameterized datatypes
2012-11-27	First chunk of boolean-terms support.	Morgan Deters
	Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	Tuples and records merge. Resolves bug 270.	Morgan Deters
	Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-26	Improved implementation of Integer::length() with CLN enabled. Additional ↵	Tim King
	tests to sanity check both versions CLN and GMP versions of length.
2012-11-17	* enable previously-failing (now succeeding) datatype example that uses records	Morgan Deters
	* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-17	fix for language bindings (fixes debian build fail last night)	Morgan Deters

2012-11-17	* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ↵	Morgan Deters
	ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-15	Fix for bug 447.	Tim King

2012-11-13	refactoring of quantifiers rewriter based on code review from yesterday, ↵	Andrew Reynolds
	refactoring code out of instantiators in preparation for quantifiers equality engine