]> git.unchartedbackwaters.co.uk Git - francis/stp.git/shortlog
projects / francis / stp.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
francis/stp.git
2010-05-27 trevor_hansen* Improve the simplifications of inequalities and equal... commit | commitdiff | tree | snapshot
2010-05-26 trevor_hansenImplements booth recoding when bitblasting multiplication. commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansenAdd the "eric-tests" to regressall. commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansenbugfix. Allow distinct to be used for both formulae... commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansenThese scripts (though I don't know what they do) seem... commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansenBugfix. Rare types of array reads were causing a type... commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansen* Letize booleans when printing back smb2lib format. commit | commitdiff | tree | snapshot
2010-05-24 trevor_hansenRun tests with the .smt2 extension. commit | commitdiff | tree | snapshot
2010-05-23 trevor_hansenFix the memory leaks in the SMTLIB2 parser. commit | commitdiff | tree | snapshot
2010-05-23 trevor_hansen* fix reduce/reduce error in the smtlib2 format. commit | commitdiff | tree | snapshot
2010-05-23 trevor_hansenThe SMTLIB2 parser now accepts valid, but extremely... commit | commitdiff | tree | snapshot
2010-05-22 trevor_hansenFix the defintion of what a symbol is in the SMTLIB2... commit | commitdiff | tree | snapshot
2010-05-21 trevor_hansenUse the flex options recommended by its manual. commit | commitdiff | tree | snapshot
2010-05-21 trevor_hansen* Add binary & hexidecimal for smtlib2 format. commit | commitdiff | tree | snapshot
2010-05-21 trevor_hansenAn initial version of an smtlib2 format parser. It... commit | commitdiff | tree | snapshot
2010-05-21 trevor_hansen* The bvsmod operation can now be output by the printers. commit | commitdiff | tree | snapshot
2010-05-20 trevor_hansenFix the build by adding a missing function. commit | commitdiff | tree | snapshot
2010-05-19 trevor_hansenFix: lets, types, extends and extracts in the SMTLIB2... commit | commitdiff | tree | snapshot
2010-05-19 trevor_hansenThe SMT-LIB2 format changes names from "implies" to... commit | commitdiff | tree | snapshot
2010-05-18 trevor_hansenA first attempt at an SMT-LIB2 output printer. I haven... commit | commitdiff | tree | snapshot
2010-05-17 katelmanBOOLEXTRACT seems to have been implemented backward... commit | commitdiff | tree | snapshot
2010-05-15 trevor_hansen* Convert BVAND( ite(p,1,1) , ite(p2,0,1)) to ite(p... commit | commitdiff | tree | snapshot
2010-05-13 trevor_hansenDelete an unnecessary copy of c_interface.h, ammend... commit | commitdiff | tree | snapshot
2010-05-13 trevor_hansenRemove the code for the "ReferenceCount". This was... commit | commitdiff | tree | snapshot
2010-05-13 trevor_hansen* Use the simplifying node factory and the type checkin... commit | commitdiff | tree | snapshot
2010-05-12 trevor_hansenAdd an encoding of multiplication that explicitly uses... commit | commitdiff | tree | snapshot
2010-05-12 trevor_hansenFirst attempt at tracking time spent building the count... commit | commitdiff | tree | snapshot
2010-05-12 trevor_hansenFix 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_hansenWhen sending clauses to the SAT solver, create fewer... commit | commitdiff | tree | snapshot
2010-05-10 trevor_hansenRemove iterators from BBLShift to remove a spurious... commit | commitdiff | tree | snapshot
2010-05-07 vijay_ganeshAdded info to the INSTALL file about the various config... commit | commitdiff | tree | snapshot
2010-05-07 trevor_hansenSimplify the division operation. An unnecessary compari... commit | commitdiff | tree | snapshot
2010-05-06 vijay_ganeshfixed the problem with Alvin Cheung's testcase. The... commit | commitdiff | tree | snapshot
2010-05-06 trevor_hansenRefactoring. Take out some ASTNodes from the bitblaster. commit | commitdiff | tree | snapshot
2010-05-05 vijay_ganeshfixed the order in which the regressions are run. The... commit | commitdiff | tree | snapshot
2010-05-05 vijay_ganeshPerennial problem with svn. Does not give me the list... commit | commitdiff | tree | snapshot
2010-05-05 vijay_ganeshfixed TEST_PREFIX in Makefile.common. Ideally this... commit | commitdiff | tree | snapshot
2010-05-05 trevor_hansenSmall changes to the array transformer: commit | commitdiff | tree | snapshot
2010-05-05 trevor_hansenEnable counter example checking by default. commit | commitdiff | tree | snapshot
2010-05-02 trevor_hansenDon't test a22 in valgrind because it leaks commit | commitdiff | tree | snapshot
2010-04-30 msoosCMS2: Hyper-binary resolution was wrong. Removed. commit | commitdiff | tree | snapshot
2010-04-29 trevor_hansenApplying 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_hansenRemoving an .o file accidently checked in. commit | commitdiff | tree | snapshot
2010-04-28 trevor_hansenBugfix. Refactoring of ToCNF broke some ifdef CRYPTOMIN... commit | commitdiff | tree | snapshot
2010-04-28 msoosTurning on simplification&subpart-solving in CMS2 commit | commitdiff | tree | snapshot
2010-04-28 msoosUpdating CMS2 commit | commitdiff | tree | snapshot
2010-04-28 trevor_hansenRemove some unnecesarry memory churn. Extra objects... commit | commitdiff | tree | snapshot
2010-04-28 trevor_hansenRefactoring. This creates a separate ClauseList class... commit | commitdiff | tree | snapshot
2010-04-28 trevor_hansenMaking 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_hansenFix regressbio. I missed an 's' in its path commit | commitdiff | tree | snapshot
2010-04-26 trevor_hansenInclude the STP version in the regression log commit | commitdiff | tree | snapshot
2010-04-26 trevor_hansenAdd crypto and bio regression targets commit | commitdiff | tree | snapshot
2010-04-26 trevor_hansenUse 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_hansenFix the renameAllSiblings option in the CNF generator... commit | commitdiff | tree | snapshot
2010-04-25 trevor_hansenReverting r465. Based on Stephen's example: stp-tests... commit | commitdiff | tree | snapshot
2010-04-24 trevor_hansenFix leaks in the CVC parser commit | commitdiff | tree | snapshot
2010-04-24 trevor_hansenFix memory leaks in the SMT-LIB parser. commit | commitdiff | tree | snapshot
2010-04-22 msoosUpdating CMS2 to fix some bugs commit | commitdiff | tree | snapshot
2010-04-21 msoosUpdating CMS2 to correct destructor segfault commit | commitdiff | tree | snapshot
2010-04-19 msoosFixing CMS2's library debug routine commit | commitdiff | tree | snapshot
2010-04-19 msoosUpdating CMS2 to fix bug in Conglomerate.cpp commit | commitdiff | tree | snapshot
2010-04-19 msoosCMS2 update missed out on the MTL library changes.... commit | commitdiff | tree | snapshot
2010-04-18 msoosCMS2 now has two types of learnt clause evaluation commit | commitdiff | tree | snapshot
2010-04-16 msoosImporting new version of CMS2 commit | commitdiff | tree | snapshot
2010-04-16 msoosDon't clean non-existing CryptoMiniSat1 dir commit | commitdiff | tree | snapshot
2010-04-16 msoosRemoving CryptoMiniSat ver. 1 commit | commitdiff | tree | snapshot
2010-04-16 msoosMerge branch 'cryptominisat1_removed_and_rest_cleaned' commit | commitdiff | tree | snapshot
2010-04-16 msoosUpdating CMS2 to fix two bugs commit | commitdiff | tree | snapshot
2010-04-15 msoosCMS2 update: Extending the conglomerated clauses was... commit | commitdiff | tree | snapshot
2010-04-15 msoosLast commit contained some strange merging information... commit | commitdiff | tree | snapshot
2010-04-15 msoosMerge branch 'newcrypto' commit | commitdiff | tree | snapshot
2010-04-14 msoosImporting the new cryptominisat commit | commitdiff | tree | snapshot
2010-04-14 trevor_hansenbugfix. r671 re-enabled checking counter-examples.... commit | commitdiff | tree | snapshot
2010-04-14 trevor_hansenBugfix to r667. I discarded a variable instead of addin... commit | commitdiff | tree | snapshot
2010-04-14 trevor_hansenChange 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_hansenBugfix. r284 or earlier removed checking of counter... commit | commitdiff | tree | snapshot
2010-04-13 trevor_hansenIf STP is compiled with minisat-core, add a command... commit | commitdiff | tree | snapshot
2010-04-13 trevor_hansenRemove unsound-minisat as per Vijay's advice. commit | commitdiff | tree | snapshot
2010-04-12 smccamAdd configuration options for selecting SAT solver... commit | commitdiff | tree | snapshot
2010-04-05 trevor_hansenFix for failure reported by Alvin Cheung (r666) commit | commitdiff | tree | snapshot
2010-04-05 trevor_hansenDisable expensive "and"/"or" simplifications in the... commit | commitdiff | tree | snapshot
2010-04-05 trevor_hansenEnable the simplifying node factory when parsing smt... commit | commitdiff | tree | snapshot
2010-04-05 trevor_hansenThis 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 smccamSpecify default arguments only when compiling C++. commit | commitdiff | tree | snapshot
2010-03-30 smccamCall "make clean" *after* configure in clean-install... commit | commitdiff | tree | snapshot
2010-03-30 smccamRemove trailing comma at the end of an enumerator list... commit | commitdiff | tree | snapshot
2010-03-30 trevor_hansenFix the command line flag to output the bench format. commit | commitdiff | tree | snapshot
2010-03-24 vijay_ganeshadded a bunch of crypto examples to stp-tests/broken... commit | commitdiff | tree | snapshot
2010-03-24 vijay_ganeshadded more crypto tests to stp/tests/crypto-tests commit | commitdiff | tree | snapshot
2010-03-22 vijay_ganeshcommented out the mtrand initial seeding with time... commit | commitdiff | tree | snapshot
2010-03-22 vijay_ganeshadded new crypto tests, and perl-based crypto test... commit | commitdiff | tree | snapshot
2010-03-19 smccamAdd more destructors to the C interface, to help client... commit | commitdiff | tree | snapshot
next
STP Constraint Solver.