]> 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-04-16 trevor_hansenExtra upfront simplification rules. commit | commitdiff | tree | snapshot
2011-04-14 trevor_hansenAdd some missing simplification rules for AND/OR/ propo... commit | commitdiff | tree | snapshot
2011-04-14 trevor_hansenShortcut in a rare circumstance. commit | commitdiff | tree | snapshot
2011-04-14 trevor_hansenExtra BVXOR simplification rules. commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenAdds the reverse of rules to catch an obscure but impor... commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenImprovement. Add a warning message when using --exit... commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenImprovement. Fix the difficulty score for subtraction. commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenFix the build. Without -NDEBUG wouldn't compile. commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenImprovement. Look for nodes that are true/false when... commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenRemove some assertions that don't necessarily hold. commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenImprovement. Replace the hashing node factory with... commit | commitdiff | tree | snapshot
2011-04-13 trevor_hansenExtra simplification rule. commit | commitdiff | tree | snapshot
2011-04-11 trevor_hansenoops. Meant to add this too. commit | commitdiff | tree | snapshot
2011-04-11 trevor_hansenAdd an extra simplification rule to the simplifying... commit | commitdiff | tree | snapshot
2011-04-11 trevor_hansenMove some division be zero code into the bitblaster... commit | commitdiff | tree | snapshot
2011-04-10 trevor_hansenAdds code, that's not currently enabled, to read-out... commit | commitdiff | tree | snapshot
2011-04-10 trevor_hansenImprovement. Use the simplifying node factory in transf... commit | commitdiff | tree | snapshot
2011-04-10 trevor_hansenRevert the previous revision. It broke lots. commit | commitdiff | tree | snapshot
2011-04-08 trevor_hansenImprovement. Use the simplifying node factory in transf... commit | commitdiff | tree | snapshot
2011-04-08 trevor_hansenImprovement. Don't add NOT FALSE at the end of the... commit | commitdiff | tree | snapshot
2011-04-07 trevor_hansenImprovement. When a node is simplified set a value... commit | commitdiff | tree | snapshot
2011-04-07 trevor_hansenImprovement. Output the time spent in a stage with -s. commit | commitdiff | tree | snapshot
2011-04-07 trevor_hansenHack. The ITE context simplification blows out ff.stp... commit | commitdiff | tree | snapshot
2011-04-07 trevor_hansenRevert. I didn't mean to checkin all those changes. commit | commitdiff | tree | snapshot
2011-04-07 trevor_hansenHack. The ITE context simplification blows out ff.stp... commit | commitdiff | tree | snapshot
2011-04-06 trevor_hansenRemove junk. commit | commitdiff | tree | snapshot
2011-04-06 trevor_hansenImprove the bvsolver.If the substitution of a monomial... commit | commitdiff | tree | snapshot
2011-04-06 trevor_hansenRefactor. Remove junk. commit | commitdiff | tree | snapshot
2011-04-03 trevor_hansenImprovement. Some extra simplifications for the simplif... commit | commitdiff | tree | snapshot
2011-04-03 trevor_hansenImprovement. The simplifying node factory never creates... commit | commitdiff | tree | snapshot
2011-03-31 trevor_hansenTiny improvement. Add the one-bit operations that evalu... commit | commitdiff | tree | snapshot
2011-03-31 trevor_hansenSmall improvement. Discard the inner write if the two... commit | commitdiff | tree | snapshot
2011-03-29 trevor_hansenWork around rare problem caused by the simplifying... commit | commitdiff | tree | snapshot
2011-03-28 trevor_hansenMake applySubstitutionMap idempotent (I hope). commit | commitdiff | tree | snapshot
2011-03-28 trevor_hansenImprovement. The simplifying node factory now eliminate... commit | commitdiff | tree | snapshot
2011-03-28 trevor_hansenDuring the size reducing transformations, now set the... commit | commitdiff | tree | snapshot
2011-03-28 trevor_hansenChange the names for some statistics. commit | commitdiff | tree | snapshot
2011-03-28 trevor_hansenExtra simplification rule for BVXOR. commit | commitdiff | tree | snapshot
2011-03-27 trevor_hansenAdd experimental code (not presently enabled), that... commit | commitdiff | tree | snapshot
2011-03-26 trevor_hansenImprovement. The simplifying node factory no longer... commit | commitdiff | tree | snapshot
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
next
STP Constraint Solver.