From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 18 Dec 2008 00:22:36 +0000 (+0000)
Subject: added parsing capability in c_interface
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cb9e1cbfa9e4c53108e56fd671f02aa2052d53ba;p=francis%2Fstp.git

added parsing capability in c_interface

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

diff --git a/c-api-tests/parsefile-using-cinterface.c b/c-api-tests/parsefile-using-cinterface.c
new file mode 100644
index 0000000..7f642c6
--- /dev/null
+++ b/c-api-tests/parsefile-using-cinterface.c
@@ -0,0 +1,18 @@
+//g++ -I$(HOME)/stp/c_interface print.c -L$(HOME)/stp/lib -lstp -o hex
+
+#include <stdio.h>
+#include "c_interface.h"
+
+int main() {
+  VC vc = vc_createValidityChecker();
+  vc_setFlags('n');
+  vc_setFlags('d');
+  vc_setFlags('p');
+
+  Expr c = vc_parseExpr(vc,"./t.cvc"); 
+  
+  vc_printExpr(vc, c);
+  printf("\n");
+  vc_Destroy(vc);
+}
+
diff --git a/c-api-tests/t.cvc b/c-api-tests/t.cvc
new file mode 100644
index 0000000..0a6f9f4
--- /dev/null
+++ b/c-api-tests/t.cvc
@@ -0,0 +1,132 @@
+__tmpInt8  : BITVECTOR(8);
+__tmpInt16  : BITVECTOR(16);
+__tmpInt32  : BITVECTOR(32);
+__tmpInt64  : BITVECTOR(64);
+arr665  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr667  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr676  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr680  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr684  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr671  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr694  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr698  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr702  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr689  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr712  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr716  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr720  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr707  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr724  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr732  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr736  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr740  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr727  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr750  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr754  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr758  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr745  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr769  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr773  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr777  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr764  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr666  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+arr82  : ARRAY BITVECTOR(32) OF BITVECTOR(8);
+%----------------------------------------------------
+ASSERT( (LET let_k_0 = (arr665[0hex00000003] @ (arr665[0hex00000002] @ (arr665[0hex00000001] @ arr665[0hex00000000])
+)
+)
+ IN 
+NOT((NOT(0hex00000001 = let_k_0
+) 
+ AND NOT(0hex00000000 = let_k_0
+) 
+
+)) 
+)  );
+ASSERT( SBVLT(0hex00000000,(arr665[0hex00000003] @ (arr665[0hex00000002] @ (arr665[0hex00000001] @ arr665[0hex00000000])
+)
+)
+)
+ );
+ASSERT( (LET let_k_0 = (arr667[0hex00000003] @ (arr667[0hex00000002] @ (arr667[0hex00000001] @ arr667[0hex00000000])
+)
+)
+ IN 
+NOT((NOT(0hex00000002 = let_k_0
+) 
+ AND (NOT(0hex00000001 = let_k_0
+) 
+ AND NOT(0hex00000000 = let_k_0
+) 
+
+)
+)) 
+)  );
+ASSERT( NOT(SBVLT(0hex00000000,(arr667[0hex00000003] @ (arr667[0hex00000002] @ (arr667[0hex00000001] @ arr667[0hex00000000])
+)
+)
+)
+) 
+ );
+ASSERT( NOT(0hex0000000000000000 = ((arr694[0hex0000005F] @ (arr694[0hex0000005E] @ (arr694[0hex0000005D] @ (arr694[0hex0000005C] @ (arr694[0hex0000005B] @ (arr694[0hex0000005A] @ (arr694[0hex00000059] @ arr694[0hex00000058])
+)
+)
+)
+)
+)
+)
+ & 0hex000000007FFFFFFF)
+) 
+ );
+ASSERT( BVLT((arr694[0hex00000037] @ (arr694[0hex00000036] @ (arr694[0hex00000035] @ arr694[0hex00000034])
+)
+)
+,0hex00010000)
+ );
+ASSERT( NOT(0hex0000000000000000 = ((arr698[0hex0000005F] @ (arr698[0hex0000005E] @ (arr698[0hex0000005D] @ (arr698[0hex0000005C] @ (arr698[0hex0000005B] @ (arr698[0hex0000005A] @ (arr698[0hex00000059] @ arr698[0hex00000058])
+)
+)
+)
+)
+)
+)
+ & 0hex000000007FFFFFFF)
+) 
+ );
+ASSERT( BVLT((arr698[0hex00000037] @ (arr698[0hex00000036] @ (arr698[0hex00000035] @ arr698[0hex00000034])
+)
+)
+,0hex00010000)
+ );
+ASSERT( NOT(0hex0000000000000000 = ((arr702[0hex0000005F] @ (arr702[0hex0000005E] @ (arr702[0hex0000005D] @ (arr702[0hex0000005C] @ (arr702[0hex0000005B] @ (arr702[0hex0000005A] @ (arr702[0hex00000059] @ arr702[0hex00000058])
+)
+)
+)
+)
+)
+)
+ & 0hex000000007FFFFFFF)
+) 
+ );
+ASSERT( BVLT((arr702[0hex00000037] @ (arr702[0hex00000036] @ (arr702[0hex00000035] @ arr702[0hex00000034])
+)
+)
+,0hex00010000)
+ );
+ASSERT( 0hex00000001 = (arr689[0hex00000003] @ (arr689[0hex00000002] @ (arr689[0hex00000001] @ arr689[0hex00000000])
+)
+)
+
+ );
+ASSERT( 0hex2D = arr666[0hex00000000]
+ );
+ASSERT( 0hex55 = arr666[0hex00000001]
+ );
+ASSERT( NOT(0hex00 = arr666[0hex00000002]
+) 
+ );
+ASSERT( NOT(0hex00 = arr666[0hex00000003]
+) 
+ );
+ASSERT( 0hex00 = arr666[0hex00000004]
+ );