Improvements. Move the hard timeout function to a utility file, apply max. precise...

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 e9a208be61e5b9951d578eb0cb4fb610c99b3db6..aecb98c4cfb4768b6dd4a28ceb48e384d21f3e2d 100644 (file)
--- 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 fd8f6e08cf1286598e74891b77c70eebf31d7de3..03a2bb24c63e27b359d0cf4a3359818081ba31df 100644 (file)
--- 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<AbsRefine_CounterExample> 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 2693c89900a52cfd8c4855f5269b7c4b87208678..34da917bd8e3a86d81c5e5fa2ee9a5729bb4d8a0 100644 (file)
--- 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 098bdfc109eadefb88ab76136eef0676e30e4f99..003ec8167ffd27a5194b7ee580e57c7c512c00e9 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp
+++ b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp
@@ -373,9 +373,11 @@ bool maxPrecision(vector<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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 4a914ab47f4442ffb5c577049191e33d1cd052e8..6095239dfbf8bf4a88b1e140c36bb4c2d97cbaaa 100644 (file)
--- 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 0e253b1426d7963ee586c0e333bffdab045f27c7..680dc5cf3236ef587ef0ef125f562874bdac3fbc 100644 (file)
--- 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<FixedBits*>& operands, const unsigned position);
 }
 }

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 423867b2aafa8579653273cf62dbaf6f142b2edc..89a538a5cb557767400be0e279d98e3b5970dd9c 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -8,6 +8,7 @@
 #include <iostream>
 #include <fstream>
 #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<FixedBits*>& children,
         FixedBits& output, const ASTNode n, MultiplicationStatsMap *msm = NULL);
 
-    Result
-    dispatchToMaximallyPrecise(const Kind k, vector<FixedBits*>& 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 e576f72e28832dbd998079fcc18ae28aad3d19ba..21fd657ca1c452323c1edb8f5785d164ab4b7285 100644 (file)
--- 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 5871d176eb944caffa4818f63ed23ac3b5923c9b..7873b8cde77f8b7c4f2591d38c10101630dd9c82 100644 (file)
--- 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);