BDD encoding of the at least n
BDD encoding of the at least n
the Boolean expression addressed by the at least
the bound
the equivalent BDD expression expressed as if-then-else
Express at most n with Sequential encoding
Express at most n with Sequential encoding
the Boolean expression addressed by the at most
the bound
the equivalent Boolean expression
Find the ith element of the enumeration sort of Z3 contained in a substitution variable
Find the ith element of the enumeration sort of Z3 contained in a substitution variable
the substitution constant
the value to find
the index of the value
Return the index of a given element in the enumeration sort of Z3 contained in a substitution variable
Return the index of a given element in the enumeration sort of Z3 contained in a substitution variable
the substitution constant
the value to find
the index of the value
Create a bit vector bounded variable
Create a bit vector bounded variable
the De Bruijn index
the bit vector sort
bounded variable
Create Z3 bit vector constant
Create Z3 bit vector constant
the name of the constant
the bit vector sort of the constant
the bitvector constant
Create a Boolean bounded variable
Create a Boolean bounded variable
the De Bruijn index
bounded variable
Create an uninterpreted Boolean constant
Create an uninterpreted Boolean constant
the identifier of the constant
Z3 Boolean constant
Create a predicate declaration
Create a predicate declaration
the name of the predicate
its domain
the function declaration
Create an if then else structure
Create an if then else structure
the type of the else and then expression
the if expression
the then expression
the else expression
the if-then-else term
Substitute the variable of Z3 SMT expression by some other variables
Substitute the variable of Z3 SMT expression by some other variables
the type of the expression
the type of the variables
the initial expression
the map from initial to new variables
the expression where variables have been substituted
Transform a set of
Transform a set of
the set of substitution variable / value couples
the conjunction of the "sub = val" equalities
(Since version KCR analyzer 1.0) Should use the Choose predicate to force value of a substitution predicate
Trait for utility operations on Z3 SMT terms