diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
commit | dea679ce032c130d210d54c2e5482f95db1ff04a (patch) | |
tree | 6c36f68150172b20717f7d504274ab0bf82791b0 /examples/api/strings.cpp | |
parent | d95fe7675e20eaee86b8e804469e6db83265a005 (diff) |
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).
Diffstat (limited to 'examples/api/strings.cpp')
-rw-r--r-- | examples/api/strings.cpp | 202 |
1 files changed, 101 insertions, 101 deletions
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index a424c654a..14ab0e64d 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -1,101 +1,101 @@ -/********************* */
-/*! \file sets.cpp
- ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Reasoning about strings with CVC4 via C++ API.
- **
- ** A simple demonstration of reasoning about strings with CVC4 via C++ API.
- **/
-
-#include <iostream>
-
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-
-int main() {
- ExprManager em;
- SmtEngine smt(&em);
-
- // Set the logic
- smt.setLogic("S");
-
- // Produce models
- smt.setOption("produce-models", true);
-
- // The option strings-exp is needed
- smt.setOption("strings-exp", true);
-
- // Set output language to SMTLIB2
- std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
-
- // String type
- Type string = em.stringType();
-
- // std::string
- std::string std_str_ab("ab");
- // CVC4::String
- CVC4::String cvc4_str_ab(std_str_ab);
- CVC4::String cvc4_str_abc("abc");
- // String constants
- Expr ab = em.mkConst(cvc4_str_ab);
- Expr abc = em.mkConst(CVC4::String("abc"));
- // String variables
- Expr x = em.mkVar("x", string);
- Expr y = em.mkVar("y", string);
- Expr z = em.mkVar("z", string);
-
- // String concatenation: x.ab.y
- Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y);
- // String concatenation: abc.z
- Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z);
- // x.ab.y = abc.z
- Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs);
-
- // Length of y: |y|
- Expr leny = em.mkExpr(kind::STRING_LENGTH, y);
- // |y| >= 0
- Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0)));
-
- // Regular expression: (ab[c-e]*f)|g|h
- Expr r = em.mkExpr(kind::REGEXP_UNION,
- em.mkExpr(kind::REGEXP_CONCAT,
- em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))),
- em.mkExpr(kind::REGEXP_STAR,
- em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))),
- em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))),
- em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))),
- em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h"))));
-
- // String variables
- Expr s1 = em.mkVar("s1", string);
- Expr s2 = em.mkVar("s2", string);
- // String concatenation: s1.s2
- Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2);
-
- // s1.s2 in (ab[c-e]*f)|g|h
- Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r);
-
- // Make a query
- Expr q = em.mkExpr(kind::AND,
- formula1,
- formula2,
- formula3);
-
- // check sat
- Result result = smt.checkSat(q);
- std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
-
- if(result == Result::SAT) {
- std::cout << " x = " << smt.getValue(x) << std::endl;
- std::cout << " s1.s2 = " << smt.getValue(s) << std::endl;
- }
-}
+/********************* */ +/*! \file sets.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Reasoning about strings with CVC4 via C++ API. + ** + ** A simple demonstration of reasoning about strings with CVC4 via C++ API. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "smt/smt_engine.h" + +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // Set the logic + smt.setLogic("S"); + + // Produce models + smt.setOption("produce-models", true); + + // The option strings-exp is needed + smt.setOption("strings-exp", true); + + // Set output language to SMTLIB2 + std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + + // String type + Type string = em.stringType(); + + // std::string + std::string std_str_ab("ab"); + // CVC4::String + CVC4::String cvc4_str_ab(std_str_ab); + CVC4::String cvc4_str_abc("abc"); + // String constants + Expr ab = em.mkConst(cvc4_str_ab); + Expr abc = em.mkConst(CVC4::String("abc")); + // String variables + Expr x = em.mkVar("x", string); + Expr y = em.mkVar("y", string); + Expr z = em.mkVar("z", string); + + // String concatenation: x.ab.y + Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs); + + // Length of y: |y| + Expr leny = em.mkExpr(kind::STRING_LENGTH, y); + // |y| >= 0 + Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0))); + + // Regular expression: (ab[c-e]*f)|g|h + Expr r = em.mkExpr(kind::REGEXP_UNION, + em.mkExpr(kind::REGEXP_CONCAT, + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))), + em.mkExpr(kind::REGEXP_STAR, + em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))), + em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("h")))); + + // String variables + Expr s1 = em.mkVar("s1", string); + Expr s2 = em.mkVar("s2", string); + // String concatenation: s1.s2 + Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2); + + // s1.s2 in (ab[c-e]*f)|g|h + Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r); + + // Make a query + Expr q = em.mkExpr(kind::AND, + formula1, + formula2, + formula3); + + // check sat + Result result = smt.checkSat(q); + std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + + if(result == Result::SAT) { + std::cout << " x = " << smt.getValue(x) << std::endl; + std::cout << " s1.s2 = " << smt.getValue(s) << std::endl; + } +} |