From: trevor_hansen Date: Fri, 4 Sep 2009 12:37:55 +0000 (+0000) Subject: * Remove NEQ. NEQ is converted by the CVC parser into NOT(=(..)). This makes our... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5124dc05e9275e47dca3dd011e23134a0077923d;p=francis%2Fstp.git * Remove NEQ. NEQ is converted by the CVC parser into NOT(=(..)). This makes our internal format slightly more canonical. If this change works OK, I'd like to later remove: NAND, NOR, etc. * 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 e0106a5..4f2e38f 100644 --- 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 e7d84f9..2b2a586 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -33,13 +33,15 @@ #include "ASTUtil.h" #include "ASTKind.h" #include -#include "../sat/core/Solver.h" -//#include "../sat/simp/SimpSolver.h" -//#include "../sat/unsound/UnsoundSimpSolver.h" -#include "../sat/core/SolverTypes.h" #include #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 0257e96..35e06d7 100644 --- 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 f18d330..955c7c5 100644 --- 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 dc90b51..816ff0a 100644 --- 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 bf4bc26..2931bb0 100644 --- 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 +#include +#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 11265b0..0f00460 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -17,8 +17,10 @@ #include "AST.h" -#include -#include +#include +#include +#include + 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 2a56271..73b22cb 100644 --- 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 +#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 2edce1f..f272b69 100644 --- a/src/AST/printer/CPrinter.cpp +++ b/src/AST/printer/CPrinter.cpp @@ -1,4 +1,5 @@ #include "printers.h" +#include 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 b010506..b76515b 100644 --- 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 1bba628..15ca41e 100644 --- a/src/AST/printer/SMTLIBPrinter.cpp +++ b/src/AST/printer/SMTLIBPrinter.cpp @@ -1,4 +1,5 @@ #include "printers.h" +#include namespace printer { diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp index adacde6..294388e 100644 --- a/src/bitvec/consteval.cpp +++ b/src/bitvec/consteval.cpp @@ -9,6 +9,8 @@ #include "../AST/AST.h" #include "../AST/ASTUtil.h" +#include + 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 b0538e4..15b068d 100644 --- 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 c8b3359..756ff3e 100644 --- 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 b4920d3..c53a1ef 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -9,6 +9,8 @@ #include "../AST/AST.h" #include "../AST/ASTUtil.h" +#include + 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: