More efficient computation of inductive invariants from k-inductive ones

The computation only needs interpolation, not quantifier elimination, it
is based on the analysis of reinforced unfold transformation from the
2015 paper Horn Clause Solvers for Program Verification.

src/TransitionSystem.cc

@@ -9,6 +9,8 @@
 
 #include "TermUtils.h"
 #include "QuantifierElimination.h"
+#include "utils/SmtSolver.h"
+#include "utils/Timer.h"
 
 bool TransitionSystem::isWellFormed() {
 //    return systemType->isStateFormula(init) && systemType->isStateFormula(query) && systemType->isTransitionFormula(transition);
@@ -177,8 +179,19 @@ PTRef TransitionSystem::reverseTransitionRelation(TransitionSystem const & trans
     return transition;
 }
 
+PTRef KTo1Inductive::kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) const {
+    switch (mode) {
+        case Mode::UNFOLD:
+            return unfold(invariant, k, system);
+        case Mode::LEGACY:
+            return legacy(invariant, k, system);
+        default:
+            assert(false);
+            throw std::logic_error("Unreachable!");
+    }
+}
 
-PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem const & system) {
+PTRef KTo1Inductive::legacy(PTRef invariant, unsigned k, TransitionSystem const & system) {
     /*
      * If P(x) is k-inductive invariant then the following formula is 1-inductive invariant:
      * P(x_0)
@@ -223,7 +236,7 @@ PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem c
     resArgs.push(logic.mkNot(afterElimination));
     helpers.push(transition);
     // steps 2 to k-1
-    for (unsigned long i = 2; i < k; ++i) {
+    for (unsigned i = 2; i < k; ++i) {
 //        std::cout << "Step " << i << " out of " << k << std::endl;
         PTRef helper = logic.mkAnd({helpers[i-1], getNextVersion(invariant, i-1), getNextVersion(transition, i-1)});
         helper = QuantifierElimination(logic).eliminate(helper, getStateVars(i-1));
@@ -232,4 +245,78 @@ PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem c
         resArgs.push(logic.mkNot(afterElimination));
     }
     return logic.mkAnd(std::move(resArgs));
+}
+
+namespace {
+
+PTRef buildFormula(unsigned index, PTRef invariant, TransitionSystem const & system) {
+    if (index == 0) { return system.getLogic().getTerm_true(); }
+    Logic & logic = system.getLogic();
+    TimeMachine timeMachine(logic);
+    PTRef previous = buildFormula(index - 1, invariant, system);
+    PTRef invariantShifted = timeMachine.sendFlaThroughTime(invariant, index - 1);
+    PTRef stepShifted = timeMachine.sendFlaThroughTime(system.getTransition(), index - 1);
+    PTRef initShifted = timeMachine.sendFlaThroughTime(system.getInit(), index);
+    return logic.mkOr(initShifted, logic.mkAnd({previous, invariantShifted, stepShifted}));
+}
+} // namespace
+
+/**
+ * Computes 1-inductive invariant from a k-inductive one using only interpolation.
+ * The idea is an application of the more general concept of reinforced unfold tranformation for CHCs from the paper
+ * "Horn Clause Solvers for Program Verification", (https://link.springer.com/chapter/10.1007/978-3-319-23534-9_2).
+ * Section 4.2 of the paper proves the correctness of the transformation and hints on use we implement here.
+ * Here we use a variant that halves the \p k (rounded up) in every iteration.
+ *
+ * Consider the definition of 1-inductive invariant as a single Horn clause in NNF:
+ * init(x^1) \lor (Inv(x^0) \land step(x^0,x^1)) \implies Inv(x^1)
+ *
+ * Unfolding this definition of $Inv$ k-1 times yields a formula equivalent to the definition of k-inductive invariant.
+ * Following the approach described in the paper, we can split the formula in two parts and compute an interpolant.
+ * Conjoining the interpolant to the original invariant yields k'-inductive invariant with k' < k.
+ * Depending on how we split the formula, we can get to different k'. The smallest k' we can get to is k/2 (rounded up).
+ *
+ * @param invariant k-inductive invsariant for the transition system \p system
+ * @param k
+ * @param system
+ * @return 1-inductive invariant for the same system that is logically stronger than the k-inductive one
+ */
+PTRef KTo1Inductive::unfold(PTRef invariant, unsigned k, TransitionSystem const & system) {
+    Logic & logic = system.getLogic();
+    TimeMachine tm(logic);
+    while (k > 1) {
+        // Split k into i + j such that i >= j
+        unsigned j = k / 2;
+        unsigned i = k - j;
+        // Build the two formulas
+        PTRef ipart = buildFormula(i, invariant, system);
+        PTRef jpart = i == j ? ipart : buildFormula(j, invariant, system);
+        PTRef shifted = tm.sendFlaThroughTime(jpart, i);
+        PTRef negatedInvariant = logic.mkNot(tm.sendFlaThroughTime(invariant, k));
+        SMTSolver solver(logic, SMTSolver::WitnessProduction::ONLY_INTERPOLANTS);
+        solver.assertProp(ipart);
+        solver.assertProp(logic.mkAnd(shifted, negatedInvariant));
+        auto res = solver.check();
+        if (res != SMTSolver::Answer::UNSAT) {
+            throw std::logic_error("Error in reducing k-inductive invariant to 1-inductive: Query must be UNSAT!");
+        }
+        auto itpContext = solver.getInterpolationContext();
+        vec<PTRef> itps;
+        ipartitions_t partitions = 1;
+        itpContext->getSingleInterpolant(itps, partitions);
+        assert(itps.size() == 1);
+        PTRef itp = tm.sendFlaThroughTime(itps[0], -static_cast<int>(i));
+        invariant = TermUtils(logic).conjoin(invariant, itp);
+        assert(i < k);
+        k = i;
+    }
+    return invariant;
+}
+
+PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) {
+    // std::cout << "Reducing k-inductive invariant with k=" << k << std::endl;
+    // Timer timer;
+    PTRef res = KTo1Inductive{KTo1Inductive::Mode::UNFOLD}.kinductiveToInductive(invariant, k, system);
+    // std::cout << timer.elapsedMilliseconds() << " ms" << std::endl;
+    return res;
 }

src/TransitionSystem.h

@@ -82,7 +82,19 @@ class TransitionSystem {
     PTRef toNextStateVar(PTRef var) const;
 };
 
-PTRef kinductiveToInductive(PTRef invariant, unsigned long k, TransitionSystem const & system);
+struct KTo1Inductive {
+    enum class Mode { UNFOLD, LEGACY };
+    explicit KTo1Inductive(Mode mode) : mode(mode) {}
+    [[nodiscard]] PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system) const;
+private:
+    Mode mode;
+
+    [[nodiscard]] static PTRef legacy(PTRef invariant, unsigned k, TransitionSystem const & system);
+    [[nodiscard]] static PTRef unfold(PTRef invariant, unsigned k, TransitionSystem const & system);
+
+};
+
+PTRef kinductiveToInductive(PTRef invariant, unsigned k, TransitionSystem const & system);