examples: Enable FF examples when built with cocoa. (cvc5#10121)

ajreynol · Oct 25, 2023 · 2c862d3 · 2c862d3
1 parent f53fc5f
commit 2c862d3
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 16 deletions.
diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in
@@ -16,6 +16,7 @@
 set(CVC5_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@)
 set(CVC5_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@)
 set(CVC5_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@)
+set(CVC5_USE_COCOA @USE_COCOA@)
 
 if(NOT TARGET cvc5::cvc5)
   include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake)

diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
@@ -37,7 +37,7 @@ foreach(example ${CVC5_EXAMPLES_API})
   cvc5_add_example(${example} "" "api/cpp")
 endforeach()
 
-if(USE_COCOA)
+if(CVC5_USE_COCOA)
   cvc5_add_example(finite_field "" "api/cpp")
 endif()
 

diff --git a/examples/api/cpp/finite_field.cpp b/examples/api/cpp/finite_field.cpp
@@ -31,16 +31,17 @@ int main()
   Term b = solver.mkConst(f5, "b");
   Term z = solver.mkFiniteFieldElem("0", f5);
 
-  Term inv =
-      solver.mkTerm(EQUAL,
-                    {solver.mkTerm(FINITE_FIELD_ADD,
-                                   {solver.mkTerm(FINITE_FIELD_MULT, {a, b}),
-                                    solver.mkFiniteFieldElem("-1", f5)}),
-                     z});
-  Term aIsTwo = solver.mkTerm(
-      EQUAL,
-      {solver.mkTerm(FINITE_FIELD_ADD, {a, solver.mkFiniteFieldElem("-2", f5)}),
+  Term inv = solver.mkTerm(
+      Kind::EQUAL,
+      {solver.mkTerm(Kind::FINITE_FIELD_ADD,
+                     {solver.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}),
+                      solver.mkFiniteFieldElem("-1", f5)}),
        z});
+  Term aIsTwo =
+      solver.mkTerm(Kind::EQUAL,
+                    {solver.mkTerm(Kind::FINITE_FIELD_ADD,
+                                   {a, solver.mkFiniteFieldElem("-2", f5)}),
+                     z});
   // ab - 1 = 0
   solver.assertFormula(inv);
   // a = 2
@@ -54,10 +55,11 @@ int main()
   cout << "b = " << solver.getValue(b) << endl;
 
   // b = 2
-  Term bIsTwo = solver.mkTerm(
-      EQUAL,
-      {solver.mkTerm(FINITE_FIELD_ADD, {b, solver.mkFiniteFieldElem("-2", f5)}),
-       z});
+  Term bIsTwo =
+      solver.mkTerm(Kind::EQUAL,
+                    {solver.mkTerm(Kind::FINITE_FIELD_ADD,
+                                   {b, solver.mkFiniteFieldElem("-2", f5)}),
+                     z});
 
   // should be UNSAT, 2*2 - 1 != 0
   solver.assertFormula(bIsTwo);

diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
@@ -58,6 +58,6 @@ foreach(example ${EXAMPLES_API_JAVA})
   add_java_example(${example})
 endforeach()
 
-if(USE_COCOA)
+if(CVC5_USE_COCOA)
   add_java_example(FiniteField)
 endif()
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
@@ -63,6 +63,6 @@ foreach(example ${EXAMPLES_API_PYTHON})
   create_python_example(${example})
 endforeach()
 
-if(USE_COCOA)
+if(CVC5_USE_COCOA)
   create_python_example("finite_field")
 endif()