git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk...

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index e7f5aedec2e4c43e1d363e8a74e3cfd4e2b59726..35caa2ac8510d5e30fa63204f2c724df4a99d752 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -335,7 +335,7 @@ namespace BEEV
   ASTNode BeevMgr::CreateBVConst(unsigned int width, unsigned long long int bvconst)
   {
     if (width > (sizeof(unsigned long long int) << 3) || width <= 0)
-      FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, width);
+      FatalError("CreateBVConst: trying to create a bvconst using unsigned long long of width: ", ASTUndefined, width);
 
     CBV bv = CONSTANTBV::BitVector_Create(width, true);
     unsigned long c_val = (~((unsigned long) 0)) & bvconst;
@@ -811,6 +811,10 @@ namespace BEEV
           case FALSE:
           case SYMBOL:
             return true;
+         case PARAMBOOL:
+           if(2 != n.Degree())
+             FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n);
+           break;
           case EQ:
             if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth()))
               {

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 41190cf9b3a16429c6808638dbe10b5d7718823b..f8e523528296f53b76955f9c296bdcae29a75a50 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -93,6 +93,11 @@ namespace BEEV
     // Usual constructor.
     ASTNode(ASTInternal *in);
 
+    //Integer that helps sort the ASTNodes. This sorting is different
+    //from the sorting based on NodeNum. This is used as a way of
+    //achieving abstraction-refinement.
+    unsigned int _sort_for_absrefine;
+
     //Equal iff ASTIntNode pointers are the same.
     friend bool operator==(const ASTNode node1, const ASTNode node2)
     {
@@ -117,6 +122,18 @@ namespace BEEV
     }
 
   public:
+    //Set the sorting integer for abstraction refinement
+    void SetAbsRefineInt(unsigned int a) {_sort_for_absrefine = a;}
+
+    //Get the sorting integer for abstraction refinement
+    unsigned int GetAbsRefineInt(void) {return _sort_for_absrefine;}
+
+    //Compare two ASTNodes based on their abstraction refinement
+    //number
+    bool CmpAbsRefine(const ASTNode node1, const ASTNode node2) {
+      return (node1._sort_for_absrefine < node2._sort_for_absrefine);
+    }
+
     //Check if it points to a null node
     bool IsNull() const
     {
@@ -194,6 +211,7 @@ namespace BEEV
     ASTNode() :
       _int_node_ptr(NULL)
     {
+      _sort_for_absrefine=0;
     }
     ;
 
@@ -810,6 +828,9 @@ namespace BEEV
                    ASTNode::ASTNodeHasher, 
                    ASTNode::ASTNodeEqual> ASTNodeCountMap;
 
+//   typedef hash_map<int32_t,
+//                ASTVec,
+//                hash(int32_t)> IntToASTVecMap;
 
   // Function to dump contents of ASTNodeMap
   ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
@@ -1506,7 +1527,7 @@ namespace BEEV
     //by PUSH/POP
     std::vector<ASTVec *> _asserts;
     //The query for the current logical context.
-    ASTNode _current_query;
+    ASTNode _current_query;    
 
     //this flag, when true, indicates that counterexample is being
     //checked by the counterexample checker

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 3418008fe315b66b893989c1bb5eb662ca059dc7..40bfd2d4dacc12565a1ec8d67c0576a19af4a69b 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -31,27 +31,25 @@ extern int cvcparse(void*);
 
 void vc_setFlags(char c) {
   std::string helpstring = "Usage: stp [-option] [infile]\n\n";
-  helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
-  helpstring +=  "-w  : switch wordlevel solver off (optimizations are ON by default)\n";
+  helpstring += "STP version: " + BEEV::version + "\n\n";
   helpstring +=  "-a  : switch optimizations off (optimizations are ON by default)\n";
-  helpstring +=  "-s  : print function statistics\n";
-  helpstring +=  "-v  : print nodes \n";
   helpstring +=  "-c  : construct counterexample\n";
   helpstring +=  "-d  : check counterexample\n";
-  helpstring +=  "-p  : print counterexample\n";
-  helpstring +=  "-y  : print counterexample in binary\n";
-  helpstring +=  "-b  : print STP input back to cout\n";
-  helpstring +=  "-x  : flatten nested XORs\n";
+  helpstring +=  "-e  : expand finite-for construct\n";
+  helpstring +=  "-f  : number of abstraction-refinement loops\n";
   helpstring +=  "-h  : help\n";
   helpstring +=  "-m  : use the SMTLIB parser\n";
-  
+  helpstring +=  "-p  : print counterexample\n";
+  helpstring +=  "-r  : switch refinement off (optimizations are ON by default)\n";
+  helpstring +=  "-s  : print function statistics\n";
+  helpstring +=  "-v  : print nodes \n";
+  helpstring +=  "-w  : switch wordlevel solver off (optimizations are ON by default)\n";
+  helpstring +=  "-x  : flatten nested XORs\n";
+  helpstring +=  "-y  : print counterexample in binary\n";
+
   switch(c) {
   case 'a' :
     BEEV::optimize_flag = false;
-    BEEV::wordlevel_solve_flag = false;
-    break;
-  case 'b':
-    BEEV::print_STPinput_back_flag = true;
     break;
   case 'c':
     BEEV::construct_counterexample_flag = true;
@@ -60,13 +58,26 @@ void vc_setFlags(char c) {
     BEEV::construct_counterexample_flag = true;
     BEEV::check_counterexample_flag = true;
     break;
+  case 'e':
+    BEEV::expand_finitefor_flag = true;
+    break;
+  case 'f':
+    BEEV::num_absrefine_flag = true;
+    //BEEV::num_absrefine = atoi(argv[++i]);
+    break;            
   case 'h':
+    BEEV::fprintf(stderr,BEEV::usage,BEEV::prog);
     cout << helpstring;
-    BEEV::FatalError("");
+    //FatalError("");
+    //return -1;
     break;
   case 'n':
     BEEV::print_output_flag = true;
     break;
+  case 'm':
+    BEEV::smtlib_parser_flag=true;
+    BEEV::division_by_zero_returns_one = true;
+    break;
   case 'p':
     BEEV::print_counterexample_flag = true;
     break;
@@ -80,8 +91,8 @@ void vc_setFlags(char c) {
     BEEV::stats_flag = true;
     break;
   case 'u':
-    BEEV::arraywrite_refinement_flag = true;
-    break;  
+    BEEV::arraywrite_refinement_flag = false;
+    break;
   case 'v' :
     BEEV::print_nodes_flag = true;
     break;
@@ -89,17 +100,22 @@ void vc_setFlags(char c) {
     BEEV::wordlevel_solve_flag = false;
     break;
   case 'x':
-    cinterface_exprdelete_on_flag = true;
+    BEEV::xor_flatten_flag = true;
+    break;
+  case 'y':
+    BEEV::print_binary_flag = true;
     break;
   case 'z':
     BEEV::print_sat_varorder_flag = true;
-    break;
+    break;    
   default:
     std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n";
     s += helpstring;
     BEEV::FatalError(s.c_str());
     break;
   }
+
+  
 }
 
 //Create a validity Checker. This is the global BeevMgr
@@ -364,7 +380,7 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) {
 /////////////////////////////////////////////////////////////////////////////
 //! Assert a new formula in the current context.  
 /*! The formula must have Boolean type. */
-void vc_assertFormula(VC vc, Expr e) {
+void vc_assertFormula(VC vc, Expr e, int absrefine_num) {
   nodestar a = (nodestar)e;
   bmstar b = (bmstar)vc;
 
@@ -372,6 +388,7 @@ void vc_assertFormula(VC vc, Expr e) {
     BEEV::FatalError("Trying to assert a NON formula: ",*a);
 
   b->BVTypeCheck(*a);
+  a->SetAbsRefineInt(absrefine_num);
   b->AddAssert(*a);
 }
 
@@ -387,13 +404,12 @@ int vc_query(VC vc, Expr e) {
   if(!BEEV::is_Form_kind(a->GetKind()))
     BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a);
 
-  //printf("kill all humans\n");
   //a->LispPrint(cout, 0);
   //printf("##################################################\n");
   b->BVTypeCheck(*a);
   b->AddQuery(*a);
 
-  const BEEV::ASTVec v = b->GetAsserts();
+  const BEEV::ASTVec v = b->GetAsserts();  
   node o;
   if(!v.empty()) {
     if(v.size()==1)
@@ -646,6 +662,23 @@ Expr vc_orExprN(VC vc, Expr* cc, int n) {
   return output;
 }
 
+Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* cc, int n) {
+  bmstar b = (bmstar)vc;
+  nodestar * c = (nodestar *)cc;
+  nodelist d;
+  
+  for(int i =0; i < n; i++)
+    d.push_back(*c[i]);
+  
+  node o = b->CreateTerm(BEEV::BVPLUS, n_bits, d);
+  b->BVTypeCheck(o);
+
+  nodestar output = new node(o);
+  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
+  return output;
+}
+
+
 Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart){
   bmstar b = (bmstar)vc;
   nodestar c = (nodestar)cond;
@@ -721,6 +754,23 @@ Expr vc_boolToBVExpr(VC vc, Expr form) {
   return output;
 }
 
+Expr vc_paramBoolExpr(VC vc, Expr boolvar, Expr parameter){
+  bmstar b = (bmstar)vc;
+  nodestar c = (nodestar)boolvar;
+  nodestar t = (nodestar)parameter;
+  
+  b->BVTypeCheck(*c);
+  b->BVTypeCheck(*t);
+  node o;
+
+  o = b->CreateNode(BEEV::PARAMBOOL,*c,*t);
+  //b->BVTypeCheck(o);
+  nodestar output = new node(o);
+  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
+  return output;
+}
+
+
 /////////////////////////////////////////////////////////////////////////////
 // BITVECTOR EXPR Creation methods                                         //
 /////////////////////////////////////////////////////////////////////////////

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 89ede246e2ea83eeab8446a446c3162f15ac30a6..863d0437fc85d59590373e64268586e4a5fa88d8 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -103,6 +103,9 @@ extern "C" {
   //Boolean to single bit BV Expression
   Expr vc_boolToBVExpr(VC vc, Expr form);
 
+  //Parameterized Boolean Expression (PARAMBOOL, Boolean_Var, parameter)
+  Expr vc_paramBoolExpr(VC vc, Expr var, Expr param);
+
   // Arrays
   
   //! Create an expression for the value of array at the given index
@@ -166,7 +169,7 @@ extern "C" {
   
   //! Assert a new formula in the current context.  
   /*! The formula must have Boolean type. */
-  void vc_assertFormula(VC vc, Expr e);
+  void vc_assertFormula(VC vc, Expr e, int absrefine_num=0);
   
   //! Simplify e with respect to the current context
   Expr vc_simplify(VC vc, Expr e);
@@ -214,6 +217,7 @@ extern "C" {
   
   Expr vc_bvConcatExpr(VC vc, Expr left, Expr right);
   Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right);
+  Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* children, int numOfChildNodes);
   Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right);
   Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right);
   Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right);

diff --git a/src/main/main.cpp b/src/main/main.cpp
index ffe6e7024486af8de8a5bcc887e892d3d2df808d..f7bcfa914c34d83a2c903917f74acf2238c9cedf 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -114,9 +114,6 @@ int main(int argc, char ** argv) {
             case 'p':
               print_counterexample_flag = true;
               break;
-            case 'y':
-              print_binary_flag = true;
-              break;
             case 'q':
               print_arrayval_declaredorder_flag = true;
               break;
@@ -141,6 +138,9 @@ int main(int argc, char ** argv) {
             case 'x':
               xor_flatten_flag = true;
               break;
+           case 'y':
+              print_binary_flag = true;
+              break;            
             case 'z':
               print_sat_varorder_flag = true;
               break;