Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 8 additions & 1 deletion cvc5_pythonic_api/cvc5_pythonic.py
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it similar or does it correspond to?


>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down