| 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 |
| 2010-07-08 |
Christopher... | Moving cluster-qf_lra-full to scripts project |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Moving cluster-qf_lra-benchmark to scripts project |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Adding missing operators in SMT2 parser: UMINUS, DIVISI... |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Fixing Array type in SMT v1.2 |
commit | commitdiff | tree |
| 2010-07-08 |
Tim King | I am adding my smt-crunch scripts to source control... |
commit | commitdiff | tree |
| 2010-07-08 |
Morgan Deters | context work to support cdmaps with elements allocated... |
commit | commitdiff | tree |
| 2010-07-08 |
Tim King | Updates to the post_mortem.py script. |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Shared term manager tested and working |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Making plus-mult.cvc test a bit more torturous (as... |
commit | commitdiff | tree |
| 2010-07-07 |
Tim King | Fixes arith rewriter to allow for division by a constan... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Fixing test plus-mult.cvc by making it linear (Fixes... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | minor changes to cdmap/cdset interface for detection... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | chris and i committed the same fix; reverting the ... |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Updated headers |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Disabling failing tests |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | add exit status to regression that was failing |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | some build system changes reverted after the CLN build... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | competition submission should be fully static |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | fixed submission target |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | things for competition upload: new "make submission... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Adding tests for precedence of arithmetic in CVC inputs |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Adding config.reconfig to .gitignore |
commit | commitdiff | tree |
| 2010-07-06 |
Tim King | Fixed exit status for competition mode. |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | Don't eagerly collect zombies. This should speed up... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | add Configuration::isCompetitionBuild() and some main... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | fix crash on command line parsing |
commit | commitdiff | tree |
| 2010-07-06 |
Clark Barrett | Moved registration to theory engine |
commit | commitdiff | tree |
| 2010-07-06 |
Christopher... | Adding Array types to SMT2 parser |
commit | commitdiff | tree |
| 2010-07-06 |
Christopher... | Adding arithmetic symbols to CVC parser (Fixes: #176) |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog