]> 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-07-02 msoosUpdating CryptoMiniSat2 commit | commitdiff | tree | snapshot
2010-07-02 trevor_hansenRename the bitblaster class fron BitBlasterNew to BitBl... commit | commitdiff | tree | snapshot
2010-07-01 trevor_hansenRefactor, getting ready for AIGs. This does add additio... commit | commitdiff | tree | snapshot
2010-06-29 trevor_hansenSpeedup. Generate nicer circuits for unsigned division. commit | commitdiff | tree | snapshot
2010-06-28 trevor_hansenChange how the counter example is built. Previously... commit | commitdiff | tree | snapshot
2010-06-28 trevor_hansenSpeedup. Add solving for xors to the bitvector solver. commit | commitdiff | tree | snapshot
2010-06-28 trevor_hansenSpeedup. if (xor a b) is found, replaced a with (not... commit | commitdiff | tree | snapshot
2010-06-27 trevor_hansenSpeedup. Sort EQ nodes. This prevents duplicate nodes... commit | commitdiff | tree | snapshot
2010-06-27 trevor_hansenSpeedup. Don't push extracts through ites. Sometimes... commit | commitdiff | tree | snapshot
2010-06-27 trevor_hansenDefault to bash shell rather than sh for some calls... commit | commitdiff | tree | snapshot
2010-06-27 trevor_hansenSpeedup. Revert back to minisat's default parameters. commit | commitdiff | tree | snapshot
2010-06-27 trevor_hansenSpeedup. Flatten ands at the start of the bvsolver. commit | commitdiff | tree | snapshot
2010-06-26 trevor_hansenclean up two regression log names commit | commitdiff | tree | snapshot
2010-06-26 trevor_hansenSpeedups. commit | commitdiff | tree | snapshot
2010-06-26 trevor_hansenSpeedups. commit | commitdiff | tree | snapshot
2010-06-25 trevor_hansenSpeedups. commit | commitdiff | tree | snapshot
2010-06-25 trevor_hansenMeasure the difficulty of formula by using a simple... commit | commitdiff | tree | snapshot
2010-06-25 trevor_hansenUse the new method to determine whether the sub-graph... commit | commitdiff | tree | snapshot
2010-06-25 trevor_hansenThe array transformer now respects optimisations being... commit | commitdiff | tree | snapshot
2010-06-25 trevor_hansen* Add containsArrayOps(..) to check if any array terms... commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenFix the build. commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenAdd a new function to replace using the substitution... commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenRemoving duplicate files commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenRemove bio tests from regressstp. They are all included... commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenAdding realistic expected times to these test cases commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenBugfix. The script that was called by regressstp didn... commit | commitdiff | tree | snapshot
2010-06-24 trevor_hansenSpeedup. Better cache the variables that are discovered... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenUse simplifying minisat for unit tests. commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenBugfix. Simplifying minisat wasn't using the separate... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenSpeedup/bugfix. Change how duplicate symbols are search... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenShort cut on constant evaluation commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenBugfix. Keep track of which symbols* have been deleted... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenDon't perform simplifications when creating the substit... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenReduce memory usage. Clear out the caches from the... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenFix grammar. Extra assertion. commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenSpeedup. Remove some unnecessary tests. commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenRefactor. Make the TermOrder function a non-member... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenSpeedup. Shortcut if the thing we are simplifying is... commit | commitdiff | tree | snapshot
2010-06-23 trevor_hansenSpeedup. The bvsolver now uses a reduced version of... commit | commitdiff | tree | snapshot
2010-06-18 trevor_hansenCheck for duplicate variables using a different function commit | commitdiff | tree | snapshot
2010-06-18 trevor_hansenBugfix. Variables were reported as only occuring a... commit | commitdiff | tree | snapshot
2010-06-18 trevor_hansenRefactor & slight performance improvement for the bvsolver. commit | commitdiff | tree | snapshot
2010-06-18 trevor_hansenBugfix. Fix rotate_left and rotate_right to take the... commit | commitdiff | tree | snapshot
2010-06-16 trevor_hansenSpeedup. When printing out the counter example, don... commit | commitdiff | tree | snapshot
2010-06-16 trevor_hansenSpeedup. Reduce the amount of checking that the bvsolve... commit | commitdiff | tree | snapshot
2010-06-16 trevor_hansenSpeed up VarSeenInTerm(..) slightly. commit | commitdiff | tree | snapshot
2010-06-14 trevor_hansenAdd some unit tests (which run when regressall is run... commit | commitdiff | tree | snapshot
2010-06-14 trevor_hansenBugfix. Enable the same options for when the parser... commit | commitdiff | tree | snapshot
2010-06-14 trevor_hansenChange the properties so that SMTLIB2 format files... commit | commitdiff | tree | snapshot
2010-06-14 trevor_hansenBugfix. Save the value of print counter example as... commit | commitdiff | tree | snapshot
2010-06-14 trevor_hansenFix regresscapi. This file wasn't checked in commit | commitdiff | tree | snapshot
2010-06-13 trevor_hansenFix the build. Add doug Lea's malloc implementation commit | commitdiff | tree | snapshot
2010-06-13 trevor_hansenPut the clauses of the SAT solver in a separate heap... commit | commitdiff | tree | snapshot
2010-06-12 trevor_hansenFree up more memory before SAT solving. In particular... commit | commitdiff | tree | snapshot
2010-06-12 trevor_hansenFix. I didn't update al l the function calls I should... commit | commitdiff | tree | snapshot
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
next
STP Constraint Solver.