| 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 |
| 2010-09-02 |
Morgan Deters | neglected build system update from r848 (last commit) |
commit | commitdiff | tree |
| 2010-09-02 |
Morgan Deters | * add TimerStat statistic type |
commit | commitdiff | tree |
| 2010-09-01 |
Morgan Deters | "make check" now places binaries in the proper place... |
commit | commitdiff | tree |
| 2010-09-01 |
Morgan Deters | reflect in build strings that -gmp is now the default... |
commit | commitdiff | tree |
| 2010-09-01 |
Morgan Deters | added documentation, closes bug 97 |
commit | commitdiff | tree |
| 2010-08-24 |
Christopher... | Making GMP default, CLN opt-in with --with-cln |
commit | commitdiff | tree |
| 2010-08-20 |
Dejan Jovanović | updating the minisat restart parameters after running... |
commit | commitdiff | tree |
| 2010-08-20 |
Morgan Deters | turn off extra-checking (which does extra theory-rewrit... |
commit | commitdiff | tree |
| 2010-08-19 |
Morgan Deters | UF theory bug fixes, code cleanup, and extra debugging... |
commit | commitdiff | tree |
| 2010-08-18 |
Morgan Deters | more tests, configuration for UF |
commit | commitdiff | tree |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
commit | commitdiff | tree |
| 2010-08-17 |
Morgan Deters | Add "no trash" CDMap elements, so that CDMap elements... |
commit | commitdiff | tree |
| 2010-08-17 |
Morgan Deters | Change TheoryEngine to use pointers to theories instead of |
commit | commitdiff | tree |
| 2010-08-16 |
Morgan Deters | add zlib checks to configure (new minisat requires... |
commit | commitdiff | tree |
| 2010-08-16 |
Dejan Jovanović | Fixing failures in minisat |
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | renaming minisat .C to .cc |
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | Adding the changes to the original copy |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Importing MiniSat2 070721 into trunk |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Removing newer version of MiniSat for Dejan's preferred... |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Importing MiniSat2 2.2.0 into trunk |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Removing old version of MiniSat for proper vendor import |
commit | commitdiff | tree |
| 2010-07-29 |
Christopher... | Adding configuration_private.h to allow inlining of... |
commit | commitdiff | tree |
| 2010-07-29 |
Morgan Deters | fix TheoryEngineWhite, add documentation; related to... |
commit | commitdiff | tree |
| 2010-07-28 |
Christopher... | Adding TypeCheckingException to throws clause in SMT... |
commit | commitdiff | tree |
| 2010-07-28 |
Christopher... | Forcing a type check on Node construction in debug... |
commit | commitdiff | tree |
| 2010-07-28 |
Morgan Deters | fixed theory engine white test for new (old) theoryOf... |
commit | commitdiff | tree |
| 2010-07-27 |
Christopher... | Moving EQ->IFF handling from TheoryEngine to parser... |
commit | commitdiff | tree |
| 2010-07-27 |
Christopher... | Adding optional 'check' parameter to getType() methods |
commit | commitdiff | tree |
| 2010-07-22 |
Morgan Deters | incorporate a fix from smtcomp2010 version for handling... |
commit | commitdiff | tree |
| 2010-07-22 |
Tim King | Added test file for fuzzsmt bug, bug187.smt2. |
commit | commitdiff | tree |
| 2010-07-10 |
Morgan Deters | add >, <=, and >= comparisons for Exprs and Nodes |
commit | commitdiff | tree |
| 2010-07-10 |
Dejan Jovanović | Fix for the type in sat propagation. |
commit | commitdiff | tree |
| 2010-07-09 |
Dejan Jovanović | the tableaux optimization |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog