summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus

added examples to exercise new monotonicity code

fixed quantifier handling of new monotonicity calculus

tune parentheses and indentation

proper handling of frames for connectives in monotonicity calculus

tune indentation

removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications

implemented All rules from new monotonicity calculus

fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints

started implementing the new monotonicity rules for application