1

I'm just getting started out and I'm curious if there is a way to add hypotheses. Using (assert ...) isn't what I want as for my application sometimes the assumptions are allowed to be false and therefore everything should become satisfiable. I know I can just use implications such as (assert (implies assumption conclusion)) but if there are many assumptions, it seems clumsy convert all of my assertions into implications. Roughly I'd like to have an interaction model like

(assume ...)

...

(assume ...)

(assert ...)

...

(assert ...)

(check-sat)

user1063042
  • 273
  • 2
  • 11

1 Answers1

1

Using assert with implications is the way to go, there is no assume (see the SMT-LIB manual, section 3.9, http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf ).

If you have many assertions you'd like to use as assumptions, you may want to use one of the programmatic APIs to help automate this conversion for you: http://z3.codeplex.com/documentation

Alternatively, if the assertions are simple enough, you could just write a script operating on string representations of the assertions to print the SMT-LIB formulas with the implications.

You may also be interested in this: Soft/Hard constraints in Z3

Community
  • 1
  • 1
Taylor T. Johnson
  • 2,834
  • 16
  • 17