| 2010-05-12 |
trevor_hansen | Add an encoding of multiplication that explicitly uses... |
commit | commitdiff | tree | snapshot |
| 2010-05-12 |
trevor_hansen | First attempt at tracking time spent building the count... |
commit | commitdiff | tree | snapshot |
| 2010-05-12 |
trevor_hansen | Fix the flattenOneLevel function as per r294 |
commit | commitdiff | tree | snapshot |
| 2010-05-12 |
trevor_hansen | * Make the arguments to ==, !=, > for ASTNode reference... |
commit | commitdiff | tree | snapshot |
| 2010-05-10 |
trevor_hansen | * Fix the use of an invalidated iterator in the CVC... |
commit | commitdiff | tree | snapshot |
| 2010-05-10 |
trevor_hansen | When sending clauses to the SAT solver, create fewer... |
commit | commitdiff | tree | snapshot |
| 2010-05-10 |
trevor_hansen | Remove iterators from BBLShift to remove a spurious... |
commit | commitdiff | tree | snapshot |
| 2010-05-07 |
vijay_ganesh | Added info to the INSTALL file about the various config... |
commit | commitdiff | tree | snapshot |
| 2010-05-07 |
trevor_hansen | Simplify the division operation. An unnecessary compari... |
commit | commitdiff | tree | snapshot |
| 2010-05-06 |
vijay_ganesh | fixed the problem with Alvin Cheung's testcase. The... |
commit | commitdiff | tree | snapshot |
| 2010-05-06 |
trevor_hansen | Refactoring. Take out some ASTNodes from the bitblaster. |
commit | commitdiff | tree | snapshot |
| 2010-05-05 |
vijay_ganesh | fixed the order in which the regressions are run. The... |
commit | commitdiff | tree | snapshot |
| 2010-05-05 |
vijay_ganesh | Perennial problem with svn. Does not give me the list... |
commit | commitdiff | tree | snapshot |
| 2010-05-05 |
vijay_ganesh | fixed TEST_PREFIX in Makefile.common. Ideally this... |
commit | commitdiff | tree | snapshot |
| 2010-05-05 |
trevor_hansen | Small changes to the array transformer: |
commit | commitdiff | tree | snapshot |
| 2010-05-05 |
trevor_hansen | Enable counter example checking by default. |
commit | commitdiff | tree | snapshot |
| 2010-05-02 |
trevor_hansen | Don't test a22 in valgrind because it leaks |
commit | commitdiff | tree | snapshot |
| 2010-04-30 |
msoos | CMS2: Hyper-binary resolution was wrong. Removed. |
commit | commitdiff | tree | snapshot |
| 2010-04-29 |
trevor_hansen | Applying a patch provided by Hume to parse cvc and... |
commit | commitdiff | tree | snapshot |
| 2010-04-29 |
trevor_hansen | * Send the -t flag to STP when running regressstp.... |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
trevor_hansen | Removing an .o file accidently checked in. |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
trevor_hansen | Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMIN... |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
msoos | Turning on simplification&subpart-solving in CMS2 |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
msoos | Updating CMS2 |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
trevor_hansen | Remove some unnecesarry memory churn. Extra objects... |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
trevor_hansen | Refactoring. This creates a separate ClauseList class... |
commit | commitdiff | tree | snapshot |
| 2010-04-28 |
trevor_hansen | Making some functions ASTNode memberfunctions |
commit | commitdiff | tree | snapshot |
| 2010-04-27 |
trevor_hansen | * Delete a test script that's no longer used |
commit | commitdiff | tree | snapshot |
| 2010-04-27 |
trevor_hansen | Fix regressbio. I missed an 's' in its path |
commit | commitdiff | tree | snapshot |
| 2010-04-26 |
trevor_hansen | Include the STP version in the regression log |
commit | commitdiff | tree | snapshot |
| 2010-04-26 |
trevor_hansen | Add crypto and bio regression targets |
commit | commitdiff | tree | snapshot |
| 2010-04-26 |
trevor_hansen | Use gunzip so that we can run tests that are gzipped. |
commit | commitdiff | tree | snapshot |
| 2010-04-26 |
trevor_hansen | * Make regressall depend on "all". If any changes have... |
commit | commitdiff | tree | snapshot |
| 2010-04-25 |
trevor_hansen | * Reduce the number of scripts we use to run regression... |
commit | commitdiff | tree | snapshot |
| 2010-04-25 |
trevor_hansen | Fix the renameAllSiblings option in the CNF generator... |
commit | commitdiff | tree | snapshot |
| 2010-04-25 |
trevor_hansen | Reverting r465. Based on Stephen's example: stp-tests... |
commit | commitdiff | tree | snapshot |
| 2010-04-24 |
trevor_hansen | Fix leaks in the CVC parser |
commit | commitdiff | tree | snapshot |
| 2010-04-24 |
trevor_hansen | Fix memory leaks in the SMT-LIB parser. |
commit | commitdiff | tree | snapshot |
| 2010-04-22 |
msoos | Updating CMS2 to fix some bugs |
commit | commitdiff | tree | snapshot |
| 2010-04-21 |
msoos | Updating CMS2 to correct destructor segfault |
commit | commitdiff | tree | snapshot |
| 2010-04-19 |
msoos | Fixing CMS2's library debug routine |
commit | commitdiff | tree | snapshot |
| 2010-04-19 |
msoos | Updating CMS2 to fix bug in Conglomerate.cpp |
commit | commitdiff | tree | snapshot |
| 2010-04-19 |
msoos | CMS2 update missed out on the MTL library changes.... |
commit | commitdiff | tree | snapshot |
| 2010-04-18 |
msoos | CMS2 now has two types of learnt clause evaluation |
commit | commitdiff | tree | snapshot |
| 2010-04-16 |
msoos | Importing new version of CMS2 |
commit | commitdiff | tree | snapshot |
| 2010-04-16 |
msoos | Don't clean non-existing CryptoMiniSat1 dir |
commit | commitdiff | tree | snapshot |
| 2010-04-16 |
msoos | Removing CryptoMiniSat ver. 1 |
commit | commitdiff | tree | snapshot |
| 2010-04-16 |
msoos | Merge branch 'cryptominisat1_removed_and_rest_cleaned' |
commit | commitdiff | tree | snapshot |
| 2010-04-16 |
msoos | Updating CMS2 to fix two bugs |
commit | commitdiff | tree | snapshot |
| 2010-04-15 |
msoos | CMS2 update: Extending the conglomerated clauses was... |
commit | commitdiff | tree | snapshot |
| 2010-04-15 |
msoos | Last commit contained some strange merging information... |
commit | commitdiff | tree | snapshot |
| 2010-04-15 |
msoos | Merge branch 'newcrypto' |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
msoos | Importing the new cryptominisat |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
trevor_hansen | bugfix. r671 re-enabled checking counter-examples.... |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
trevor_hansen | Bugfix to r667. I discarded a variable instead of addin... |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
trevor_hansen | Change a reference to a regular variable. This fixes... |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
trevor_hansen | * Bugfix. Fix the printed counterexample sometimes... |
commit | commitdiff | tree | snapshot |
| 2010-04-14 |
trevor_hansen | Bugfix. r284 or earlier removed checking of counter... |
commit | commitdiff | tree | snapshot |
| 2010-04-13 |
trevor_hansen | If STP is compiled with minisat-core, add a command... |
commit | commitdiff | tree | snapshot |
| 2010-04-13 |
trevor_hansen | Remove unsound-minisat as per Vijay's advice. |
commit | commitdiff | tree | snapshot |
| 2010-04-12 |
smccam | Add configuration options for selecting SAT solver... |
commit | commitdiff | tree | snapshot |
| 2010-04-05 |
trevor_hansen | Fix for failure reported by Alvin Cheung (r666) |
commit | commitdiff | tree | snapshot |
| 2010-04-05 |
trevor_hansen | Disable expensive "and"/"or" simplifications in the... |
commit | commitdiff | tree | snapshot |
| 2010-04-05 |
trevor_hansen | Enable the simplifying node factory when parsing smt... |
commit | commitdiff | tree | snapshot |
| 2010-04-05 |
trevor_hansen | This fixes things I broke in r662: |
commit | commitdiff | tree | snapshot |
| 2010-04-05 |
trevor_hansen | * Rename let-funcs.cpp to LetMgr.cpp |
commit | commitdiff | tree | snapshot |
| 2010-04-01 |
smccam | Specify default arguments only when compiling C++. |
commit | commitdiff | tree | snapshot |
| 2010-03-30 |
smccam | Call "make clean" *after* configure in clean-install... |
commit | commitdiff | tree | snapshot |
| 2010-03-30 |
smccam | Remove trailing comma at the end of an enumerator list... |
commit | commitdiff | tree | snapshot |
| 2010-03-30 |
trevor_hansen | Fix the command line flag to output the bench format. |
commit | commitdiff | tree | snapshot |
| 2010-03-24 |
vijay_ganesh | added a bunch of crypto examples to stp-tests/broken... |
commit | commitdiff | tree | snapshot |
| 2010-03-24 |
vijay_ganesh | added more crypto tests to stp/tests/crypto-tests |
commit | commitdiff | tree | snapshot |
| 2010-03-22 |
vijay_ganesh | commented out the mtrand initial seeding with time... |
commit | commitdiff | tree | snapshot |
| 2010-03-22 |
vijay_ganesh | added new crypto tests, and perl-based crypto test... |
commit | commitdiff | tree | snapshot |
| 2010-03-19 |
smccam | Add more destructors to the C interface, to help client... |
commit | commitdiff | tree | snapshot |
| 2010-03-19 |
smccam | Exclude main/main.o from libstp.a. |
commit | commitdiff | tree | snapshot |
| 2010-03-18 |
smccam | Oops, different fix for the same problem as r646. Actua... |
commit | commitdiff | tree | snapshot |
| 2010-03-18 |
smccam | Remove obsolete top-level svn:ignore entries: since... |
commit | commitdiff | tree | snapshot |
| 2010-03-18 |
smccam | Update svn:ignore properties with "depend" and more... |
commit | commitdiff | tree | snapshot |
| 2010-03-18 |
trevor_hansen | Output flags for bench format, and a rough CNF. |
commit | commitdiff | tree | snapshot |
| 2010-03-17 |
trevor_hansen | When outputting to SMTLIB format handle properly some... |
commit | commitdiff | tree | snapshot |
| 2010-03-14 |
trevor_hansen | * When printing in CVC format, traverse the nodes looki... |
commit | commitdiff | tree | snapshot |
| 2010-03-13 |
trevor_hansen | * Mark some single argument functions as commutative. |
commit | commitdiff | tree | snapshot |
| 2010-03-13 |
trevor_hansen | Cleanup after better after the lexer. |
commit | commitdiff | tree | snapshot |
| 2010-03-13 |
trevor_hansen | Add command line arguments to print back gdl,dot,cvc... |
commit | commitdiff | tree | snapshot |
| 2010-03-13 |
trevor_hansen | Fix the DIMACS CNF header |
commit | commitdiff | tree | snapshot |
| 2010-03-10 |
trevor_hansen | * Fix the SMT-LIB format printer so that it produces... |
commit | commitdiff | tree | snapshot |
| 2010-03-09 |
trevor_hansen | Allow lefshift by zero. |
commit | commitdiff | tree | snapshot |
| 2010-03-09 |
trevor_hansen | Bugfix. Rightshift in CVC was broken. Thanks to Elnatan... |
commit | commitdiff | tree | snapshot |
| 2010-03-07 |
trevor_hansen | Deleting the contents of the clause list before SAT... |
commit | commitdiff | tree | snapshot |
| 2010-03-07 |
trevor_hansen | Clear the contents of the BBTermMemo and BBFormMemo... |
commit | commitdiff | tree | snapshot |
| 2010-03-07 |
trevor_hansen | Removing unused inputs to the ToSAT class. |
commit | commitdiff | tree | snapshot |
| 2010-03-07 |
trevor_hansen | Cosmetic changes. |
commit | commitdiff | tree | snapshot |
| 2010-03-07 |
trevor_hansen | Fixing build. My last checkin forgot to add building... |
commit | commitdiff | tree | snapshot |
| 2010-03-06 |
trevor_hansen | Add the parts of the ABC system for sequential synthesi... |
commit | commitdiff | tree | snapshot |
| 2010-03-02 |
trevor_hansen | * When outputting runtimes with the -t flag, omit anyth... |
commit | commitdiff | tree | snapshot |
| 2010-03-02 |
trevor_hansen | * Merged in all the changes made to the bitblaster... |
commit | commitdiff | tree | snapshot |
| 2010-03-01 |
trevor_hansen | First step of integrating Bitblasting to AIGs. |
commit | commitdiff | tree | snapshot |
| 2010-02-28 |
trevor_hansen | Adding nodefactory classes to libstp so that libast... |
commit | commitdiff | tree | snapshot |
| 2010-02-28 |
trevor_hansen | Adding in test 21 to all. |
commit | commitdiff | tree | snapshot |
| next |
projects / francis / stp.git / shortlog