fix for issue #109

src/interp/iz3mgr.cpp

@@ -616,6 +616,30 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
     extract_lcd(rats);
 }
 
+void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& coeffs){
+    std::vector<rational> rats;
+    get_gomory_cut_coeffs(proof,rats);
+    coeffs.resize(rats.size());
+    for(unsigned i = 0; i < rats.size(); i++){
+        coeffs[i] = make_int(rats[i]);
+    }
+}
+
+void iz3mgr::get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats){
+    symb s = sym(proof);
+    int numps = s->get_num_parameters();
+    rats.resize(numps-2);
+    for(int i = 2; i < numps; i++){
+        rational r;
+        bool ok = s->get_parameter(i).is_rational(r);
+        if(!ok)
+            throw "Bad Farkas coefficient";
+        rats[i-2] = r;
+    }
+    abs_rat(rats);
+    extract_lcd(rats);
+}
+
 void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& coeffs){
     std::vector<rational> rats;
     get_assign_bounds_rule_coeffs(proof,rats);

src/interp/iz3mgr.h

@@ -396,7 +396,7 @@ class iz3mgr  {
         return UnknownTheory;
     }
 
-    enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
+    enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,GomoryCutKind,ArithMysteryKind,UnknownKind};
 
     lemma_kind get_theory_lemma_kind(const ast &proof){
         symb s = sym(proof);
@@ -417,6 +417,8 @@ class iz3mgr  {
             return AssignBoundsKind;
         if(foo == "eq-propagate")
             return EqPropagateKind;
+        if(foo == "gomory-cut")
+            return GomoryCutKind;
         return UnknownKind;
     }
 
@@ -434,6 +436,10 @@ class iz3mgr  {
   
     void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& rats);
 
+    void get_gomory_cut_coeffs(const ast &proof, std::vector<rational>& rats);
+
+    void get_gomory_cut_coeffs(const ast &proof, std::vector<ast>& rats);
+
     bool is_farkas_coefficient_negative(const ast &proof, int n);
 
     bool is_true(ast t){

src/interp/iz3translate.cpp

@@ -1182,6 +1182,31 @@ public:
         return res;
     }
 
+    ast GomoryCutRule2Farkas(const ast &proof, const ast &con, std::vector<Iproof::node> prems){
+        std::vector<Iproof::node>  my_prems = prems;
+        std::vector<ast>  my_coeffs;
+        std::vector<Iproof::node>  my_prem_cons;
+        get_gomory_cut_coeffs(proof,my_coeffs);
+        int nargs = num_prems(proof);
+        if(nargs != (int)(my_coeffs.size()))
+            throw "bad gomory-cut theory lemma";
+        for(int i = 0; i < nargs; i++)
+            my_prem_cons.push_back(conc(prem(proof,i)));
+        ast my_con = normalize_inequality(sum_inequalities(my_coeffs,my_prem_cons));
+        Iproof::node hyp = iproof->make_hypothesis(mk_not(my_con));
+        my_prems.push_back(hyp);
+        my_coeffs.push_back(make_int("1"));
+        my_prem_cons.push_back(mk_not(my_con));
+        Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_prem_cons,my_coeffs);
+        ast t = arg(my_con,0);
+        ast c = arg(my_con,1);
+        ast d = gcd_of_coefficients(t);
+        t = z3_simplify(mk_idiv(t,d));
+        c = z3_simplify(mk_idiv(c,d));
+        ast cut_con = make(op(my_con),t,c);
+        return iproof->make_cut_rule(my_con,d,cut_con,res);
+    }
+
     Iproof::node RewriteClause(Iproof::node clause, const ast &rew){
         if(pr(rew) == PR_MONOTONICITY){
             int nequivs = num_prems(rew);
@@ -1912,6 +1937,13 @@ public:
                             res = AssignBounds2Farkas(proof,conc(proof));
                         break;
                     }
+                    case GomoryCutKind: {
+                        if(args.size() > 0)
+                            res =  GomoryCutRule2Farkas(proof, conc(proof), args);
+                        else
+                            throw unsupported();
+                        break;
+                    }
                     case EqPropagateKind: {
                         std::vector<ast> prems(nprems);
                         for(unsigned i = 0; i < nprems; i++)