added more tests

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

diff --git a/README b/README
index 4794a206e1f6f3e4727fd1d7412184625d2c69dd..816bbe75d46437a23ba48c91e3c46b0ee6b2fa15 100644 (file)
--- a/README
+++ b/README
@@ -1,6 +1,4 @@
 
-
-
 /********************************************************************
  * PROGRAM NAME: STP (Simple Theorem Prover)   
  *             

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 24be83ad7444241d6190082faec0aa061296f630..cd1be0ca1ba248e84ce2e58fd18dddf3f56971e6 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -287,13 +287,9 @@ namespace BEEV
      *both indexwidth and valuewidth should never be less than 0
      */
     unsigned int GetIndexWidth() const;
-
-    // FIXME: This function is dangerous.  Try to eliminate it's use.
     void SetIndexWidth(unsigned int iw) const;
 
     unsigned int GetValueWidth() const;
-
-    // FIXME: This function is dangerous.  Try to eliminate it's use.
     void SetValueWidth(unsigned int vw) const;
 
     //return the type of the ASTNode

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 2a204e717d11057528d8daf2023e827c845191e2..2630d610077a71fb26c3d142c70aa0b2cf2b5da9 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -388,12 +388,11 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_num) {
     BEEV::FatalError("Trying to assert a NON formula: ",*a);
 
   b->BVTypeCheck(*a);
-  //a->SetAbsRefineInt(absrefine_num);
   b->AddAssert(*a);
 }
 
 //! Check validity of e in the current context.
-/*!  If the result is true, then the resulting context is the same as
+/*! If the result is true, then the resulting context is the same as
  * the starting context.  If the result is false, then the resulting
  * context is a context in which e is false.  e must have Boolean
  * type. */
@@ -421,6 +420,30 @@ int vc_query(VC vc, Expr e) {
     return b->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a);
 }
 
+// int vc_absRefineQuery(VC vc, Expr e) {
+//   nodestar a = (nodestar)e;
+//   bmstar b   = (bmstar)vc;
+
+//   if(!BEEV::is_Form_kind(a->GetKind()))
+//     BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a);
+
+//   //a->LispPrint(cout, 0);
+//   //printf("##################################################\n");
+//   b->BVTypeCheck(*a);
+//   b->AddQuery(*a);
+
+//   const BEEV::ASTVec v = b->GetAsserts();
+//   node o;
+//   if(!v.empty()) {
+//     if(v.size()==1)
+//       return b->TopLevelSAT(v[0],*a);
+//     else
+//       return b->TopLevelSAT(b->CreateNode(BEEV::AND,v),*a);
+//   }
+//   else
+//     return b->TopLevelSAT(b->CreateNode(BEEV::TRUE),*a);
+// }
+
 void vc_push(VC vc) {
   bmstar b = (bmstar)vc;
   b->ClearAllCaches();