]> 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-06-11 trevor_hansenRemove no longer used bitblaster commit | commitdiff | tree | snapshot
2010-06-11 trevor_hansenRemove the experimental bvsolver. I've copied its chang... commit | commitdiff | tree | snapshot
2010-06-11 trevor_hansen* Make GetUnsignedConst a member function of ASTNode. commit | commitdiff | tree | snapshot
2010-06-11 trevor_hansenRefactoring. Move all the substitutionmap functions... commit | commitdiff | tree | snapshot
2010-06-11 trevor_hansenThis makes SimplifyTerm idempotent. My hope is that... commit | commitdiff | tree | snapshot
2010-06-11 trevor_hansenAdds a simplification rule to replace BVANDS with zeroe... commit | commitdiff | tree | snapshot
2010-06-09 trevor_hansenbugfix. Constraints were ignored when they should have... commit | commitdiff | tree | snapshot
2010-06-09 trevor_hansenBugfix. Recursively simplify array ITES. commit | commitdiff | tree | snapshot
2010-06-09 trevor_hansenAdd back code I removed in the last revision. Without... commit | commitdiff | tree | snapshot
2010-06-09 trevor_hansenBugfix. Simplify the proposition of array-ITEs. I don... commit | commitdiff | tree | snapshot
2010-06-09 trevor_hansen* In the bvsolver perform cheap tests which maybe short... commit | commitdiff | tree | snapshot
2010-06-08 trevor_hansenBugfix. Avoid creating cycles with the bvsolver. commit | commitdiff | tree | snapshot
2010-06-08 trevor_hansenBugfix. The bvsolver would replace a variable with... commit | commitdiff | tree | snapshot
2010-06-08 trevor_hansenCopy the cleaner new SplitEven_into_Oddnum_PowerOf2... commit | commitdiff | tree | snapshot
2010-06-04 msoosLast commit was wrong. Importing again CryptoMiniSat... commit | commitdiff | tree | snapshot
2010-06-04 msoosImporting CryptoMiniSat version 'Cluster56'. commit | commitdiff | tree | snapshot
2010-05-30 trevor_hansenFix the method to count the number of instances in... commit | commitdiff | tree | snapshot
2010-05-30 trevor_hansenSplit out the class which lazily builds the variables... commit | commitdiff | tree | snapshot
2010-05-30 trevor_hansenSmall speedup in the cnf generator. commit | commitdiff | tree | snapshot
2010-05-30 trevor_hansenAdd histar to regressall. We use far far too much memor... commit | commitdiff | tree | snapshot
2010-05-30 trevor_hansenMoving histar tests to the main test directory. commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansenAdd my experimental BVSolver. It's much slower than... commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansenEnable upfront simplifications of terms. commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansen* Make the constant evaluator a non member function... commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansenSimplifyin BVSX to CONCAT if the topmost bit of the... commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansen* Add a disabled-by-default option to simplify the... commit | commitdiff | tree | snapshot
2010-05-29 trevor_hansenAdd a simplification so that (ite(p,5,7) <= 8) is alway... commit | commitdiff | tree | snapshot
2010-05-28 trevor_hansenBugfix. If given bad input, the SMTLIB2 parser would... commit | commitdiff | tree | snapshot
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
next
STP Constraint Solver.