save

example/Makefile

@@ -16,9 +16,12 @@ FPOPTFLAGS += -mllvm --enzyme-enable-fpopt \
 		   -mllvm --enzyme-print-herbie \
 		   -mllvm --enzyme-print-fpopt \
 		   -mllvm --fpopt-log-path=example.txt \
-		   -mllvm --fpopt-target-func-regex=Pendulum \
+		   -mllvm --fpopt-target-func-regex=example \
 		   -mllvm --fpopt-enable-solver \
-		   -mllvm --fpopt-comp-cost-budget=1000
+		   -mllvm --fpopt-enable-pt \
+		   -mllvm --fpopt-comp-cost-budget=0 \
+		   -mllvm --fpopt-num-samples=1000 \
+		   -mllvm --fpopt-cost-model-path=microbm/cm.csv
 
 SRC ?= example.c
 LOGGER ?= fp-logger.cpp
@@ -29,10 +32,10 @@ EXE ?= example.exe example-logged.exe example-fpopt.exe
 all: $(EXE)
 
 example.cpp: $(SRC)
-	python3 fpopt-original-driver-generator.py $(SRC) "Pendulum"
+	python3 fpopt-original-driver-generator.py $(SRC) example
 
 example-logged.cpp: $(SRC)
-	python3 fpopt-logged-driver-generator.py $(SRC) "Pendulum"
+	python3 fpopt-logged-driver-generator.py $(SRC) example
 
 example.exe: example.cpp
 	$(CXX) -Wall -O3 example.cpp $(CXXFLAGS) -o $@

example/example.c

@@ -3,29 +3,19 @@
 #define TRUE 1
 #define FALSE 0
 
-// ## PRE t0: -2, 2
-// ## PRE w0: -5, 5
-// ## PRE N: 1000, 1000
-double Pendulum(double t0, double w0, double N) {
-	double h = 0.01;
-	double L = 2.0;
-	double m = 1.5;
-	double g = 9.80665;
-	double t = t0;
-	double w = w0;
-	double n = 0.0;
-	int tmp = n < N;
-	while (tmp) {
-		double k1w = (-g / L) * sin(t);
-		double k2t = w + ((h / 2.0) * k1w);
-		double t_1 = t + (h * k2t);
-		double k2w = (-g / L) * sin((t + ((h / 2.0) * w)));
-		double w_2 = w + (h * k2w);
-		double n_3 = n + 1.0;
-		t = t_1;
-		w = w_2;
-		n = n_3;
-		tmp = n < N;
-	}
-	return t;
+// ## PRE c: 1, 9
+// ## PRE a: 1, 9
+// ## PRE b: 1, 9
+double example(double a, double b, double c) {
+  double tmp;
+  if (a < b) {
+    tmp = sqrt(((((c + (b + a)) * (a - (c - b))) * (a + (c - b))) *
+                (c + (b - a)))) /
+          4.0;
+  } else {
+    tmp = sqrt(((((c + (a + b)) * (b - (c - a))) * (b + (c - a))) *
+                (c + (a - b)))) /
+          4.0;
+  }
+  return tmp;
 }