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

Age	Commit message (Collapse)	Author
2018-08-07	Require Swig 3 (#2283)	Andres Noetzli
	Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h
2018-08-07	Delete functions instead of using CVC4_UNDEFINED (#1794)	Andres Noetzli
	C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable.
2018-03-26	Make Java bindings work with newer build envs (#1709)	Andres Noetzli
	Our current build scripts did not work with Automake 1.16. At configure time, the .swig_deps target in src/bindings/Makefile.am was executed due to the `@mk_include@ .swig_deps` (which is not the case with older versions of Automake). This ultimately caused configure to fail because SWIG was complaining about missing files (generated source files, such as src/expr/expr.h). This commit fixes the issue by adding `-ignoremissing` to the call to SWIG. With that option, SWIG is not complaining about the missing files and the dependency generation completes successfully. Currently, the src/bindings/compat/java/create_impl.py script is not compatible with Python 3, which leads to errors when building on systems where `python` links to Python 3 (e.g. on Arch Linux). This commit makes the script compatible with both Python 2 and 3. Our build scripts were using old -source/-target versions when calling `javac`. Those are not supported by newer Java versions (e.g. Java 9). This commit updates the version to 1.6, which is still fairly old, so should be broadly supported. Finally, some systems (e.g. Arch Linux' AUR package for SWIG 2) refer to SWIG 2 as `swig-2`. This commit adds support for detecting this at configure time.
2013-05-16	minor changes to language bindings	Morgan Deters

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

2012-11-27	give warning at configure-time about unsupported language bindings, and ↵	Morgan Deters
	don't advertise them in help listing for --enable-language-bindings
2012-10-06	* Some documentation about building compatibility and language bindings	Morgan Deters
	* Better errors/warnings when SWIG isn't installed (resolves bug 373) * Allow compatibility bindings to be built when SWIG isn't available
2012-02-03	updating configure to use python-config for building python bindings	Dejan Jovanović

2011-11-16	Fix "make dist". Fixes to python and ruby bindings; ruby example written. ↵	Morgan Deters
	They should both work out of the box, now, with swig 2.0.4 at least. "make install" likely still needs to be adjusted to install them sensibly.
2011-11-16	* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!	Morgan Deters
	* Also some better configure script wording
2011-11-15	Bindings work (ocaml bindings are now sort of working); also minor cleanup	Morgan Deters

2011-10-06	don't build language bindings unless expressly requested with ↵	Morgan Deters
	--enable-language-bindings
2011-10-03	user push/pop support in minisat and simplification; also bindings work	Morgan Deters

2011-09-27	more interface work; adding legacy C interface	Morgan Deters

2011-09-21	Java binding now working. Some interface types still need some work (e.g. ↵	Morgan Deters
	iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
2011-09-20	Merge from "swig" branch: language binding for Java is compiling and ↵	Morgan Deters
	linking. Enable with --enable-language-bindings=java
2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.