summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
** 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.
2010-06-04Missing files in last commitChristopher L. Conway
2010-06-04Enabling RDL/IDL in SMT v1 and adding some simple testsChristopher L. Conway
2010-06-03Implementing input from stdin (Fixes: #144)Christopher L. Conway
2010-06-03Fixes 2 issues with assignments. The first is constructing an initial ↵Tim King
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.
2010-06-03Adds toString to DeltaRationalTim King
2010-06-03Fixes a bug where registration occurs before preregistration.Tim King
2010-06-03Changing ANTLR3 detection in configure (Fixes #147)Christopher L. Conway
2010-06-03* Added NodeBuilder<>::getChild() to make interface more consistentMorgan Deters
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.
2010-06-03resolving bug 139: metaKindOf() warnings still exist, but it's probably a ↵Morgan Deters
g++ 4.3 and 4.4 issue
2010-06-02added a handful of debugTagIsOn("context") checks to resolve bug 143Morgan Deters
2010-06-02more VERBOSE test failuresMorgan Deters
2010-06-01Fixing test failures in production buildChristopher L. Conway
2010-06-01This commit adds a debugTagIsOn() guard around some extremely verbose ↵Tim King
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.
2010-06-01This commit is a fix for a bug in removeITEs(). The check that the then ↵Tim King
branch is a boolean should now be working. This fixes bug 138.
2010-06-01Adding SMT v2 parsing support for: QF_IDL, QF_NIA, QF_RDL, QF_UFIDLChristopher L. Conway
2010-06-01Checking for executable permission on antlr3 scriptChristopher L. Conway
2010-06-01Fixed a bug in partial_model.cpp where the data was immediately deallocated ↵Tim King
before being used. Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.
2010-06-01Fixing failing test in r521Christopher L. Conway
Adding general support for associative operators in SMT v1 and v2
2010-06-01In order for splitting on demand to be able to retract clauses every ↵Dejan Jovanović
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.
2010-05-31First draft implementation of mkAssociativeChristopher L. Conway
2010-05-29Adding a couple of example from fuzzsmt to regress1.Tim King
2010-05-29Couple of fixes to theory arith. pivotAndUpdate now multiplies by a_kj. And ↵Tim King
the tableau now simulates older pivots while adding a new row.
2010-05-29After blasting the disjuncts, TheoryEngine rewrite needs to reinvoke itself. ↵Tim King
QF_LRA is now no longer complaining about seeing nodes that can be rewritten to CONST_BOOLEAN.
2010-05-28This update enables TheoryArith to accept assertions that rewrite to true or ↵Tim King
false. This is temporary and will be removed once TheoryEngine rewriting is more fully debugged.
2010-05-28Bug fixes for combining coefficients of rewritten nodes.Tim King
2010-05-28Added printModel() to src/theory/arith/partial_model.cpp. This is a ↵Tim King
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.
2010-05-28A few changes to the organization of TheoryEngine rewriting. A few bug fixes ↵Tim King
for it as well. make check should now work again.
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ↵Tim King
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.
2010-05-27fix bug #134: infinite deallocation loopMorgan Deters
2010-05-27small cosmetic change to tests summary outputMorgan Deters
2010-05-27Remove isAtomic() as per 4/27/2010 meeting. Add comments about its ↵Morgan Deters
potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
2010-05-27fix compiler comparison-signedness warningsMorgan Deters
2010-05-27Reverting this file to not include any comments. (Morgan's revision and my ↵Tim King
revision were in conflict.)
2010-05-27added the ability to add custom expected stdout, stderr, and exit codes to ↵Morgan Deters
smt and smt2 regressions; resolves bug 132
2010-05-27Preregistration has been turned on. Highly experimental eager splitting ↵Tim King
support has been added. Also a few bug fixes to Tableau.
2010-05-27Use the newer automake test driver "parallel-tests". This driver:Morgan Deters
* 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.
2010-05-27Adding debug assertions on most TNode operationsChristopher L. Conway
2010-05-27Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)Christopher L. Conway
2010-05-27Adding .cvc4_config to .gitignoreChristopher L. Conway
2010-05-27fix bug #111: errors in building lcov-allMorgan Deters
2010-05-27fix bug 120; competition mode regression failures for intentionally-buggy inputMorgan Deters
2010-05-26 . '+Outstanding case split in theory arith'Tim King
2010-05-26Adding CnfStreamBlack tests for all Boolean connectivesChristopher L. Conway
2010-05-26Fixing test failures in CnfStreamBlack (it was the test's fault)Christopher L. Conway
2010-05-26Adding documentation to my-configureChristopher L. Conway
2010-05-26Fixing my-configureChristopher L. Conway
2010-05-26Adding contrib/my-configureChristopher L. Conway
2010-05-26Adding CnfStream unit testsChristopher L. Conway
2010-05-26CDMap<> and CDOmap<> fixes to resolve bug 123Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback