| 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 |
| 2010-02-28 |
trevor_hansen | Testcase and temporary bugfix for an interface problem... |
commit | commitdiff | tree | snapshot |
| 2010-02-25 |
trevor_hansen | Updates to the "bench" printer. |
commit | commitdiff | tree | snapshot |
| 2010-02-22 |
trevor_hansen | * The bench printer prints out bitblasted formula which... |
commit | commitdiff | tree | snapshot |
| 2010-02-13 |
trevor_hansen | Bugfix. Bitblasting failed when a BVSX didn't increase... |
commit | commitdiff | tree | snapshot |
| 2010-02-04 |
trevor_hansen | Apply patch to fix Macos compilation provided by Mieszk... |
commit | commitdiff | tree | snapshot |
| 2010-02-01 |
trevor_hansen | NodeFactory classes that are used to build functions... |
commit | commitdiff | tree | snapshot |
| 2010-01-21 |
vijay_ganesh | fixed an important problem with YACC STACK DEPTH. It... |
commit | commitdiff | tree | snapshot |
| 2010-01-20 |
trevor_hansen | Bugfix. revision 558 broke all the solvers except for... |
commit | commitdiff | tree | snapshot |
| 2010-01-18 |
trevor_hansen | Bugfix. revision 556 broke cryptominisat. If cryptomini... |
commit | commitdiff | tree | snapshot |
| 2010-01-18 |
trevor_hansen | Fix some leaks |
commit | commitdiff | tree | snapshot |
| 2010-01-11 |
trevor_hansen | Bugfix. Simplifying minisat not setting a return code... |
commit | commitdiff | tree | snapshot |
| 2010-01-10 |
vijay_ganesh | BitBlast.cpp: Was generating XOR-clauses by default... |
commit | commitdiff | tree | snapshot |
| 2010-01-09 |
vijay_ganesh | minor modification to Makefile.common to isolate some... |
commit | commitdiff | tree | snapshot |
| 2010-01-07 |
xiw | avoid UINT32_MAX redefinition warning |
commit | commitdiff | tree | snapshot |
| 2009-12-25 |
msoos | Updating CMS2 to r686 |
commit | commitdiff | tree | snapshot |
| 2009-12-24 |
msoos | Updating to CMS2 r 685, fixing some bugs and doing... |
commit | commitdiff | tree | snapshot |
| 2009-12-22 |
msoos | Updating CMS2 to r681, fixing multiple bugs, and adding... |
commit | commitdiff | tree | snapshot |
| 2009-12-16 |
msoos | Updating CryptoMiniSat2 to r656 |
commit | commitdiff | tree | snapshot |
| 2009-12-16 |
trevor_hansen | Fix simplifying minisat. Previously when the SIMP flag... |
commit | commitdiff | tree | snapshot |
| 2009-12-11 |
vijay_ganesh | accidental Makefile.common commit |
commit | commitdiff | tree | snapshot |
| 2009-12-11 |
vijay_ganesh | branched STP into a programmable branch. Add programmab... |
commit | commitdiff | tree | snapshot |
| 2009-12-11 |
vijay_ganesh | fixed erroneous checkin. reverted NOT functionality... |
commit | commitdiff | tree | snapshot |
| 2009-12-11 |
vijay_ganesh | converting NOT(a) into XOR(a, true). Helps with bio... |
commit | commitdiff | tree | snapshot |
| 2009-12-10 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-10 |
vijay_ganesh | added some relatively hard bio examples |
commit | commitdiff | tree | snapshot |
| 2009-12-10 |
vijay_ganesh | Set RenameAllSibs Flag to false. It was slowing down bio |
commit | commitdiff | tree | snapshot |
| 2009-12-10 |
vijay_ganesh | made -fPIC and -march=native optional |
commit | commitdiff | tree | snapshot |
| 2009-12-10 |
msoos | Updating CryptoMiniSat2 to r614. dynamicRestart is... |
commit | commitdiff | tree | snapshot |
| 2009-12-09 |
vijay_ganesh | added SAT verbosity to statistics option |
commit | commitdiff | tree | snapshot |
| 2009-12-09 |
vijay_ganesh | added -fPIC flag for Java programs that want to use... |
commit | commitdiff | tree | snapshot |
| 2009-12-09 |
vijay_ganesh | fixed the bug in CNF translation that caused test000013... |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | good options of CMS2 set |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | fixed compile error on MacOS X |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | clausal bucketing back in business |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | completely got rid of abs-refine at boolean clausal... |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | fixed a small bug in cryptominisat2 |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
msoos | Updating CryptoMiniSat to r594. dynamicRestarts is... |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | minor edits |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | completed the cnf dumping feature. it works |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | added cnf dumping facility |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-08 |
msoos | Updating CryptoMiniSat to r586. Need to call 'void... |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
msoos | Updating CryptoMiniSat to r579, fixing a small bug... |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | XOR output for ITE |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
msoos | Updating CryptoMiniSat2 to r577 |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | added a regression script for synthesis tests |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
msoos | Updating CryptoMiniSat to r565. Should solve the proble... |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | minor edit |
commit | commitdiff | tree | snapshot |
| 2009-12-07 |
vijay_ganesh | cryptominisat2 is now the official SAT solver of STP |
commit | commitdiff | tree | snapshot |
| 2009-12-06 |
vijay_ganesh | added option to that allows STP to give randomized... |
commit | commitdiff | tree | snapshot |
| 2009-12-06 |
msoos | Updating CryptoMiniSat to SVN r561, fixing a log of... |
commit | commitdiff | tree | snapshot |
| 2009-12-05 |
vijay_ganesh | changed the way BVDIV is bitblasted |
commit | commitdiff | tree | snapshot |
| next |
projects / francis / stp.git / shortlog