added symbolic link in include/stp/c_interface.h to the appropriate c_interface.h

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

diff --git a/AUTHORS b/AUTHORS
index 25cfc3c3b74c280019e80787b17d032f2c392824..7f5368ed81c133baf415393ce5ed1a88729c4c39 100644 (file)
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,5 +1,3 @@
-
-
 /********************************************************************
  * PROGRAM NAME: STP (Simple Theorem Prover)   
  *             
@@ -10,31 +8,32 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 
-
-Primary Author
---------------
-Vijay Ganesh, Stanford University, Stanford, CA, USA (Nov, 2005 to 2007),
-MIT, Cambridge, MA, USA (Oct, 2007 to present)
+Primary Author and Project Leader
+---------------------------------
+* Vijay Ganesh, 
+  Stanford University, Stanford, CA, USA (Nov, 2005 to 2007),
+  MIT, Cambridge, MA, USA (Oct, 2007 to present)
 
 
 Other Significant Author
 ------------------------
-Trevor Alexander Hansen, University of Melbourne, Australia (Sep, 2008 - present)
+* Trevor Alexander Hansen, 
+  University of Melbourne, Australia (Sep, 2008 - present)
 
 
 Authors who contributed some code
 ---------------------------------------
-Michael Katelman, University of Illinois, Urbana-Champaign, USA (July - Oct, 2008)
-David L. Dill, Stanford University, Stanford, CA, USA (Nov - Dec, 2005)
-Tim King, Stanford University, Stanford, CA, USA (July - Sep, 2007)
-Philip Guo, Stanford University, Stanford, CA, USA (Dec 2008 - Jan 2009)
+* Michael Katelman, 
+  University of Illinois, Urbana-Champaign, USA (July - Oct, 2008)
 
+* David L. Dill, 
+  Stanford University, Stanford, CA, USA (Nov - Dec, 2005)
 
-Following authors provided some code to Makefiles and configuration scripts
----------------------------------------------------------------------------
-Cristian Cadar, Stanford University, Stanford, CA, USA
-Paul Twohey, Stanford University, Stanford, CA, USA
-Sergey Berezin, ATG Synopsys, Mountain View, CA, USA
-Clark Barrett, New York University, New York, NY, USA
+* Tim King, 
+  Stanford University, Stanford, CA, USA (July - Sep, 2007)
 
+* Philip Guo, 
+  Stanford University, Stanford, CA, USA (Dec 2008)
 
+* Mate Soos,
+  Paris University 6, Paris, France (Nov 2009 - present)

diff --git a/include/stp/c_interface.h b/include/stp/c_interface.h
new file mode 120000 (symlink)
index 0000000..68bfb2e
--- /dev/null
+++ b/include/stp/c_interface.h
@@ -0,0 +1 @@
+../../src/c_interface/c_interface.h
\ No newline at end of file

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index c2e443d63a3f85c6d1e94d92c5bbe891b9528d85..2bf9ad9743aa48260695ff01968452b99bc29e0f 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -940,6 +940,14 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
 
   delete $1;
 }
+/* |      Expr BVRIGHTSHIFT_TOK Expr */
+/* { */
+/*   //$1 is being shifted by variable shift amount $3 */
+/*   // */
+
+/*   delete $1; */
+/*   delete $3; */
+/* } */
 |      BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' 
 {
   ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, $3, *$5));