From b076c152b34ccf8f2822b83b23ee9901d53e056e Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Thu, 7 Nov 2013 16:17:56 -0800
Subject: [PATCH] adding farkas axiom to interpolation

---
 src/interp/iz3translate.cpp | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 4feb35faa..ede4286fb 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1253,13 +1253,23 @@ public:
 	  case FarkasKind: {
 	    std::vector<ast> farkas_coeffs, prem_cons;
 	    get_farkas_coeffs(proof,farkas_coeffs);
-	    if(farkas_coeffs.size() != nprems){
-	      pfgoto(proof);
-	      throw unsupported();
+	    if(nprems == 0) {// axiom, not rule
+	      int nargs = num_args(con);
+	      if(farkas_coeffs.size() != nargs){
+		pfgoto(proof);
+		throw unsupported();
+	      }
+	      for(unsigned i = 0; i < nargs; i++){
+		ast lit = mk_not(arg(con,i));
+		prem_cons.push_back(lit);
+		args.push_back(iproof->make_hypothesis(lit));
+	      }
+	    }
+	    else {  // rule version (proves false)
+	      prem_cons.resize(nprems);
+	      for(unsigned i = 0; i < nprems; i++)
+		prem_cons[i] = conc(prem(proof,i));
 	    }
-	    prem_cons.resize(nprems);
-	    for(unsigned i = 0; i < nprems; i++)
-	      prem_cons[i] = conc(prem(proof,i));
 	    res = iproof->make_farkas(con,args,prem_cons,farkas_coeffs);
 	    break;
 	  }