From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 25 Sep 2009 20:13:02 +0000 (+0000)
Subject: added more tests
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b7df3e4dfbe0b67cfe7b85c383aad136a0d9d382;p=francis%2Fstp.git

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 4794a20..816bbe7 100644
--- 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 24be83a..cd1be0c 100644
--- 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 2a204e7..2630d61 100644
--- 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();