summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-10-04fix gdb issues (at least for static builds); resolves bug 194Morgan Deters
2010-10-04fix regular expressions in build systemMorgan Deters
2010-10-04fixing CLN builds, which had broken the build tonight; will re-run ↵Morgan Deters
regression script
2010-10-04re-add a dependency to fix compile warningsMorgan Deters
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply ↵Morgan Deters
coding standards
2010-10-04Fix to bug 211. ArithVar is now typedefed to uint32_t.Tim King
2010-10-03file header documentation regenerated with contributors names; no code ↵Morgan Deters
modified in this commit
2010-10-02revert a workaround fix to CDMap that was committed as part of the ↵Morgan Deters
arith-indexed-vars merge, and fix the root cause (maybe?) in attribute.cpp: previously, items from the cdnodes attribute table weren't properly being "obliterated" from the table due to a typo
2010-10-02dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout...Morgan Deters
2010-10-02branches/arith-indexed-variables merged into the main trunk.Tim King
2010-10-01re-add no-deprecated to C sources; update some file-level documentation; ↵Morgan Deters
first look at cdvector for code review
2010-10-01last update broke the parser inadvertently, fixing...Morgan Deters
2010-10-01replacement implementation for clock_gettime() on mac os x, build ↵Morgan Deters
portability (resolving mac os x issues), code cleanup, fix compiler warnings
2010-09-30fixed a number of problems with mac os x builds. build now works on mac os ↵Morgan Deters
x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)
2010-09-28fix predicate bug in UF; code cleanup in theory.cppMorgan Deters
2010-09-28node iterator workMorgan Deters
2010-09-28fix pre-registration of operator, previously committed; clean up theory ↵Morgan Deters
engine code and unit test
2010-09-28fix unit test for kinded iterators in Node/TNodeMorgan Deters
2010-09-28fix TLS support for platforms (e.g. Mac OS X) where __thread storage class ↵Morgan Deters
doesn't exist, and clean up a few things in NodeManager
2010-09-28comment fix as per this morning's meeting; also, don't theory-rewrite ↵Morgan Deters
operators (resolves bug #198)
2010-09-27add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵ACSYS
also configure script auto-detection of __thread support and syntax
2010-09-27- This update adds DynamicArray<T>. This is a bare bones heap allocated ↵Tim King
array that dynamically can increase in size. This has functionality similar to vector<T>. The main difference is that it can be constructed in an ill-formed manner. This means that it can generalize CDList<T>. - CDVector<T> has been added. This is intended to allow for context-dependent destructive updates, while the vector size increases are permanent. Behaviorally, this is most similar to vector< CDO<T> >. The differences between the two are: only one ContextObj is registered to the Context, backtracks are done in a lazy fashion, CDVector::push_back(val) sets the value of back() at context level 0 to val where vector<CDO<T>>::push_back(val) sets back() at the current context level to val and back() at context level 0 to the default constructor T().
2010-09-24equality triggers for the equality engineDejan Jovanović
fixed order of destruction in smt_engine
2010-09-24roll back an unintended change with r900Morgan Deters
2010-09-24Fix build system for Mac OS X builds (resolves bug #203)Morgan Deters
2010-09-24basic union find for bitvectorsDejan Jovanović
2010-09-22Fixing NodeBuilderBlackChristopher L. Conway
2010-09-21Rm'ing automatic type check in NodeBuilder for vars/constantsChristopher L. Conway
2010-09-21remove assertion in TNode destructor and ensure all TNode methods check rc > ↵Morgan Deters
0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction
2010-09-21fix statistics-registry-related memory leaksMorgan Deters
2010-09-21part of review (bug #197): coding conventions, file-level documentation, ↵Morgan Deters
re-ran update-copyright.pl, etc.
2010-09-21svn:ignore properties for new bv stuffMorgan Deters
2010-09-21some code cleanup, documentation, review of "kinded-iterator" code, and ↵Morgan Deters
addition of a unit test
2010-09-21iterators for tim, begin<PLUS>() and end<PLUS>() should give him what he wantsDejan Jovanović
2010-09-21Rm'ing Makefile.in'sChristopher L. Conway
2010-09-21Moving automatic type check to NodeBuilder (Fixes: #199)Christopher L. Conway
2010-09-20hooking up the bitvector testsDejan Jovanović
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-09-16Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. ↵Tim King
test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default. Tiny documentation fix for the arithmetic normal form.
2010-09-14* added test/regress/regress0/arith for easy arithmetic regress tests.Tim King
2010-09-14ensure uf/congruence closure debugging stuff isn't called in production buildsMorgan Deters
2010-09-13make Node iterators more STL-friendly, resolves bug #196Morgan Deters
2010-09-13build system consistency in target names for unit test targetsMorgan Deters
2010-09-13statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is givenMorgan Deters
2010-09-13link TAGS file into builds/ directory, when built. Resolves bug #195Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
* src/theory/arith/normal_form.{h,cpp} contains the description for the new normal form as well as utilities for dealing with the normal form. * src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter. The new rewriter implements preRewrite() and postRewrite() for arithmetic. * src/theory/arith/arith_rewriter.{h,cpp} have been removed. * TheoryArith::rewrite() has been removed. * Arithmetic with the new normal form outperforms the trunk where the branch occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable difference.) Some important optimizations are stilling pending to the code for handling the new normal form. (Bug 196.)
2010-09-02"Leftist NodeBuilders" are now supported.Morgan Deters
That is, "nb << a << b << c << OR << d << AND" turns into (AND (OR a b c) d) The rule is: pushing a kind onto a NodeBuilder with a nonzero number of child Nodes in it, the action "collapses" it. If a kind is already associated to the NodeBuilder, it is an error. Thus: NodeBuilder<> nb(AND); nb << AND; and NodeBuilder<> nb; nb << AND << OR; are both errors (if assertions are on). In reality, though, the implementation is trickier, as the collapsing is done lazily on the following push. This complicates things a bit, but by placing an Assert(false), I found that we aren't depending on the old behavior (at least for any unit tests or regressions in the source tree). The Assert(false) is now removed and leftist NodeBuilders are in business. Fixes bug 101.
2010-09-02recategorize eq_diamond14 as a regress2 test (instead of regress0)Morgan Deters
2010-09-02fix an error in TimerStatMorgan Deters
2010-09-02neglected build system update from r848 (last commit)Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback