Refactored examples

usi-verification-and-security · Aug 18, 2024 · ce8ba63 · ce8ba63
1 parent 297cf27
commit ce8ba63
Show file tree

Hide file tree

Showing 8 changed files with 27 additions and 15 deletions.
diff --git a/examples/test1.cc b/examples/test1.cc
@@ -1,9 +1,11 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 int main()
 {
-    Logic logic{opensmt::Logic_t::QF_UF}; // UF Logic
+    Logic logic{Logic_t::QF_UF}; // UF Logic
     SMTConfig c;
     MainSolver mainSolver(logic, c, "test solver");
     PTRef v = logic.mkBoolVar("a");

diff --git a/examples/test2.cc b/examples/test2.cc
@@ -1,9 +1,11 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 int main()
 {
-    Logic logic{opensmt::Logic_t::QF_UF}; // UF Logic
+    Logic logic{Logic_t::QF_UF}; // UF Logic
     SMTConfig c;
     MainSolver mainSolver(logic, c, "test solver");
 

diff --git a/examples/test_arrays.cc b/examples/test_arrays.cc
@@ -7,6 +7,8 @@
 
 #include <opensmt/opensmt2.h>
 
+using namespace opensmt;
+
 void usingWrapper();
 void creatingComponentsDirectly();
 
@@ -54,7 +56,7 @@ void usingWrapper() {
 }
 
 void creatingComponentsDirectly() {
-    ArithLogic logic{opensmt::Logic_t::QF_ALIA};
+    ArithLogic logic{Logic_t::QF_ALIA};
     SMTConfig config;
     MainSolver mainSolver(logic, config, "ALIA solver");
 
@@ -79,5 +81,3 @@ void creatingComponentsDirectly() {
     else
         printf("error\n");
 }
-
-
diff --git a/examples/test_itp.cc b/examples/test_itp.cc
@@ -1,6 +1,8 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 Opensmt*
 pre()
 {
@@ -13,12 +15,12 @@ pre()
 
 int main()
 {
-    
+
     Opensmt* osmt = pre();
     SMTConfig& c = osmt->getConfig();
     MainSolver& mainSolver = osmt->getMainSolver();
     Logic& logic = osmt->getLogic();
-    
+
     // Let's build two assertions
 
     // First assertion (a /\ b)
@@ -64,7 +66,7 @@ int main()
     	// It can be converted to OpenSMT's representation via
 	    ipartitions_t mask = 0;
     	for(unsigned i = 0; i < part.size(); ++i)
-	    	opensmt::setbit(mask, part[i] + 1);
+	    	setbit(mask, part[i] + 1);
 
         std::vector<PTRef> itps;
         itp_context->getSingleInterpolant(itps, mask);

diff --git a/examples/test_lia.cc b/examples/test_lia.cc
@@ -5,6 +5,8 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 void usingWrapper();
 void creatingComponentsDirectly();
 
@@ -50,7 +52,7 @@ void usingWrapper() {
 }
 
 void creatingComponentsDirectly() {
-    ArithLogic logic{opensmt::Logic_t::QF_LIA};
+    ArithLogic logic{Logic_t::QF_LIA};
     SMTConfig config;
     MainSolver mainSolver(logic, config, "LIA solver");
 
@@ -76,5 +78,3 @@ void creatingComponentsDirectly() {
     else
         printf("error\n");
 }
-
-
diff --git a/examples/test_lra.cc b/examples/test_lra.cc
@@ -1,6 +1,8 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 Opensmt*
 pre()
 {

diff --git a/examples/test_lra_itp.cc b/examples/test_lra_itp.cc
@@ -1,6 +1,8 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 Opensmt*
 pre()
 {
@@ -13,14 +15,14 @@ pre()
 
 int main()
 {
-    
+
     Opensmt* osmt = pre();
     SMTConfig& c = osmt->getConfig();
     MainSolver& mainSolver = osmt->getMainSolver();
     auto & logic = osmt->getLRALogic();
 
     // Let's build two assertions
- 
+
     // Create vars
     PTRef x1 = logic.mkRealVar("x1");
     PTRef x2 = logic.mkRealVar("x2");
@@ -72,7 +74,7 @@ int main()
     	// It can be converted to OpenSMT's representation via
 	    ipartitions_t mask = 0;
     	for(unsigned i = 0; i < part.size(); ++i)
-	    	opensmt::setbit(mask, part[i] + 1);
+	    	setbit(mask, part[i] + 1);
 
         std::vector<PTRef> itps;
         itp_context->getSingleInterpolant(itps, mask);

diff --git a/examples/test_lra_value.cc b/examples/test_lra_value.cc
@@ -1,6 +1,8 @@
 #include <opensmt/opensmt2.h>
 #include <stdio.h>
 
+using namespace opensmt;
+
 Opensmt*
 pre()
 {
@@ -105,7 +107,7 @@ int main()
 	    ipartitions_t mask = 0;
 
         for(unsigned i = 0; i < part.size(); ++i)
-	    	opensmt::setbit(mask, part[i] + 1);
+	    	setbit(mask, part[i] + 1);
 
         std::vector<PTRef> itps;
         itp_context->getSingleInterpolant(itps, mask);