From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 17 Mar 2012 11:51:42 +0000 (+0000)
Subject: Changes to the C-interface. I forgot that C doesn't allow default arguments, this... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=afdb8be890f8819c092a588e35b6c2efed7bdd21;p=francis%2Fstp.git

Changes to the C-interface. I forgot that C doesn't allow default arguments, this rectifies the mistake, but will break any recently written code that uses the timeout functionality.

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 52cade4..d67a0f2 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -44,6 +44,11 @@ void vc_setFlags(VC vc, char c, int param_value) {
   process_argument(c, b);
 }
 
+void vc_setFlag(VC vc, char c) {
+  bmstar b = (bmstar)(((stpstar)vc)->bm);
+  process_argument(c, b);
+}
+
 void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value) {
     bmstar b = (bmstar)(((stpstar)vc)->bm);
     switch (f) {
@@ -435,7 +440,12 @@ void soft_time_out(int ignored)
  * the starting context.  If the result is false, then the resulting
  * context is a context in which e is false.  e must have Boolean
  * type. */
-int vc_query(VC vc, Expr e, int timeout_ms) {
+int vc_query(VC vc, Expr e)
+{
+  return vc_query_with_timeout(vc,e,-1);
+}
+
+int vc_query_with_timeout(VC vc, Expr e, int timeout_ms) {
   nodestar a = (nodestar)e;
   stpstar stp = ((stpstar)vc);
   bmstar b = (bmstar)(stp->bm);
diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 57f7921..62492a3 100644
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -48,7 +48,10 @@ extern "C" {
   // h  : help
   // s  : stats
   // v  : print nodes
+
+  // The "num_absrefine" argument isn't used at all. It's left for compatibility with existing code.
   void vc_setFlags(VC vc, char c, int num_absrefine _CVCL_DEFAULT_ARG(0));
+  void vc_setFlag(VC vc, char c);
 
   //! Interface-only flags.
   enum ifaceflag_t {
@@ -218,7 +221,12 @@ extern "C" {
   // and if the time has passed, then "timeout" will be returned. It's only checked
   // sometimes though, so the actual timeout may be larger. Cryptominisat doesn't check
   // the timeout yet..
-  int vc_query(VC vc, Expr e, int timeout_ms= -1);
+
+  // The C-language doesn't allow default arguments, so to get it compiling, I've split
+  // it into two functions.
+  int vc_query_with_timeout(VC vc, Expr e, int timeout_ms);
+  int vc_query(VC vc, Expr e);
+
 
   //! Return the counterexample after a failed query.
   Expr vc_getCounterExample(VC vc, Expr e);