]> git.unchartedbackwaters.co.uk Git - francis/stp.git/shortlog
francis/stp.git
2010-05-24 trevor_hansenBugfix. Rare types of array reads were causing a type...
2010-05-24 trevor_hansen* Letize booleans when printing back smb2lib format.
2010-05-24 trevor_hansenRun tests with the .smt2 extension.
2010-05-23 trevor_hansenFix the memory leaks in the SMTLIB2 parser.
2010-05-23 trevor_hansen* fix reduce/reduce error in the smtlib2 format.
2010-05-23 trevor_hansenThe SMTLIB2 parser now accepts valid, but extremely...
2010-05-22 trevor_hansenFix the defintion of what a symbol is in the SMTLIB2...
2010-05-21 trevor_hansenUse the flex options recommended by its manual.
2010-05-21 trevor_hansen* Add binary & hexidecimal for smtlib2 format.
2010-05-21 trevor_hansenAn initial version of an smtlib2 format parser. It...
2010-05-21 trevor_hansen* The bvsmod operation can now be output by the printers.
2010-05-20 trevor_hansenFix the build by adding a missing function.
2010-05-19 trevor_hansenFix: lets, types, extends and extracts in the SMTLIB2...
2010-05-19 trevor_hansenThe SMT-LIB2 format changes names from "implies" to...
2010-05-18 trevor_hansenA first attempt at an SMT-LIB2 output printer. I haven...
2010-05-17 katelmanBOOLEXTRACT seems to have been implemented backward...
2010-05-15 trevor_hansen* Convert BVAND( ite(p,1,1) , ite(p2,0,1)) to ite(p...
2010-05-13 trevor_hansenDelete an unnecessary copy of c_interface.h, ammend...
2010-05-13 trevor_hansenRemove the code for the "ReferenceCount". This was...
2010-05-13 trevor_hansen* Use the simplifying node factory and the type checkin...
2010-05-12 trevor_hansenAdd an encoding of multiplication that explicitly uses...
2010-05-12 trevor_hansenFirst attempt at tracking time spent building the count...
2010-05-12 trevor_hansenFix the flattenOneLevel function as per r294
2010-05-12 trevor_hansen* Make the arguments to ==, !=, > for ASTNode reference...
2010-05-10 trevor_hansen* Fix the use of an invalidated iterator in the CVC...
2010-05-10 trevor_hansenWhen sending clauses to the SAT solver, create fewer...
2010-05-10 trevor_hansenRemove iterators from BBLShift to remove a spurious...
2010-05-07 vijay_ganeshAdded info to the INSTALL file about the various config...
2010-05-07 trevor_hansenSimplify the division operation. An unnecessary compari...
2010-05-06 vijay_ganeshfixed the problem with Alvin Cheung's testcase. The...
2010-05-06 trevor_hansenRefactoring. Take out some ASTNodes from the bitblaster.
2010-05-05 vijay_ganeshfixed the order in which the regressions are run. The...
2010-05-05 vijay_ganeshPerennial problem with svn. Does not give me the list...
2010-05-05 vijay_ganeshfixed TEST_PREFIX in Makefile.common. Ideally this...
2010-05-05 trevor_hansenSmall changes to the array transformer:
2010-05-05 trevor_hansenEnable counter example checking by default.
2010-05-02 trevor_hansenDon't test a22 in valgrind because it leaks
2010-04-30 msoosCMS2: Hyper-binary resolution was wrong. Removed.
2010-04-29 trevor_hansenApplying a patch provided by Hume to parse cvc and...
2010-04-29 trevor_hansen* Send the -t flag to STP when running regressstp....
2010-04-28 trevor_hansenRemoving an .o file accidently checked in.
2010-04-28 trevor_hansenBugfix. Refactoring of ToCNF broke some ifdef CRYPTOMIN...
2010-04-28 msoosTurning on simplification&subpart-solving in CMS2
2010-04-28 msoosUpdating CMS2
2010-04-28 trevor_hansenRemove some unnecesarry memory churn. Extra objects...
2010-04-28 trevor_hansenRefactoring. This creates a separate ClauseList class...
2010-04-28 trevor_hansenMaking some functions ASTNode memberfunctions
2010-04-27 trevor_hansen* Delete a test script that's no longer used
2010-04-27 trevor_hansenFix regressbio. I missed an 's' in its path
2010-04-26 trevor_hansenInclude the STP version in the regression log
2010-04-26 trevor_hansenAdd crypto and bio regression targets
2010-04-26 trevor_hansenUse gunzip so that we can run tests that are gzipped.
2010-04-26 trevor_hansen* Make regressall depend on "all". If any changes have...
2010-04-25 trevor_hansen* Reduce the number of scripts we use to run regression...
2010-04-25 trevor_hansenFix the renameAllSiblings option in the CNF generator...
2010-04-25 trevor_hansenReverting r465. Based on Stephen's example: stp-tests...
2010-04-24 trevor_hansenFix leaks in the CVC parser
2010-04-24 trevor_hansenFix memory leaks in the SMT-LIB parser.
2010-04-22 msoosUpdating CMS2 to fix some bugs
2010-04-21 msoosUpdating CMS2 to correct destructor segfault
2010-04-19 msoosFixing CMS2's library debug routine
2010-04-19 msoosUpdating CMS2 to fix bug in Conglomerate.cpp
2010-04-19 msoosCMS2 update missed out on the MTL library changes....
2010-04-18 msoosCMS2 now has two types of learnt clause evaluation
2010-04-16 msoosImporting new version of CMS2
2010-04-16 msoosDon't clean non-existing CryptoMiniSat1 dir
2010-04-16 msoosRemoving CryptoMiniSat ver. 1
2010-04-16 msoosMerge branch 'cryptominisat1_removed_and_rest_cleaned'
2010-04-16 msoosUpdating CMS2 to fix two bugs
2010-04-15 msoosCMS2 update: Extending the conglomerated clauses was...
2010-04-15 msoosLast commit contained some strange merging information...
2010-04-15 msoosMerge branch 'newcrypto'
2010-04-14 msoosImporting the new cryptominisat
2010-04-14 trevor_hansenbugfix. r671 re-enabled checking counter-examples....
2010-04-14 trevor_hansenBugfix to r667. I discarded a variable instead of addin...
2010-04-14 trevor_hansenChange a reference to a regular variable. This fixes...
2010-04-14 trevor_hansen* Bugfix. Fix the printed counterexample sometimes...
2010-04-14 trevor_hansenBugfix. r284 or earlier removed checking of counter...
2010-04-13 trevor_hansenIf STP is compiled with minisat-core, add a command...
2010-04-13 trevor_hansenRemove unsound-minisat as per Vijay's advice.
2010-04-12 smccamAdd configuration options for selecting SAT solver...
2010-04-05 trevor_hansenFix for failure reported by Alvin Cheung (r666)
2010-04-05 trevor_hansenDisable expensive "and"/"or" simplifications in the...
2010-04-05 trevor_hansenEnable the simplifying node factory when parsing smt...
2010-04-05 trevor_hansenThis fixes things I broke in r662:
2010-04-05 trevor_hansen* Rename let-funcs.cpp to LetMgr.cpp
2010-04-01 smccamSpecify default arguments only when compiling C++.
2010-03-30 smccamCall "make clean" *after* configure in clean-install...
2010-03-30 smccamRemove trailing comma at the end of an enumerator list...
2010-03-30 trevor_hansenFix the command line flag to output the bench format.
2010-03-24 vijay_ganeshadded a bunch of crypto examples to stp-tests/broken...
2010-03-24 vijay_ganeshadded more crypto tests to stp/tests/crypto-tests
2010-03-22 vijay_ganeshcommented out the mtrand initial seeding with time...
2010-03-22 vijay_ganeshadded new crypto tests, and perl-based crypto test...
2010-03-19 smccamAdd more destructors to the C interface, to help client...
2010-03-19 smccamExclude main/main.o from libstp.a.
2010-03-18 smccamOops, different fix for the same problem as r646. Actua...
2010-03-18 smccamRemove obsolete top-level svn:ignore entries: since...
2010-03-18 smccamUpdate svn:ignore properties with "depend" and more...
2010-03-18 trevor_hansenOutput flags for bench format, and a rough CNF.
next