]> 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-10 trevor_hansenBugfix. Properly print out the counter example of booleans. commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenFix the build + extra options for constant bit propagat... commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenSpeedup. Flatten multiplications, sort, then re-assable... commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenExtra code (not enabled), for constant bit propagation. commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenExtra code (that's not currently enabled), so reduce... commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenOutput quick statistics if enabled, and exiting after... commit | commitdiff | tree | snapshot
2010-07-09 trevor_hansenDecision. This optimisation helps our cvc regressions... commit | commitdiff | tree | snapshot
2010-07-09 trevor_hansenAdd the option to exit after generating the CNF. Curren... commit | commitdiff | tree | snapshot
2010-07-09 trevor_hansenBugfix. If a new-line occured in a string literal,... commit | commitdiff | tree | snapshot
2010-07-08 petercolIntroduce vc_setInterfaceFlags function commit | commitdiff | tree | snapshot
2010-07-08 trevor_hansenFix some small leaks when performing division by zero... commit | commitdiff | tree | snapshot
2010-07-08 trevor_hansenOnly run the bvsolver if optimisations have been enable... commit | commitdiff | tree | snapshot
2010-07-08 trevor_hansenFix the unit test script: commit | commitdiff | tree | snapshot
2010-07-07 trevor_hansenBugfix. Remove a null pointer reference. commit | commitdiff | tree | snapshot
2010-07-07 trevor_hansenSimplify (bvdiv x x ) to one. Likewise for the other... commit | commitdiff | tree | snapshot
2010-07-07 trevor_hansenFix the building of the stp library. commit | commitdiff | tree | snapshot
2010-07-07 trevor_hansenFix the build. commit | commitdiff | tree | snapshot
2010-07-07 trevor_hansenNeaten up the code for constant bit propagation. Note... commit | commitdiff | tree | snapshot
2010-07-06 trevor_hansenBugfix. Fix a check to ensure that the type of nodes... commit | commitdiff | tree | snapshot
2010-07-06 trevor_hansen* Interface changes for constant bit propagation. Not... commit | commitdiff | tree | snapshot
2010-07-06 trevor_hansenFix. stp.a didn't have necessary cbitp file included... commit | commitdiff | tree | snapshot
2010-07-06 trevor_hansenFix. The unit tests expect the cnf's to be called outpu... commit | commitdiff | tree | snapshot
2010-07-06 trevor_hansenRevert. In r915 I removed the default -m32 flag by... commit | commitdiff | tree | snapshot
2010-07-05 trevor_hansenMore getting ready for constant bit propagation. This... commit | commitdiff | tree | snapshot
2010-07-05 msoosCryptoMiniSat can now be built commit | commitdiff | tree | snapshot
2010-07-05 msoosFor low-cutoff speed reasons, it's best not to subsume... commit | commitdiff | tree | snapshot
2010-07-05 trevor_hansenAdd the interface code for constant bit propagation... commit | commitdiff | tree | snapshot
2010-07-04 msoosCleaning up some bugs in CryptoMS commit | commitdiff | tree | snapshot
2010-07-04 trevor_hansenFree the memory allocatated to the AIGs before SAT... commit | commitdiff | tree | snapshot
2010-07-04 trevor_hansenTiny speedup. Generate the encoding of multiplication... commit | commitdiff | tree | snapshot
2010-07-04 trevor_hansenI didn't enable capturing of quick statistics (the... commit | commitdiff | tree | snapshot
2010-07-04 trevor_hansenBugfix. The SMTLIB2 defines the outer bars (if present... commit | commitdiff | tree | snapshot
2010-07-04 trevor_hansenGet cryptominisat2 compiling: commit | commitdiff | tree | snapshot
2010-07-03 trevor_hansenBitblast formula that don't contain arrays into and... commit | commitdiff | tree | snapshot
2010-07-02 msoosCorrecting small bug in CMS2 commit | commitdiff | tree | snapshot
2010-07-02 msoosUpdating CMS2 to get rid of a small bug commit | commitdiff | tree | snapshot
2010-07-02 msoosRemoving trailing code related to pools' #ifdefs in... commit | commitdiff | tree | snapshot
2010-07-02 msoosFurther updating of CryptoMiniSat2 commit | commitdiff | tree | snapshot
2010-07-02 msoosUpdating CryptoMiniSat2 to fix some minor bugs commit | commitdiff | tree | snapshot
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
next
STP Constraint Solver.