Implement property generalization

modifiers/mod_ts_prop.cpp

@@ -17,9 +17,10 @@
 #include "modifiers/mod_ts_prop.h"
 
 #include "core/rts.h"
+#include "smt-switch/smt.h"
 #include "smt-switch/utils.h"
 #include "utils/logger.h"
-#include "utils/term_analysis.h"
+#include "utils/term_walkers.h"
 #include "utils/ts_manipulation.h"
 
 using namespace smt;
@@ -151,4 +152,59 @@ TransitionSystem promote_inputvars(const TransitionSystem & ts)
   return new_ts;
 }
 
+void generalize_property(TransitionSystem & ts, Term & prop)
+{
+  UnorderedTermSet free_variables;
+
+  // Get sets of all terms in INIT and TRANS.
+  SubTermCollector term_collector{ ts.solver() };
+  term_collector.collect_subterms(ts.init());
+  auto init_terms = term_collector.get_subterms();
+  auto init_predicates = term_collector.get_predicates();
+  term_collector.collect_subterms(ts.trans());
+  auto trans_terms = term_collector.get_subterms();
+  auto trans_predicates = term_collector.get_predicates();
+
+  // Filter out free variables that appear in INIT or TRANS, where they could
+  // have been added by constraints.
+  for (const auto & var_set : { ts.inputvars(), ts.statevars_with_no_update() })
+    for (const auto & var : var_set) {
+      if ((init_terms.count(var->get_sort()) == 0
+           || init_terms.at(var->get_sort()).count(var) == 0)
+          && init_predicates.count(var) == 0
+          && (trans_terms.count(var->get_sort()) == 0
+              || trans_terms.at(var->get_sort()).count(var) == 0)
+          && trans_predicates.count(var) == 0) {
+        free_variables.insert(var);
+      }
+    }
+
+  // Universally quantify all free variables (inputs and update-less states).
+  SubTermParametrizer term_parametrizer{ ts.solver(), free_variables };
+  auto parametrized_prop = term_parametrizer.parametrize_subterms(prop);
+  auto params = term_parametrizer.parameters();
+  if (params.size() == 0) {
+    // Nothing to generalize.
+    logger.log(1,
+               "Properties without free variables cannot be generalized yet");
+    return;
+  }
+  params.emplace_back(parametrized_prop);
+  auto generalized_prop = ts.solver()->make_term(PrimOp::Forall, params);
+
+  // Verify that this still implies the property.
+  ts.solver()->push();
+  ts.solver()->assert_formula(
+      ts.solver()->make_term(PrimOp::And,
+                             generalized_prop,
+                             ts.solver()->make_term(PrimOp::Not, prop)));
+  if (ts.solver()->check_sat().is_sat()) {
+    logger.log(1, "Property generalization failed, using original one");
+  } else {
+    prop = generalized_prop;
+    logger.log(1, "Generalized property to: {}", prop->to_string());
+  }
+  ts.solver()->pop();
+}
+
 }  // namespace pono

modifiers/mod_ts_prop.h

@@ -17,6 +17,7 @@
 #pragma once
 
 #include "core/ts.h"
+#include "smt-switch/smt.h"
 
 namespace pono {
 
@@ -50,4 +51,11 @@ void prop_in_trans(TransitionSystem & ts, const smt::Term & prop);
  */
 TransitionSystem promote_inputvars(const TransitionSystem & ts);
 
+/** Generalizes the property by adding quantifiers over variables that don't
+ *  have a next state defined which can help to prove it.
+ *  @param ts the transition system that the property refers to
+ *  @param prop the property to generalize, modified in place
+ */
+void generalize_property(TransitionSystem & ts, smt::Term & prop);
+
 }  // namespace pono

options/options.cpp

@@ -15,9 +15,11 @@
  **/
 
 #include "options/options.h"
+
 #include <iostream>
 #include <string>
 #include <vector>
+
 #include "optionparser.h"
 #include "utils/exceptions.h"
 
@@ -40,6 +42,7 @@ enum optionIndex
   STATICCOI,
   SHOW_INVAR,
   CHECK_INVAR,
+  GENERALIZE_PROP,
   RESET,
   RESET_BND,
   CLK,
@@ -222,6 +225,13 @@ const option::Descriptor usage[] = {
     Arg::None,
     "  --check-invar \tFor engines that produce invariants, check that they "
     "hold." },
+  { GENERALIZE_PROP,
+    0,
+    "",
+    "generalize-prop",
+    Arg::None,
+    "  --generalize-prop \tattempt to strengthen the property by universally "
+    "quantifying variables (default: false)" },
   { RESET,
     0,
     "r",
@@ -701,6 +711,7 @@ ProverResult PonoOptions::parse_and_set_options(int argc,
         case STATICCOI: static_coi_ = true; break;
         case SHOW_INVAR: show_invar_ = true; break;
         case CHECK_INVAR: check_invar_ = true; break;
+        case GENERALIZE_PROP: generalize_prop_ = true; break;
         case RESET: reset_name_ = opt.arg; break;
         case RESET_BND: reset_bnd_ = atoi(opt.arg); break;
         case CLK: clock_name_ = opt.arg; break;

options/options.h

@@ -100,6 +100,7 @@ class PonoOptions
         static_coi_(default_static_coi_),
         show_invar_(default_show_invar_),
         check_invar_(default_check_invar_),
+        generalize_prop_(default_generalize_prop_),
         ic3_pregen_(default_ic3_pregen_),
         ic3_indgen_(default_ic3_indgen_),
         ic3_gen_max_iter_(default_ic3_gen_max_iter_),
@@ -192,6 +193,7 @@ class PonoOptions
   bool static_coi_;
   bool show_invar_;   ///< display invariant when running from command line
   bool check_invar_;  ///< check invariants (if available) when run through CLI
+  bool generalize_prop_; ///< attempt to strengthen property before proving
   // ic3 options
   bool ic3_pregen_;  ///< generalize counterexamples in IC3
   bool ic3_indgen_;  ///< inductive generalization in IC3
@@ -304,6 +306,7 @@ class PonoOptions
   static const bool default_static_coi_ = false;
   static const bool default_show_invar_ = false;
   static const bool default_check_invar_ = false;
+  static const bool default_generalize_prop_ = false;
   static const size_t default_reset_bnd_ = 1;
   // TODO distinguish when solver is not set and choose a
   //      good solver for the provided engine automatically

pono.cpp

@@ -111,6 +111,10 @@ ProverResult check_prop(PonoOptions pono_options,
     prop_in_trans(ts, prop);
   }
 
+  if (pono_options.generalize_prop_) {
+    generalize_property(ts, prop);
+  }
+
   Property p(s, prop, prop_name);
 
   // end modification of the transition system and property

utils/term_walkers.cpp

@@ -16,7 +16,11 @@
 
 #include "utils/term_walkers.h"
 
+#include <algorithm>
+
 #include "assert.h"
+#include "smt-switch/identity_walker.h"
+#include "smt-switch/smt.h"
 #include "utils/term_analysis.h"
 
 using namespace smt;
@@ -123,4 +127,30 @@ WalkerStepResult SubTermCollector::visit_term(smt::Term & term)
   return Walker_Continue;
 }
 
+SubTermParametrizer::SubTermParametrizer(const smt::SmtSolver & solver,
+                                         const smt::UnorderedTermSet & filter)
+    : super(solver, true), filter_(filter)
+{
+}
+
+Term SubTermParametrizer::parametrize_subterms(Term & term)
+{
+  parameters_ = {};
+  auto new_term = visit(term);
+  reverse(parameters_.begin(), parameters_.end());
+  return new_term;
+}
+
+WalkerStepResult SubTermParametrizer::visit_term(Term & term)
+{
+  if (preorder_) {
+    if (filter_.count(term) > 0) {
+      auto param = solver_->make_param(term->to_string(), term->get_sort());
+      parameters_.emplace_back(param);
+      save_in_cache(term, param);
+    }
+  }
+  return super::visit_term(term);
+}
+
 }  // namespace pono

utils/term_walkers.h

@@ -15,8 +15,11 @@
 **/
 #pragma once
 
+#include <unordered_set>
+
 #include "smt-switch/identity_walker.h"
 #include "smt-switch/smt.h"
+#include "smt-switch/term.h"
 
 namespace pono {
 
@@ -67,7 +70,8 @@ class SubTermCollector : public smt::IdentityWalker
 
   void collect_subterms(smt::Term term);
 
-  const std::unordered_map<smt::Sort, smt::UnorderedTermSet> & get_subterms() const
+  const std::unordered_map<smt::Sort, smt::UnorderedTermSet> & get_subterms()
+      const
   {
     return subterms_;
   };
@@ -92,4 +96,32 @@ class SubTermCollector : public smt::IdentityWalker
   smt::WalkerStepResult visit_term(smt::Term & term) override;
 };
 
+/** Class for transforming a given set of subterms into parameters. */
+class SubTermParametrizer : public smt::IdentityWalker
+{
+ public:
+  /** Constructs a SubTermParametrizer for a given set of terms.
+   * @param solver the solver instance that the terms are defined in
+   * @param filter set of variables which should be searched for terms to replace
+   */
+  SubTermParametrizer(const smt::SmtSolver & solver,
+                      const smt::UnorderedTermSet & filter);
+
+  typedef smt::IdentityWalker super;
+
+  /** Replaces all occurences of the terms in filters with parameters
+   * @param term term to transform
+   * @return transformed term
+   */
+  smt::Term parametrize_subterms(smt::Term & term);
+
+  smt::TermVec parameters() const { return parameters_; };
+
+ protected:
+  smt::WalkerStepResult visit_term(smt::Term & term) override;
+
+  const smt::UnorderedTermSet filter_;
+  smt::TermVec parameters_;
+};
+
 }  // namespace pono