getConsequences method

List<Expr>? getConsequences(
  1. List<Expr> assumptions,
  2. List<Expr> variables
)

Implementation

List<Expr>? getConsequences(List<Expr> assumptions, List<Expr> variables) {
  final assumptionsVec = _c._packAstVector(assumptions);
  _c._z3.ast_vector_inc_ref(assumptionsVec);
  final variablesVec = _c._packAstVector(variables);
  _c._z3.ast_vector_inc_ref(variablesVec);
  final consequencesVec = _c._z3.mk_ast_vector();
  _c._z3.ast_vector_inc_ref(consequencesVec);
  final result = _c._bool(_c._z3.solver_get_consequences(
    _solver,
    assumptionsVec,
    variablesVec,
    consequencesVec,
  ));
  final consequences = _c._unpackAstVector(consequencesVec).cast<Expr>();
  _c._z3.ast_vector_dec_ref(assumptionsVec);
  _c._z3.ast_vector_dec_ref(variablesVec);
  _c._z3.ast_vector_dec_ref(consequencesVec);
  if (result == false) {
    return null;
  }
  return consequences;
}