diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-30 22:22:24 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-30 22:22:24 -0600 |
commit | 6489cf590b441aeb5e1bdf9800c9718d06842149 (patch) | |
tree | 98eaa6adb49fea33593a770d37d2e89cc7c15bbb /src/smt/quant_elim_solver.h | |
parent | acdffc72bd559fa4b64da2ee2b3373208354e7a1 (diff) |
More fixes for quantifier elimination (#5533)
Fixes #5506, fixes #5507.
Diffstat (limited to 'src/smt/quant_elim_solver.h')
-rw-r--r-- | src/smt/quant_elim_solver.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ |