| 2010-10-26 |
Morgan Deters | GetValueCommand now gives a TUPLE as output, with the... |
commit | commitdiff | tree |
| 2010-10-26 |
Christopher... | Cleaning up some header files |
commit | commitdiff | tree |
| 2010-10-26 |
Christopher... | Adding dependency info to README |
commit | commitdiff | tree |
| 2010-10-25 |
Morgan Deters | for static linking of driver binary, list libmain.a... |
commit | commitdiff | tree |
| 2010-10-25 |
Morgan Deters | missing case in expr output; resolves bug 226 |
commit | commitdiff | tree |
| 2010-10-24 |
Christopher... | Adding unit test for InteractiveShell |
commit | commitdiff | tree |
| 2010-10-24 |
Morgan Deters | add a CVC4_UNDEFINED keyword, for intentionally undefin... |
commit | commitdiff | tree |
| 2010-10-23 |
Tim King | Removed slack.h, and arith_activity.h. Replaced IsBasic... |
commit | commitdiff | tree |
| 2010-10-23 |
Christopher... | Adding Parser::setInput and using it in InteractiveShel... |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | removing unused functionality from util; related to... |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | fix valgrind-reported errors in parser builder; a non... |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Saving state between lines in interactive mode (Fixes... |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Using Options in ParserBuilder and InteractiveShell |
commit | commitdiff | tree |
| 2010-10-22 |
Christopher... | Merging main/getopt.cpp, main/usage.h, and smt/options... |
commit | commitdiff | tree |
| 2010-10-22 |
Tim King | Code cleanup for TheoryArith. |
commit | commitdiff | tree |
| 2010-10-22 |
Morgan Deters | comment out the "interactive" check in SmtEngine::getVa... |
commit | commitdiff | tree |
| 2010-10-22 |
Tim King | Fixes to getValue for TheoryArith. |
commit | commitdiff | tree |
| 2010-10-21 |
Christopher... | * Option --no-type-checking now disables type checks... |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Changing --no-early-type-checking to --no-type-checking |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Enabling semantic checks in ParserBuilder |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Adding detection of TTY vs. piped input for interactive... |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Fixing minor whitespace bug in the parser |
commit | commitdiff | tree |
| 2010-10-20 |
Christopher... | Adding support for interactive mode |
commit | commitdiff | tree |
| 2010-10-20 |
Morgan Deters | fix bug #220 (assertion fails if no query/check-sat... |
commit | commitdiff | tree |
| 2010-10-14 |
Tim King | Fixed computation of infinitesimals for arithmetic... |
commit | commitdiff | tree |
| 2010-10-13 |
Tim King | Removed vector<Monomial> monos from Polynomial. Now... |
commit | commitdiff | tree |
| 2010-10-13 |
Tim King | Added test/regress/regress1/arith and populated it... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | with --stats, statistics are dumped for memouts and... |
commit | commitdiff | tree |
| 2010-10-12 |
Tim King | IDENTITY has been removed. |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | minor unit test fix-ups |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | fix debugPrintNode(), debugPrintTNode(), debugPrintNode... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | fix some leaks in parser, add debug code to node manage... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | hooked up "we are incomplete" flag after conversation... |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | Merge from cc-memout branch. Here are the main points |
commit | commitdiff | tree |
| 2010-10-12 |
Morgan Deters | check last result in (get-assignment); some context... |
commit | commitdiff | tree |
| 2010-10-11 |
Morgan Deters | use "forward" headers |
commit | commitdiff | tree |
| 2010-10-10 |
Morgan Deters | additional model gen and SMT-LIBv2 compliance work... |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | reverting some changes to parser from last commit |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | support for SMT-LIBv2 :named attributes, and attributes... |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | fix to unit tests |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | bug fixes to model gen |
commit | commitdiff | tree |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
commit | commitdiff | tree |
| 2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
commit | commitdiff | tree |
| 2010-10-08 |
Morgan Deters | support (set-info) on status, source, category, difficu... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | oops, reverting a change to a regression test that... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | NodeSelfIterator implementation and unit test (resolves... |
commit | commitdiff | tree |
| 2010-10-07 |
Tim King | Small tableau optimization. |
commit | commitdiff | tree |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
commit | commitdiff | tree |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
commit | commitdiff | tree |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fix gdb issues (at least for static builds); resolves... |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fix regular expressions in build system |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | fixing CLN builds, which had broken the build tonight... |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | re-add a dependency to fix compile warnings |
commit | commitdiff | tree |
| 2010-10-04 |
Morgan Deters | remove/shuffle some #include dependencies; fix some... |
commit | commitdiff | tree |
| 2010-10-04 |
Tim King | Fix to bug 211. ArithVar is now typedefed to uint32_t. |
commit | commitdiff | tree |
| 2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
commit | commitdiff | tree |
| 2010-10-02 |
Morgan Deters | revert a workaround fix to CDMap that was committed... |
commit | commitdiff | tree |
| 2010-10-02 |
Morgan Deters | dump statistics on abnormal output: unexpected exceptio... |
commit | commitdiff | tree |
| 2010-10-02 |
Tim King | branches/arith-indexed-variables merged into the main... |
commit | commitdiff | tree |
| 2010-10-01 |
Morgan Deters | re-add no-deprecated to C sources; update some file... |
commit | commitdiff | tree |
| 2010-10-01 |
Morgan Deters | last update broke the parser inadvertently, fixing... |
commit | commitdiff | tree |
| 2010-10-01 |
Morgan Deters | replacement implementation for clock_gettime() on mac... |
commit | commitdiff | tree |
| 2010-09-30 |
Morgan Deters | fixed a number of problems with mac os x builds. build... |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | fix predicate bug in UF; code cleanup in theory.cpp |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | node iterator work |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | fix pre-registration of operator, previously committed... |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | fix unit test for kinded iterators in Node/TNode |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | fix TLS support for platforms (e.g. Mac OS X) where... |
commit | commitdiff | tree |
| 2010-09-28 |
Morgan Deters | comment fix as per this morning's meeting; also, don... |
commit | commitdiff | tree |
| 2010-09-27 |
ACSYS | add workaround for systems (i.e., Mac OS X) that don... |
commit | commitdiff | tree |
| 2010-09-27 |
Tim King | - This update adds DynamicArray<T>. This is a bare... |
commit | commitdiff | tree |
| 2010-09-24 |
Dejan Jovanović | equality triggers for the equality engine |
commit | commitdiff | tree |
| 2010-09-24 |
Morgan Deters | roll back an unintended change with r900 |
commit | commitdiff | tree |
| 2010-09-24 |
Morgan Deters | Fix build system for Mac OS X builds (resolves bug... |
commit | commitdiff | tree |
| 2010-09-24 |
Dejan Jovanović | basic union find for bitvectors |
commit | commitdiff | tree |
| 2010-09-22 |
Christopher... | Fixing NodeBuilderBlack |
commit | commitdiff | tree |
| 2010-09-21 |
Christopher... | Rm'ing automatic type check in NodeBuilder for vars... |
commit | commitdiff | tree |
| 2010-09-21 |
Morgan Deters | remove assertion in TNode destructor and ensure all... |
commit | commitdiff | tree |
| 2010-09-21 |
Morgan Deters | fix statistics-registry-related memory leaks |
commit | commitdiff | tree |
| 2010-09-21 |
Morgan Deters | part of review (bug #197): coding conventions, file... |
commit | commitdiff | tree |
| 2010-09-21 |
Morgan Deters | svn:ignore properties for new bv stuff |
commit | commitdiff | tree |
| 2010-09-21 |
Morgan Deters | some code cleanup, documentation, review of "kinded... |
commit | commitdiff | tree |
| 2010-09-21 |
Dejan Jovanović | iterators for tim, begin<PLUS>() and end<PLUS>() should... |
commit | commitdiff | tree |
| 2010-09-21 |
Christopher... | Rm'ing Makefile.in's |
commit | commitdiff | tree |
| 2010-09-21 |
Christopher... | Moving automatic type check to NodeBuilder (Fixes:... |
commit | commitdiff | tree |
| 2010-09-20 |
Dejan Jovanović | hooking up the bitvector tests |
commit | commitdiff | tree |
| 2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases |
commit | commitdiff | tree |
| 2010-09-16 |
Tim King | Bug fix to CVC4::theory::arith::VarList as well as... |
commit | commitdiff | tree |
| 2010-09-14 |
Tim King | * added test/regress/regress0/arith for easy arithmetic... |
commit | commitdiff | tree |
| 2010-09-14 |
Morgan Deters | ensure uf/congruence closure debugging stuff isn't... |
commit | commitdiff | tree |
| 2010-09-13 |
Morgan Deters | make Node iterators more STL-friendly, resolves bug... |
commit | commitdiff | tree |
| 2010-09-13 |
Morgan Deters | build system consistency in target names for unit test... |
commit | commitdiff | tree |
| 2010-09-13 |
Morgan Deters | statistics are now printed on timeout (SIGXCPU) and... |
commit | commitdiff | tree |
| 2010-09-13 |
Morgan Deters | link TAGS file into builds/ directory, when built.... |
commit | commitdiff | tree |
| 2010-09-13 |
Tim King | * New normal form for arithmetic is in place. |
commit | commitdiff | tree |
| 2010-09-02 |
Morgan Deters | "Leftist NodeBuilders" are now supported. |
commit | commitdiff | tree |
| 2010-09-02 |
Morgan Deters | recategorize eq_diamond14 as a regress2 test (instead... |
commit | commitdiff | tree |
| 2010-09-02 |
Morgan Deters | fix an error in TimerStat |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog