Age | Commit message (Collapse) | Author |
|
** 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.
|
|
|
|
|
|
|
|
assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.
|
|
|
|
|
|
|
|
with that of Node.
* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
related to children now throw an IllegalArgumentException:
* getNumChildren()
* begin()
* end()
* operator[]
* getChild()
This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
the children are "reinterpreted" -- the first being an operator. Interface-wise,
it doesn't make sense to return one thing for nb[0], then later, after setting
the kind, to return another thing for nb[0].
* Fixed unit tests depending on this behavior.
* Added a warning to the testing summary if unit tests didn't run (because this
is likely due to compilation problems, and without a warning it looks kind of
like a test success)
* VERBOSE wasn't exported to the environment for unit test "make check." Fixed.
|
|
g++ 4.3 and 4.4 issue
|
|
|
|
|
|
|
|
debugging statements. There is some evidence that these debugging statements were 20% of the running time for QF_LRA/miplib/fixnet-1000.smt in debug mode.
|
|
branch is a boolean should now be working. This fixes bug 138.
|
|
|
|
|
|
before being used. Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.
|
|
Adding general support for associative operators in SMT v1 and v2
|
|
translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
|
|
|
|
|
|
the tableau now simulates older pivots while adding a new row.
|
|
QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.
|
|
false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.
|
|
|
|
debugging utility that prints out the lower bound, upper bound, assignment, and the constraints that were asserted that caused the lower bound and upperbound to be asserted.
|
|
for it as well. make check should now work again.
|
|
to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.
|
|
|
|
|
|
potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
|
|
|
|
revision were in conflict.)
|
|
smt and smt2 regressions; resolves bug 132
|
|
support has been added. Also a few bug fixes to Tableau.
|
|
* keeps test logs around
* provides parallel testing functionality (with make -jN).
I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information.
Resolves bug 117.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|