Significant good changes to SAT makefiles by Mate. Issues with STP library creation...

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

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index aad561c7c23fc932f4d176966a5795f24f3b4578..e9c18734c4691c75c66f330d8e39a0d3df7956e3 100644 (file)
--- 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 f4524d93eb9d0555b24c31e35049dc67db6ace6e..28d11ff9b67017a843738860d51e1c5d3f6456a8 100644 (file)
--- 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 c36465fbe84708df232a51ee90756ee2c5b77667..6e0e96708b044fed073658203f2f46b52d4c16ed 100644 (file)
--- 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 8ae59c58ddb503db01feec8b0ff5f517345385a0..c42131eda3256806bd486e0d2a9ffff581fbe3e8 100644 (file)
--- 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 9e2a508fdfd5c77d1a6a3417f2b40d3c4108e550..1ba50ead33aab2d697f411dfd730e708ecbac5ca 100644 (file)
--- 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 d329b1d644689711517396b58dc73740827bac75..238a0972f88af380e6a9d0a28edde89881345afe 100644 (file)
--- 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 $@