Added CEGIS control benchmark 4

CEGIS control benchmark 4 tests the __CPROVER_fixedbv semantics
fixed in 1f1a11e.

Author: pkesseli

regression/cegis/cegis_control_benchmark_04/benchmark.h

@@ -0,0 +1,11 @@
+#define INT_BITS 12
+#define FRAC_BITS 12
+#include "control_types.h"
+
+#define NSTATES 3
+#define NINPUTS 1
+#define NOUTPUTS 1
+#define INPUT_LOWERBOUND (__plant_typet)-1
+#define INPUT_UPPERBOUND (__plant_typet)1
+const __plant_typet _controller_A[NSTATES][NSTATES] = { { interval(0.9905),interval(0.075687),interval(0.021033) }, { interval(0.125),interval(0),interval(0) }, { interval(0),interval(0.015625),interval(0) } };
+const __plant_typet _controller_B[NSTATES] = { interval(16), interval(0), interval(0) };

regression/cegis/cegis_control_benchmark_04/control_types.h

@@ -0,0 +1,48 @@
+/*
+ * control_types.h
+ *
+ *  Created on: 18 Jan 2017
+ *      Author: elipol
+ */
+
+#ifndef CONTROL_TYPES_H_
+#define CONTROL_TYPES_H_
+
+#ifdef CPROVER
+    #ifdef INTERVAL
+      typedef   __CPROVER_fixedbv[_CONTROL_FLOAT_WIDTH][_CONTORL_RADIX_WIDTH] __plant_precisiont;
+      #include "intervals.h"
+      typedef   struct intervalt __plant_typet;
+      typedef   __CPROVER_fixedbv[_CONTROL_FLOAT_WIDTH][_CONTORL_RADIX_WIDTH] __controller_precisiont;
+      typedef   struct intervalt __controller_typet;
+      #define interval(x) interval_cast(x);
+    #else
+      typedef __CPROVER_fixedbv[_CONTROL_FLOAT_WIDTH][_CONTORL_RADIX_WIDTH] __plant_precisiont;
+      typedef __plant_precisiont __plant_typet;
+      typedef __CPROVER_fixedbv[INT_BITS+FRAC_BITS][FRAC_BITS] __controller_precisiont;
+      typedef  __controller_precisiont __controller_typet;
+      #define plant_cast(x) ((__plant_typet)x)
+      #define controller_cast(x) ((__controller_typet)x)
+      #define interval(x) x
+    #endif
+#else
+   #ifdef INTERVAL
+     typedef double __plant_precisiont;
+      #include "intervals.h"
+     typedef struct intervalt __plant_typet;
+     typedef double __controller_precisiont; //fixed point arithmetic is implemented using doubles
+     typedef struct intervalt __controller_typet;
+     #define interval(x) interval_cast(x)
+   #endif
+  #ifndef INTERVAL
+     typedef double __plant_precisiont;
+     typedef __plant_precisiont __plant_typet;
+     typedef double __controller_precisiont; //fixed point arithmetic is implemented using doubles
+     typedef __controller_precisiont __controller_typet;
+     #define interval(x) (x)
+     #define plant_cast(x) x
+     #define controller_cast(x) x
+  #endif
+#endif
+
+#endif /* CONTROL_TYPES_H_ */

regression/cegis/cegis_control_benchmark_04/operators.h

@@ -0,0 +1,57 @@
+/*
+ * operators.h
+ *
+ *  Created on: 18 Jan 2017
+ *      Author: elipol
+ */
+
+#ifndef OPERATORS_H_
+#define OPERATORS_H_
+
+#ifndef INTERVAL
+  #define controller_mult(x,y) ((x) *(y))
+  #define mult(x,y) ( (x) * (y))
+
+  #define _abs(a) ( (a) < 0 ? -(a) : (a))
+  #define add(x,y) ( (x) + (y))
+
+  #define lessthan(x,y) ((x)<(y))
+  #define greaterthan(x,y) ((x)>(y))
+  #define lessthanzero(x) ((x) < 0)
+  #define lessthan_equaltozero(x) ((x) <= 0)
+  #define zero_type 0
+  #define one_type (__plant_precisiont)1.0
+  #define minusone  (__plant_precisiont)-1
+  #define div(x,y) ( (x) / (y))
+  #define sub(x,y) ( (x) - (y))
+  #define set(x,y) (x)=(y)
+
+
+#endif
+#ifdef INTERVAL
+
+  #define controller_mult(x,y) (interval_fxp_mult((x),(y)))
+  #define mult(x,y) ( interval_mult((x),(y)))
+
+  #define _abs(a) ( abs_interval(a))
+
+  #define lessthan(x,y) (interval_lessthan(x,y))
+  #define greaterthan(x,y) (interval_greaterthan((x),(y)))
+  #define add(x,y) (interval_add((x),(y)))
+  #define lessthanzero(x) (interval_lessthanzero(x))
+  #define lessthan_equaltozero(x) (interval_lessthan_equal_to_zero(x))
+
+  #define zero_type (zero_interval)
+  #define minusone  (minusone_interval)
+  #define one_type one_interval
+  #define div(x,y) (interval_posDiv((x),(y)))
+  #define sub(x,y) (interval_sub((x),(y)))
+
+  #define controller_cast(x) (fxp_interval_check(x))
+  #define plant_cast(x) x
+  #define set(x,y) (x.low=y, x.high=y)
+
+
+#endif
+
+#endif /* OPERATORS_H_ */