Simplify input format

Z3 supports input in the Simplify format. Use the command-line switch /s or the file extension .sx, .smp, or .simplify to invoke the Simplify parser.

Simplify extensions

Besides the usual Simplify constructs Z3 adds selected extensions.

Let-expressions

which are of the form:

     '('LET '(' ( '(' ( FORMULA | TERM )  id term-or-formula ')' )+ ')' term-or-formula ')'
  

If-then-else

If-then-else can be used in both formula and term context.

   '(' ITE cond then-formula else-formula ')'   - If-then-else formula.
   '(' ITE cond then-term else-term ')'         - If-then-else term.
 

Parameters

You can set and change selected parameters using Simplify commands. The parameters that can be set are:

    (SETPARAMETER SOFT_TIMEOUT <timeout>) - sets the soft timeout (in milliseconds) for queries.
    (SETPARAMETER VERBOSITY <level>) - sets the verbosity level for feedback on search progress.
 

Quantifiers

The following annotations may be used in connection with quantifier declarations.

    (WEIGHT <num>)       - Quantifiers are associated with weights indicating
                           how much the user expects instantiation of this particular
                           quantifier will cost. Heavier quantifiers are instantiated
                           more lazily.

    (SKOLEMID <id>)      - An annotation to control the names used during skolemization.

    (QID <id>)           - An annotation to identify the quantifier when tracing proof search.
 

Assumptions

You can check which axioms are used for proving a theorem by using CHECK* and use the command-line option DISPLAY_UNSAT_CORE=true.

Example:

(DEFPRED (member x s))
(DEFPRED (subset s1 s2))
(DEFPRED (seteq s1 s2))

(BG_PUSH
  (OR p1
  (FORALL (x s1 s2) 
          (IMPLIES (AND (member x s1) (subset s1 s2))
                   (member x s2)))))

(BG_PUSH
  (OR p2
  (FORALL (s1 s2)
          (IMPLIES (NOT (subset s1 s2))
                   (EXISTS (x)
                           (AND (member x s1)
                                (NOT (member x s2))))))))

(BG_PUSH
  (OR p3
  (FORALL (s1 s2)
          (IMPLIES (FORALL (x) 
                           (IMPLIES (member x s1) (member x s2)))
                   (subset s1 s2)))))

(BG_PUSH
  (OR p4
  (FORALL (s1 s2)
          (IFF (EQ s1 s2) (AND (subset s1 s2) (subset s2 s1))))))

(BG_PUSH
  (OR p5
  (FORALL (x s1 s2) 
          (IFF (member x (union s1 s2))
               (OR (member x s1) (member x s2))))))

(BG_PUSH
  (OR p6
  (FORALL (x s1 s2)
          (IFF (member x (difference s1 s2))
               (AND (member x s1) (NOT (member x s2)))))))

(BG_PUSH
  (OR p7
  (FORALL (s1 s2) (PATS (seteq s1 s2))
          (IFF (seteq s1 s2) (AND (subset s1 s2) (subset s2 s1))))
  ))

(BG_PUSH 
  (OR p8 (NOT (seteq (union a b) (union b a)))))

(CHECK* (NOT p1) (NOT p2) (NOT p3) (NOT p4) (NOT p5) (NOT p6) (NOT p7) (NOT p8))

A possible result is:

   1: Valid.
   (not p3)
   (not p5)
   (not p7)
   (not p8)