]> 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
2011-03-25 trevor_hansenImprovement. Convert left/right (NOT aritmetic), shifts... commit | commitdiff | tree | snapshot
2011-03-25 trevor_hansenImprovement. Better unsigned interval propagation of... commit | commitdiff | tree | snapshot
2011-03-25 trevor_hansenFix remove an extra pair of brackets from LETs. Thanks... commit | commitdiff | tree | snapshot
2011-03-24 trevor_hansenSlight speedup to the hashing node factory. commit | commitdiff | tree | snapshot
2011-03-24 trevor_hansenImprovement. Create fewer objects. commit | commitdiff | tree | snapshot
2011-03-24 trevor_hansenImprovement. No longer have vectors in the ASTSymbol... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenSpeedup. Short cut before some copies were created. commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenMove CVC parser to using strings for LET names. Removes... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenImprovement. SMTLIB2 lets now use strings for names... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenFix the SMTLIB1 to not accept badly formed input. Previ... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenIf there are unapplied substitutions before starting... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenRefactor. Changes to whitespace only. commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenRefactor. A new function to check if there are unapplie... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenNow assume there will be no unapplied substitutions... commit | commitdiff | tree | snapshot
2011-03-23 trevor_hansenRefactor. Convert from if-then-else to a switch. commit | commitdiff | tree | snapshot
2011-03-21 trevor_hansenAdds extra cases to the simplifying node factory. commit | commitdiff | tree | snapshot
2011-03-21 trevor_hansenFix division by zero results. x % 0, now equals x. commit | commitdiff | tree | snapshot
2011-03-20 trevor_hansenFix. x bvmod 0, now evaluates to x, not to 0. commit | commitdiff | tree | snapshot
2011-03-20 trevor_hansenImprovement. More cases for the simplifying node factory. commit | commitdiff | tree | snapshot
2011-03-18 trevor_hansenRemove debugging printf. commit | commitdiff | tree | snapshot
2011-03-18 trevor_hansenTest case for r1217. commit | commitdiff | tree | snapshot
2011-03-18 trevor_hansenImprovement. Pull bvsx through multiplication, signed... commit | commitdiff | tree | snapshot
2011-03-18 trevor_hansenImprovement. Add more operations to the unsigned interv... commit | commitdiff | tree | snapshot
2011-03-17 trevor_hansenImproved unsigned interval analysis. Extra operations... commit | commitdiff | tree | snapshot
2011-03-16 trevor_hansenAdd some extra simplifications to the simplifying node... commit | commitdiff | tree | snapshot
2011-03-14 trevor_hansen* The simplifying node factory now removes TRUEs when... commit | commitdiff | tree | snapshot
2011-03-14 trevor_hansenImprovement. Start to use the simplifying node factory... commit | commitdiff | tree | snapshot
2011-03-14 trevor_hansenImprovement. With stats enabled, only output the first... commit | commitdiff | tree | snapshot
2011-03-14 trevor_hansenMake SimplifyFormula idempotent. I don't know if this... commit | commitdiff | tree | snapshot
2011-03-14 trevor_hansenExperimental. Simplify all the bit-vector children... commit | commitdiff | tree | snapshot
2011-03-13 trevor_hansenImprovement. Add a simple read over write simplificatio... commit | commitdiff | tree | snapshot
2011-03-13 trevor_hansen* Clean up the simplifier some. commit | commitdiff | tree | snapshot
2011-03-13 trevor_hansenRefactor. Remove the simplify_upfront option. It's... commit | commitdiff | tree | snapshot
2011-03-13 trevor_hansenRefactor. Remove code that's not used. commit | commitdiff | tree | snapshot
2011-03-12 trevor_hansenFix. Missing break; in a switch. Dumb luck meant it... commit | commitdiff | tree | snapshot
2011-03-12 trevor_hansenFix. r1201 added a message to cout. commit | commitdiff | tree | snapshot
2011-03-12 trevor_hansenImprovement. Add a size reducing phase prior to perform... commit | commitdiff | tree | snapshot
2011-03-12 trevor_hansenImprovements. commit | commitdiff | tree | snapshot
2011-03-12 trevor_hansenFix. This assert() was very slow sometimes. commit | commitdiff | tree | snapshot
2011-03-10 trevor_hansenBugfix. r1194 didn't preserve the doubly linked list. commit | commitdiff | tree | snapshot
2011-03-10 trevor_hansenFiddle with the difficulty scorer. commit | commitdiff | tree | snapshot
2011-03-10 trevor_hansenFiddle with the difficulty scorer to better estimate... commit | commitdiff | tree | snapshot
2011-03-09 trevor_hansenMiscellaneous improvements. commit | commitdiff | tree | snapshot
2011-03-09 trevor_hansenFix. In the prior checkin I didn't keep track of which... commit | commitdiff | tree | snapshot
2011-03-09 trevor_hansenImprovement. Now do unconstrained elimination for all... commit | commitdiff | tree | snapshot
2011-03-07 trevor_hansenExtra simplification rules for BVAND, and EQ. These... commit | commitdiff | tree | snapshot
2011-03-07 trevor_hansenImprovement. Add an extra simplification rule for BVDIV... commit | commitdiff | tree | snapshot
2011-03-06 trevor_hansenAdd simplification of the top-most propositional part... commit | commitdiff | tree | snapshot
2011-03-05 trevor_hansenimprovement. Use the simplifying node factory be defaul... commit | commitdiff | tree | snapshot
2011-03-05 trevor_hansenTiny improvement. Create slightly fewer nodes. commit | commitdiff | tree | snapshot
2011-03-05 trevor_hansenFix a leak. I'd forgotten to call fclose(). commit | commitdiff | tree | snapshot
2011-03-05 trevor_hansenFix a leak introduced in r1184. commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenImprovement. Specialise the replace function more for... commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenRefactor. Neaten up the CreateSubstitutionMap function. commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenFixes / Improvements. commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenImprovement. Only create possible values if it can... commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenEnable ITE Context stuff by default. commit | commitdiff | tree | snapshot
2011-03-03 trevor_hansenRefactor. I experimented with changing the allocator... commit | commitdiff | tree | snapshot
2011-03-01 trevor_hansenImprovement. Add an equality simplification. commit | commitdiff | tree | snapshot
2011-02-28 trevor_hansenImprovement. Enable ITE context simplifications again. commit | commitdiff | tree | snapshot
2011-02-27 trevor_hansenDisable ITE context simplifications. It's too slow... commit | commitdiff | tree | snapshot
2011-02-27 trevor_hansenBugfix. Terrible. Forgot to delete debugging code.... commit | commitdiff | tree | snapshot
2011-02-27 trevor_hansenBugfix. Terrible. The last checkin causes STP to someti... commit | commitdiff | tree | snapshot
2011-02-27 trevor_hansenImprovement. An analysis that simplifies ITES by determ... commit | commitdiff | tree | snapshot
2011-02-26 trevor_hansenNo semantic change. Fix a mistake that caused no effect. commit | commitdiff | tree | snapshot
2011-02-26 trevor_hansenFix. XORs with >2 children sometimes reached the simpl... commit | commitdiff | tree | snapshot
2011-02-26 trevor_hansenBugfix. Terrible! Another fix. STP r1149 to here will... commit | commitdiff | tree | snapshot
2011-02-26 trevor_hansenBugfix. Terrible! STP r1149 to here will sometimes... commit | commitdiff | tree | snapshot
2011-02-24 trevor_hansenBugfix. The prior checkin added an assertion that didn... commit | commitdiff | tree | snapshot
2011-02-24 trevor_hansenFinish refactoring of the ArrayTransformer class. commit | commitdiff | tree | snapshot
2011-02-24 trevor_hansenPartial refactor. Remove the Arrayread_SymbolMap. commit | commitdiff | tree | snapshot
2011-02-24 trevor_hansenPartial refactor. Removing the Arrayname_ReadindicesMap. commit | commitdiff | tree | snapshot
2011-02-24 trevor_hansenPartial refactoring. Removing the arrayread_itemap. commit | commitdiff | tree | snapshot
2011-02-23 trevor_hansenRefactoring. commit | commitdiff | tree | snapshot
2011-02-23 trevor_hansenBugfix. Fix the prior checkin. commit | commitdiff | tree | snapshot
2011-02-23 trevor_hansenPartial Refactor. I'm reducing the number of collection... commit | commitdiff | tree | snapshot
2011-02-23 trevor_hansenExtra test cases that should be simplified down to... commit | commitdiff | tree | snapshot
2011-02-22 trevor_hansenRefactor. Overcome a temporary static fetish. Now better. commit | commitdiff | tree | snapshot
2011-02-22 trevor_hansenImprovement. Match the difficulty score better to the... commit | commitdiff | tree | snapshot
2011-02-22 trevor_hansenImprovement. The start of an unsigned interval simplifi... commit | commitdiff | tree | snapshot
2011-02-22 trevor_hansenImprovement. Handle extracts especially when doing... commit | commitdiff | tree | snapshot
2011-02-21 trevor_hansenBugfix. r1152 was broken. It got the widths wrong. commit | commitdiff | tree | snapshot
2011-02-21 trevor_hansenA new test case for the special unconstrained extract... commit | commitdiff | tree | snapshot
2011-02-21 trevor_hansenImprovement. Simplifying EQ a little better. commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenAdd find pure literals code.oooops. commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenEnable pure literal elimination, and unconstrained... commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenRemove unused configuration option. Update qualifiers. commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenAdd --config options to enable CNF conversion via Tseit... commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenAdd the code for unconstrained variable elimination... commit | commitdiff | tree | snapshot
2011-02-14 trevor_hansenImprovements. commit | commitdiff | tree | snapshot
2011-02-11 trevor_hansenAdd categories to the RunTime class for new simplifications commit | commitdiff | tree | snapshot
2011-02-10 trevor_hansenFix a leak in _asserts. I know of no other leaks. commit | commitdiff | tree | snapshot
2011-02-10 trevor_hansenImprovement. The SMTLIB1 & SMTLIB2 parsers were holding... commit | commitdiff | tree | snapshot
2011-02-10 khooypAdd conditional workaround for flex < 2.5.20, such... commit | commitdiff | tree | snapshot
2011-02-10 khooypClean up the build system for src/parser. commit | commitdiff | tree | snapshot
2011-02-10 khooypTemporarily rename CVC.* to cvclib.*; to be renamed... commit | commitdiff | tree | snapshot
2011-02-10 khooypFix inconsistent line endings, and execute bit on a... commit | commitdiff | tree | snapshot
2011-02-10 khooypFix a typo in the help string. commit | commitdiff | tree | snapshot
2011-02-08 trevor_hansenFix. For r1131 I deleted the wrong file. commit | commitdiff | tree | snapshot
2011-02-08 trevor_hansenPatch from Khoo Yit Phang. commit | commitdiff | tree | snapshot
next
STP Constraint Solver.