RSolver Activity
Brought to you by:
stefan_ratschan
Activity for RSolver
-
stefan_ratschan committed [r345]
negative powers
-
arctan
-
-
-
-
-
-
stefan_ratschan committed [r338]
-
-
empty box
-
distance to empty box
-
corner_hi, corner_lo
-
dist
-
norm2
-
parsing EXISTS*, FORALL* (no branching)
-
initial checkin
-
corrected spec of zero_dim
-
adapted paths in makefiles
-
trace_branching off
-
Initial import.
-
new: prune_crude_neg
-
version 1.10: printing of volume of result
-
--none-- committed [r3]
This commit was manufactured by cvs2svn to create tag 'start'.
-
EXISTS* FORALL*
-
makefile for library version
-
initial version
-
updated version message
-
bugfix: parsing without meanvalue constraint
-
external solver interfaces via symbolic links
-
relaxation: minor changes, documentation
-
improved docu for -b option
-
bugfix parsing MINUS
-
version 2:00
-
*** empty log message ***
-
--none-- committed [r83]
This commit was manufactured by cvs2svn to create tag 'PAPER_bwrec'.
-
first version with mean value constraint
-
primitive constraint for unary minus
-
statistics: number of primitive constraints
-
--none-- committed [r78]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_19'.
-
TODO file added
-
unary minus added
-
Sven Bünte committed [r75]
debugging...
-
comments added
-
--none-- committed [r86]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_21'.
-
address updated
-
*** empty log message ***
-
bugfix pruneUnivQuantBound: store result of pruning
-
--none-- committed [r22]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_13'.
-
array_for_all bug removed
-
new
-
README file under CVS
-
*** empty log message ***
-
--none-- committed [r17]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_12'.
-
version number updated
-
spec for diff
-
producing correct box boundaries
-
non-recursive version of mean value constraints
-
non-recursive version of mean value constraints
-
Widest splitting bug removed
-
mean-value constraint for several function symbols
-
sampling: compute verified samples, -f SampleApproximate, try to sample always
-
unary minus: mean value constraint
-
*** empty log message ***
-
faithful printing of box boundaries
-
bugfixes
-
more debugging, comments updated
-
old mean value implementation removed
-
*** empty log message ***
-
relaxation dummy files added
-
--none-- committed [r15]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_11'.
-
tan/atan added
-
debugging prints removed
-
new makefile creating symbolic links to external solver interfaces
-
--none-- committed [r29]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_15'.
-
--none-- committed [r35]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_16'.
-
--none-- committed [r42]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_17'.
-
first preperation for mean-value constraints: redundant constraint, universal quantifiers that take bounds from other variable
-
updated stub interface
-
removed some bugs, introduced probably some new.
-
bound on variable "t" in quantifier now expressed via IsElement-constraint
-
relaxation: return witnesses
-
substitution changed
-
*** empty log message ***
-
--none-- committed [r46]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_18'.
-
bugfix constraint copy
-
sven mentioned
-
made conversion from integers to intervals precise
-
--none-- committed [r48]
This commit was manufactured by cvs2svn to create tag 'rsolver-1_18a'.
-
new
-
pruneUnivQuantBound: clear bounds after pruning
-
omitted opening the Constr-structure at the beginning of the file (3rd line)
-
bug in conversion from string to float (hopefully) removed
-
sampling bugfix
-
relaxation: without prints
-
changed order in generation of branches in atomic constr.. Simplifies test
-
uni-variate mean value contractor on all variables implemented
-
not needed anymore
-
relaxation: without prints
-
changes for multivariate mean value contractor
-
comments added (cygwin related)
1 >
