From 14854bc7f688f8db6849b7aaa8e02c816310c824 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 26 Nov 2009 19:22:52 +0000
Subject: [PATCH] Significant good changes to SAT makefiles by Mate. Issues
 with STP library creation. Now Fixed.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@428 e59a4935-1847-0410-ae03-e826735625c1
---
 src/parser/CVC.y               | 64 ++++++++++++++++++++++++++++++++++
 src/sat/Makefile               |  5 ---
 src/sat/core/Makefile          |  3 +-
 src/sat/cryptominisat/Makefile |  3 +-
 src/sat/simp/Makefile          |  3 +-
 src/sat/unsound/Makefile       | 27 ++++++++------
 6 files changed, 87 insertions(+), 18 deletions(-)

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index aad561c..e9c1873 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -919,6 +919,70 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
   $$ = n;
   delete $1;
 }
+/* |      Expr BVLEFTSHIFT_TOK Expr */
+/* { */
+/*   // VARIABLE LEFT SHIFT */
+/*   // */
+/*   // $1 (THEEXPR) is being shifted */
+/*   // */
+/*   // $3 is the variable shift amount */
+/*   ASTNode inputExpr = *$1; */
+/*   ASTNode varShiftAmt = *$3; */
+
+/*   unsigned int exprWidth = $1->GetValueWidth(); */
+/*   unsigned int shiftAmtWidth = $3->GetValueWidth(); */
+/*   ASTNode exprWidthNode = ParserBM->CreateBVConst(shiftAmtWidth, exprWidth); */
+  
+/*   ASTNode cond, thenExpr, elseExpr; */
+/*   unsigned int count = 0; */
+/*   while(count < exprWidth) */
+/*     { */
+/*       if(0 == count) */
+/* 	{ */
+/* 	  // if count is zero then the appropriate rightshift expression is */
+/* 	  // THEEXPR itself */
+/* 	  elseExpr = inputExpr; */
+/* 	} */
+/*       else */
+/* 	{ */
+/* 	  // 1 <= count < exprWidth */
+/* 	  // */
+/* 	  // Construct appropriate conditional */
+/* 	  ASTNode countNode = ParserBM->CreateBVConst(shiftAmtWidth, count); */
+/* 	  cond = ParserBM->CreateNode(EQ, countNode, varShiftAmt); */
+
+/* 	  //Construct the rightshift expression padding @ Expr[hi:low] */
+/* 	  ASTNode low = */
+/* 	    ParserBM->CreateBVConst(32,count); */
+/* 	  ASTNode extract = */
+/* 	    ParserBM->CreateTerm(BVEXTRACT,exprWidth-count,inputExpr,hi,low); */
+/* 	  ASTNode padding = */
+/* 	    ParserBM->CreateZeroConst(count); */
+/* 	  thenExpr = */
+/* 	    ParserBM->CreateTerm(BVCONCAT, exprWidth, padding, extract); */
+/* 	  ASTNode ite = */
+/* 	    ParserBM->CreateTerm(ITE, exprWidth, cond, thenExpr, elseExpr); */
+/* 	  BVTypeCheck(ite); */
+/* 	  elseExpr = ite; */
+/* 	} */
+/*       count++; */
+/*     } //End of while loop */
+
+/*   // if shiftamount is greater than or equal to exprwidth, then */
+/*   // output is zero. */
+/*   cond = ParserBM->CreateNode(BVGE, varShiftAmt, exprWidthNode); */
+/*   thenExpr = ParserBM->CreateZeroConst(exprWidth); */
+/*   ASTNode * ret = */
+/*     new ASTNode(ParserBM->CreateTerm(ITE, */
+/* 				     exprWidth, */
+/* 				     cond, thenExpr, elseExpr)); */
+/*   BVTypeCheck(*ret); */
+/*   //cout << *ret; */
+
+/*   $$ = ret; */
+/*   delete $1; */
+/*   delete $3; */
+/* } */
 |      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK
 {
   ASTNode len = ParserBM->CreateZeroConst($3);
diff --git a/src/sat/Makefile b/src/sat/Makefile
index f4524d9..28d11ff 100644
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -1,21 +1,16 @@
 .PHONY: core
 core:
 	$(MAKE) -C core lib all	
-	mv Solver.or Solver.o
 
 .PHONY: simp
 simp:
 	$(MAKE) -C core lib all	
-	mv Solver.or Solver.o
 	$(MAKE) -C simp lib all
-	mv SimpSolver.or SimpSolver.o
 
 .PHONY: unsound
 unsound:
 	$(MAKE) -C core lib all	
-	mv Solver.or Solver.o
 	$(MAKE) -C unsound lib all
-	mv UnsoundSimpSolver.or UnsoundSimpSolver.o
 
 .PHONY: cryptominisat
 cryptominisat:
diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index c36465f..6e0e967 100644
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -15,9 +15,10 @@ $(LIB): $(OBJECTS)
 	rm -f $@
 	ar cq $@ $(OBJECTS)
 	cp $(LIB) ../
+	cp $(OBJECTS) ../
 
 clean:
-	rm $(OBJECTS) $(LIB) ../$(LIB)
+	rm -f $(OBJECTS) $(LIB)
 
 .C.o:
 	$(CC) $(CFLAGS) $< -o $@
diff --git a/src/sat/cryptominisat/Makefile b/src/sat/cryptominisat/Makefile
index 8ae59c5..c42131e 100644
--- a/src/sat/cryptominisat/Makefile
+++ b/src/sat/cryptominisat/Makefile
@@ -15,9 +15,10 @@ $(LIB): $(OBJECTS)
 	rm -f $@
 	ar cq $@ $(OBJECTS)
 	cp $(LIB) ../
+	cp $(OBJECTS) ../
 
 clean:
-	rm $(OBJECTS) $(LIB) ../$(LIB)
+	rm -f $(OBJECTS) $(LIB)
 
 .cpp.o:
 	$(CC) $(CFLAGS) $< -o $@
diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile
index 9e2a508..1ba50ea 100644
--- a/src/sat/simp/Makefile
+++ b/src/sat/simp/Makefile
@@ -15,9 +15,10 @@ $(LIB): $(OBJECTS)
 	rm -f $@
 	ar cq $@ $(OBJECTS)
 	cp $(LIB) ../
+	cp $(OBJECTS) ../
 
 clean:
-	rm $(OBJECTS) $(LIB) ../$(LIB)
+	rm -f $(OBJECTS) $(LIB)
 
 .C.o:
 	$(CC) $(CFLAGS) $< -o $@
diff --git a/src/sat/unsound/Makefile b/src/sat/unsound/Makefile
index d329b1d..238a097 100644
--- a/src/sat/unsound/Makefile
+++ b/src/sat/unsound/Makefile
@@ -1,17 +1,24 @@
 include   ../../../scripts/Makefile.common
+
 MTL       = ../mtl
-CORE      = ../core
-CHDRS     = $(wildcard *.h) $(wildcard $(MTL)/*.h)
+SOURCES   = UnsoundSimpSolver.C ../core/Solver.C
+OBJECTS   = $(SOURCES:.C=.o)
+LIB       = libminisat.a
+CFLAGS    += -I$(MTL) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
 EXEC      = minisat
-CFLAGS    = -I$(MTL) -I$(CORE) -ffloat-store $(CFLAGS_M32)
 LFLAGS    = -lz
 
-CSRCS     = $(wildcard *.C)
-COBJS     = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o
+all: $(LIB) #$(EXEC)
+lib: $(LIB)
+
+$(LIB): $(OBJECTS)
+	rm -f $@
+	ar cq $@ $(OBJECTS)
+	cp $(LIB) ../
+	cp $(OBJECTS) ../
 
+clean:
+	rm -f $(OBJECTS) $(LIB)
 
-include ../mtl/template.mk
-all: libminisat.a
-	ranlib libminisat.a
-	cp *.or ../
-	cp libminisat.a ../
+.C.o:
+	$(CC) $(CFLAGS) $< -o $@
-- 
2.47.3