CODEWITHSUNDEEP
z3
Anton
Anton

Reputation: 559

strange output using ctx-simplify tactic

Small example is prepared below:

(declare-datatypes () ((Type1 a b c d e g h i f k l m n o p q r s t u v w z)))
(declare-const x Type1)
(declare-const y Type1)
(assert (and (= y x) (or (and (not (= x g)) (not (= x a))) (and (or (not (= x g)) (not (= x q))) (not (= x a))))))
(apply ctx-simplify)

The output is:

(goals
(goal
  (= y x)
  (or (not and) (not (= x a)))
  :precision precise :depth 1)
)

What (or (not and) (not (= x a))) means? Bug?

Thank you.

Upvotes: 0

Views: 127

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Thanks for pointing this out. I agree it looks strange with the "and" taking no arguments in the printout. The context simplifier creates a conjunction with 0 arguments. It gets printed as simply "and". So the expression returned by ctx-simplify is equivalent to (not (= x a)). I will update the ctx-simplify tactic to return expressions without the empty conjunction.

Upvotes: 1

Related Questions