diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b38aa4e..1ecca6a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,9 +24,10 @@ jobs: with: repository: cvc5/cvc5 path: cvc5 - + - name: Install dependencies uses: ./cvc5/.github/actions/install-dependencies + working-directory: ./cvc5 with: with-documentation: false with-python-bindings: true diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 61d1cda..5138adb 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -6620,6 +6620,8 @@ def eval(self, t, model_completion=False): automatically added for symbols that do not have an interpretation in the model `self`. + This method is similar to the SMT-LIB `get-value` command. + >>> x = Int('x') >>> s = Solver() >>> s.add(x > 0, x < 2) @@ -6672,6 +6674,8 @@ def __getitem__(self, idx): The elements can be retrieved using position or the actual declaration. + This method is similar to the SMT-LIB `get-value` command. + >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> s = Solver() @@ -6718,7 +6722,10 @@ def decls(self): def evaluate(t): - """Evaluates the given term (assuming it is constant!)""" + """Evaluates the given term (assuming it is constant!) + + This method is similar to the SMT-LIB `get-value` command. + """ s = Solver() s.check() m = s.model()