some examples for miniBDD

Author: kroening

src/solvers/miniBDD/example.cpp

@@ -0,0 +1,52 @@
+#include <iostream>
+
+#include "miniBDD.h"
+
+int main()
+{
+  miniBDD::mgr mgr;
+  miniBDD::BDD result;
+
+  #if 0
+  {
+    auto x=mgr.Var("x");
+    auto y=mgr.Var("y");
+    auto z=mgr.Var("z");
+    result=x | (y & z);
+  }
+  #elif 0
+  {
+    auto y=mgr.Var("y");
+    auto x=mgr.Var("x");
+    auto z=mgr.Var("z");
+    result=x | (y & z);
+  }
+  #elif 0
+  {
+    auto x1=mgr.Var("x_1");
+    auto x2=mgr.Var("x_2");
+    auto x3=mgr.Var("x_3");
+    auto x4=mgr.Var("x_4");
+    result=(x1&x2)|(x3&x4);
+  }
+  #elif 0
+  {
+    auto x1=mgr.Var("x_1");
+    auto x2=mgr.Var("x_2");
+    auto x3=mgr.Var("x_3");
+    auto x4=mgr.Var("x_4");
+    auto tmp=(x1&x2)|(x3&x4);
+    result=restrict(tmp, x2.var(), 0);
+  }
+  #else
+  {
+    auto a=mgr.Var("a");
+    auto b=mgr.Var("b");
+    auto f=!a|b;
+    auto fp=!b;
+    result=f==fp;
+  }
+  #endif
+
+  mgr.DumpTikZ(std::cout);
+}