summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2010-10-09support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ↵Morgan Deters
define-fun; several set-info, set-option, get-option, get-info improvementss
2010-10-09bug fixes to model genMorgan Deters
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec, you must pass --interactive --produce-models on the command line (although they don't currently make us do any extra work). Closes bug #213.
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
(resolves bug #212) * also closed some other type checking loopholes in SmtEngine * small fixes to define-sort (resolves bug #214) * infrastructural support for printing expressions in languages other than the internal representation language using an IO manipulator, e.g.: cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr; main() sets the output language for all streams to correspond to the input language * support delaying type checking in debug builds, so that one can debug the type checker itself (before it was difficult, because debug builds did all the type checking on Node creation!): new command-line flag --no-early-type-checking (only makes sense for debug builds) * disallowed copy-construction of ExprManager and NodeManager, and made other constructors explicit; previously it was easy to unintentionally create duplicate managers, with really weird results (i.e., disappearing attributes!)
2010-10-08support (set-info) on status, source, category, difficulty, smt-lib-version, ↵Morgan Deters
and notes; reduces extraneous "unsupported" output
2010-10-07type checking for define-fun in production builds; related to (and might ↵Morgan Deters
resolve) bug 212
2010-10-07NodeSelfIterator implementation and unit test (resolves bug #204); also fix ↵Morgan Deters
ParserBlack unit test initialization
2010-10-07Small tableau optimization.Tim King
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at ↵Morgan Deters
preprocessing time
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ↵Morgan Deters
working (just need to decide where to expand)
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, ↵Morgan Deters
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
2010-10-04fix gdb issues (at least for static builds); resolves bug 194Morgan 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 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-24Fix build system for Mac OS X builds (resolves bug #203)Morgan Deters
2010-09-24basic union find for bitvectorsDejan Jovanović
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-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-21Moving automatic type check to NodeBuilder (Fixes: #199)Christopher L. Conway
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-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-13statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is givenMorgan 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-02fix an error in TimerStatMorgan Deters
2010-09-02* add TimerStat statistic typeMorgan Deters
* add Stats black-box unit test * new make target: "make units" now runs unit tests only * revised make target: "make regress" now runs regressions only * configure.ac: pull in librt for clock_gettime()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback