summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/ast/ast_printer.cpp4
-rw-r--r--src/printer/ast/ast_printer.h4
-rw-r--r--src/printer/cvc/cvc_printer.cpp2
-rw-r--r--src/printer/cvc/cvc_printer.h4
-rw-r--r--src/printer/dagification_visitor.cpp4
-rw-r--r--src/printer/dagification_visitor.h4
-rw-r--r--src/printer/printer.cpp17
-rw-r--r--src/printer/printer.h4
-rw-r--r--src/printer/smt2/smt2_printer.cpp104
-rw-r--r--src/printer/smt2/smt2_printer.h3
-rw-r--r--src/printer/sygus_print_callback.cpp2
-rw-r--r--src/printer/sygus_print_callback.h4
-rw-r--r--src/printer/tptp/tptp_printer.cpp4
-rw-r--r--src/printer/tptp/tptp_printer.h2
14 files changed, 55 insertions, 107 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 2e32e9c12..1923594f3 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -2,9 +2,9 @@
/*! \file ast_printer.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Liana Hadarean
+ ** Morgan Deters, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index fa109c779..2fd7da749 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -2,9 +2,9 @@
/*! \file ast_printer.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 1178c7299..65117c9db 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 1694ea1ec..f5a06a082 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -2,9 +2,9 @@
/*! \file cvc_printer.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 5463b1c22..50cf7b210 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -2,9 +2,9 @@
/*! \file dagification_visitor.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds
+ ** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
index 6df5f32b4..5ebbc6e18 100644
--- a/src/printer/dagification_visitor.h
+++ b/src/printer/dagification_visitor.h
@@ -2,9 +2,9 @@
/*! \file dagification_visitor.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index f8d62a8be..5d54759b9 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Aina Niemetz, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -52,14 +52,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
case LANG_CVC4:
return unique_ptr<Printer>(new printer::cvc::CvcPrinter());
- case LANG_Z3STR:
- return unique_ptr<Printer>(
- new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
-
- case LANG_SYGUS_V1:
- return unique_ptr<Printer>(
- new printer::smt2::Smt2Printer(printer::smt2::sygus_variant));
-
case LANG_SYGUS_V2:
// sygus version 2.0 does not have discrepancies with smt2, hence we use
// a normal smt2 variant here.
@@ -122,9 +114,10 @@ Printer* Printer::getPrinter(OutputLanguage lang)
lang = language::toOutputLanguage(options::inputLanguage());
}
}
- if(lang == language::output::LANG_AUTO) {
- lang = language::output::LANG_CVC4; // default
- }
+ if (lang == language::output::LANG_AUTO)
+ {
+ lang = language::output::LANG_SMTLIB_V2_6; // default
+ }
}
if(d_printers[lang] == NULL) {
d_printers[lang] = makePrinter(lang);
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 85b7d498f..b18e318ee 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -2,9 +2,9 @@
/*! \file printer.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Andrew Reynolds
+ ** Tim King, Andrew Reynolds, Aina Niemetz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0c0c4c3a8..784e321a0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -21,6 +21,7 @@
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/dtype.h"
#include "expr/node_manager_attributes.h"
#include "expr/node_visitor.h"
@@ -146,31 +147,25 @@ void Smt2Printer::toStream(std::ostream& out,
<< n.getConst<FloatingPointSize>().significand()
<< ")";
break;
- case kind::CONST_BITVECTOR: {
+ case kind::CONST_BITVECTOR:
+ {
const BitVector& bv = n.getConst<BitVector>();
- const Integer& x = bv.getValue();
- unsigned width = bv.getSize();
- if (d_variant == sygus_variant || options::bvPrintConstsInBinary())
+ if (options::bvPrintConstsAsIndexedSymbols())
{
- out << "#b" << bv.toString();
+ out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
}
else
{
- out << "(_ ";
- out << "bv" << x << " " << width;
- out << ")";
+ out << "#b" << bv.toString();
}
-
- // //out << "#b";
-
- // while(n-- > 0) {
- // out << (x.testBit(n) ? '1' : '0');
- // }
break;
}
case kind::CONST_FLOATINGPOINT:
- out << n.getConst<FloatingPoint>();
+ {
+ out << n.getConst<FloatingPoint>().toString(
+ options::bvPrintConstsAsIndexedSymbols());
break;
+ }
case kind::CONST_ROUNDINGMODE:
switch (n.getConst<RoundingMode>()) {
case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
@@ -292,26 +287,22 @@ void Smt2Printer::toStream(std::ostream& out,
out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")";
break;
case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
- // out << "to_fp_bv "
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
<< n.getConst<FloatingPointToFPIEEEBitVector>().t.significand()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
- // out << "to_fp_fp "
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
<< n.getConst<FloatingPointToFPFloatingPoint>().t.significand()
<< ")";
break;
case kind::FLOATINGPOINT_TO_FP_REAL_OP:
- // out << "to_fp_real "
out << "(_ to_fp " << n.getConst<FloatingPointToFPReal>().t.exponent()
<< ' ' << n.getConst<FloatingPointToFPReal>().t.significand() << ")";
break;
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
- // out << "to_fp_signed "
out << "(_ to_fp "
<< n.getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
<< n.getConst<FloatingPointToFPSignedBitVector>().t.significand()
@@ -598,40 +589,14 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::PARTIAL_SELECT_0:
case kind::PARTIAL_SELECT_1:
case kind::ARRAY_TYPE:
- out << smtKindString(k, d_variant) << " ";
- break;
+ case kind::EQ_RANGE: out << smtKindString(k, d_variant) << " "; break;
// string theory
case kind::STRING_CONCAT:
- if(d_variant == z3str_variant) {
- out << "Concat ";
- for(unsigned i = 0; i < n.getNumChildren(); ++i) {
- toStream(out, n[i], -1, types, TypeNode::null());
- if(i + 1 < n.getNumChildren()) {
- out << ' ';
- }
- if(i + 2 < n.getNumChildren()) {
- out << "(Concat ";
- }
- }
- for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) {
- out << ")";
- }
- return;
- }
out << "str.++ ";
break;
case kind::STRING_IN_REGEXP: {
stringstream ss;
- if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) {
- out << "= ";
- toStream(out, n[0], -1, types, TypeNode::null());
- out << " ";
- Node str = NodeManager::currentNM()->mkConst(String(ss.str()));
- toStream(out, str, -1, types, TypeNode::null());
- out << ")";
- return;
- }
out << smtKindString(k, d_variant) << " ";
break;
}
@@ -642,6 +607,8 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::STRING_STRIDOF:
case kind::STRING_STRREPL:
case kind::STRING_STRREPLALL:
+ case kind::STRING_REPLACE_RE:
+ case kind::STRING_REPLACE_RE_ALL:
case kind::STRING_TOLOWER:
case kind::STRING_TOUPPER:
case kind::STRING_REV:
@@ -1077,6 +1044,8 @@ static string smtKindString(Kind k, Variant v)
case kind::ARRAY_TYPE: return "Array";
case kind::PARTIAL_SELECT_0: return "partial_select_0";
case kind::PARTIAL_SELECT_1: return "partial_select_1";
+ case kind::EQ_RANGE:
+ return "eqrange";
// bv theory
case kind::BITVECTOR_CONCAT: return "concat";
@@ -1194,13 +1163,15 @@ static string smtKindString(Kind k, Variant v)
//string theory
case kind::STRING_CONCAT: return "str.++";
- case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
+ case kind::STRING_LENGTH: return "str.len";
case kind::STRING_SUBSTR: return "str.substr" ;
case kind::STRING_STRCTN: return "str.contains" ;
case kind::STRING_CHARAT: return "str.at" ;
case kind::STRING_STRIDOF: return "str.indexof" ;
case kind::STRING_STRREPL: return "str.replace" ;
case kind::STRING_STRREPLALL: return "str.replace_all";
+ case kind::STRING_REPLACE_RE: return "str.replace_re";
+ case kind::STRING_REPLACE_RE_ALL: return "str.replace_re_all";
case kind::STRING_TOLOWER: return "str.tolower";
case kind::STRING_TOUPPER: return "str.toupper";
case kind::STRING_REV: return "str.rev";
@@ -1289,7 +1260,6 @@ void Smt2Printer::toStream(std::ostream& out,
|| tryToStream<EmptyCommand>(out, c)
|| tryToStream<EchoCommand>(out, c, d_variant)
|| tryToStream<SynthFunCommand>(out, c)
- || tryToStream<DeclareSygusPrimedVarCommand>(out, c)
|| tryToStream<DeclareSygusFunctionCommand>(out, c)
|| tryToStream<DeclareSygusVarCommand>(out, c)
|| tryToStream<SygusConstraintCommand>(out, c)
@@ -1672,8 +1642,8 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c)
static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
{
- const vector<Expr>& funcs = c->getFunctions();
- const vector<vector<Expr> >& formals = c->getFormals();
+ const vector<api::Term>& funcs = c->getFunctions();
+ const vector<vector<api::Term> >& formals = c->getFormals();
out << "(define-fun";
if (funcs.size() > 1)
{
@@ -1696,10 +1666,10 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
}
out << funcs[i] << " (";
// print its type signature
- vector<Expr>::const_iterator itf = formals[i].begin();
+ vector<api::Term>::const_iterator itf = formals[i].begin();
for (;;)
{
- out << "(" << (*itf) << " " << (*itf).getType() << ")";
+ out << "(" << (*itf) << " " << (*itf).getSort() << ")";
++itf;
if (itf != formals[i].end())
{
@@ -1710,8 +1680,8 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
break;
}
}
- Type type = funcs[i].getType();
- type = static_cast<FunctionType>(type).getRangeType();
+ api::Sort type = funcs[i].getSort();
+ type = type.getFunctionCodomainSort();
out << ") " << type;
if (funcs.size() > 1)
{
@@ -1722,7 +1692,7 @@ static void toStream(std::ostream& out, const DefineFunctionRecCommand* c)
{
out << ") (";
}
- const vector<Expr>& formulas = c->getFormulas();
+ const vector<api::Term>& formulas = c->getFormulas();
for (unsigned i = 0, size = formulas.size(); i < size; i++)
{
if (i > 0)
@@ -1856,12 +1826,7 @@ static void toStream(std::ostream& out,
const SetBenchmarkLogicCommand* c,
Variant v)
{
- // Z3-str doesn't have string-specific logic strings(?), so comment it
- if(v == z3str_variant) {
- out << "; (set-logic " << c->getLogic() << ")";
- } else {
- out << "(set-logic " << c->getLogic() << ")";
- }
+ out << "(set-logic " << c->getLogic() << ")";
}
static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v)
@@ -2025,7 +1990,7 @@ static void toStream(std::ostream& out, const CommentCommand* c, Variant v)
string s = c->getComment();
size_t pos = 0;
while((pos = s.find_first_of('"', pos)) != string::npos) {
- s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+ s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(set-info :notes \"" << s << "\")";
@@ -2039,7 +2004,7 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v)
// escape all double-quotes
size_t pos = 0;
while((pos = s.find('"', pos)) != string::npos) {
- s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+ s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(echo \"" << s << "\")";
@@ -2159,12 +2124,6 @@ static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c)
out << " (" << argTypes << ") " << ft.getRangeType() << ')';
}
-static void toStream(std::ostream& out, const DeclareSygusPrimedVarCommand* c)
-{
- out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
- << ' ' << c->getType() << ')';
-}
-
static void toStream(std::ostream& out, const DeclareSygusVarCommand* c)
{
out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType()
@@ -2244,7 +2203,7 @@ static void errorToStream(std::ostream& out, std::string message, Variant v) {
// escape all double-quotes
size_t pos = 0;
while((pos = message.find('"', pos)) != string::npos) {
- message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\"");
+ message.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\"");
pos += 2;
}
out << "(error \"" << message << "\")" << endl;
@@ -2274,9 +2233,6 @@ static OutputLanguage variantToLanguage(Variant variant)
switch(variant) {
case smt2_0_variant:
return language::output::LANG_SMTLIB_V2_0;
- case z3str_variant:
- return language::output::LANG_Z3STR;
- case sygus_variant: return language::output::LANG_SYGUS_V1;
case no_variant:
default: return language::output::LANG_SMTLIB_V2_6;
}
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index b34acacbb..398e510cb 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
@@ -33,7 +33,6 @@ enum Variant
smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with
// support for the string standard
- z3str_variant, // old-style 2.0 and also z3str syntax
sygus_variant // variant for sygus
}; /* enum Variant */
class Smt2Printer : public CVC4::Printer {
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index 92a89a18e..a15bde3c3 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index a53fbc85f..925c80ae8 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -2,9 +2,9 @@
/*! \file sygus_print_callback.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa
+ ** Andrew Reynolds, Haniel Barbosa, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index d06b80e7b..f1c1089ad 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -2,9 +2,9 @@
/*! \file tptp_printer.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Andrew Reynolds
+ ** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index 63272891e..d183a19d0 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback