Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve Yices usage #281

Open
marcogario opened this issue Jul 10, 2016 · 1 comment
Open

Improve Yices usage #281

marcogario opened this issue Jul 10, 2016 · 1 comment

Comments

@marcogario
Copy link
Contributor

There are some features of yices that we are currently not using, but it would make sense to integrate.

  1. Stand-alone model: We are currently using an EagerModel to represent the models of Yices. However, the method yices_get_model returns a stand-alone model. This object should be wrapped (as done for mathsat and z3), and returned when calling Solver.get_model
  2. Rich configuration options: The creation of a configuation for Yices is quite powerful. It includes multiple solvers for fragments of logics and modes of operations. We should at least consider the logic being passed to the solver (see code snippet below) and whether we are doing incremental calls or note (option 'mode' in yices API)
  3. Support for QF_NRA is given via MC-SAT. However, there are no clear methods to extract the value. In particular, it would seem that approximations of the results are given (instead of an exact solution as done by Z3).

Code-snippet for Logic to config:

config = yicespy.yices_new_config()
code = yicespy.yices_default_config_for_logic(config, str(logic))
if code != 0:
    raise InternalSolverError("Yices returned non-zero code upon assert"\
                              ": %s (code: %s)" % \
                              (yicespy.yices_error_string(), code))
self.yices = yicespy.yices_new_context(config)

# Other options to set:
# From Yices documentation:
# "mode"  | "one-shot"          |  only one call to check is supported
#         |                     |
#         | "multi-checks"      |  several calls to assert and check are
#         |                     |  possible
#         |                     |
#         | "push-pop"          |  like multi-check and with support for
#         |                     |  retracting assertions (via push/pop)
#         |                     |
#         | "interactive"       |  like push-pop, but with automatic context clean
#         |                     |  up when search is interrupted.
@marcogario
Copy link
Contributor Author

Improved option-handling is part of PR #338 .

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Status: Todo
Development

No branches or pull requests

1 participant