Introduce monitor state when creating a property

core/prop.cpp

@@ -14,10 +14,13 @@
  **
  **/
 
-#include "smt-switch/utils.h"
-
 #include "core/prop.h"
+
+#include "assert.h"
+#include "core/rts.h"
+#include "smt-switch/utils.h"
 #include "utils/exceptions.h"
+#include "utils/logger.h"
 
 using namespace smt;
 
@@ -26,23 +29,14 @@ namespace pono {
 Property::Property(TransitionSystem & ts, const Term & p, std::string name)
   : ts_(ts), prop_(p), name_(name)
 {
-  const UnorderedTermSet & states = ts.statevars();
-  TermVec free_vars;
-  get_free_symbolic_consts(p, free_vars);
-  for (auto s : free_vars) {
-    if (!ts.is_curr_var(s))
-    {
-      throw PonoException("Property should only use state variables");
-    }
-  }
-
   // find a name if it wasn't provided
   // if no name is associated with it in the ts, then it will just
   // be the to_string of the term
   if (name_.empty())
   {
     name_ = ts_.get_name(prop_);
   }
+  initialize();
 }
 
 Property::Property(Property & prop, TermTranslator & tt)
@@ -58,4 +52,50 @@ Property::Property(Property & prop, TermTranslator & tt)
 
 Property::~Property() {}
 
+void Property::initialize()
+{
+  if (ts_.only_curr(prop_)) {
+    // nothing to do
+    return;
+  }
+
+  // otherwise, need to make sure prop_ is over state vars
+  logger.log(1,
+             "Got next state or input variables in property. Generating a "
+             "monitor state.");
+
+  Term monitor;
+  size_t id = 0;
+  while (true) {
+    try {
+      monitor = ts_.make_statevar("_monitor_" + std::to_string(id),
+                                  ts_.make_sort(BOOL));
+      break;
+    }
+    catch (SmtException & e) {
+      ++id;
+    }
+  }
+  assert(monitor);
+
+  // monitor starts true
+  ts_.constrain_init(monitor);
+
+  if (ts_.no_next(prop_)) {
+    ts_.assign_next(monitor, prop_);
+    ;
+  } else if (!ts_.is_functional()) {
+    RelationalTransitionSystem & rts =
+        static_cast<RelationalTransitionSystem &>(ts_);
+    rts.constrain_trans(rts.make_term(Equal, rts.next(monitor), prop_));
+  } else {
+    assert(ts_.is_functional());
+    throw PonoException(
+        "Cannot use next in property of a functional transition system.");
+  }
+
+  // update prop_
+  prop_ = monitor;
+}
+
 }  // namespace pono

core/prop.h

@@ -42,9 +42,11 @@ class Property
   std::string name() { return name_; };
 
  private:
+  void initialize();
+
   TransitionSystem ts_;
 
-  const smt::Term prop_;
+  smt::Term prop_;
 
   std::string name_; ///< a name for the property. If no name is given, just uses the to_string
 

engines/mbic3.cpp

@@ -142,6 +142,9 @@ void ModelBasedIC3::initialize()
   frames_.push_back({ ts_.init() });
   push_frame();
 
+  assert(ts_.only_curr(bad_));
+  assert(ts_.only_curr(ts_.init()));
+
   // check if there are arrays or uninterpreted sorts and fail if so
   for (auto vec : { ts_.statevars(), ts_.inputvars() }) {
     for (auto st : vec) {

engines/prover.cpp

@@ -61,7 +61,7 @@ Prover::Prover(const PonoOptions & opt,
       orig_ts_(p.transition_system()),
       unroller_(ts_, solver_),
       options_(opt)
-{  
+{
 }
 
 Prover::~Prover() {}
@@ -70,6 +70,7 @@ void Prover::initialize()
 {
   reached_k_ = -1;
   bad_ = solver_->make_term(smt::PrimOp::Not, property_.prop());
+  assert(ts_.only_curr(bad_));
   if (options_.static_coi_) {
     if (!ts_.is_functional())
       throw PonoException("Temporary restriction: cone-of-influence analysis currently "\
@@ -117,7 +118,7 @@ void Prover::print_term_dfs(const Term & term)
       cout << "  visiting term: " << cur << "\n";
       if (cur->is_symbol())
         cout << "    ..is symbol\n";
-      
+
       for (auto child : cur) {
         cout << "    pushing child: " << child << "\n";
         open_terms.push_back(child);
@@ -148,8 +149,7 @@ void Prover::print_coi_info()
     cout << "  " << statevar << "\n";
 
   cout << "constraints: \n";
-  for (auto constr : ts_.constraints())
-    cout << "  " << constr << "\n";  
+  for (auto constr : ts_.constraints()) cout << "  " << constr << "\n";
 }
 
 /* Add 'term' to 'set' if it does not already appear there. */
@@ -196,7 +196,7 @@ void Prover::compute_term_coi(const Term & term,
           collect_coi_term(new_coi_input_vars, cur);
         }
       }
-      
+
       for (auto child : cur) {
         logger.log(3, "    pushing child: {}", child);
         open_terms.push_back(child);
@@ -244,9 +244,9 @@ void Prover::compute_coi_next_state_funcs()
     for (auto sv : new_coi_input_vars) {
       collect_coi_term(inputvars_in_coi_, sv);
     }
-         
+
     new_coi_state_vars.clear();
-    new_coi_input_vars.clear();  
+    new_coi_input_vars.clear();
   }
 }
 
@@ -263,10 +263,10 @@ void Prover::compute_coi_trans_constraints()
   }
 
   /* Add newly collected variables to global collections. */
-  for (auto sv : new_coi_state_vars) 
+  for (auto sv : new_coi_state_vars)
     if (statevars_in_coi_.find(sv) == statevars_in_coi_.end())
       statevars_in_coi_.insert(sv);
-  
+
   for (auto sv : new_coi_input_vars)
     if (inputvars_in_coi_.find(sv) == inputvars_in_coi_.end())
       inputvars_in_coi_.insert(sv);
@@ -341,7 +341,7 @@ void Prover::compute_coi()
       logger.log(3, "  - inputvar {}", var);
   }
 }
-  
+
 bool Prover::witness(std::vector<UnorderedTermMap> & out)
 {
   // TODO: make sure the solver state is SAT

frontends/btor2_encoder.cpp

@@ -402,31 +402,9 @@ void BTOR2Encoder::parse(const std::string filename)
       no_next_states_.erase(id2statenum.at(l_->args[0]));
     } else if (l_->tag == BTOR2_TAG_bad) {
       Term bad = bv_to_bool(termargs_[0]);
-      TermVec free_vars;
-      get_free_symbolic_consts(bad, free_vars);
-      const UnorderedTermSet & states = ts_.statevars();
-
-      bool need_witness = false;
-      for (auto s : free_vars) {
-        if (states.find(s) == states.end()) {
-          need_witness = true;
-          break;
-        }
-      }
-
-      if (need_witness) {
-        Term witness =
-            ts_.make_statevar("witness_" + std::to_string(witness_id_++),
-                              solver_->make_sort(BOOL));
-        ts_.constrain_init(witness);
-        ts_.assign_next(witness, solver_->make_term(Not, bad));
-        propvec_.push_back(witness);
-        terms_[l_->id] = witness;
-      } else {
-        Term prop = solver_->make_term(Not, bad);
-        propvec_.push_back(prop);
-        terms_[l_->id] = prop;
-      }
+      Term prop = solver_->make_term(Not, bad);
+      propvec_.push_back(prop);
+      terms_[l_->id] = prop;
     } else if (l_->tag == BTOR2_TAG_justice) {
       std::cout << "Warning: ignoring justice term" << std::endl;
       justicevec_.push_back(termargs_[0]);