Appendix: Syntax summaryΒΆ
The following code illustrates the syntax of the various blocks used in IDP-Z3.
T denotes a type, c a constructor, p a proposition or predicate, f a constant or function. The equivalent ASCII-only encoding is shown on the right.
vocabulary V {
type T
type T := {c1, c2, c3}
type T := constructed from {c1, c2(T1, f:T2)}
type T := {1,2,3}
type T := {1..3}
// built-in types: πΉ, β€, β, Date, Concept Bool, Int, Real, Date, Concept
p : () β πΉ p: () -> Bool
p1, p2 : T1 β¨― T2 β πΉ p1, p2: T1*T2 -> Bool
f: T β T f: T -> T
f1, f2: Concept[T1->T2] β T f1, f2: Concept[T1->T2] -> T
[this is the intended meaning of p]
p : () β πΉ
extern vocabulary W
}
theory T:V {
(Β¬p1()β§p2() β¨ p3() β p4() β p5()) β p6(). (~p1()&p2() | p3() => p4() <=> p5()) <= p6().
p(f1(f2())).
f1() < f2() β€ f3() = f4() β₯ f5() > f6(). f1() < f2() =< f3() = f4() >= f5() > f6().
f() β c. f() ~= c.
βx,y β T: p(x,y). !x,y in T: p(x,y).
βx β p, (y,z) β q: q(x,x) β¨ p(y) β¨ p(z). !x in p, (y,z) in q: q(x,x) | p(y) | p(z).
βx β Concept[()βB]: $(x)(). ?x in Concept[()->B]: $(x)().
βx β Concept: arity(x)=0 β§ $(x)(). ?x in Concept: arity(x)=0 & $(x)().
βx β $(input_domain(`p,1)): p(x). ?x in $(input_domain(`p,1)): p(x).
βx: p(x). ?x: p(x).
f() in {1,2,3}.
f() = #{xβT: p(x)}. f() = #{x in T: p(x)}.
f() = sum(lambda xβT: f(x)). f() = sum(lambda x in T: f(x)).
if p1() then p2() else p3().
f1() = if p() then f2() else f3().
p := {1,2,3}
p(#2020-01-01) is enumerated.
p(#TODAY) is not enumerated.
{ p(1).
βxβT: p1(x) β p2(x). !x in T: p1(x) <- p2(x).
f(1)=1.
βx: f(x)=1 β p(x). !x: f(x)=1 <- p(x).
}
[this is the intended meaning of the rule]
p().
}
structure S:V {
p := false
p := {1,2,3}
p := {0..9, 100}
p := {#2021-01-01}
p := {(1,2), (3,4)}
p := {
1 2
3 4
}
f := 1
f := {β1} f := {-> 1}
f := {1β1, 2β2} f := {1->1, 2->2}
f := {(1,2)β3} else 2 f := {(1,2)->3} else 2
}
display {
goal_symbol := {`p1, `p2}
hide(`p).
expand := {`p}.
view() = expanded.
optionalPropagation().
}
procedure main() {
pretty_print(model_check (T,S))
pretty_print(model_expand (T,S))
pretty_print(model_propagate(T,S))
}
See also the Built-in functions.