Add more destructors to the C interface, to help clients avoid memory

leaks. And fix a type so that linking works correctly.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@649 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 363a9cbaf33e654af0d8bab944dd4b457cf01176..cd5400fa6e789306358a17f670122197b48954cc 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -276,6 +276,10 @@ void vc_printVarDecls(VC vc) {
   vc_printVarDeclsToStream(vc, cout);
 }
 
+void vc_clearDecls(VC vc) {
+  decls->clear();
+}
+
 static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   BEEV::ASTVec v = b->GetAsserts();
@@ -611,7 +615,7 @@ WholeCounterExample vc_getWholeCounterExample(VC vc) {
   return c;
 }
 
-Expr vc_getTermFromCounterExample(VC vc, Expr e, CompleteCEStar cc) {
+Expr vc_getTermFromCounterExample(VC vc, Expr e, WholeCounterExample cc) {
   //bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar n = (nodestar)e;
   CompleteCEStar c = (CompleteCEStar)cc;
@@ -620,6 +624,12 @@ Expr vc_getTermFromCounterExample(VC vc, Expr e, CompleteCEStar cc) {
   return output;
 }
 
+void vc_deleteWholeCounterExample(WholeCounterExample cc) {
+  CompleteCEStar c = (CompleteCEStar)cc;
+
+  delete c;
+}
+
 int vc_getBVLength(VC vc, Expr ex) {
   nodestar e = (nodestar)ex;
 

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index c795c52cca013dd4b6fbd65a734a29885215db6f..029907bf1d074029ece526fbbc438eeec9708516 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -146,6 +146,11 @@ extern "C" {
   //! Prints variable declarations to stdout.
   void vc_printVarDecls(VC vc);
 
+  //! Clear the internal list of variables to declare maintained for
+  //  vc_printVarDecls. Do this after you've printed them, or if you
+  //  never want to print them, to prevent a memory leak.
+  void vc_clearDecls(VC vc);
+
   //! Prints asserts to stdout. The flag simplify_print must be set to
   //"1" if you wish simplification to occur dring printing. It must be
   //set to "0" otherwise
@@ -319,6 +324,10 @@ extern "C" {
   //Get the value of a term expression from the CounterExample
   Expr vc_getTermFromCounterExample(VC vc, Expr e, WholeCounterExample c);
 
+
+  // Free the return value of vc_getWholeCounterExample
+  void vc_deleteWholeCounterExample(WholeCounterExample cc);
+
   //Kinds of Expr
   enum exprkind_t{
       UNDEFINED,