diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 15:24:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-07-10 15:24:22 +0000 |
commit | ff5ecc85124857dccb6fa6ed542bb90e678bdc77 (patch) | |
tree | 1ae254a832b4f93666a81d8b3a07340066b24a7a /examples/simple_vc_cxx.cpp | |
parent | 00af00c419b965ed26fff540a565dee748c7e4ed (diff) |
* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)
* adding as examples the programs i used to translate nonlinear smt2 problems to other formats
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 819b1fc97..557199e75 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -37,16 +37,16 @@ int main() { Expr x = em.mkVar("x", integer); Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(Integer(0)); + Expr zero = em.mkConst(Rational(0)); Expr x_positive = em.mkExpr(kind::GT, x, zero); Expr y_positive = em.mkExpr(kind::GT, y, zero); - Expr two = em.mkConst(Integer(2)); + Expr two = em.mkConst(Rational(2)); Expr twox = em.mkExpr(kind::MULT, two, x); Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); - Expr three = em.mkConst(Integer(3)); + Expr three = em.mkConst(Rational(3)); Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); BoolExpr formula = |