* Remove NEQ. NEQ is converted by the CVC parser into NOT(=(..)). This makes our...

* Move the sat headers into sat/sat.h. AST.h now contains a forward declaration of just the types it needs. This should speed up compilation.
* Reduce the number of compiler warnings.

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

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index e0106a57c0f10e21d7b84efcedf51073e4092cf7..4f2e38f02f94ddbccceb884801842e978c99d219 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -185,7 +185,7 @@ namespace BEEV
   }
 
   // Get the name from a symbol (char *).  It's an error if kind != SYMBOL
-  const char * const ASTNode::GetName() const
+  const char * /**const**/ ASTNode::GetName() const
   {
     if (GetKind() != SYMBOL)
       FatalError("GetName: Called GetName on a non-symbol: ", *this);
@@ -579,7 +579,8 @@ namespace BEEV
   }
 
   // Get the value of bvconst from a bvconst.  It's an error if kind != BVCONST
-  CBV const ASTNode::GetBVConst() const
+  // Treat the result as const (the compiler can't enforce it).
+  CBV /**const**/ ASTNode::GetBVConst() const
   {
     if (GetKind() != BVCONST)
       FatalError("GetBVConst: non bitvector-constant: ", *this);
@@ -874,7 +875,6 @@ namespace BEEV
           case SYMBOL:
             return true;
           case EQ:
-          case NEQ:
             if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth()))
               {
                 cerr << "valuewidth of lhs of EQ: " << n[0].GetValueWidth() << endl;
@@ -1249,7 +1249,7 @@ namespace BEEV
   bool isAtomic(Kind kind)
   {
     if (TRUE == kind  || FALSE == kind || 
-       EQ == kind    || NEQ == kind   || 
+       EQ == kind    ||
        BVLT == kind  || BVLE == kind  || 
        BVGT == kind  || BVGE == kind  || 
        BVSLT == kind || BVSLE == kind || 

diff --git a/src/AST/AST.h b/src/AST/AST.h
index e7d84f9e49e919dc0682a2336ca635be03161cea..2b2a586e1f1841fb4f45c180071c60d2f3fc99f0 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -33,13 +33,15 @@
 #include "ASTUtil.h"
 #include "ASTKind.h"
 #include <stdint.h>
-#include "../sat/core/Solver.h"
-//#include "../sat/simp/SimpSolver.h"
-//#include "../sat/unsound/UnsoundSimpSolver.h"
-#include "../sat/core/SolverTypes.h"
 #include <stdlib.h>
 #include "../constantbv/constantbv.h"
 
+namespace MINISAT
+{
+       class Solver;
+       typedef int Var;
+}
+
 /*****************************************************************************
  * LIST OF CLASSES DECLARED IN THIS FILE:
  *
@@ -268,10 +270,12 @@ namespace BEEV
     ;
 
     // Get the name from a symbol (char *).  It's an error if kind != SYMBOL
-    const char * const GetName() const;
+    // The result should be treated as const.
+    const char * /**const**/ GetName() const;
 
     //Get the BVCONST value
-    const CBV GetBVConst() const;
+    // The result should be treated as const.
+    /*const*/ CBV GetBVConst() const;
 
     /*ASTNode is of type BV <==> ((indexwidth=0)&&(valuewidth>0))
      *
@@ -307,7 +311,7 @@ namespace BEEV
     types GetType(void) const;
 
     // Hash is pointer value of _int_node_ptr.
-    const size_t Hash() const
+    /* const */ size_t Hash() const
     {
       return (size_t) _int_node_ptr;
       //return GetNodeNum();
@@ -434,7 +438,8 @@ namespace BEEV
     // table entry so it can be deleted without looking it up again.
     void DecRef();
 
-    virtual const Kind GetKind() const
+    // Treat the result as const pleases
+    virtual /**const**/ Kind GetKind() const
     {
       return _kind;
     }
@@ -632,7 +637,7 @@ namespace BEEV
       return (strcmp(sym1._name, sym2._name) == 0);
     }
 
-    const char * const GetName() const
+    const char * /**const**/ GetName() const
     {
       return _name;
     }
@@ -1302,7 +1307,8 @@ namespace BEEV
 
     //looksup a MINISAT var from the minisat-var memo-table. if none
     //exists, then creates one.
-    const MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n);
+    // Treat the result as const.
+    /**const**/ MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n);
 
     // Memo table for CheckBBandCNF debugging function
     ASTNodeMap CheckBBandCNFMemo;

diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds
index 0257e96bf5ba6ea01f10636a9bbb5cb2f450cf1c..35e06d71fa65435fbebe503488db31d0008dcc45 100644 (file)
--- a/src/AST/ASTKind.kinds
+++ b/src/AST/ASTKind.kinds
@@ -49,7 +49,6 @@ BVSLE         2       2       Form
 BVSGT          2       2       Form
 BVSGE          2       2       Form
 EQ             2       2       Form
-NEQ            2       2       Form
 FALSE          0       0       Form
 TRUE           0       0       Form
 NOT            1       1       Form

diff --git a/src/AST/BitBlast.cpp b/src/AST/BitBlast.cpp
index f18d33029cd017bb0de65d2430e32cdc2cb340ac..955c7c5f0d7fce3893f1f4fae111aea9451ba1b1 100644 (file)
--- a/src/AST/BitBlast.cpp
+++ b/src/AST/BitBlast.cpp
@@ -661,12 +661,6 @@ namespace BEEV
           break;
         }
 
-      case NEQ:
-        {
-          ASTNode bbkid = BBForm(CreateNode(EQ, form.GetChildren()));
-          result = CreateSimpNot(bbkid);
-          break;
-        }
 
       case EQ:
         {

diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp
index dc90b51952a372dcdb3d7758d9293c94645b4255..816ff0a61a4a788fbf0bbe650fd6161cb5f7329a 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/AST/ToCNF.cpp
@@ -9,6 +9,7 @@
 
 #include "AST.h"
 #include "../simplifier/bvsolver.h"
+#include "../sat/sat.h"
 
 namespace BEEV
 {
@@ -194,11 +195,6 @@ namespace BEEV
             result = true;
             break;
           }
-        case NEQ:
-          {
-            result = true;
-            break;
-          }
         default:
           {
             result = false;

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index bf4bc2641817e877071a454996a404e660935fae..2931bb03d70fd4fed0531c66da22df28b19b6932 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -9,7 +9,8 @@
 #include "AST.h"
 #include "ASTUtil.h"
 #include "../simplifier/bvsolver.h"
-#include <math.h>
+#include <cmath>
+#include "../sat/sat.h"
 
 namespace BEEV
 {
@@ -17,7 +18,7 @@ namespace BEEV
    * lookup or create new MINISAT Vars from the global MAP
    * _ASTNode_to_SATVar.
    */
-  const MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n)
+  /**const**/ MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n)
   {
     ASTtoSATMap::iterator it;
     MINISAT::Var v;
@@ -731,7 +732,6 @@ namespace BEEV
           output = ASTFalse;
         break;
       case EQ:
-      case NEQ:
       case BVLT:
       case BVLE:
       case BVGT:

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 11265b0eab5a0040d648c0de8331814470d387d3..0f00460cf22b884063052384b6325dc43e01337f 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -17,8 +17,10 @@
 
 
 #include "AST.h"
-#include <stdlib.h>
-#include <stdio.h>
+#include <cstdlib>
+#include <cstdio>
+#include <cassert>
+
 namespace BEEV
 {
 
@@ -217,7 +219,6 @@ namespace BEEV
       case BVSLE:
       case BVSGT:
       case BVSGE:
-      case NEQ:
         {
           ASTVec c;
           c.push_back(TransformTerm(simpleForm[0]));

diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index 2a56271cff36f4707c4200d45b8883d47ce9685a..73b22cbe9a9febcabaa2f6fc7d12b5005f1ab67c 100644 (file)
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -9,6 +9,12 @@
 #include "../AST.h"
 #include "AssortedPrinters.h"
 #include "printers.h"
+#include "../../sat/sat.h"
+
+// to get the PRIu64 macro from inttypes, this needs to be defined.
+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+#undef __STDC_FORMAT_MACROS
 
 namespace BEEV
 {
@@ -71,11 +77,11 @@ namespace BEEV
       return;
     double cpu_time = MINISAT::cpuTime();
     uint64_t mem_used = MINISAT::memUsed();
-    reportf("restarts              : %llu\n",                      s.starts);
-    reportf("conflicts             : %llu   (%.0f /sec)\n",        s.conflicts   , s.conflicts   /cpu_time);
-    reportf("decisions             : %llu   (%.0f /sec)\n",        s.decisions   , s.decisions   /cpu_time);
-    reportf("propagations          : %llu   (%.0f /sec)\n",        s.propagations, s.propagations/cpu_time);
-    reportf("conflict literals     : %llu   (%4.2f %% deleted)\n", s.tot_literals,
+    reportf("restarts              : %"PRIu64"\n",                      s.starts);
+    reportf("conflicts             : %"PRIu64"   (%.0f /sec)\n",        s.conflicts   , s.conflicts   /cpu_time);
+    reportf("decisions             : %"PRIu64"   (%.0f /sec)\n",        s.decisions   , s.decisions   /cpu_time);
+    reportf("propagations          : %"PRIu64"   (%.0f /sec)\n",        s.propagations, s.propagations/cpu_time);
+    reportf("conflict literals     : %"PRIu64"   (%4.2f %% deleted)\n", s.tot_literals,
             (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
     if (mem_used != 0)
       reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);

diff --git a/src/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp
index 2edce1fdde5d4cf3eb0eb9473bda4047ff67f533..f272b69b44dd52f9374e495df8e9a8cb7643387e 100644 (file)
--- a/src/AST/printer/CPrinter.cpp
+++ b/src/AST/printer/CPrinter.cpp
@@ -1,4 +1,5 @@
 #include "printers.h"
+#include <cassert>
 
 namespace printer
 {
@@ -329,12 +330,6 @@ namespace printer
           }
 
         break;
-      case NEQ:
-        C_Print1(os, c[0], indentation, letize);
-        os << " != ";
-        C_Print1(os, c[1], indentation, letize);
-        os << endl;
-        break;
       case AND:
       case OR:
       case NAND:

diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp
index b0105069af3928a7657aacbfed151b23a7093618..b76515be24bac82c6bcbd4c4f162d22e9bec56ba 100644 (file)
--- a/src/AST/printer/PLPrinter.cpp
+++ b/src/AST/printer/PLPrinter.cpp
@@ -212,12 +212,6 @@ namespace printer
         PL_Print1(os, c[1], indentation, letize);
         os << endl;
         break;
-      case NEQ:
-        PL_Print1(os, c[0], indentation, letize);
-        os << " /= ";
-        PL_Print1(os, c[1], indentation, letize);
-        os << endl;
-        break;
       case AND:
       case OR:
       case NAND:

diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp
index 1bba6282a20676c00196ae7876d1986ff544cb3e..15ca41e643e868bd975d0bb52d711ca3feafbafe 100644 (file)
--- a/src/AST/printer/SMTLIBPrinter.cpp
+++ b/src/AST/printer/SMTLIBPrinter.cpp
@@ -1,4 +1,5 @@
 #include "printers.h"
+#include <cassert>
 
 namespace printer
 {

diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp
index adacde631fc35a21d9556790721419374a500761..294388e961ef81f85a6c4bcd3f7f8fa11e7a396c 100644 (file)
--- a/src/bitvec/consteval.cpp
+++ b/src/bitvec/consteval.cpp
@@ -9,6 +9,8 @@
 
 #include "../AST/AST.h"
 #include "../AST/ASTUtil.h"
+#include <cassert>
+
 namespace BEEV
 {
 
@@ -483,12 +485,6 @@ namespace BEEV
         else
           OutputNode = ASTFalse;
         break;
-      case NEQ:
-        if (!CONSTANTBV::BitVector_equal(tmp0, tmp1))
-          OutputNode = ASTTrue;
-        else
-          OutputNode = ASTFalse;
-        break;
       case BVLT:
         if (-1 == CONSTANTBV::BitVector_Lexicompare(tmp0, tmp1))
           OutputNode = ASTTrue;

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index b0538e409e63b89a628f9f385138448268e8acc4..15b068dc00fc145d28e234bac27483fb5fb60814 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -436,7 +436,7 @@ Formula             :     '(' Formula ')' { $$ = $2; }
                       } 
                |      Expr NEQ_TOK Expr 
                        {
-                        BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NEQ, *$1, *$3));
+                        BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *$1, *$3)));
                         BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
                         $$ = n;
                         delete $1;

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index c8b335926d8c8dbc4a1be7679e3fad2939c31470..756ff3e9e1b9690508070b1fbf154b79fc25aa99 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -477,7 +477,7 @@ an_formula:
       for(BEEV::ASTVec::const_iterator it=terms.begin(),itend=terms.end();
           it!=itend; it++) {
         for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) {
-          BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NEQ, *it, *it2));
+          BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *it, *it2)));
 
           globalBeevMgr_for_parser->BVTypeCheck(*n);
           

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index b4920d3b89cad5619a3d803447b56c70ab7ddd2e..c53a1ef33941d73b3752d86d1659da6fb666f80d 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -9,6 +9,8 @@
 
 #include "../AST/AST.h"
 #include "../AST/ASTUtil.h"
+#include <cassert>
+
 namespace BEEV
 {
 
@@ -407,18 +409,6 @@ namespace BEEV
             output = pushNeg ? CreateNode(NOT, output) : output;
           break;
         }
-      case NEQ:
-        {
-          output = CreateSimplifiedEQ(left, right);
-          output = LhsMinusRhs(output);
-          if (output == ASTTrue)
-            output = pushNeg ? ASTTrue : ASTFalse;
-          else if (output == ASTFalse)
-            output = pushNeg ? ASTFalse : ASTTrue;
-          else
-            output = pushNeg ? output : CreateNode(NOT, output);
-          break;
-        }
       case BVLT:
       case BVLE:
       case BVGT: