From 4c6a3812ad67b6ad40237d43821d233a5be754d1 Mon Sep 17 00:00:00 2001
From: smccam <smccam@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 19 Mar 2010 02:23:59 +0000
Subject: [PATCH] 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
---
 src/c_interface/c_interface.cpp | 12 +++++++++++-
 src/c_interface/c_interface.h   |  9 +++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 363a9cb..cd5400f 100644
--- 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 c795c52..029907b 100644
--- 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,
-- 
2.47.3