libsmt.rs icon indicating copy to clipboard operation
libsmt.rs copied to clipboard

Published 20 hours ago • verified publisher icon sushant94

Extend supported commands

Open sushant94 opened this issue 8 years ago • 0 comments

smtlib.rs currently only supports a few of the defined standard command. According to the SMTLIB2 standard the following functions are to be recognized and implemented for every solver:

  • [x] set-logic
  • [ ] define-fun
  • [x] declare-fun
  • [ ] declare-sort
  • [ ] define-sort
  • [x] assert
  • [ ] get-assertions
  • [x] check-sat
  • [ ] get-proof
  • [ ] get-unsat-core
  • [ ] get-value
  • [x] get-assignment
  • [ ] push
  • [ ] pop
  • [ ] get-option
  • [ ] set-option
  • [ ] get-info
  • [ ] set-info
  • [x] exit

We would like to support them all

sushant94 avatar Mar 02 '16 21:03 sushant94