added functionality for converting CVC to C code

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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index 2ecff2f19c3b219cb1251216be04b50d4ccf53a8..f607c1eca986656d2dba599ac3b9268e4b92e85c 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -8,6 +8,9 @@
 // -*- c++ -*-
 
 #include "AST.h"
+
+#include <assert.h>
+
 namespace BEEV {
   //some global variables that are set through commandline options. it
   //is best that these variables remain global. Default values set
@@ -682,6 +685,498 @@ namespace BEEV {
     }
   } //end of PL_Print1()
 
+
+  // printer for C code (copied from PL_Print())
+  // TODO: this does not fully implement printing of all of the STP
+  // language - FatalError calls inserted for unimplemented
+  // functionality, e.g.,:
+  //   FatalError("C_Print1: printing not implemented for this kind: ",*this);
+
+  //two pass algorithm: 
+  //
+  //1. In the first pass, letize this Node, N: i.e. if a node
+  //1. appears more than once in N, then record this fact.
+  //
+  //2. In the second pass print a "global let" and then print N
+  //2. as follows: Every occurence of a node occuring more than
+  //2. once is replaced with the corresponding let variable.
+  ostream& ASTNode::C_Print(ostream &os,
+                            int indentation) const {
+    // Clear the PrintMap
+    BeevMgr& bm = GetBeevMgr(); 
+    bm.PLPrintNodeSet.clear();
+    bm.NodeLetVarMap.clear();
+    bm.NodeLetVarVec.clear();
+    bm.NodeLetVarMap1.clear();
+
+    //pass 1: letize the node
+    LetizeNode();
+
+    unsigned int lower, upper, num_bytes = 0;
+
+    //pass 2: 
+    //
+    //2. print all the let variables and their counterpart expressions
+    //2. as follows (LET var1 = expr1, var2 = expr2, ...
+    //
+    //3. Then print the Node itself, replacing every occurence of
+    //3. expr1 with var1, expr2 with var2, ...
+    //os << "(";
+    if(0 < bm.NodeLetVarMap.size()) {
+      //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
+      //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
+      std::vector<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
+      std::vector<pair<ASTNode,ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+
+      // start a new block to create new static scope
+      os << "{" << endl;
+
+      for(;it!=itend;it++) {
+
+        // see if it's a BVEXTRACT, and if so, whether it's multi-byte
+        if (it->second.GetKind() == BVEXTRACT) {
+          upper = GetUnsignedConst(it->second.GetChildren()[1]);
+          lower = GetUnsignedConst(it->second.GetChildren()[2]);
+          num_bytes = (upper - lower + 1) / 8;
+          assert(num_bytes > 0);
+        }
+
+        //print the let var first
+        if (num_bytes > 1) {
+          // for multi-byte assignment, use 'memcpy' and array notation
+          os << "unsigned char ";
+          it->first.C_Print1(os,indentation,false);
+          os << "[" << num_bytes << "]; ";
+          os << "memcpy(";
+          it->first.C_Print1(os,indentation,false);
+          os << ", ";
+          //print the expr
+          it->second.C_Print1(os,indentation,false);
+          os << ", " << num_bytes << ");";
+        }
+        else {
+          // for single-byte assignment, use '='
+          os << "unsigned char ";
+          it->first.C_Print1(os,indentation,false);
+          os << " = ";
+          //print the expr
+          it->second.C_Print1(os,indentation,false);
+          os << ";" << endl;
+        }
+
+        //update the second map for proper printing of LET
+        bm.NodeLetVarMap1[it->second] = it->first;
+      }
+    
+      os << endl << "stp_assert ";
+      C_Print1(os,indentation, true);
+
+      os << ";" << endl << "}";
+    }
+    else {
+      os << "stp_assert ";
+      C_Print1(os,indentation, false);
+      os << ";";
+    }
+    //os << " )";
+    //os << " ";
+
+    return os;
+  } //end of C_Print()
+
+  // helper function for printing C code (copied from PL_Print1())
+  void ASTNode::C_Print1(ostream& os,
+                         int indentation, 
+                         bool letize) const {
+
+    unsigned int upper, lower, num_bytes;
+    Kind LHSkind, RHSkind;
+
+    //os << spaces(indentation);
+    //os << endl << spaces(indentation);
+    if (!IsDefined()) {
+      os << "<undefined>";
+      return;
+    }
+    
+    //if this node is present in the letvar Map, then print the letvar
+    BeevMgr &bm = GetBeevMgr();
+
+    //this is to print letvars for shared subterms inside the printing
+    //of "(LET v0 = term1, v1=term1@term2,...
+    if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) {
+      (bm.NodeLetVarMap1[*this]).C_Print1(os,indentation,letize);
+      return;
+    }
+
+    //this is to print letvars for shared subterms inside the actual
+    //term to be printed
+    if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) {
+      (bm.NodeLetVarMap[*this]).C_Print1(os,indentation,letize);
+      return;
+    }
+    
+    //otherwise print it normally
+    Kind kind = GetKind();
+    const ASTVec &c = GetChildren();     
+    switch(kind) {
+    case BVGETBIT:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this);
+      c[0].C_Print1(os,indentation,letize);
+      os << "{";
+      c[1].C_Print1(os,indentation,letize);
+      os << "}";
+      break;
+    case BITVECTOR:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this);
+      os << "BITVECTOR(";
+      unsigned char * str;
+      str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
+      os << str << ")";
+      CONSTANTBV::BitVector_Dispose(str);
+      break;
+    case BOOLEAN:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this);
+      os << "BOOLEAN";
+      break;
+    case FALSE:
+      os << "0";
+      break;
+    case TRUE:
+      os << "1";
+      break;
+    case BVCONST:
+    case SYMBOL:
+      // print in C friendly format:
+      _int_node_ptr->nodeprint(os, true); 
+      break;
+    case READ:
+      c[0].C_Print1(os, indentation,letize);
+      os << "[";
+      c[1].C_Print1(os,indentation,letize);
+      os << "]";
+      break;
+    case WRITE:
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " WITH [";
+      c[1].C_Print1(os,indentation,letize);
+      os << "] := ";
+      c[2].C_Print1(os,indentation,letize);
+      os << ")";
+      os << endl;
+      break;
+    case BVUMINUS:
+      os << kind << "( ";
+      c[0].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case NOT:
+      os << "!(";
+      c[0].C_Print1(os,indentation,letize);
+      os << ") " << endl;
+      break;
+    case BVNEG:
+      os << " ~(";
+      c[0].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVCONCAT:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " @ ";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")" << endl;
+      break;
+    case BVOR:
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " | ";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVAND:
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " & ";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVEXTRACT:
+
+      // we only accept indices that are byte-aligned
+      // (e.g., [15:8], [23:16])
+      // and round down to byte indices rather than bit indices
+      upper = GetUnsignedConst(c[1]);
+      lower = GetUnsignedConst(c[2]);
+      assert(upper > lower);
+      assert(lower % 8 == 0);
+      assert((upper + 1) % 8 == 0);
+      num_bytes = (upper - lower + 1) / 8;
+      assert (num_bytes > 0);
+
+      // for multi-byte extraction, use the ADDRESS
+      if (num_bytes > 1) {
+        os << "&";
+        c[0].C_Print1(os,indentation,letize);
+        os << "[" << lower / 8 << "]";
+      }
+      // for single-byte extraction, use the VALUE
+      else {
+        c[0].C_Print1(os,indentation,letize);
+        os << "[" << lower / 8 << "]";
+      }
+
+      break;
+    case BVLEFTSHIFT:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " << ";
+      os << GetUnsignedConst(c[1]);
+      os << ")";
+      break;
+    case BVRIGHTSHIFT:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << " >> ";
+      os << GetUnsignedConst(c[1]);
+      os << ")";
+      break;
+    case BVMULT:
+    case BVSUB:
+    case BVPLUS:
+    case SBVDIV:      
+    case SBVREM:
+    case BVDIV:      
+    case BVMOD:
+      os << kind << "(";
+      os << this->GetValueWidth();
+      for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) {
+       os << ", " << endl;
+       it->C_Print1(os,indentation,letize);    
+      }
+      os << ")" << endl;
+      break;    
+    case ITE:
+      os << "if (";
+      c[0].C_Print1(os,indentation,letize);
+      os << ")" << endl;
+      os << "{";
+      c[1].C_Print1(os,indentation,letize);
+      os << endl << "} else {";
+      c[2].C_Print1(os,indentation,letize);
+      os << endl << "}";
+      break;
+    case BVLT:
+      // convert to UNSIGNED before doing comparison!
+      os << "((unsigned char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " < ";
+      os << "(unsigned char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVLE:
+      // convert to UNSIGNED before doing comparison!
+      os << "((unsigned char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " <= ";
+      os << "(unsigned char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVGT:
+      // convert to UNSIGNED before doing comparison!
+      os << "((unsigned char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " > ";
+      os << "(unsigned char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVGE:
+      // convert to UNSIGNED before doing comparison!
+      os << "((unsigned char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " >= ";
+      os << "(unsigned char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVXOR:
+    case BVNAND:
+    case BVNOR:
+    case BVXNOR:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      break;
+    case BVSLT:
+      // convert to SIGNED before doing comparison!
+      os << "((signed char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " < ";
+      os << "(signed char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVSLE:
+      // convert to SIGNED before doing comparison!
+      os << "((signed char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " <= ";
+      os << "(signed char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVSGT:
+      // convert to SIGNED before doing comparison!
+      os << "((signed char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " > ";
+      os << "(signed char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case BVSGE:
+      // convert to SIGNED before doing comparison!
+      os << "((signed char)";
+      c[0].C_Print1(os,indentation,letize);
+      os << " >= ";
+      os << "(signed char)";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      break;
+    case EQ:
+      // tricky tricky ... if it's a single-byte comparison,
+      // simply do ==, but if it's multi-byte, must do memcmp
+      LHSkind = c[0].GetKind();
+      RHSkind = c[1].GetKind();
+
+      num_bytes = 0;
+
+      // try to figure out whether it's a single-byte or multi-byte
+      // comparison
+      if (LHSkind == BVEXTRACT) {
+        upper = GetUnsignedConst(c[0].GetChildren()[1]);
+        lower = GetUnsignedConst(c[0].GetChildren()[2]);
+        num_bytes = (upper - lower + 1) / 8;
+      }
+      else if (RHSkind == BVEXTRACT) {
+        upper = GetUnsignedConst(c[1].GetChildren()[1]);
+        lower = GetUnsignedConst(c[1].GetChildren()[2]);
+        num_bytes = (upper - lower + 1) / 8;
+      }
+
+      if (num_bytes > 1) {
+        os << "(memcmp(";
+        c[0].C_Print1(os,indentation,letize);
+        os << ", ";
+        c[1].C_Print1(os,indentation,letize);      
+        os << ", ";
+        os << num_bytes;
+        os << ") == 0)";
+      }
+      else if (num_bytes == 1) {
+        os << "(";
+        c[0].C_Print1(os,indentation,letize);
+        os << " == ";
+        c[1].C_Print1(os,indentation,letize);      
+        os << ")";
+      }
+      else {
+        FatalError("C_Print1: ugh problem in implementing ==");
+      }
+
+      break;
+    case NEQ:
+      c[0].C_Print1(os,indentation,letize);
+      os << " != ";
+      c[1].C_Print1(os,indentation,letize);      
+      os << endl;
+      break;
+    case AND:
+    case OR:
+    case NAND:
+    case NOR:
+    case XOR: {
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      ASTVec::const_iterator it=c.begin();
+      ASTVec::const_iterator itend=c.end();
+
+      it++;
+      for(;it!=itend;it++) {
+        switch (kind) {
+          case AND:
+            os << " && ";
+            break;
+          case OR:
+            os << " || ";
+            break;
+          case NAND:
+            FatalError("unsupported boolean type in C_Print1");
+            break;
+          case NOR:
+            FatalError("unsupported boolean type in C_Print1");
+            break;
+          case XOR: 
+            FatalError("unsupported boolean type in C_Print1");
+            break;
+          default:
+            FatalError("unsupported boolean type in C_Print1");
+        }
+        it->C_Print1(os,indentation,letize);
+      }
+      os << ")";
+      break;
+    }
+    case IFF:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      os << "(";
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << ")";
+      os << " <=> ";
+      os << "(";
+      c[1].C_Print1(os,indentation,letize);      
+      os << ")";
+      os << ")";
+      os << endl;
+      break;
+    case IMPLIES:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+      os << "(";
+      os << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << ")";
+      os << " => ";
+      os << "(";
+      c[1].C_Print1(os,indentation,letize);
+      os << ")";
+      os << ")";
+      os << endl;
+      break;
+    case BVSX:
+      FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
+
+      os << kind << "(";
+      c[0].C_Print1(os,indentation,letize);
+      os << ",";
+      os << this->GetValueWidth();
+      os << ")" << endl;
+      break;
+    default:
+      //remember to use LispPrinter here. Otherwise this function will
+      //go into an infinite loop. Recall that "<<" is overloaded to
+      //the lisp printer. FatalError uses lispprinter
+      FatalError("C_Print1: printing not implemented for this kind: ",*this);
+      break;
+    }
+  } //end of C_Print1()
+
+
   ////////////////////////////////////////////////////////////////
   //  BeevMgr members
   ////////////////////////////////////////////////////////////////

diff --git a/AST/AST.h b/AST/AST.h
index 56dde97a32f84a3d9d013dc54fff13ac9cc2cef1..adcce5eae1aa88d7638e5e14a810e99a21cb9d81 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -295,6 +295,11 @@ namespace BEEV {
 
     void PL_Print1(ostream &os, int indentation = 0, bool b = false) const;
 
+    // C code printer
+    ostream& C_Print(ostream &os, int indentation = 0) const;
+    void C_Print1(ostream &os, int indentation = 0, bool b = false) const;
+
+
     //Construct let variables for shared subterms
     void LetizeNode(void) const;
 
@@ -461,7 +466,8 @@ namespace BEEV {
     virtual ~ASTInternal();
 
     // Abstract virtual print function for internal node.
-    virtual void nodeprint(ostream& os) { os << "*"; };
+    // (c_friendly is for printing hex. numbers that C compilers will accept)
+    virtual void nodeprint(ostream& os, bool c_friendly = false) { os << "*"; };
   }; //End of Class ASTInternal
 
   // FIXME: Should children be only in interior node type?
@@ -506,7 +512,8 @@ namespace BEEV {
 
     // Returns kinds.  "lispprinter" handles printing of parenthesis
     // and childnodes.
-    virtual void nodeprint(ostream& os) {
+    // (c_friendly is for printing hex. numbers that C compilers will accept)
+    virtual void nodeprint(ostream& os, bool c_friendly = false) {
       os << _kind_names[_kind];
     }
     public:
@@ -574,7 +581,8 @@ namespace BEEV {
     const char * const GetName() const{return _name;}  
 
     // Print function for symbol -- return name */
-    virtual void nodeprint(ostream& os) { os << _name;}
+    // (c_friendly is for printing hex. numbers that C compilers will accept)
+    virtual void nodeprint(ostream& os, bool c_friendly = false) { os << _name;}
 
     // Call this when deleting a node that has been stored in the
     // the unique table
@@ -652,16 +660,27 @@ namespace BEEV {
     virtual void CleanUp();
 
     // Print function for bvconst -- return _bvconst value in bin format
-    virtual void nodeprint(ostream& os) {
+    // (c_friendly is for printing hex. numbers that C compilers will accept)
+    virtual void nodeprint(ostream& os, bool c_friendly = false) {
       unsigned char *res;
       const char *prefix;
 
       if (_value_width%4 == 0) {
         res = CONSTANTBV::BitVector_to_Hex(_bvconst);
-        prefix = "0hex";
+        if (c_friendly) {
+          prefix = "0x";
+        }
+        else {
+          prefix = "0hex";
+        }
       } else {      
         res = CONSTANTBV::BitVector_to_Bin(_bvconst);
-        prefix = "0bin";
+        if (c_friendly) {
+          prefix = "0b";
+        }
+        else {
+          prefix = "0bin";
+        }
       }
       if (NULL == res) {
         os << "nodeprint: BVCONST : could not convert to string" << _bvconst;
@@ -774,7 +793,7 @@ namespace BEEV {
     }
 
     // Print function for bvconst -- return _bvconst value in binary format
-    virtual void nodeprint(ostream& os) {
+    virtual void nodeprint(ostream& os, bool c_friendly = false) {
       string s = "0bin";
       unsigned long long int bitmask = 0x8000000000000000LL;
       bitmask = bitmask >> (64-_value_width);

diff --git a/README b/README
index 7aa371dd42880a671a8ce44279b68b2a72f06525..ae2a16eafe517c4a3d187860ab5b507fd4a3db0f 100644 (file)
--- a/README
+++ b/README
@@ -22,6 +22,7 @@ Others Who Have Contributed Some Code
 David L. Dill, Stanford University, Stanford, CA, USA (Nov - Dec, 2005)
 Michael Katelman, University of Illinois, Urbana-Champaign, USA (July - Oct, 2008)
 Tim King, Stanford University, Stanford, CA, USA (July - Sep, 2007)
+Philip Guo, Stanford University, Stanford, CA, USA (Dec 2008, Jan 2009)
 
 
 Makefiles and configuration scripts

diff --git a/c-api-tests/cvc-to-c.cpp b/c-api-tests/cvc-to-c.cpp
new file mode 100644 (file)
index 0000000..1b0db4f
--- /dev/null
+++ b/c-api-tests/cvc-to-c.cpp
@@ -0,0 +1,28 @@
+/*
+
+Take a .cvc file specified by argv[1] and transform to C code
+
+g++ -I$HOME/stp/c_interface cvc-to-c.cpp -L$HOME/stp/lib -lstp -o cvc-to-c
+
+*/
+
+#include "c_interface.h"
+#include <iostream>
+
+using namespace std;
+
+int main(int argc, char** argv) {
+  VC vc = vc_createValidityChecker();
+
+  //vc_setFlags('n');
+  //vc_setFlags('d');
+  //vc_setFlags('p');
+
+  Expr c = vc_parseExpr(vc, argv[1]);
+
+  vc_printExprCCode(vc, c);
+
+  vc_Destroy(vc);
+  return 0;
+}
+

diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp
index 631179c69a856a12ad479443cdfd47789b847547..518268081f4c62cd26ec2c9c7d6c4870ae6c1e0b 100644 (file)
--- a/c_interface/c_interface.cpp
+++ b/c_interface/c_interface.cpp
@@ -26,7 +26,7 @@ bool cinterface_exprdelete_on = false;
 
 /* GLOBAL FUNCTION: parser
  */
-extern int yyparse();
+extern int cvcparse();
 
 void vc_setFlags(char c) {
   std::string helpstring = "Usage: stp [-option] [infile]\n\n";
@@ -134,6 +134,34 @@ void vc_printExpr(VC vc, Expr e) {
   q.PL_Print(cout);
 }
 
+// prints Expr 'e' to stdout as C code
+void vc_printExprCCode(VC vc, Expr e) {
+  BEEV::ASTNode q = (*(nodestar)e);
+
+  // print variable declarations
+  BEEV::ASTVec declsFromParser = (nodelist)BEEV::globalBeevMgr_for_parser->_special_print_set;
+
+  for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) {
+    if(BEEV::BITVECTOR_TYPE == it->GetType()) {
+      const char* name = it->GetName();
+      unsigned int bitWidth = it->GetValueWidth();
+      assert(bitWidth % 8 == 0);
+      unsigned int byteWidth = bitWidth / 8;
+      cout << "unsigned char " << name << "[" << byteWidth << "];" << endl;
+    }
+    else {
+      // vc_printExprCCode: unsupported decl. type
+      assert(0);
+    }
+  }
+
+  cout << endl;
+
+  // print constraints and assert
+  q.C_Print(cout);
+}
+
+
 void vc_printExprFile(VC vc, Expr e, int fd) {
   fdostream os(fd);
   ((nodestar)e)->PL_Print(os);
@@ -1409,11 +1437,11 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) {
 
 Expr vc_parseExpr(VC vc, char* infile) {
   bmstar b = (bmstar)vc;
-  extern FILE* yyin;
+  extern FILE* cvcin;
   const char * prog = "stp";
   
-  yyin = fopen(infile,"r");
-  if(yyin == NULL) {
+  cvcin = fopen(infile,"r");
+  if(cvcin == NULL) {
     fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
     BEEV::FatalError("");
   }
@@ -1426,7 +1454,7 @@ Expr vc_parseExpr(VC vc, char* infile) {
     return 0;
   }
 
-  yyparse();
+  cvcparse();
   nodelist aaa = b->GetAsserts();
   node o =  b->CreateNode(BEEV::AND,aaa);
   

diff --git a/c_interface/c_interface.h b/c_interface/c_interface.h
index b6a1e78c3c8818e160f3ff2e049b5c59c5587ee5..35afbd6388fbf916d4b3a8a92a0d13a6baf9a0a1 100644 (file)
--- a/c_interface/c_interface.h
+++ b/c_interface/c_interface.h
@@ -117,6 +117,9 @@ extern "C" {
   //! Prints 'e' to stdout.
   void vc_printExpr(VC vc, Expr e);
 
+  //! Prints 'e' to stdout as C code
+  void vc_printExprCCode(VC vc, Expr e);
+
   //! Prints 'e' into an open file descriptor 'fd'
   void vc_printExprFile(VC vc, Expr e, int fd);