diff options
Diffstat (limited to 'examples')
61 files changed, 1023 insertions, 980 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 4b0e547dc..2552d455c 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Mathias Preiner, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Aina Niemetz, Mathias Preiner, Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + cmake_minimum_required(VERSION 3.4) project(cvc4-examples) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index b597c80ea..0ae1b4a51 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -1,27 +1,26 @@ -/********************* */ -/*! \file SimpleVC.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the Java interface - ** - ** A simple demonstration of the Java interface. - ** - ** To run the resulting class file, you need to do something like the - ** following: - ** - ** java \ - ** -cp path/to/CVC4.jar:SimpleVC.jar \ - ** -Djava.library.path=/dir/containing/libcvc4jni.so \ - ** SimpleVC - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Aina Niemetz, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Java interface. + * + * To run the resulting class file, you need to do something like the + * following: + * + * java \ + * -cp path/to/CVC4.jar:SimpleVC.jar \ + * -Djava.library.path=/dir/containing/libcvc4jni.so \ + * SimpleVC + * + */ import edu.stanford.CVC4.*; diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py index d0a7914d8..05857e737 100644 --- a/examples/SimpleVC.py +++ b/examples/SimpleVC.py @@ -1,35 +1,25 @@ #! /usr/bin/python -##################### -## SimpleVC.py -## Top contributors (to current version): -## Morgan Deters, Aina Niemetz, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Morgan Deters, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the Python interface +# +# A simple demonstration of the Python interface. Compare to the +# C++ interface in simple_vc_cxx.cpp; they are quite similar. +# +# To run from a build directory, use something like: +# +# PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py ## -##! \file SimpleVC.py -### \verbatim -### Original author: mdeters -### Major contributors: none -### Minor contributors (to current version): none -### This file is part of the CVC4 prototype. -### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) -### Courant Institute of Mathematical Sciences -### New York University -### See the file COPYING in the top-level source directory for licensing -### information.\endverbatim -### -### \brief A simple demonstration of the Python interface -### -### A simple demonstration of the Python interface. Compare to the -### C++ interface in simple_vc_cxx.cpp; they are quite similar. -### -### To run from a build directory, use something like: -### -### PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py -#### import CVC4 from CVC4 import ExprManager, SmtEngine, Rational, Expr diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 5612b10f7..e05039e43 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Mathias Preiner, Abdalrhman Mohamed, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Mathias Preiner, Abdalrhman Mohamed, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + set(CVC5_EXAMPLES_API bitvectors bitvectors_and_arrays diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index be9557c99..d59733d76 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file bitvectors.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Liana Hadarean, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Liana Hadarean, Makai Mann + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector solver. + * + */ #include <cvc5/cvc5.h> diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index ca9869503..547b294a0 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file bitvectors_and_arrays.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector and array solvers. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Liana Hadarean + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector and array solvers. + * + */ #include <cvc5/cvc5.h> diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 82c2978e6..c4b99a56a 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -1,20 +1,21 @@ -/********************* */ -/*! \file combination.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the capabilities of CVC4 - ** - ** A simple demonstration of how to use uninterpreted functions, combining this - ** with arithmetic, and extracting a model at the end of a satisfiable query. - ** The model is displayed using getValue(). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the capabilities of CVC4 + * + * A simple demonstration of how to use uninterpreted functions, combining this + * with arithmetic, and extracting a model at the end of a satisfiable query. + * The model is displayed using getValue(). + */ #include <cvc5/cvc5.h> diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index f9a1484da..76c6da0f0 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file datatypes.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of using inductive datatypes in CVC4 - ** - ** An example of using inductive datatypes in CVC4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Morgan Deters, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of using inductive datatypes in CVC4. + */ #include <cvc5/cvc5.h> diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index d2f631d25..d21c59d59 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -1,18 +1,19 @@ -/********************* */ -/*! \file extract.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Makai Mann, Clark Barrett + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the CVC4 + * bit-vector solver. + * + */ #include <cvc5/cvc5.h> diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index b5881f312..21eb8e8fc 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file helloworld.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A very simple CVC4 example - ** - ** A very simple CVC4 tutorial example. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A very simple CVC4 example. + */ #include <cvc5/cvc5.h> diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 4fcc814da..1ef0ea23f 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -1,18 +1,19 @@ -/********************* */ -/*! \file BitVectors.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Liana Hadarean, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the cvc5 bit-vector + * solver. + * + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 474a3af16..526ee8d99 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -1,18 +1,19 @@ -/********************* */ -/*! \file BitVectorsAndArrays.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Liana Hadarean, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector and array solvers. - ** - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Liana Hadarean, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the solving capabilities of the cvc5 bit-vector + * and array solvers. + * + */ import edu.stanford.CVC4.*; import java.util.*; diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index 338cf193e..915ce817c 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Andres Noetzli, Aina Niemetz, Mathias Preiner -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Andres Noetzli, Aina Niemetz, Mathias Preiner +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + set(EXAMPLES_API_JAVA ## disabled until bindings for the new API are in place (issue #2284) # BitVectors diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java index 37e04e588..7330b235d 100644 --- a/examples/api/java/CVC4Streams.java +++ b/examples/api/java/CVC4Streams.java @@ -1,18 +1,19 @@ -/********************* */ -/*! \file CVC4Streams.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Example of driving CVC4 parsing from Java streams - ** - ** This example shows how CVC4 can be driven from Java streams. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Example of driving CVC4 parsing from Java streams + * + * This example shows how CVC4 can be driven from Java streams. + */ import java.io.*; import edu.stanford.CVC4.*; diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 6e5ec538b..0960b7ff3 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -1,20 +1,21 @@ -/********************* */ -/*! \file Combination.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the capabilities of CVC4 - ** - ** A simple demonstration of how to use uninterpreted functions, combining this - ** with arithmetic, and extracting a model at the end of a satisfiable query. - ** The model is displayed using getValue(). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the capabilities of CVC4 + * + * A simple demonstration of how to use uninterpreted functions, combining this + * with arithmetic, and extracting a model at the end of a satisfiable query. + * The model is displayed using getValue(). + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 8985ea006..d4dd85d2b 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -1,18 +1,17 @@ -/********************* */ -/*! \file Datatypes.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of using inductive datatypes in CVC4 (Java version) - ** - ** An example of using inductive datatypes in CVC4 (Java version). - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andres Noetzli, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of using inductive datatypes in CVC4 (Java version). + */ import edu.stanford.CVC4.*; import java.util.Iterator; diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index 9c8b66a73..c8aa678c6 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -1,18 +1,19 @@ -/********************* */ -/*! \file Exceptions.java - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Catching CVC4 exceptions via the Java API. - ** - ** A simple demonstration of catching CVC4 execptions via the Java API. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Catching CVC4 exceptions via the Java API. + * + * A simple demonstration of catching CVC4 execptions via the Java API. + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 69d6b3b10..bf8d3a238 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -1,22 +1,23 @@ -/********************* */ -/*! \file FloatingPointArith.java - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of solving floating-point problems with CVC4's Java API - ** - ** This example shows how to check whether CVC4 was built with floating-point - ** support, how to create floating-point types, variables and expressions, and - ** how to create rounding mode constants by solving toy problems. The example - ** also shows making special values (such as NaN and +oo) and converting an - ** IEEE 754-2008 bit-vector to a floating-point number. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of solving floating-point problems with CVC4's Java API + * + * This example shows how to check whether CVC4 was built with floating-point + * support, how to create floating-point types, variables and expressions, and + * how to create rounding mode constants by solving toy problems. The example + * also shows making special values (such as NaN and +oo) and converting an + * IEEE 754-2008 bit-vector to a floating-point number. + */ import edu.stanford.CVC4.*; import java.util.Iterator; diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index b1f8b560a..4cd4fae6a 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -1,24 +1,17 @@ -/********************* */ -/*! \file HelloWorld.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A very simple CVC4 example - ** - ** A very simple CVC4 tutorial example. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A very simple CVC4 tutorial example. + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 886b501dd..08f3792d6 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -1,19 +1,18 @@ -/********************* */ -/*! \file LinearArith.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 - ** - ** A simple demonstration of the linear arithmetic solving capabilities and - ** the push pop of CVC4. This also gives an example option. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the linear arithmetic solving capabilities and + * the push pop of CVC4. This also gives an example option. + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java index 064f59b7e..db6c1f902 100644 --- a/examples/api/java/PipedInput.java +++ b/examples/api/java/PipedInput.java @@ -1,20 +1,18 @@ -/********************* */ -/*! \file PipedInput.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the input parsing capabilities of CVC4 - ** when used from Java - ** - ** A simple demonstration of the input parsing capabilities of CVC4 when - ** used from Java. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the input parsing capabilities of CVC4 when + * used from Java. + */ import edu.stanford.CVC4.*; import java.io.*; diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index f462515c0..9a6beb6cc 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -1,18 +1,17 @@ -/********************* */ -/*! \file Relations.java - ** \verbatim - ** Top contributors (to current version): - ** Mudathir Mohamed, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reasoning about relations with CVC4 via Java API. - ** - ** A simple demonstration of reasoning about strings with CVC4 via Jave API. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about relations with CVC4 via Java API. + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index c0049050c..0637f66de 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -1,18 +1,17 @@ -/********************* */ -/*! \file Statistics.java - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of accessing CVC4's statistics using the Java API - ** - ** An example of accessing CVC4's statistics using the Java API. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of accessing CVC4's statistics using the Java API. + */ import edu.stanford.CVC4.*; import java.util.Iterator; diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index 8bc9d7f26..e5947abcc 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -1,18 +1,17 @@ -/********************* */ -/*! \file Strings.java - ** \verbatim - ** Top contributors (to current version): - ** Tianyi Liang, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Tianyi Liang, Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about strings with CVC4 via Java API. + */ import edu.stanford.CVC4.*; diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index 968639b00..42633e803 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -1,18 +1,17 @@ -/********************* */ -/*! \file UnsatCores.java - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief An example of interacting with unsat cores using CVC4's Java API - ** - ** An example of interacting with unsat cores using CVC4's Java API. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * An example of interacting with unsat cores using CVC4's Java API. + */ import edu.stanford.CVC4.*; import java.util.Iterator; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index ee9663455..02ddd956c 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -1,19 +1,18 @@ -/********************* */ -/*! \file linear_arith.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tim King, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 - ** - ** A simple demonstration of the linear arithmetic solving capabilities and - ** the push pop of CVC4. This also gives an example option. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the linear arithmetic solving capabilities and + * the push pop of CVC4. This also gives an example option. + */ #include <iostream> diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index f460c8841..0eed825eb 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + set(EXAMPLES_API_PYTHON bitvectors_and_arrays bitvectors diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 0bd6dc38a..15973472c 100644 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## bitvectors.py -## Top contributors (to current version): -## Makai Mann, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## bit-vector solver through the Python API. This is a direct translation -## of bitvectors-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 bit-vector +# solver through the Python API. This is a direct translation of +# bitvectors-new.cpp. ## import pycvc4 diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py index 69acf3de7..8f76ac709 100644 --- a/examples/api/python/bitvectors_and_arrays.py +++ b/examples/api/python/bitvectors_and_arrays.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## bitvectors_and_arrays.py -## Top contributors (to current version): -## Makai Mann -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## bit-vector and array solvers through the Python API. This is a direct -## translation of bitvectors_and_arrays-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 +# bit-vector and array solvers through the Python API. This is a direct +# translation of bitvectors_and_arrays-new.cpp. ## import pycvc4 diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 0289f07d3..eb40f6ba3 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## combination.py -## Top contributors (to current version): -## Makai Mann, Mudathir Mohamed, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## combination solver through the Python API. This is a direct translation -## of combination-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Mudathir Mohamed, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 combination +# solver through the Python API. This is a direct translation of +# combination-new.cpp. ## import pycvc4 diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 1c972da13..e15fe709c 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## datatypes.py -## Top contributors (to current version): -## Makai Mann, Andrew Reynolds, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## \brief A simple demonstration of the solving capabilities of the CVC4 -## datatypes solver through the Python API. This is a direct translation -## of datatypes-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Andrew Reynolds, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 datatypes +# solver through the Python API. This is a direct translation of +# datatypes-new.cpp. ## import pycvc4 diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py index 017aa82be..c779390d9 100644 --- a/examples/api/python/exceptions.py +++ b/examples/api/python/exceptions.py @@ -1,18 +1,19 @@ #!/usr/bin/env python -##################### -## exceptions.py -## Top contributors (to current version): -## Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## Catching CVC4 exceptions with the legacy Python API. -## -## A simple demonstration of catching CVC4 execptions with the legacy Python -## API. +############################################################################### +# Top contributors (to current version): +# Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# Catching cvc5 exceptions with the legacy Python API. +# +# A simple demonstration of catching cvc5 exceptions with the legacy Python API. ## import pycvc4 diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index e4378674c..d708a7045 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## extract.py -## Top contributors (to current version): -## Makai Mann, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## bit-vector solver through the Python API. This is a direct translation -## of extract-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 bit-vector +# solver through the Python API. This is a direct translation of +# extract-new.cpp. ## from pycvc4 import Solver diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index d22e2be5f..5444a7df3 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## floating_point.py -## Top contributors (to current version): -## Makai Mann, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## floating point solver through the Python API contributed by Eva -## Darulova. This requires building CVC4 with symfpu. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 +# floating point solver through the Python API contributed by Eva +# Darulova. This requires building cvc5 with symfpu. ## import pycvc4 diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py index e4ca5ec93..8e585073c 100644 --- a/examples/api/python/helloworld.py +++ b/examples/api/python/helloworld.py @@ -1,15 +1,17 @@ #!/usr/bin/env python -##################### -## helloworld.py -## Top contributors (to current version): -## Makai Mann, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A very simple CVC4 tutorial example, adapted from helloworld-new.cpp +############################################################################### +# Top contributors (to current version): +# Makai Mann, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A very simple example, adapted from helloworld-new.cpp ## import pycvc4 diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index 9b236777a..bc48b452e 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## linear_arith.py -## Top contributors (to current version): -## Makai Mann, Mudathir Mohamed, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## linear arithmetic solver through the Python API. This is a direct -## translation of linear_arith-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Mudathir Mohamed, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 linear +# arithmetic solver through the Python API. This is a direct translation of +# linear_arith-new.cpp. ## import pycvc4 diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py index d2cff87bf..fa8c1bc4f 100644 --- a/examples/api/python/sequences.py +++ b/examples/api/python/sequences.py @@ -1,17 +1,18 @@ #!/usr/bin/env python -##################### -## sequences.py -## Top contributors (to current version): -## Andres Noetzli, Makai Mann, Mudathir Mohamed -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## strings solver through the Python API. This is a direct translation -## of sequences.cpp. +############################################################################### +# Top contributors (to current version): +# Andres Noetzli, Makai Mann, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 strings solver +# through the Python API. This is a direct translation of sequences.cpp. ## import pycvc4 diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 0c5b37ad8..01c14cb87 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -1,17 +1,18 @@ #!/usr/bin/env python -##################### -## sets.py -## Top contributors (to current version): -## Makai Mann, Mudathir Mohamed, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## \brief A simple demonstration of the solving capabilities of the CVC4 -## sets solver through the Python API. This is a direct translation -## of sets-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Mudathir Mohamed, Aina Niemetz +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 sets solver +# through the Python API. This is a direct translation of sets-new.cpp. ## import pycvc4 diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 22ee24ae1..aa540f89c 100644 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -1,17 +1,18 @@ #!/usr/bin/env python -##################### -## strings.py -## Top contributors (to current version): -## Makai Mann, Mudathir Mohamed, Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## strings solver through the Python API. This is a direct translation -## of strings-new.cpp. +############################################################################### +# Top contributors (to current version): +# Makai Mann, Mudathir Mohamed, Andres Noetzli +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 strings solver +# through the Python API. This is a direct translation of strings-new.cpp. ## import pycvc4 diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index c3ae06140..8c490f47e 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -1,18 +1,18 @@ #!/usr/bin/env python -##################### -## sygus-fun.py -## Top contributors (to current version): -## Yoni Zohar, Andres Noetzli, Mudathir Mohamed -## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## sygus solver through the Python API. This is a direct -## translation of sygus-fun.cpp. +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Andres Noetzli, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 sygus solver +# through the Python API. This is a direct translation of sygus-fun.cpp. ## import copy diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 881e488a7..0bcc0815d 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## sygus-grammar.py -## Top contributors (to current version): -## Yoni Zohar, Mudathir Mohamed -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## sygus solver through the Python API. This is a direct -## translation of sygus-grammar.cpp. +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 +# sygus solver through the Python API. This is a direct +# translation of sygus-grammar.cpp. ## import copy diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py index 9d2216bef..08a50ce63 100644 --- a/examples/api/python/sygus-inv.py +++ b/examples/api/python/sygus-inv.py @@ -1,17 +1,19 @@ #!/usr/bin/env python -##################### -## sygus-inv.py -## Top contributors (to current version): -## Yoni Zohar, Mudathir Mohamed -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -## A simple demonstration of the solving capabilities of the CVC4 -## sygus solver through the Python API. This is a direct -## translation of sygus-inv.cpp . +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# A simple demonstration of the solving capabilities of the cvc5 +# sygus solver through the Python API. This is a direct +# translation of sygus-inv.cpp . ## import pycvc4 diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 39117c090..5ee66048f 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sequences.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Aina Niemetz, Tianyi Liang - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reasoning about sequences with CVC4 via C++ API. - ** - ** A simple demonstration of reasoning about sequences with CVC4 via C++ API. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Aina Niemetz, Tianyi Liang + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about sequences with CVC4 via C++ API. + */ #include <cvc5/cvc5.h> diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index c8b8bcc9e..5c9652707 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file sets.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Kshitij Bansal, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Reasoning about sets with CVC4. - ** - ** A simple demonstration of reasoning about sets with CVC4. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Kshitij Bansal, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about sets with CVC4. + */ #include <cvc5/cvc5.h> diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 548d25b81..a952b31d1 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file strings.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Tianyi Liang, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tianyi Liang, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of reasoning about strings with CVC4 via C++ API. + */ #include <cvc5/cvc5.h> diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index 44e276ddc..6eeffff1c 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -1,49 +1,50 @@ -/********************* */ -/*! \file sygus-fun.cpp - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the Sygus API. - ** - ** A simple demonstration of how to use the Sygus API to synthesize max and min - ** functions. Here is the same problem written in Sygus V2 format: - ** - ** (set-logic LIA) - ** - ** (synth-fun max ((x Int) (y Int)) Int - ** ((Start Int) (StartBool Bool)) - ** ((Start Int (0 1 x y - ** (+ Start Start) - ** (- Start Start) - ** (ite StartBool Start Start))) - ** (StartBool Bool ((and StartBool StartBool) - ** (not StartBool) - ** (<= Start Start))))) - ** - ** (synth-fun min ((x Int) (y Int)) Int) - ** - ** (declare-var x Int) - ** (declare-var y Int) - ** - ** (constraint (>= (max x y) x)) - ** (constraint (>= (max x y) y)) - ** (constraint (or (= x (max x y)) - ** (= y (max x y)))) - ** (constraint (= (+ (max x y) (min x y)) - ** (+ x y))) - ** - ** (check-synth) - ** - ** The printed output to this example should be equivalent to: - ** (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) - ** (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize max and min + * functions. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun max ((x Int) (y Int)) Int + * ((Start Int) (StartBool Bool)) + * ((Start Int (0 1 x y + * (+ Start Start) + * (- Start Start) + * (ite StartBool Start Start))) + * (StartBool Bool ((and StartBool StartBool) + * (not StartBool) + * (<= Start Start))))) + * + * (synth-fun min ((x Int) (y Int)) Int) + * + * (declare-var x Int) + * (declare-var y Int) + * + * (constraint (>= (max x y) x)) + * (constraint (>= (max x y) y)) + * (constraint (or (= x (max x y)) + * (= y (max x y)))) + * (constraint (= (+ (max x y) (min x y)) + * (+ x y))) + * + * (check-synth) + * + * The printed output to this example should be equivalent to: + * (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x)) + * (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) + */ #include <cvc5/cvc5.h> diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 441cfa30c..095f15889 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -1,46 +1,47 @@ -/********************* */ -/*! \file sygus-grammar.cpp - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the Sygus API. - ** - ** A simple demonstration of how to use Grammar to add syntax constraints to - ** the Sygus solution for the identity function. Here is the same problem - ** written in Sygus V2 format: - ** - ** (set-logic LIA) - ** - ** (synth-fun id1 ((x Int)) Int - ** ((Start Int)) ((Start Int ((- x) (+ x Start))))) - ** - ** (synth-fun id2 ((x Int)) Int - ** ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) - ** - ** (synth-fun id3 ((x Int)) Int - ** ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) - ** - ** (synth-fun id4 ((x Int)) Int - ** ((Start Int)) ((Start Int ((- x) (+ x Start))))) - ** - ** (declare-var x Int) - ** - ** (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) - ** - ** (check-synth) - ** - ** The printed output to this example should look like: - ** (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) - ** (define-fun id2 ((x Int)) Int x) - ** (define-fun id3 ((x Int)) Int (+ x 0)) - ** (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use Grammar to add syntax constraints to + * the Sygus solution for the identity function. Here is the same problem + * written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-fun id1 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (synth-fun id2 ((x Int)) Int + * ((Start Int)) ((Start Int ((Variable Int) (- x) (+ x Start))))) + * + * (synth-fun id3 ((x Int)) Int + * ((Start Int)) ((Start Int (0 (- x) (+ x Start))))) + * + * (synth-fun id4 ((x Int)) Int + * ((Start Int)) ((Start Int ((- x) (+ x Start))))) + * + * (declare-var x Int) + * + * (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x)) + * + * (check-synth) + * + * The printed output to this example should look like: + * (define-fun id1 ((x Int)) Int (+ x (+ x (- x)))) + * (define-fun id2 ((x Int)) Int x) + * (define-fun id3 ((x Int)) Int (+ x 0)) + * (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) + */ #include <cvc5/cvc5.h> diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 5d6789759..820fe8630 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -1,37 +1,38 @@ -/********************* */ -/*! \file sygus-inv.cpp - ** \verbatim - ** Top contributors (to current version): - ** Abdalrhman Mohamed, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the Sygus API. - ** - ** A simple demonstration of how to use the Sygus API to synthesize a simple - ** invariant. Here is the same problem written in Sygus V2 format: - ** - ** (set-logic LIA) - ** - ** (synth-inv inv-f ((x Int))) - ** - ** (define-fun pre-f ((x Int)) Bool - ** (= x 0)) - ** (define-fun trans-f ((x Int) (xp Int)) Bool - ** (ite (< x 10) (= xp (+ x 1)) (= xp x))) - ** (define-fun post-f ((x Int)) Bool - ** (<= x 10)) - ** - ** (inv-constraint inv-f pre-f trans-f post-f) - ** - ** (check-synth) - ** - ** The printed output to this example should be equivalent to: - ** (define-fun inv-f ((x Int)) Bool (not (>= x 11))) - **/ +/****************************************************************************** + * Top contributors (to current version): + * Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the Sygus API. + * + * A simple demonstration of how to use the Sygus API to synthesize a simple + * invariant. Here is the same problem written in Sygus V2 format: + * + * (set-logic LIA) + * + * (synth-inv inv-f ((x Int))) + * + * (define-fun pre-f ((x Int)) Bool + * (= x 0)) + * (define-fun trans-f ((x Int) (xp Int)) Bool + * (ite (< x 10) (= xp (+ x 1)) (= xp x))) + * (define-fun post-f ((x Int)) Bool + * (<= x 10)) + * + * (inv-constraint inv-f pre-f trans-f post-f) + * + * (check-synth) + * + * The printed output to this example should be equivalent to: + * (define-fun inv-f ((x Int)) Bool (not (>= x 11))) + */ #include <cvc5/cvc5.h> diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt index 2a4ef4799..94af86090 100644 --- a/examples/nra-translate/CMakeLists.txt +++ b/examples/nra-translate/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Mathias Preiner -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Aina Niemetz, Mathias Preiner +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate) set(CVC5_EXAMPLES_NRA_TRANSLATE diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index 635c369a0..de00cd745 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file normalize.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Aina Niemetz, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> #include <cvc4/expr/expr_iomanip.h> diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 413601769..73b7e6f9a 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2info.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Aina Niemetz, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 62a1f4b5e..dd4d97c2c 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2todreal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> #include <cvc4/expr/expr_iomanip.h> diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 5898e5cff..9a960b372 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2toisat.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Aina Niemetz, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index b2c73d48e..5de9415f7 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2tomathematica.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Andrew Reynolds, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 760a7024c..8f4350d58 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2toqepcad.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Tim King, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index dd6fb9bb6..0aa95a8d2 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file smt2toredlog.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Andrew Reynolds, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Aina Niemetz, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt index a1f5d70ef..b5b78d63e 100644 --- a/examples/sets-translate/CMakeLists.txt +++ b/examples/sets-translate/CMakeLists.txt @@ -1,13 +1,18 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Aina Niemetz, Mathias Preiner -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. +############################################################################### +# Top contributors (to current version): +# Aina Niemetz, Mathias Preiner +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# The build system configuration. ## + if(Boost_FOUND) cvc4_add_example(sets2arrays "sets_translate.cpp" "sets-translate" diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 0f924072c..661ab94b5 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file sets_translate.cpp - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Andres Noetzli, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ +/****************************************************************************** + * Top contributors (to current version): + * Kshitij Bansal, Andres Noetzli, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * [[ Add one-line brief description here ]] + * + * [[ Add lengthier description here ]] + * \todo document this file + */ #include <cvc5/cvc5.h> #include <cvc4/options/set_language.h> diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 4042e15cb..026665561 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -1,20 +1,20 @@ -/********************* */ -/*! \file simple_vc_cxx.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the C++ interface - ** - ** A simple demonstration of the C++ interface. Compare to the Java - ** interface in SimpleVC.java; they are virtually line-by-line - ** identical. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Morgan Deters, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the C++ interface + * + * Compare to the Java interface in SimpleVC.java; they are virtually + * line-by-line identical. + */ #include <cvc5/cvc5.h> diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 3d6a6e103..9ef48bf76 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -1,18 +1,17 @@ -/********************* */ -/*! \file simple_vc_quant_cxx.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Andrew Reynolds, Mudathir Mohamed - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A simple demonstration of the C++ interface for quantifiers - ** - ** A simple demonstration of the C++ interface for quantifiers. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli, Andrew Reynolds, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the C++ interface for quantifiers. + */ #include <cvc5/cvc5.h> diff --git a/examples/translator.cpp b/examples/translator.cpp index bcdf2b2d2..dcceca2ae 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -1,19 +1,20 @@ -/********************* */ -/*! \file translator.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief CVC4 translator - ** - ** The CVC4 translator executable. This program translates from one of - ** CVC4's input languages to one of its output languages. - **/ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Aina Niemetz, Tim King + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * CVC4 translator + * + * The CVC4 translator executable. This program translates from one of + * CVC4's input languages to one of its output languages. + */ #include <cvc5/cvc5.h> #include <cvc4/expr/expr_iomanip.h> |