Fix naming of automatically generated next-state variables (stanford-…

…centaur#349)

If a user has state variables called both `x` and `x.next` in their BTOR2 file, Pono currently throws an error, because `TransitionSystem.make_statevar` creates two solver symbols, an identically-named one for the current value of the state variable, and one with `".next"` appended for the next value. This PR changes the suffix to be something that is less likely to clash with actual signals. It is still possible to cause a crash deliberately, but the only way to avoid that would be to make the variable names less readable and using something like an UUID.

Changes included in this commit:
* Unify TS constructors
* Make next-state suffix configurable
* Change TS test to exhibit bug
* Change default next-state suffix

core/ts.cpp

@@ -41,6 +41,7 @@ void swap(TransitionSystem & ts1, TransitionSystem & ts2)
   std::swap(ts1.no_state_updates_, ts2.no_state_updates_);
   std::swap(ts1.next_map_, ts2.next_map_);
   std::swap(ts1.curr_map_, ts2.curr_map_);
+  std::swap(ts1.next_suffix_, ts2.next_suffix_);
   std::swap(ts1.functional_, ts2.functional_);
   std::swap(ts1.deterministic_, ts2.deterministic_);
   std::swap(ts1.constraints_, ts2.constraints_);
@@ -128,6 +129,8 @@ TransitionSystem::TransitionSystem(const TransitionSystem & other_ts,
   for (const auto & e : other_ts.constraints_) {
     constraints_.push_back({ transfer_as(e.first, BOOL), e.second });
   }
+
+  next_suffix_ = other_ts.next_suffix_;
   functional_ = other_ts.functional_;
   deterministic_ = other_ts.deterministic_;
 }
@@ -146,6 +149,7 @@ bool TransitionSystem::operator==(const TransitionSystem & other) const
           no_state_updates_ == other.no_state_updates_ &&
           next_map_ == other.next_map_ &&
           curr_map_ == other.curr_map_ &&
+          next_suffix_ == other.next_suffix_ &&
           functional_ == other.functional_ &&
           deterministic_ == other.deterministic_ &&
           constraints_ == other.constraints_);
@@ -292,7 +296,7 @@ Term TransitionSystem::make_statevar(const string name, const Sort & sort)
   deterministic_ = false;
 
   Term state = solver_->make_symbol(name, sort);
-  Term next_state = solver_->make_symbol(name + ".next", sort);
+  Term next_state = solver_->make_symbol(name + next_suffix_, sort);
   add_statevar(state, next_state);
   return state;
 }

core/ts.h

@@ -32,19 +32,17 @@ class TransitionSystem
    *  it supports the most theories and doesn't rewrite-on-the-fly or alias
    * sorts
    *  this makes it a great candidate for representing the TransitionSystem */
-  TransitionSystem()
-      : solver_(smt::Cvc5SolverFactory::create(false)),
-        init_(solver_->make_term(true)),
-        trans_(solver_->make_term(true)),
-        functional_(false),
-        deterministic_(false)
+  TransitionSystem() : TransitionSystem(smt::Cvc5SolverFactory::create(false))
   {
   }
 
-  TransitionSystem(const smt::SmtSolver & s)
+  TransitionSystem(
+      const smt::SmtSolver & s,
+      const std::string & next_state_suffix = ".pono_generated__next")
       : solver_(s),
         init_(s->make_term(true)),
         trans_(s->make_term(true)),
+        next_suffix_(next_state_suffix),
         functional_(false),
         deterministic_(false)
   {
@@ -69,7 +67,7 @@ class TransitionSystem
    */
   TransitionSystem(const TransitionSystem & other_ts, smt::TermTranslator & tt);
 
-  virtual ~TransitionSystem(){};
+  virtual ~TransitionSystem() {};
 
   /** Equality comparison between TransitionSystems
    *  compares each member variable
@@ -524,6 +522,9 @@ class TransitionSystem
   // maps next back to curr
   smt::UnorderedTermMap curr_map_;
 
+  // Text appended to generate names for next-state variables.
+  std::string next_suffix_;
+
   // whether the TransitionSystem is functional
   bool functional_;
   // whether the TransitionSystem is fully deterministic

tests/test_ts.cpp

@@ -57,8 +57,8 @@ TEST_P(TSUnitTests, FTS_IsFunc)
   EXPECT_FALSE(fts.is_deterministic());
   EXPECT_EQ(fts.statevars_with_no_update().size(), 0);
 
-  Term z = fts.make_statevar("z", bvsort);
-  EXPECT_EQ(fts.statevars_with_no_update(), UnorderedTermSet({z}));
+  Term ynext = fts.make_statevar("y.next", bvsort);
+  EXPECT_EQ(fts.statevars_with_no_update(), UnorderedTermSet({ynext}));
 
   TransitionSystem ts_copy = fts;
   EXPECT_EQ(fts.is_functional(), ts_copy.is_functional());