fixed a bug in the CVC parser. It was allowing the user to input only assertions...

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

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 370ebd1963e04bc57dc59b2fefd84baae9b5bbbc..0e1a293cba71fee01665767687b7ae6c1756d8be 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -247,8 +247,21 @@ int main(int argc, char ** argv) {
     }
   bm->GetRunTimes()->stop(RunTimes::Parsing);
 
+  if(((ASTVec*)AssertsQuery)->empty())
+    {
+      FatalError("Input is Empty. Please enter some asserts and query\n");
+    }
+
+  if(((ASTVec*)AssertsQuery)->size() != 2)
+    {
+      FatalError("Input must contain a query\n");
+    }
+
   ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
+  //cout << "asserts: " << asserts << endl;
   ASTNode query   = (*(ASTVec*)AssertsQuery)[1];
+  //cout << "query: " << query << endl;
+
   if(bm->UserFlags.print_STPinput_back_flag)
     {
       if(bm->UserFlags.smtlib_parser_flag)

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 6026f857c80db10d4e83aaa4a9326f659d290ce2..b12e3d133426b96623d4687efaae113127f1e64b 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -184,7 +184,21 @@ counterexample  :      COUNTEREXAMPLE_TOK ';'
 }                              
 ;
 
-other_cmd       :      other_cmd1
+other_cmd       :
+/* other_cmd1 */
+/* { */
+/*   ASTVec aaa = ParserBM->GetAsserts(); */
+/*   if(aaa.size() == 0) */
+/*     { */
+/*       yyerror("Fatal Error: parsing:  GetAsserts() call: no assertions: "); */
+/*     } */
+
+/*   ASTNode asserts =  */
+/*     aaa.size() == 1 ?  */
+/*     aaa[0] : */
+/*     ParserBM->CreateNode(AND, aaa); */
+/*   ((ASTVec*)AssertsQuery)->push_back(asserts);   */
+/* } */
 |      Query 
 { 
   ((ASTVec*)AssertsQuery)->push_back(ParserBM->CreateNode(TRUE));

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 36a701d4e148cd1af5b641838369d6669ded7f21..48ce34eb89e6e9e11f2188d85a168cd5087add04 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -811,7 +811,7 @@ namespace BEEV
   void CNFMgr::doRenamingPosXor(const ASTNode& varphi)
   {
     CNFInfo* x = info[varphi];
-    
+
     //########################################
     // step 1, calc new variable
     //########################################
@@ -1650,6 +1650,14 @@ namespace BEEV
   {
 #ifdef FALSE
     //#ifdef CRYPTOMINISAT
+    // CNFInfo * xx = info[varphi];
+    //     if(NULL != xx
+    //        && sharesPos(*xx) > 0
+    //        && sharesNeg(*xx) > 0)
+    //       {
+    //         return;
+    //       }
+
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     ClausePtr xor_clause = new vector<const ASTNode*>();
 

diff --git a/tests/misc-tests/cryptominisat-bug.cvc b/tests/misc-tests/cryptominisat-bug.cvc
new file mode 100644 (file)
index 0000000..9bd46ed
--- /dev/null
+++ b/tests/misc-tests/cryptominisat-bug.cvc
@@ -0,0 +1,4 @@
+X : BITVECTOR(4);
+
+ASSERT 0bin0000 = BVPLUS(4,0bin0110, X);
+QUERY FALSE;
\ No newline at end of file

diff --git a/tests/misc-tests/no-query.cvc b/tests/misc-tests/no-query.cvc
new file mode 100644 (file)
index 0000000..96ef2c9
--- /dev/null
+++ b/tests/misc-tests/no-query.cvc
@@ -0,0 +1 @@
+ASSERT FALSE;
\ No newline at end of file