|
definition:
|
reduceAsInCmd :: SMT.Command -> SMT.Command
reduceAsInCmd c = case c of
SMT.Assert t -> SMT.Assert (reduceAsInTerm t)
SMT.DefineFunsRec fs -> SMT.DefineFunsRec $ map (\(fd,t) -> (fd, reduceAsInTerm t)) fs
SMT.GetValue ts -> SMT.GetValue (map reduceAsInTerm ts)
_ -> c
|
|
demand:
|
argument 1
|
|
deterministic:
|
deterministic operation
|
|
failfree:
|
_
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{({Assert}) |-> {Assert} || ({DefineFunsRec}) |-> _ || ({GetValue}) |-> {GetValue} || ({CheckSat}) |-> {CheckSat} || ({CheckSatAssuming}) |-> {CheckSatAssuming} || ({DeclareConst}) |-> {DeclareConst} || ({DeclareDatatype}) |-> {DeclareDatatype} || ({DeclareDatatypes}) |-> {DeclareDatatypes} || ({DeclareFun}) |-> {DeclareFun} || ({DeclareSort}) |-> {DeclareSort} || ({DefineFun}) |-> {DefineFun} || ({DefineFunRec}) |-> {DefineFunRec} || ({DefineSort}) |-> {DefineSort} || ({Echo}) |-> {Echo} || ({Exit}) |-> {Exit} || ({GetAssertions}) |-> {GetAssertions} || ({GetAssignment}) |-> {GetAssignment} || ({GetInfo}) |-> {GetInfo} || ({GetModel}) |-> {GetModel} || ({GetOption}) |-> {GetOption} || ({GetProof}) |-> {GetProof} || ({GetUnsatAssumptions}) |-> {GetUnsatAssumptions} || ({GetUnsatCore}) |-> {GetUnsatCore} || ({Pop}) |-> {Pop} || ({Push}) |-> {Push} || ({Reset}) |-> {Reset} || ({ResetAssertions}) |-> {ResetAssertions} || ({SetInfo}) |-> {SetInfo} || ({SetLogic}) |-> {SetLogic} || ({SetOption}) |-> {SetOption} || ({Comment}) |-> {Comment}}
|
|
name:
|
reduceAsInCmd
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Language.SMTLIB.Types.Command -> Language.SMTLIB.Types.Command
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
reducible on all ground data terms
|