Automatically promote input variables in BTOR2 constraints (#261)

* Add promote_inputvar feature to TS

* Automatically promote input variables in BTOR2 constraints

* Add test for input constraints in btor2 file

core/ts.cpp

@@ -648,6 +648,23 @@ void TransitionSystem::drop_state_updates(const TermVec & svs)
   }
 }
 
+void TransitionSystem::promote_inputvar(const Term & iv)
+{
+  size_t num_erased = inputvars_.erase(iv);
+  if (!num_erased) {
+    throw PonoException("Tried to promote non-input to state variable: "
+                        + iv->to_string());
+  }
+
+  // now turn into a state variable
+
+  // set to false until there is a next state update for this statevar
+  deterministic_ = false;
+  Term next_state_var =
+      solver_->make_symbol(iv->to_string() + ".next", iv->get_sort());
+  add_statevar(iv, next_state_var);
+}
+
 void TransitionSystem::replace_terms(const UnorderedTermMap & to_replace)
 {
   // first check that all the replacements contain known symbols

core/ts.h

@@ -306,6 +306,19 @@ class TransitionSystem
    */
   void drop_state_updates(const smt::TermVec & svs);
 
+  /** EXPERTS ONLY
+   *  Turns an input variable into a state variable
+   *  IMPORTANT: this does not retroactively change constraints
+   *  e.g. if a constraint was not added to init because it
+   *  contains an input variable
+   *
+   *  @param iv the input variable to promote
+   *
+   *  The input variable iv stays the same, but it will now
+   *  be registered as a state variable.
+   */
+  void promote_inputvar(const smt::Term & iv);
+
   /** EXPERTS ONLY
    * Replace terms in the transition system with other terms
    *  Traverses all the data structures and updates them with

frontends/btor2_encoder.cpp

@@ -347,6 +347,17 @@ void BTOR2Encoder::parse(const std::string filename)
       }
     } else if (l_->tag == BTOR2_TAG_constraint) {
       Term constraint = bv_to_bool(termargs_[0]);
+
+      // BTOR2 allows constraints over inputs
+      // in Pono these need to be promoted to state variables
+      UnorderedTermSet free_vars;
+      get_free_symbolic_consts(constraint, free_vars);
+      for (const auto & v : free_vars) {
+        if (ts_.is_input_var(v)) {
+          ts_.promote_inputvar(v);
+        }
+      }
+
       ts_.add_constraint(constraint);
       terms_[l_->id] = constraint;
     } else if (l_->tag == BTOR2_TAG_init) {