SMTLIB: Supporting custom sorts in generic solvers (#524)

Fixed support for custom sorts in SMT-LIB interface to generic solvers

pysmt/smtlib/solver.py

@@ -25,7 +25,7 @@
 from pysmt.solvers.solver import Solver, SolverOptions
 from pysmt.exceptions import (SolverReturnedUnknownResultError,
                               UnknownSolverAnswerError, PysmtValueError)
-
+from pysmt.oracles import TypesOracle
 
 class SmtLibOptions(SolverOptions):
     """Options for the SmtLib Solver.
@@ -78,10 +78,11 @@ def __init__(self, args, environment, logic, LOGICS=None, **options):
                         environment,
                         logic=logic,
                         **options)
-
+        self.to = self.environment.typeso
         if LOGICS is not None: self.LOGICS = LOGICS
         self.args = args
         self.declared_vars = set()
+        self.declared_sorts = set()
         self.solver = Popen(args, stdout=PIPE, stderr=PIPE, stdin=PIPE,
                             bufsize=-1)
         # Give time to the process to start-up
@@ -132,6 +133,11 @@ def _get_value_answer(self):
         lst = self.parser.get_assignment_list(self.solver_stdout)
         self._debug("Read: %s", lst)
         return lst
+
+    def _declare_sort(self, sort):
+        cmd = SmtLibCommand(smtcmd.DECLARE_SORT, [sort])
+        self._send_silent_command(cmd)
+        self.declared_sorts.add(sort)
 
     def _declare_variable(self, symbol):
         cmd = SmtLibCommand(smtcmd.DECLARE_FUN, [symbol])
@@ -164,6 +170,10 @@ def add_assertion(self, formula, named=None):
         # This is needed because Z3 (and possibly other solvers) incorrectly
         # recognize N * M * x as a non-linear term
         formula = formula.simplify()
+        sorts = self.to.get_types(formula, custom_only=True)
+        for s in sorts:
+            if s not in self.declared_sorts:
+                self._declare_sort(s)
         deps = formula.get_free_variables()
         for d in deps:
             if d not in self.declared_vars:

pysmt/test/smtlib/test_generic_wrapper.py

@@ -20,7 +20,7 @@
 
 from pysmt.test import TestCase, main
 from pysmt.shortcuts import get_env, Solver, is_valid, is_sat
-from pysmt.shortcuts import LE, LT, Real, GT, Int, Symbol, And, Not
+from pysmt.shortcuts import LE, LT, Real, GT, Int, Symbol, And, Not, Type, FunctionType, Equals, Function
 from pysmt.typing import BOOL, REAL, INT
 from pysmt.logics import QF_UFLIRA, QF_UFLRA, QF_UFLIA, QF_BOOL, QF_UFBV
 from pysmt.exceptions import (SolverRedefinitionError, NoSolverAvailableError,
@@ -110,6 +110,21 @@ def test_generic_wrapper_eager_model(self):
             self.assertFalse(model.get_value(b).is_true())
             self.assertTrue(model.get_value(a).is_true())
 
+
+    @skipIf(len(ALL_WRAPPERS) == 0, "No wrapper available")
+    def test_custom_types(self):
+        A = Type("A", 0)
+        a, b = Symbol("a", A), Symbol("b", A)
+        p = Symbol("p", INT)
+        fun = Symbol("g", FunctionType(A, [INT, A]))
+        app = Function(fun, [p, b])
+        f_a = Equals(a, app)
+        for n in self.all_solvers:
+            with Solver(name=n, logic=QF_UFLIA) as s:
+                s.add_assertion(f_a)
+                res = s.solve()
+                self.assertTrue(res)
+
     @skipIf(len(ALL_WRAPPERS) == 0, "No wrapper available")
     def test_examples(self):
         for name in self.all_solvers: