summaryrefslogtreecommitdiff
path: root/src/bindings
AgeCommit message (Collapse)Author
2012-06-12fix a few compatibility bindings issuesMorgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-06-08minor fixes, for Mac OSMorgan Deters
2012-05-31pass JAVA_CPPFLAGS properlyMorgan Deters
2012-05-16Fixing C compatibility library (it still had a reference to CONST_INTEGER).Morgan Deters
This hopefully fixes the Debian build.
2012-03-08fix "make dist"Morgan Deters
2012-03-07fix some Java compatibility-layer interface problems; also fix some Mac OS X ↵Morgan Deters
build issues
2012-02-03updating configure to use python-config for building python bindingsDejan Jovanović
2012-01-27effecting the same change in the compat Java binding as was done to CVC3 ↵Morgan Deters
yesterday (ValidityChecker::value() and ValidityChecker::getValue())
2011-11-26Fix Java JNI installation pathMorgan Deters
2011-11-22fix module name for CVC4 jar file; part of the fix for the Debian package ↵Morgan Deters
build failure last night
2011-11-22More language bindings work:Morgan Deters
* with a patched SWIG, the ocaml bindings build correctly. ** I will provide my patch to the SWIG dev team. * fixed some class interfaces to play more nicely with SWIG. * php, perl, tcl now work; examples added. * improved binding module building and installation. Also: Stop #defining NULL ((void*) 0). This has been in cvc4_public.h for a long, long time, I forget why I added it in the first place, and it's a very, very bad idea. In C++, certain things are permitted for NULL that aren't permitted for ((void*) 0), like for instance implicit conversion to any pointer type. We didn't see an issue here (until now, when interfacing with SWIG), because GCC is usually pretty smart at working around such a broken #definition of NULL. But that's fragile. New exception-free Command architecture. Previously, some command invocations were wrapped in a try {} catch() {} and printed out an error. This is much more consistent now. Each Command invocation results in a CommandStatus. The status can be "unsupported", "error", or "success" (these are each derived classes, though, not strings, so that they can be easily printed in a language-specific way... e.g., in SMT-LIBv2, they are printed in a manner consistent with the spec, and "success" is not printed if the print-success option is off.) All Command functionality are now no-throw functions, which @cconway reports is a Good Thing for Google (where all C++ exceptions are suspect), and also I think is much cleaner than the old way in this instance. Added an --smtlib2 option that enables an "SMT-LIBv2 compliance mode"---really it just sets a few other options like strictParsing, inputLanguage, and printSuccess. In the future we might put other options into a compliance mode, or we might choose to make it the default.
2011-11-16Fix "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-16fix to build system for java bindingsMorgan Deters
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-10-31fix to "make install"Morgan Deters
2011-10-06don't build language bindings unless expressly requested with ↵Morgan Deters
--enable-language-bindings
2011-10-04cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fixMorgan Deters
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-29build system fixesMorgan Deters
2011-09-28another make dist fix for java compat bindingsMorgan Deters
2011-09-28fixes for make dist ; make installMorgan Deters
2011-09-27more interface work; adding legacy C interfaceMorgan Deters
2011-09-25first crack at compatibility java interface (not built by default)Morgan Deters
2011-09-23interface cleanup, java bindings workMorgan Deters
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-20fix buildMorgan Deters
2011-09-20Merge from "swig" branch: language binding for Java is compiling and ↵Morgan Deters
linking. Enable with --enable-language-bindings=java
2011-09-02Merge 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback