A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

2 files changed, 192 insertions, 192 deletions

diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index 9437115a9..bb9dcd822 100644
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -1,91 +1,91 @@
-/*********************                                                        */

-/*! \file Strings.java

- ** \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 Java API.

- **

- ** A simple demonstration of reasoning about strings with CVC4 via Jave API.

- **/

-

-import edu.nyu.acsys.CVC4.*;

-

-public class Strings {

-  public static void main(String[] args) {

-    System.loadLibrary("cvc4jni");

-

-    ExprManager em = new ExprManager();

-    SmtEngine smt = new SmtEngine(em);

-

-    // Set the logic

-    smt.setLogic("S");

-

-    // Produce models

-    smt.setOption("produce-models", new SExpr(true));

-    // The option strings-exp is needed

-    smt.setOption("strings-exp", new SExpr(true));

-	// output-language

-    smt.setOption("output-language", new SExpr("smt2"));

-

-    // String type

-    Type string = em.stringType();

-

-    // String constants

-    Expr ab  = em.mkConst(new CVC4String("ab"));

-    Expr abc = em.mkConst(new CVC4String("abc"));

-    // 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(new 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(new CVC4String("ab"))),

-        em.mkExpr(Kind.REGEXP_STAR,

-          em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))),

-        em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))),

-      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))),

-      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("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);

-     System.out.println("CVC4 reports: " + q + " is " + result + ".");

-

-     System.out.println("  x  = " + smt.getValue(x));

-     System.out.println("  s1.s2 = " + smt.getValue(s));

-  }

-}

+/*********************                                                        */
+/*! \file Strings.java
+ ** \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 Java API.
+ **
+ ** A simple demonstration of reasoning about strings with CVC4 via Jave API.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+
+public class Strings {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    // Set the logic
+    smt.setLogic("S");
+
+    // Produce models
+    smt.setOption("produce-models", new SExpr(true));
+    // The option strings-exp is needed
+    smt.setOption("strings-exp", new SExpr(true));
+	// output-language
+    smt.setOption("output-language", new SExpr("smt2"));
+
+    // String type
+    Type string = em.stringType();
+
+    // String constants
+    Expr ab  = em.mkConst(new CVC4String("ab"));
+    Expr abc = em.mkConst(new CVC4String("abc"));
+    // 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(new 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(new CVC4String("ab"))),
+        em.mkExpr(Kind.REGEXP_STAR,
+          em.mkExpr(Kind.REGEXP_RANGE, em.mkConst(new CVC4String("c")), em.mkConst(new CVC4String("e")))),
+        em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("f")))),
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("g"))),
+      em.mkExpr(Kind.STRING_TO_REGEXP, em.mkConst(new CVC4String("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);
+     System.out.println("CVC4 reports: " + q + " is " + result + ".");
+
+     System.out.println("  x  = " + smt.getValue(x));
+     System.out.println("  s1.s2 = " + smt.getValue(s));
+  }
+}
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;
+  }
+}