]> git.unchartedbackwaters.co.uk Git - francis/stp.git/shortlog
francis/stp.git
2011-07-12 trevor_hansenPatch from Peter Collingbourne to enable compiling...
2011-07-12 trevor_hansenRemove the include directory. It shouldn't be here.
2011-07-09 trevor_hansenFix. The SMTLIB2 parser now outputs "success" in reply...
2011-07-07 trevor_hansenMove functions around so that clang links.
2011-07-07 trevor_hansenRemove clang warnings.
2011-07-07 trevor_hansenFix clang warnings.
2011-07-07 trevor_hansenSilence a clang warning message.
2011-06-30 trevor_hansenImprovement. Needed for using STP interactively.
2011-06-27 trevor_hansenAdds the push(n) and pop(n) instructions to the SMTLIB2...
2011-06-26 trevor_hansenMove the filename counter out so it's saved between...
2011-06-26 trevor_hansenImprovement. Additional simplification rules.
2011-06-23 trevor_hansenFix. Look for fatal errors when running tests.
2011-06-23 trevor_hansenImprovement. Simplifying minisat now uses the advanced...
2011-06-22 trevor_hansenImprovement. Create fewer clauses when creating an...
2011-06-21 trevor_hansenAutomatically format this code. No semantic change.
2011-06-21 trevor_hansenCheck axioms for indexes in order of the number of...
2011-06-20 trevor_hansenImprovement. During abstraction refinement process...
2011-06-20 trevor_hansenFix. I forgot to remove the descriptions of -e -f from...
2011-06-20 trevor_hansenRemove the code for the not-working FOR construct.
2011-06-20 trevor_hansenVijay advised we aren't going to do fors.
2011-06-19 trevor_hansenUse the advanced CNF generator to encode array problems...
2011-06-16 trevor_hansenAdd boost to the licence, fix bitvector description.
2011-06-16 trevor_hansenBugfix. Fix the semantics of BVSMOD to always give...
2011-06-16 trevor_hansenSpeedup for easy instances. Don't call the SAT solver...
2011-06-14 trevor_hansenAdd cloud9 test cases.
2011-06-09 trevor_hansenA windows patch to r446 from Hume.
2011-05-12 trevor_hansenImprovement. Make error checking more normal.
2011-05-12 trevor_hansenExtra simplification rule.
2011-05-11 trevor_hansenExtra test cases that simplify down to nothing.
2011-05-11 trevor_hansenITE context is mostly bad. Now disabled by default.
2011-05-11 trevor_hansenNo longer default to the simple CNF generator for big...
2011-05-11 trevor_hansenImprovement. Exit-after-cnf would exit after sending...
2011-05-11 trevor_hansenFix. Creating the node (v + v), where v is greater...
2011-05-11 trevor_hansenBugfix. Arithmetic shifts by constants that didn't...
2011-05-11 trevor_hansenRevert the change to run_tests, I didn't mean to submit...
2011-05-11 trevor_hansenRemove the comment that 32-bit is best for arrays....
2011-05-11 trevor_hansen Improvement. Add array size statistics when printing...
2011-05-11 trevor_hansenBugfix. Maybe. Disable a comparison so that CNF convers...
2011-05-09 trevor_hansenAdds two extra simplfication rules.
2011-05-09 trevor_hansenMore simplification rules.
2011-05-07 trevor_hansenExtra simplification rules for the simplifying node...
2011-05-07 trevor_hansenSigned division now returns what is should. Signed...
2011-05-07 trevor_hansenAdd a public function that calls sizeReducing until...
2011-05-05 trevor_hansenAdds an extra BVPLUS simplification rule. Cleans up...
2011-05-05 trevor_hansenImportant bugfix. r1291 through to this revision, about...
2011-05-05 trevor_hansenAdd an extra simplification rule.
2011-05-04 trevor_hansenReplace variables before calling the interval analysis.
2011-05-04 trevor_hansenFunction to reset the stopwatch.
2011-05-04 trevor_hansenAnother fix to the same
2011-05-04 trevor_hansenCorrect the last patch. I don't think this code runs.
2011-05-04 trevor_hansenApply simplifications through arrayterms too.
2011-05-02 trevor_hansenBugfix. Rarely we get the wrong answer; I got two broke...
2011-05-01 trevor_hansenCompiling with -D_GLIBCXX_DEBUG reported warnings becau...
2011-05-01 trevor_hansenCode to apply the alwaysTrueSet. Not currently enabled.
2011-05-01 trevor_hansenEnable bitblast simplifications by default
2011-04-30 trevor_hansenTurn off the ite-context simplification by default.
2011-04-30 trevor_hansenImportant Bugfix. The prior checkin sometimes, but...
2011-04-30 trevor_hansenBugfix. The last checkin caused an infinite loop (often).
2011-04-30 trevor_hansenExtra simplification rules
2011-04-30 trevor_hansenExtra simplification rules.
2011-04-30 trevor_hansenConvert subtraction to addition in the simplifying...
2011-04-29 trevor_hansenBugfix. Reads might have been simplified down which...
2011-04-27 trevor_hansenImportant Bugfix. The prior checkin causes the WRONG...
2011-04-27 trevor_hansenExtra simplification rules. In particular a simple...
2011-04-27 trevor_hansenAdd extra simplifying rules.
2011-04-27 trevor_hansenFix. I thought that extracts don't add any information...
2011-04-27 trevor_hansenRemove signed division, modulus and remainder when...
2011-04-26 trevor_hansenTwo extra simplification rules.
2011-04-21 trevor_hansenChange the sorting network based adder (which isn't...
2011-04-20 trevor_hansenRefactor. Less verbose.
2011-04-20 trevor_hansenImprovement. Add a warning when parsing problems that...
2011-04-16 trevor_hansenExtra upfront simplification rules.
2011-04-14 trevor_hansenAdd some missing simplification rules for AND/OR/ propo...
2011-04-14 trevor_hansenShortcut in a rare circumstance.
2011-04-14 trevor_hansenExtra BVXOR simplification rules.
2011-04-13 trevor_hansenAdds the reverse of rules to catch an obscure but impor...
2011-04-13 trevor_hansenImprovement. Add a warning message when using --exit...
2011-04-13 trevor_hansenImprovement. Fix the difficulty score for subtraction.
2011-04-13 trevor_hansenFix the build. Without -NDEBUG wouldn't compile.
2011-04-13 trevor_hansenImprovement. Look for nodes that are true/false when...
2011-04-13 trevor_hansenRemove some assertions that don't necessarily hold.
2011-04-13 trevor_hansenImprovement. Replace the hashing node factory with...
2011-04-13 trevor_hansenExtra simplification rule.
2011-04-11 trevor_hansenoops. Meant to add this too.
2011-04-11 trevor_hansenAdd an extra simplification rule to the simplifying...
2011-04-11 trevor_hansenMove some division be zero code into the bitblaster...
2011-04-10 trevor_hansenAdds code, that's not currently enabled, to read-out...
2011-04-10 trevor_hansenImprovement. Use the simplifying node factory in transf...
2011-04-10 trevor_hansenRevert the previous revision. It broke lots.
2011-04-08 trevor_hansenImprovement. Use the simplifying node factory in transf...
2011-04-08 trevor_hansenImprovement. Don't add NOT FALSE at the end of the...
2011-04-07 trevor_hansenImprovement. When a node is simplified set a value...
2011-04-07 trevor_hansenImprovement. Output the time spent in a stage with -s.
2011-04-07 trevor_hansenHack. The ITE context simplification blows out ff.stp...
2011-04-07 trevor_hansenRevert. I didn't mean to checkin all those changes.
2011-04-07 trevor_hansenHack. The ITE context simplification blows out ff.stp...
2011-04-06 trevor_hansenRemove junk.
2011-04-06 trevor_hansenImprove the bvsolver.If the substitution of a monomial...
2011-04-06 trevor_hansenRefactor. Remove junk.
2011-04-03 trevor_hansenImprovement. Some extra simplifications for the simplif...
next