* In SMTLIB parsing mode, warn if the expected and actual satisfiability differ.

* Fixed a memory leak in ClearTables(), ClearCaches().
* Added back the "if_then_else" token which some SMTLIB benchmarks rely on
* Removed unnecessary tokens from the lexer.

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

diff --git a/AST/AST.cpp b/AST/AST.cpp
index 1b7b705c20ddb2a1130f5ef04a93119a35c35aaa..6f7c6e5d5227434ab6e24b1dd3c18b5b11e8f132 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -58,6 +58,12 @@ namespace BEEV {
   //print the input back
   bool print_STPinput_back = false;
   
+  enum BEEV::inputStatus input_status = NOT_DECLARED;
+
+  // Used only in smtlib lexer/parser
+  ASTNode SingleBitOne;
+  ASTNode SingleBitZero;
+
   //global BEEVMGR for the parser
   BeevMgr * globalBeevMgr_for_parser;
 
@@ -1497,6 +1503,7 @@ namespace BEEV {
     for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),
          itend=_ASTNode_to_Bitvector.end();it!=itend;it++) {
       (it->second)->clear();
+      delete (it->second);
     }
     _ASTNode_to_Bitvector.clear();
     
@@ -1556,6 +1563,7 @@ namespace BEEV {
     for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),
          itend=_ASTNode_to_Bitvector.end();it!=itend;it++) {
       (it->second)->clear();
+      delete (it->second);
     }
     _ASTNode_to_Bitvector.clear();
     

diff --git a/AST/ASTUtil.h b/AST/ASTUtil.h
index 9ae42553fe8cafb796ca16f764a7b4e3f958551b..1693847d93d829f078d5a4a4b6251f1a6d7fa524 100644 (file)
--- a/AST/ASTUtil.h
+++ b/AST/ASTUtil.h
@@ -77,6 +77,16 @@ namespace BEEV {
   //print the input back
   extern bool print_STPinput_back;
 
+  enum inputStatus
+    {
+         NOT_DECLARED =0, // Not included in the input file / stream
+         TO_BE_SATISFIABLE,
+         TO_BE_UNSATISFIABLE,
+         TO_BE_UNKNOWN // Specified in the input file as unknown.
+    };
+
+  extern enum inputStatus input_status;
+
   extern void (*vc_error_hdlr)(const char* err_msg);
   /*Spacer class is basically just an int, but the new class allows
     overloading of << with a special definition that prints the int as

diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp
index 3a73fc88301b4881be5be6ab9e6fb7aa4e896324..af3f0b4ea154d6dc7c6ec57474a62a9149082723 100644 (file)
--- a/AST/ToSAT.cpp
+++ b/AST/ToSAT.cpp
@@ -1424,6 +1424,21 @@ namespace BEEV {
   //This function prints the output of the STP solver
   void BeevMgr::PrintOutput(bool true_iff_valid) {
     //self-explanatory
+      if(print_output) {
+       if(smtlib_parser_enable)
+         {
+           if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE))
+             {
+               cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl;
+             }
+           else
+             if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE))
+               {
+                 cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl;
+               }
+         }
+      }
+
     if(true_iff_valid) {
       ValidFlag = true;
       if(print_output) {

diff --git a/parser/main.cpp b/parser/main.cpp
index 547b9dfa1f4423b1443e22533ef095c3bdb9d870..93a9370d19f19a85fb0a1f296be9e390df49eb5f 100644 (file)
--- a/parser/main.cpp
+++ b/parser/main.cpp
@@ -33,6 +33,14 @@ extern int smtparse();
 extern int cvcparse();
 
 
+namespace BEEV
+{
+extern BEEV::ASTNode SingleBitOne;
+extern BEEV::ASTNode SingleBitZero;
+}
+
+
+
 /* GLOBAL VARS: Some global vars for the Main function.
  *
  */
@@ -44,10 +52,6 @@ std::string helpstring = "\n\n";
 // Amount of memory to ask for at beginning of main.
 static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
 
-// Used only in smtlib lexer/parser
-BEEV::ASTNode SingleBitOne;
-BEEV::ASTNode SingleBitZero;
-
 /******************************************************************************
  * MAIN FUNCTION: 
  *
@@ -205,8 +209,8 @@ int main(int argc, char ** argv) {
   BEEV::print_output = true;
   BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr();  
 
-  SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1);
-  SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1);
+  BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1);
+  BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1);
   //BEEV::smtlib_parser_enable = true;
 
   if (smtlibParser)

diff --git a/parser/smtlib.lex b/parser/smtlib.lex
index a045e1f96e46790a5456907e0f75b143a8cb1d6f..c33682a6610d05d1ef1fda962eeda04d3182403f 100644 (file)
--- a/parser/smtlib.lex
+++ b/parser/smtlib.lex
@@ -51,8 +51,11 @@
     }
   }      
 
+namespace BEEV
+{
   extern BEEV::ASTNode SingleBitOne;
   extern BEEV::ASTNode SingleBitZero;
+ }
 
 /* Changed for smtlib speedup */
 /* bv{DIGIT}+      { smtlval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(smttext+2, 10)); return BVCONST_TOK;} */
@@ -84,10 +87,10 @@ ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
 bit{DIGIT}+     {
                   char c = smttext[3];
                   if (c == '1') {
-                    smtlval.node = new BEEV::ASTNode(SingleBitOne);
+                    smtlval.node = new BEEV::ASTNode(BEEV::SingleBitOne);
                   }
                   else {
-                    smtlval.node = new BEEV::ASTNode(SingleBitZero);
+                    smtlval.node = new BEEV::ASTNode(BEEV::SingleBitZero);
                   }
                   return BITCONST_TOK;
                };
@@ -128,6 +131,7 @@ bit{DIGIT}+     {
 "not"           { return NOT_TOK; }
 "implies"       { return IMPLIES_TOK; }
 "ite"           { return ITE_TOK;}
+"if_then_else"  { return ITE_TOK;} // This is in the SMTLIB benchmarks.
 "and"           { return AND_TOK; }
 "or"            { return OR_TOK; }
 "xor"           { return XOR_TOK; }
@@ -135,7 +139,6 @@ bit{DIGIT}+     {
 "let"           { return LET_TOK; }
 "flet"          { return FLET_TOK; }
 "notes"         { return NOTES_TOK; }
-"cvc_command"   { return CVC_COMMAND_TOK; }
 "sorts"         { return SORTS_TOK; }
 "funs"          { return FUNS_TOK; }
 "preds"         { return PREDS_TOK; }
@@ -171,11 +174,7 @@ bit{DIGIT}+     {
 
 "nand"         { return NAND_TOK;}
 "nor"          { return NOR_TOK;}
-"/="           { return NEQ_TOK; }
- ":="           { return ASSIGN_TOK;}
-"shift_left0"   { return BVLEFTSHIFT_TOK;}
 "bvshl"         { return BVLEFTSHIFT_1_TOK;}
-"shift_right0"  { return BVRIGHTSHIFT_TOK;}
 "bvlshr"        { return BVRIGHTSHIFT_1_TOK;}
 "bvashr"        { return BVARITHRIGHTSHIFT_TOK;}
 "bvadd"         { return BVPLUS_TOK;}

diff --git a/parser/smtlib.y b/parser/smtlib.y
index ad497435c379ec0a0ebf13d599e0ede8ffe53c1f..8a5dd658f18a7713ef9a8d9d3ef939e8c765141f 100644 (file)
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -322,10 +322,20 @@ logic_name:
 ;
 
 status:
-    SAT_TOK { $$ = NULL; }
-  | UNSAT_TOK { $$ = NULL; }
-  | UNKNOWN_TOK { $$ = NULL; }
-;
+    SAT_TOK { 
+       BEEV::input_status = BEEV::TO_BE_SATISFIABLE; 
+       $$ = NULL; 
+               }
+  | UNSAT_TOK { 
+       BEEV::input_status = BEEV::TO_BE_UNSATISFIABLE; 
+       $$ = NULL; 
+  }
+  | UNKNOWN_TOK 
+  { 
+       BEEV::input_status = BEEV::TO_BE_UNKNOWN; 
+       $$ = NULL; 
+  }
+ ;
 
 
 /* annotations: */