Skip to content
Commit 735d8ea0 authored by Mikhail R. Gadelha's avatar Mikhail R. Gadelha
Browse files

Created a tiny SMT interface and make Z3ConstraintManager implement it

Summary:
This patch implements a simple SMTConstraintManager API, and requires the implementation of two methods for now: `addRangeConstraints` and `isModelFeasible`.

Update Z3ConstraintManager to inherit it and implement required methods.

I also moved the method to dump the SMT formula from D45517 to this patch.

This patch was created based on the reviews from D47640.

Reviewers: george.karpenkov, NoQ, ddcc, dcoughlin

Reviewed By: george.karpenkov

Differential Revision: https://reviews.llvm.org/D47689

llvm-svn: 333899
parent 9438b159
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment