From: trevor_hansen Date: Thu, 17 Sep 2009 04:37:49 +0000 (+0000) Subject: * Add -m32 flag to c-api-tests to get it compiling X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9c2ebe478347606545288a230ae6588a9897c452;p=francis%2Fstp.git * Add -m32 flag to c-api-tests to get it compiling * -t now tracks the bvsolver, and the substitution mapper (which sometimes takes a freakishly large amount of time). * SimplifyCaches are no longer cleared at the start of topLevel simplify. Sometimes there is good stuff in there. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@236 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 72d7d03..c6f9ad0 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -794,6 +794,8 @@ namespace BEEV FatalError("BVTypeCheck: indices should be BVCONST\n", n); if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1) FatalError("BVTypeCheck: length mismatch\n", n); + if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth()) + FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n); break; case BVLEFTSHIFT: case BVRIGHTSHIFT: diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 80e0d7e..4c30ceb 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -15,7 +15,7 @@ #include // BE VERY CAREFUL> Update the Category Names to match. -std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "Solving"}; +std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap"}; namespace BEEV { diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h index f428823..a7c9fd6 100644 --- a/src/AST/RunTimes.h +++ b/src/AST/RunTimes.h @@ -10,7 +10,7 @@ class RunTimes public: enum Category { - Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving + Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap }; static std::string CategoryNames[]; diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index a51549d..89413cc 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -541,6 +541,8 @@ namespace BEEV //output is TRUE. The formula is thus dropped return output; } + + _bm->runTimes.start(RunTimes::BVSolver); ASTVec o; ASTVec c; if (EQ == k) @@ -589,6 +591,7 @@ namespace BEEV output = _bm->CreateNode(AND, output, evens); UpdateAlreadySolvedMap(input, output); + _bm->runTimes.stop(RunTimes::BVSolver); return output; } //end of TopLevelBVSolve() diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 9db6418..7c48139 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -308,12 +308,11 @@ ASTNode Flatten(const ASTNode& a) } } - ASTNode - BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, - bool pushNeg, ASTNodeMap* VarConstMap) + // The SimplifyMaps on entry to the topLevel functions may contain useful entries. + // E.g. The BVSolver calls SimplifyTerm() + ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { runTimes.start(RunTimes::SimplifyTopLevel); - ResetSimplifyMaps(); if (smtlib_parser_flag) BuildReferenceCountMap(b); ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); @@ -322,6 +321,16 @@ ASTNode Flatten(const ASTNode& a) return out; } +ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) +{ + runTimes.start(RunTimes::SimplifyTopLevel); + ASTNode out = SimplifyTerm(b); + ResetSimplifyMaps(); + runTimes.stop(RunTimes::SimplifyTopLevel); + return out; +} + + ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) @@ -1393,14 +1402,6 @@ ASTNode Flatten(const ASTNode& a) //memoize } //end of flattenonelevel() - ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) - { - ResetSimplifyMaps(); - ASTNode out = SimplifyTerm(b); - ResetSimplifyMaps(); - return out; - } - //This function simplifies terms based on their kind ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) @@ -3220,15 +3221,20 @@ ASTNode Flatten(const ASTNode& a) // clears() in particular. void BeevMgr::ResetSimplifyMaps() { - SimplifyMap->clear(); + // clear() is extremely expensive for hash_maps with a lot of buckets, + // in the EXT_MAP implementation it visits every bucket, checking whether + // each bucket is empty or not, if non-empty it deletes the contents. + // The destructor seems to clear everything anyway. + + //SimplifyMap->clear(); delete SimplifyMap; SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); - SimplifyNegMap->clear(); + //SimplifyNegMap->clear(); delete SimplifyNegMap; SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); - ReferenceCount->clear(); + //ReferenceCount->clear(); delete ReferenceCount; ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE); } diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index e02340b..55582e3 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -953,8 +953,10 @@ namespace BEEV if(optimize_flag) { + runTimes.start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT); + runTimes.stop(RunTimes::CreateSubstitutionMap); //printf("##################################################\n"); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); @@ -988,8 +990,10 @@ namespace BEEV if(optimize_flag) { + runTimes.start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT); + runTimes.stop(RunTimes::CreateSubstitutionMap); ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); simplified_solved_InputToSAT = diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 427e681..33c6380 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -1,64 +1,66 @@ +CXXFLAGS=-DEXT_HASH_MAP -m32 -I../../src/c_interface -L../../lib + all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 rm -rf *.out 0: - g++ -DEXT_HASH_MAP array-cvcl-02.c -I../../src/c_interface -L../../lib -lstp -o a0.out + g++ $(CXXFLAGS) array-cvcl-02.c -o a0.out -lstp ./a0.out 1: - g++ -DEXT_HASH_MAP b4-c.c -I../../src/c_interface -L../../lib -lstp -o a1.out + g++ $(CXXFLAGS) b4-c.c -lstp -o a1.out ./a1.out 2: - g++ -DEXT_HASH_MAP b4-c2.c -I../../src/c_interface -L../../lib -lstp -o a2.out + g++ $(CXXFLAGS) b4-c2.c -lstp -o a2.out ./a2.out 3: - g++ -DEXT_HASH_MAP getbvunsignedlonglong-check.c -I../../src/c_interface -L../../lib -lstp -o a3.out + g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out ./a3.out 4: - g++ -DEXT_HASH_MAP multiple-queries.c -I../../src/c_interface -L../../lib -lstp -o a4.out + g++ $(CXXFLAGS) multiple-queries.c -lstp -o a4.out ./a4.out 5: - g++ -DEXT_HASH_MAP parsefile-using-cinterface.c -I../../src/c_interface -L../../lib -lstp -o a5.out + g++ $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out ./a5.out 6: - g++ -DEXT_HASH_MAP print.c -I../../src/c_interface -L../../lib -lstp -o a6.out + g++ $(CXXFLAGS) print.c -lstp -o a6.out ./a6.out 7: - g++ -DEXT_HASH_MAP push-pop-1.c -I../../src/c_interface -L../../lib -lstp -o a7.out + g++ $(CXXFLAGS) push-pop-1.c -lstp -o a7.out ./a7.out 8: - g++ -DEXT_HASH_MAP sbvmod.c -I../../src/c_interface -L../../lib -lstp -o a8.out + g++ $(CXXFLAGS) sbvmod.c -lstp -o a8.out ./a8.out 9: - g++ -DEXT_HASH_MAP simplify.c -I../../src/c_interface -L../../lib -lstp -o a9.out + g++ $(CXXFLAGS) simplify.c -o a9.out -lstp ./a9.out 10: - g++ -DEXT_HASH_MAP simplify1.c -I../../src/c_interface -L../../lib -lstp -o a10.out + g++ $(CXXFLAGS) simplify1.c -lstp -o a10.out ./a10.out 11: - g++ -DEXT_HASH_MAP squares-leak.c -I../../src/c_interface -L../../lib -lstp -o a11.out + g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out ./a11.out 12: - g++ -DEXT_HASH_MAP stp-counterex.c -I../../src/c_interface -L../../lib -lstp -o a12.out + g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out ./a12.out 13: - g++ -DEXT_HASH_MAP stp-div-001.c -I../../src/c_interface -L../../lib -lstp -o a13.out + g++ $(CXXFLAGS) stp-div-001.c -lstp -o a13.out ./a13.out 14: - g++ -DEXT_HASH_MAP stpcheck.c -I../../src/c_interface -L../../lib -lstp -o a14.out + g++ $(CXXFLAGS) stpcheck.c -o a14.out -lstp ./a14.out 15: - g++ -DEXT_HASH_MAP x.c -I../../src/c_interface -L../../lib -lstp -o a15.out + g++ $(CXXFLAGS) x.c -lstp -o a15.out ./a15.out 16: - g++ -DEXT_HASH_MAP y.c -I../../src/c_interface -L../../lib -lstp -o a16.out + g++ $(CXXFLAGS) y.c -lstp -o a16.out ./a16.out 17: - g++ -DEXT_HASH_MAP push-pop.c -I../../src/c_interface -L../../lib -lstp -o a17.out + g++ $(CXXFLAGS) push-pop.c -lstp -o a17.out ./a17.out 18: - g++ -DEXT_HASH_MAP cvc-to-c.cpp -I../../src/c_interface -L../../lib -lstp -o a18.out + g++ $(CXXFLAGS) cvc-to-c.cpp -lstp -o a18.out ./a18.out ./t.cvc