Skip to content

Use one-time Environments for PySmt calls #302

@Langenfeld

Description

@Langenfeld

We are currently using the default pysmt environment for everything. This works well until a variable that was created with one type is assigned another type and one wants to re-run something with pysmt (e.g. the simulator). Then pysmt will complain that the variable is already existing and does have another type.

Recreate:

  1. Define variable foo with type bool
  2. Run simulator on a requirement that uses foo
  3. Change type of foo to int
  4. Try to create a new simulator instance for the requirement using foo

Fix: Use new Envorionment for each and every operation of the simulator, quickchecks, (automaton pattern) etc.
Unfortunately everything then has to come from an Environment like in the following example:

from pysmt.environment import Environment

def solve():
    env = Environment()
    mgr = env.formula_manager
    tm  = env.type_manager

    x = mgr.Symbol("x", tm.IntType())
    y = mgr.Symbol("y", tm.BoolType())

    solver = env.factory.Solver(name="z3")
    solver.add_assertion(mgr.GT(x, mgr.Int(0)))
    solver.add_assertion(y)

    return solver.solve()

print(solve())

As the environment has to be the same for one task, this will be a major refactor. Also, pysmt.shortcuts should not work anymore.

Metadata

Metadata

Assignees

No one assigned

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions