diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-29 13:26:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-29 13:26:51 -0500 |
| commit | d23ba1433846b9baaf6149137aa999c1af60c516 (patch) | |
| tree | b75389566b726edcaf32cb0f8ab2059bba9e1528 /examples/simple_vc_cxx.cpp | |
| parent | 6898ab93a3858e78b20af38e537fe48ee9140c58 (diff) | |
Add mkInteger to the API (#5274)
This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:
Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Diffstat (limited to 'examples/simple_vc_cxx.cpp')
| -rw-r--r-- | examples/simple_vc_cxx.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 49a4f576e..e648b9994 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -32,16 +32,16 @@ int main() { Term x = slv.mkConst(integer, "x"); Term y = slv.mkConst(integer, "y"); - Term zero = slv.mkReal(0); + Term zero = slv.mkInteger(0); Term x_positive = slv.mkTerm(Kind::GT, x, zero); Term y_positive = slv.mkTerm(Kind::GT, y, zero); - Term two = slv.mkReal(2); + Term two = slv.mkInteger(2); Term twox = slv.mkTerm(Kind::MULT, two, x); Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); - Term three = slv.mkReal(3); + Term three = slv.mkInteger(3); Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); Term formula = |