Merge pull request #369 from pysmt/i365/declare_variable

Remove Solver.declare_variable
pysmt · Oct 17, 2016 · 15de542 · 15de542
2 parents 5d74019 + 3f10894
commit 15de542
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 18 deletions.
diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py
@@ -100,8 +100,7 @@ def reset_assertions(self):
         self.cvc4.setLogic(self.logic_name)
 
     def declare_variable(self, var):
-        self.converter.declare_variable(var)
-        return
+        raise NotImplementedError
 
     def add_assertion(self, formula, named=None):
         self._assert_is_boolean(formula)

diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
@@ -199,7 +199,7 @@ def _reset_assertions(self):
 
     @clear_pending_pop
     def declare_variable(self, var):
-        self.converter.declare_variable(var)
+        raise NotImplementedError
 
     @clear_pending_pop
     def _add_assertion(self, formula, named=None):

diff --git a/pysmt/solvers/pico.py b/pysmt/solvers/pico.py
@@ -202,7 +202,6 @@ def _get_var_id(self, symbol):
             self._var_ids[symbol] = vid
             return vid
 
-
     @clear_pending_pop
     def reset_assertions(self):
         picosat.picosat_flushout(self._log_file_handler)
@@ -212,8 +211,7 @@ def reset_assertions(self):
 
     @clear_pending_pop
     def declare_variable(self, var):
-        # no need to declare variables
-        pass
+        raise NotImplementedError
 
     def _get_pico_lit(self, lit):
         mult = 1
@@ -225,7 +223,6 @@ def _get_pico_lit(self, lit):
         vid = self._get_var_id(var)
         return vid * mult
 
-
     @clear_pending_pop
     @catch_conversion_error
     def add_assertion(self, formula, named=None):

diff --git a/pysmt/solvers/solver.py b/pysmt/solvers/solver.py
@@ -19,6 +19,7 @@
 
 from pysmt.typing import BOOL
 from pysmt.exceptions import SolverReturnedUnknownResultError
+from pysmt.decorators import deprecated
 from six.moves import xrange
 
 
@@ -212,13 +213,6 @@ def reset_assertions(self):
         """Removes all defined assertions."""
         raise NotImplementedError
 
-    def declare_variable(self, var):
-        """Declare a variable in the solver.
-
-        :type var: FNode
-        """
-        raise NotImplementedError
-
     def add_assertion(self, formula, named=None):
         """Add assertion to the solver."""
         raise NotImplementedError

diff --git a/pysmt/solvers/yices.py b/pysmt/solvers/yices.py
@@ -159,8 +159,7 @@ def reset_assertions(self):
 
     @clear_pending_pop
     def declare_variable(self, var):
-        self.declarations.add(var)
-        return
+        raise NotImplementedError
 
     @clear_pending_pop
     def add_assertion(self, formula, named=None):

diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
@@ -158,8 +158,7 @@ def _reset_assertions(self):
 
     @clear_pending_pop
     def declare_variable(self, var):
-        self.declarations.add(var)
-        return
+        raise NotImplementedError
 
     @clear_pending_pop
     def _add_assertion(self, formula, named=None):