Improvement. Extra c-api options from Stephan Falke.

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

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index 4edefcd59410196e3a034f9c59a65e4ace05dcb3..0fc69425e7a19cbda560d111373acda279129a02 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -100,6 +100,9 @@ namespace BEEV
     //to e
     ASTNode GetCounterExample(bool t, const ASTNode& e);
       
+    //queries the counterexample, and returns a vector of index-value pairs for e
+    std::vector<std::pair<ASTNode, ASTNode> > GetCounterExampleArray(bool t, const ASTNode& e);
+
     int CounterExampleSize(void) const
     {
       return CounterExampleMap.size();

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index f633774a38506bf3d53a6609ebaf4adbe48f7f23..f3a21da45db32c2363e235b60bbc644b48fdc707 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -618,6 +618,66 @@ namespace BEEV
     return output;
   } //End of GetCounterExample
 
+  // FUNCTION: queries the counterexample, and returns the number of array locations for e
+  std::vector<std::pair<ASTNode, ASTNode> > AbsRefine_CounterExample::GetCounterExampleArray(bool t, const ASTNode& e)
+  {
+    std::vector<std::pair<ASTNode, ASTNode> > entries;
+    
+    //input is valid, no counterexample to print
+    if (bm->ValidFlag)
+      {
+        return entries;
+      }
+
+    //t is true if SAT solver generated a counterexample, else it is
+    //false
+    if (!t)
+      {
+          return entries;
+      }
+
+    // Take a copy of the counterexample map, 'cause TermToConstTermUsingModel
+    // changes it. Which breaks the iterator otherwise.
+    const ASTNodeMap c(CounterExampleMap);
+
+    ASTNodeMap::const_iterator it = c.begin();
+    ASTNodeMap::const_iterator itend = c.end();
+    for (; it != itend; it++)
+      {
+        const ASTNode& f = it->first;
+        const ASTNode& se = it->second;
+
+        if (ARRAY_TYPE == se.GetType())
+          {
+            FatalError("TermToConstTermUsingModel: "
+                       "entry in counterexample is an arraytype. bogus:", se);
+          }
+
+        //skip over introduced variables
+        if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet(
+            f)))
+          {
+            continue;
+          }
+        if (f.GetKind() == READ && f[0] == e && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)
+          {
+            ASTNode rhs;
+            if (BITVECTOR_TYPE == se.GetType())
+              {
+                rhs = TermToConstTermUsingModel(se, false);
+              }
+            else
+              {
+                rhs = ComputeFormulaUsingModel(se);
+              }
+            assert(rhs.isConstant());
+            entries.push_back(std::make_pair(f[1], rhs));
+          }
+      }
+
+    return entries;
+  } //End of GetCounterExampleArray
+
   // FUNCTION: prints a counterexample for INVALID inputs.  iterate
   // through the CounterExampleMap data structure and print it to
   // stdout

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 849f131bdacff45f9ee748a93c07742f7bb5c22a..29d9ac7e0da7dd6eae6045abc90401c9bcbc1198 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -624,6 +624,27 @@ Expr vc_getCounterExample(VC vc, Expr e) {
   return output;
 }
 
+void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) {
+  nodestar a = (nodestar)e;
+  bmstar b = (bmstar)(((stpstar)vc)->bm);
+  ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
+
+  bool t = false;
+  if(ce->CounterExampleSize())
+    t = true;
+
+  std::vector<std::pair<ASTNode, ASTNode> > entries = ce->GetCounterExampleArray(t, *a);
+  *size = entries.size();
+  if (*size != 0) {
+    *indices = (Expr *) malloc(*size * sizeof(Expr*));
+    *values = (Expr *) malloc(*size * sizeof(Expr*));
+    for (int i = 0; i < *size; ++i) {
+      (*indices)[i] = new node(entries[i].first);
+      (*values)[i] = new node(entries[i].second);
+    }
+  }
+}
+
 int vc_counterexample_size(VC vc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index a8fd9471fc9307e3d6547b4c44044e7b81189eaa..b4f57b3bd3fcdb712ac8612fb3ce6cc43e9d250e 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -215,6 +215,9 @@ extern "C" {
   //! Return the counterexample after a failed query.
   Expr vc_getCounterExample(VC vc, Expr e);
 
+  //! Return an array from a counterexample after a failed query.
+  void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size);
+    
   //! get size of counterexample, i.e. the number of variables/array
   //locations in the counterexample.
   int vc_counterexample_size(VC vc);