| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
|
|
|
|
When using the `TS_ASSERT_THROWS` marco from CxxTest, we have to make
sure that we use a reference type for the exception, otherwise the unit
test tries to catch the exception by value, resulting in "catching
polymorphic type by value" warnings.
|
|
|
|
|
|
This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
|
|
|
|
|
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.
No performance impact is expected outside of datatypes. I'm verifying that that is the case with a cluster job this morning.
|
|
|
|
** file-level documentation at the top of the sources. **
This is the "make bugzilla stop bugging me" bugfix commit.
* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
Updated documentation in the file. Resolves bug #99.
* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
moved into a separate file. Partially resolves bug #100.
* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
namespace) instead of metakind.h (where it was in CVC4::metakind).
This clears up a warning (private #inclusion) from the SMT and SMT2
parsers, and maybe makes more sense anyways, since this is based on
the kind (and not the metakind) of an operator.
* Documentation improvement; doxygen top-level \file gestures, \brief
gestures for files, etc. Changed contrib/update-copyright.pl for
this change, and post-processed to add \brief. Resolves bug #98.
* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
They no longer made sense. Resolves bug #91.
|
|
|
|
|
|
|
