From: trevor_hansen Date: Tue, 3 Apr 2012 06:43:00 +0000 (+0000) Subject: Improvements. Move the hard timeout function to a utility file, apply max. precise... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c68fd78ffa4a42eece654f99dfabb1d9d247abe8;p=francis%2Fstp.git Improvements. Move the hard timeout function to a utility file, apply max. precise propagators in cbitp. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1617 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index e9a208b..aecb98c 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -561,6 +561,38 @@ namespace BEEV return true; } //End of TypeCheck function + // callback for SIGALRM. + void handle_time_out(int parameter){ + printf("Timed Out.\n"); + + abort(); + // I replaced the exit(0) with an abort(). + // The exit was sometimes hanging, seemingly because of a bug somewhere else (e.g. loader, glibc). + // In strace it output: + + //--- SIGVTALRM (Virtual timer expired) @ 0 (0) --- + //fstat(1, {st_mode=S_IFCHR|0620, st_rdev=makedev(136, 5), ...}) = 0 + //mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fabca622000 + //write(1, "Timed Out.\n", 11Timed Out. + //) = 11 + //futex(0x7fabc9c54e40, FUTEX_WAIT, 2, NULL + + // Then it would just sit there waiting for the mutex (which never came). + //exit(0); + } + + + itimerval timeout; + void setHardTimeout(int sec) + { + signal(SIGVTALRM, handle_time_out); + timeout.it_interval.tv_usec = 0; + timeout.it_interval.tv_sec = 0; + timeout.it_value.tv_usec = 0; + timeout.it_value.tv_sec = sec; + setitimer(ITIMER_VIRTUAL, &timeout, NULL); + } + long getCurrentTime() { timeval t; diff --git a/src/main/main.cpp b/src/main/main.cpp index fd8f6e0..03a2bb2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -32,24 +32,9 @@ extern int cvclex_destroy(void); extern int smtlex_destroy(void); extern int smt2lex_destroy(void); -// callback for SIGALRM. -void handle_time_out(int parameter){ - printf("Timed Out.\n"); - - abort(); - // I replaced the exit(0) with an abort(). - // The exit was sometimes hanging, seemingly because of a bug somewhere else (e.g. loader, glibc). - // In strace it output: - - //--- SIGVTALRM (Virtual timer expired) @ 0 (0) --- - //fstat(1, {st_mode=S_IFCHR|0620, st_rdev=makedev(136, 5), ...}) = 0 - //mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fabca622000 - //write(1, "Timed Out.\n", 11Timed Out. - //) = 11 - //futex(0x7fabc9c54e40, FUTEX_WAIT, 2, NULL - - // Then it would just sit there waiting for the mutex (which never came). - //exit(0); +namespace BEEV +{ + void setHardTimeout(int); } bool onePrintBack =false; @@ -113,8 +98,6 @@ int main(int argc, char ** argv) { AbsRefine_CounterExample * Ctr_Example = new AbsRefine_CounterExample(bm, simp, arrayTransformer); auto_ptr ctrCleaner(Ctr_Example); - itimerval timeout; - ParserBM = bm; GlobalSTP = new STP(bm, @@ -324,12 +307,7 @@ int main(int argc, char ** argv) { if (argv[i][1] == 'g') { - signal(SIGVTALRM, handle_time_out); - timeout.it_interval.tv_usec = 0; - timeout.it_interval.tv_sec = 0; - timeout.it_value.tv_usec = 0; - timeout.it_value.tv_sec = atoi(argv[++i]); - setitimer(ITIMER_VIRTUAL, &timeout, NULL); + BEEV::setHardTimeout(atoi(argv[++i])); } else if (argv[i][1] == 'i') { diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp index 2693c89..34da917 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp @@ -67,20 +67,6 @@ FixedBits cbvToFixedBits(BEEV::CBV low, unsigned width) return lowBits; } -Result merge(Result r1, Result r2) -{ - if (r1 == CONFLICT || r2 == CONFLICT ) - return CONFLICT; - - if (r1 == CHANGED || r2 == CHANGED) - return CHANGED; - - if (r1 == NO_CHANGE && r2 == NO_CHANGE) - return NO_CHANGE; - - return NOT_IMPLEMENTED; - -} // The value "b" is in the range [low,high] inclusive. // Unfortunately it's not idempotent, <....1> [5,6], doesn't completely set it. diff --git a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp index 098bdfc..003ec81 100644 --- a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp @@ -373,9 +373,11 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP bool disabledProp = !beev->UserFlags.bitConstantProp_flag; bool printOutput = beev->UserFlags.print_output_flag; + bool checkCounter = beev->UserFlags.check_counterexample_flag; beev->UserFlags.bitConstantProp_flag = false; beev->UserFlags.print_output_flag = false; + beev->UserFlags.check_counterexample_flag= false; ASTVec initialFixing; @@ -384,7 +386,7 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP for (int i = 0; i < numberOfChildren; i++) { std::stringstream out; - out << "v" << i; + out << "v_VERY_SPECIALLY_NAMES" << i; unsigned valueWidth; @@ -401,7 +403,7 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP } unsigned outputWidth = output.isBoolean()? 0: output.getWidth(); - ASTNode outputNode = beev->CreateSymbol("result",0,outputWidth); + ASTNode outputNode = beev->CreateSymbol("result_WITH_SPECIAL_NAME",0,outputWidth); ASTNode expr; if (output.isBoolean()) @@ -452,7 +454,8 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP if (first) { - result = ce.CallSAT_ResultCheck(newS, expr, expr, &tosat,true); + beev->AddQuery(beev->ASTUndefined); + result = ce.CallSAT_ResultCheck(newS, expr, expr, &tosat,true); } else { @@ -460,6 +463,7 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP newS.addClause(satSolverClause); satSolverClause.clear(); + beev->AddQuery(beev->ASTUndefined); result = ce.CallSAT_ResultCheck(newS, beev->ASTTrue, beev->ASTTrue, &tosat,true); } @@ -511,6 +515,7 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP beev->UserFlags.bitConstantProp_flag = !disabledProp; beev->UserFlags.print_output_flag = printOutput; + beev->UserFlags.check_counterexample_flag= checkCounter; return first; } diff --git a/src/simplifier/constantBitP/ConstantBitP_Utility.cpp b/src/simplifier/constantBitP/ConstantBitP_Utility.cpp index 4a914ab..6095239 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Utility.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_Utility.cpp @@ -185,6 +185,20 @@ int signedCompare(const BEEV::CBV& lhs, const BEEV::CBV& rhs) return CONSTANTBV::BitVector_Compare(lhs,rhs); } +Result merge(Result r1, Result r2) +{ + if (r1 == CONFLICT || r2 == CONFLICT ) + return CONFLICT; + + if (r1 == CHANGED || r2 == CHANGED) + return CHANGED; + + if (r1 == NO_CHANGE && r2 == NO_CHANGE) + return NO_CHANGE; + + return NOT_IMPLEMENTED; +} + int toInt(const BEEV::CBV value) { diff --git a/src/simplifier/constantBitP/ConstantBitP_Utility.h b/src/simplifier/constantBitP/ConstantBitP_Utility.h index 0e253b1..680dc5c 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Utility.h +++ b/src/simplifier/constantBitP/ConstantBitP_Utility.h @@ -33,6 +33,8 @@ struct stats unsigned unfixed; }; +Result merge(Result r1, Result r2); + stats getStats(const vector& operands, const unsigned position); } } diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index 423867b..89a538a 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -8,6 +8,7 @@ #include #include #include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_MaxPrecision.h" using std::endl; using std::cout; @@ -32,10 +33,6 @@ namespace simplifier dispatchToTransferFunctions(const Kind k, vector& children, FixedBits& output, const ASTNode n, MultiplicationStatsMap *msm = NULL); - Result - dispatchToMaximallyPrecise(const Kind k, vector& children, - FixedBits& output, const ASTNode n); - const bool debug_cBitProp_messages = false; const bool output_mult_like = false; const bool debug_print_graph_after = false; @@ -217,6 +214,15 @@ namespace simplifier //Determine what must always be true. ASTNodeMap fromTo = getAllFixed(); + { + ASTNodeMap::iterator it = fromTo.begin(); + while(it != fromTo.end()) + { + assert(it->getKind() != SYMBOL); + it++; + } + } + if (debug_cBitProp_messages) { @@ -707,7 +713,7 @@ namespace simplifier } #undef MAPTFN bool mult_like = false; - + const bool lift_to_max = false; // safe approximation to no overflow multiplication. if (k == BVMULT) @@ -716,7 +722,7 @@ namespace simplifier result = bvMultiplyBothWays(children, output, n.GetSTPMgr(),&ms); if (CONFLICT != result) msm->map[n] = ms; - mult_like=true; + mult_like=true; } else if (k == BVDIV) { @@ -745,9 +751,16 @@ namespace simplifier mult_like=true; } else + result = transfer(children, output); - - result = transfer(children, output); + if (mult_like && lift_to_max) + { + int bits_before = output.countFixed() + children[0]->countFixed() + children[1]->countFixed(); + result = merge(result, maxPrecision(children, output, k, n.GetSTPMgr())? CONFLICT :NOT_IMPLEMENTED); + int difference = (output.countFixed() + children[0]->countFixed() + children[1]->countFixed()) - bits_before; + assert(difference >= 0); + cerr << "Bits fixed" << difference << endl; + } if (mult_like && output_mult_like) { diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index e576f72..21fd657 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -2829,9 +2829,11 @@ namespace BEEV ASTNode top = nf->CreateTerm(BVEXTRACT, rest, inputterm[0], _bm->CreateBVConst(32,rest-1),_bm->CreateZeroConst(32)); ASTNode bottom = nf->CreateTerm(BVEXTRACT, rest, inputterm[1], _bm->CreateBVConst(32,rest-1),_bm->CreateZeroConst(32)); + // nb. This differs from the bvdiv case. ASTNode div = nf->CreateTerm(BVMOD,rest,top,bottom); div = nf->CreateTerm(BVCONCAT,inputValueWidth,_bm->CreateZeroConst(inputValueWidth-rest),div); + // nb. This differs from the bvdiv case. output = nf->CreateTerm(ITE, inputValueWidth, cond, div, inputterm[0]); break; } diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 5871d17..7873b8c 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -267,6 +267,11 @@ namespace BEEV found = false; } } + + //void setHardTimeout(int sec); + //setHardTimeout(500); + + bm->GetRunTimes()->start(RunTimes::Solving); satSolver.solve(); bm->GetRunTimes()->stop(RunTimes::Solving);