Changes to the C-interface. I forgot that C doesn't allow default arguments, this...

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 52cade47d58ecdf3315a7f17b8d3a7ce65b80afc..d67a0f247b1515aa2d860c66b87edf612d46e837 100644 (file)
--- 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 57f7921d3e856e2ada03295f53bc1efd70ec21ea..62492a3b136e34f4541b096f64821f0c2e6ee969 100644 (file)
--- 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);