From 4106b9314285c4f8641af414566e9382e2e1bfec Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 11 Mar 2022 15:46:38 -0800
Subject: [PATCH] [API/Python] Add support for `Solver::getModel()` (#8267)

This commit implements support for Solver::getModel() in the Python API,
which was missing before.
---
 src/api/python/cvc5.pxd             |  2 ++
 src/api/python/cvc5.pxi             | 30 +++++++++++++++++++++++
 test/unit/api/python/test_solver.py | 38 +++++++++++++++++++++++++++++
 3 files changed, 70 insertions(+)

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 740a58a03..adad1467b 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -284,6 +284,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         vector[Term] getValue(const vector[Term]& terms) except +
         vector[Term] getModelDomainElements(Sort sort) except +
         bint isModelCoreSymbol(Term v) except +
+        string getModel(const vector[Sort]& sorts,
+                        const vector[Term]& consts) except +
         void declareSepHeap(Sort locSort, Sort dataSort) except +
         Term getValueSepHeap() except +
         Term getValueSepNil() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index b259687b4..b5b101231 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2117,6 +2117,36 @@ cdef class Solver:
         """
         return self.csolver.isModelCoreSymbol(v.cterm)
 
+    def getModel(self, sorts, consts):
+        """Get the model
+
+        SMT-LIB:
+
+        .. code:: smtlib
+        
+            (get-model)
+
+        Requires to enable option
+        :ref:`produce-models <lbl-option-produce-models>`.
+   
+        :param sorts: The list of uninterpreted sorts that should be printed in
+                      the model.
+        :param vars: The list of free constants that should be printed in the
+                     model. A subset of these may be printed based on
+                     isModelCoreSymbol.
+        :return: a string representing the model.
+        """
+
+        cdef vector[c_Sort] csorts
+        for sort in sorts:
+            csorts.push_back((<Sort?> sort).csort)
+
+        cdef vector[c_Term] cconsts
+        for const in consts:
+            cconsts.push_back((<Term?> const).cterm)
+
+        return self.csolver.getModel(csorts, cconsts)
+
     def getValueSepHeap(self):
         """When using separation logic, obtain the term for the heap.
 
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index a535c2502..5125b2e00 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -2379,6 +2379,44 @@ def test_is_model_core_symbol(solver):
         solver.isModelCoreSymbol(zero)
 
 
+def test_get_model(solver):
+    solver.setOption("produce-models", "true")
+    uSort = solver.mkUninterpretedSort("u")
+    x = solver.mkConst(uSort, "x")
+    y = solver.mkConst(uSort, "y")
+    z = solver.mkConst(uSort, "z")
+    f = solver.mkTerm(Kind.Not, solver.mkTerm(Kind.Equal, x, y))
+    solver.assertFormula(f)
+    solver.checkSat()
+    sorts = [uSort]
+    terms = [x, y]
+    solver.getModel(sorts, terms)
+    null = cvc5.Term(solver)
+    terms.append(null)
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+
+def test_get_model2(solver):
+    solver.setOption("produce-models", "true")
+    sorts = []
+    terms = []
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+
+def test_get_model3(solver):
+    solver.setOption("produce-models", "true")
+    sorts = []
+    terms = []
+    solver.checkSat()
+    solver.getModel(sorts, terms)
+    integer = solver.getIntegerSort()
+    sorts.append(integer)
+    with pytest.raises(RuntimeError):
+        solver.getModel(sorts, terms)
+
+
 def test_issue5893(solver):
     slv = cvc5.Solver()
     bvsort4 = solver.mkBitVectorSort(4)
-- 
2.30.2