| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
references)
|
|
|
|
|
|
|
|
|
|
don't advertise them in help listing for --enable-language-bindings
|
|
(since it doesn't appear to affect us?!), and make it non-fatal anyway, since threads aren't strictly required for all cvc4 builds. give a warning.
|
|
just in general, and some documentation adjustments.
|
|
|
|
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available
|
|
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default
Also:
* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
documentation, etc.).
* Remove sat_module.cpp, which was no longer used (was previously refactored?)
|
|
|
|
See below for details.
* Fix the "assert" name-collision bug (resolves bug #364).
Our identifiers should never be named "assert", as that's a preprocessor
definition in <assert.h>, which is often #included indirectly (so simply
having a policy of not including <assert.h> isn't good enough---one of
our dependences might include it). It was once the case that we didn't
have anything named "assert", but "assert()" has now crept back in.
Instead, name things "assertFoo()" or similar. Thanks to Tim for the
report.
To fix this, I've changed some of Dejan's circuit-propagator code from
"assert()" to "assertTrue()". Ditto for Andy's explanation manager.
Guys, if you prefer a different name in your code, please change it.
* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
Inner lets now shadow outer lets (previously, they incorrectly gave an
error). Additionally, while looking at this, I found that a sequential let
was implemented rather than a parallel let. This is now fixed. Thanks to
Liana for the report.
* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).
* There were a lot of Debug lines in bitvectors that had embedded toString()
calls. This wasted a LOT of time in debug builds for BV benchmarks
(like in "make regress"). Added if(Debug.isOn(...)) guards; much faster
now.
* Support for building public-facing interface documentation only (as opposed
to all internals documentation). Now "make doc" does the public-facing and
"make doc-internals" does documentation of everything. (Along with changes
to the nightly build script---which will now build and publish both types
of Doxygen documentation---this resolves bug #359).
* Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the
report (a long long time ago--sorry).
* The default output language for all streams is now based on the current set
of Options (if there is one). This has been a constant annoyance, especially
when stringstreams are used to construct output. However, it doesn't work
for calls from outside the library, so it's mainly an annoyance-fixer for
CVC4 library code itself.
* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
are used only in assertions-enabled builds (and thus give warnings in
production builds). This was briefly discussed at the meeting this week.
|
|
condition when reading from stdin. This should completely resolve bug #319.
However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track
Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.
Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.
Closing bug #319.
|
|
|
|
errors; threading support should only be required to build pcvc4, not cvc4
|
|
configure time; fixes a bug reported by Clark for static-binary builds on machines where no static libreadline is available (like CIMS machines)
|
|
|
|
|
|
|
|
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.
|
|
* Also some better configure script wording
|
|
|
|
- can now output LFSC checkable resolution proofs
- added configuration option --enable-proof
- added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.
|
|
v4.5.1 which has a buggy optimizer (resolves bug #266)
|
|
available
|
|
--enable-language-bindings
|
|
|
|
auto-detection of libantlr3c, I chose an innocent-looking function that was present in both versions. But it's signature had changed, breaking source compatibility in both directions. Just like the other function that started the whole mess. Silly me.
|
|
|
|
|
|
|
|
on older g++en, like Apple's 4.2 on Snow Leopard.
|
|
|
|
iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
|
|
linking. Enable with --enable-language-bindings=java
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else. Hopefully this
turns our 3000+ page user manual into something a little
more useful!
|
