]> 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-08-28 trevor_hansenFix. I thought the code I checked-in just now wasn... commit | commitdiff | tree | snapshot
2010-08-28 trevor_hansenChanges to inactive by default code. commit | commitdiff | tree | snapshot
2010-08-22 trevor_hansenRemove some assertion checks from code that's not enabl... commit | commitdiff | tree | snapshot
2010-08-22 trevor_hansenBugfix. STP returned the wrong answer when something... commit | commitdiff | tree | snapshot
2010-08-21 vijay_ganeshminor changes to INSTALL instructions commit | commitdiff | tree | snapshot
2010-08-20 trevor_hansenFix the build script commit | commitdiff | tree | snapshot
2010-08-20 trevor_hansenRemove variables from the configure script which contro... commit | commitdiff | tree | snapshot
2010-08-20 trevor_hansenRemove binaries I checked in by mistake commit | commitdiff | tree | snapshot
2010-08-20 trevor_hansenFix build. Forgot to checkin these commit | commitdiff | tree | snapshot
2010-08-20 trevor_hansen* Replace minisat 2 with minisat 2.2. commit | commitdiff | tree | snapshot
2010-08-18 trevor_hansenAdd regresssmtcomp2007 which runs the bitvector benchma... commit | commitdiff | tree | snapshot
2010-08-18 trevor_hansenChanges to inactive code. Use simple AIG simplification... commit | commitdiff | tree | snapshot
2010-08-16 trevor_hansenUpdate to currently inactive code. commit | commitdiff | tree | snapshot
2010-08-16 trevor_hansenCode for AIG rewriting with ABC. This code is not curre... commit | commitdiff | tree | snapshot
2010-08-15 trevor_hansenExtra tests for inactive by-default code commit | commitdiff | tree | snapshot
2010-08-15 trevor_hansenRefactor. Remove unncessary code. commit | commitdiff | tree | snapshot
2010-08-15 trevor_hansenChange non-enabled code. commit | commitdiff | tree | snapshot
2010-08-14 trevor_hansenImprovement? FlattenKind now recursively flattens it... commit | commitdiff | tree | snapshot
2010-08-14 trevor_hansenShould cause not runtime effects. commit | commitdiff | tree | snapshot
2010-08-13 trevor_hansenSpeedup. Reduce the number of times that SortByArith... commit | commitdiff | tree | snapshot
2010-08-11 trevor_hansenPrint out a not yet supported error. commit | commitdiff | tree | snapshot
2010-08-11 trevor_hansenAdd a sorting network implementation. This code is... commit | commitdiff | tree | snapshot
2010-08-10 trevor_hansenCleanup. Remove experimental (not active) code. commit | commitdiff | tree | snapshot
2010-08-10 trevor_hansenImprove the encoding of the full adder used by the... commit | commitdiff | tree | snapshot
2010-08-10 trevor_hansenCorrect a comment commit | commitdiff | tree | snapshot
2010-08-07 trevor_hansenBugfix. --output-CNF was broken when outputting with... commit | commitdiff | tree | snapshot
2010-08-06 trevor_hansenFix slowdown. commit | commitdiff | tree | snapshot
2010-08-05 trevor_hansenSpeedup the bvsolver. Use the applySubstitutionMap... commit | commitdiff | tree | snapshot
2010-08-05 trevor_hansenBugfix. The prior revision sometimes returned the wrong... commit | commitdiff | tree | snapshot
2010-08-01 trevor_hansenBugfix. Infinite loop. My fourth attempt to fix the... commit | commitdiff | tree | snapshot
2010-07-31 trevor_hansenBugfix. Oops. When using the quick statistics (the... commit | commitdiff | tree | snapshot
2010-07-28 trevor_hansenSpeedup. I've measured the performance of bit blasted... commit | commitdiff | tree | snapshot
2010-07-28 trevor_hansenBugfix. Infinite loop. A third fix for r947. commit | commitdiff | tree | snapshot
2010-07-28 trevor_hansenBugfix. STP may produce the wrong answer. Introduced... commit | commitdiff | tree | snapshot
2010-07-28 trevor_hansenSpeed up of the unsigned division encoding. Update... commit | commitdiff | tree | snapshot
2010-07-28 trevor_hansenRefactoring. commit | commitdiff | tree | snapshot
2010-07-26 trevor_hansenBugfix. Stop a null pointer error. commit | commitdiff | tree | snapshot
2010-07-26 msoosFurther fixing of spurious printing in CryptoMiniSat commit | commitdiff | tree | snapshot
2010-07-26 msoosFixing verbosity-related problems in CryptoMiniSat2 commit | commitdiff | tree | snapshot
2010-07-10 trevor_hansenA QF_ABV division has been added to the smt-lib. Update... commit | commitdiff | tree | snapshot
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
next
STP Constraint Solver.