diff options
author | Guy <katz911@gmail.com> | 2016-04-09 13:05:50 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-04-09 13:05:50 -0700 |
commit | c833e176a81eb193462c0efde0c6c2f28c5159fb (patch) | |
tree | c6ed3a129c7dcfc55f67dc6e48c0c46db157a38d /src/smt | |
parent | 846a2bbb482412a076120717977833dfd096d41e (diff) | |
parent | 2039eab2d76cf5f4cfe44680f5325f44a4fc5a99 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/boolean_terms.cpp | 12 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 12 | ||||
-rw-r--r-- | src/smt/command.cpp | 12 | ||||
-rw-r--r-- | src/smt/command.h | 12 | ||||
-rw-r--r-- | src/smt/command_list.cpp | 12 | ||||
-rw-r--r-- | src/smt/command_list.h | 12 | ||||
-rw-r--r-- | src/smt/dump.cpp | 12 | ||||
-rw-r--r-- | src/smt/dump.h | 12 | ||||
-rw-r--r-- | src/smt/ite_removal.cpp | 12 | ||||
-rw-r--r-- | src/smt/ite_removal.h | 12 | ||||
-rw-r--r-- | src/smt/logic_exception.h | 12 | ||||
-rw-r--r-- | src/smt/logic_request.cpp | 12 | ||||
-rw-r--r-- | src/smt/logic_request.h | 12 | ||||
-rw-r--r-- | src/smt/managed_ostreams.cpp | 12 | ||||
-rw-r--r-- | src/smt/managed_ostreams.h | 12 | ||||
-rw-r--r-- | src/smt/model.cpp | 12 | ||||
-rw-r--r-- | src/smt/model.h | 12 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 12 | ||||
-rw-r--r-- | src/smt/model_postprocessor.h | 12 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 17 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 12 | ||||
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 14 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.cpp | 12 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.h | 12 | ||||
-rw-r--r-- | src/smt/smt_statistics_registry.cpp | 14 | ||||
-rw-r--r-- | src/smt/smt_statistics_registry.h | 14 | ||||
-rw-r--r-- | src/smt/update_ostream.h | 12 |
27 files changed, 170 insertions, 165 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 1adc71d70..40b757598 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file boolean_terms.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index e1865f29f..0a63f7fd8 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -1,13 +1,13 @@ /********************* */ /*! \file boolean_terms.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5bf74a7de..bd514e2a8 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file command.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Implementation of command objects. ** diff --git a/src/smt/command.h b/src/smt/command.h index 7c9706522..db4efd819 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1,13 +1,13 @@ /********************* */ /*! \file command.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Implementation of the command pattern on SmtEngines. ** diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp index 2319d9539..78e5914aa 100644 --- a/src/smt/command_list.cpp +++ b/src/smt/command_list.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file command_list.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 context-sensitive list of Commands, and their cleanup ** diff --git a/src/smt/command_list.h b/src/smt/command_list.h index 47185b365..ea6b64940 100644 --- a/src/smt/command_list.h +++ b/src/smt/command_list.h @@ -1,13 +1,13 @@ /********************* */ /*! \file command_list.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 context-sensitive list of Commands, and their cleanup ** diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 79bf43e3c..eee7b901a 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file dump.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Dump utility classes and functions ** diff --git a/src/smt/dump.h b/src/smt/dump.h index a6fa899da..2abfe5408 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -1,13 +1,13 @@ /********************* */ /*! \file dump.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Dump utility classes and functions ** diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp index c0c6ed02b..fcd0c3254 100644 --- a/src/smt/ite_removal.cpp +++ b/src/smt/ite_removal.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file ite_removal.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Tim King, Morgan Deters - ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Removal of term ITEs ** diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h index d6d820f89..c0a46c316 100644 --- a/src/smt/ite_removal.h +++ b/src/smt/ite_removal.h @@ -1,13 +1,13 @@ /********************* */ /*! \file ite_removal.h ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters - ** Minor contributors (to current version): Clark Barrett + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Removal of term ITEs ** diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index a641f8d21..93db29a9b 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -1,13 +1,13 @@ /********************* */ /*! \file logic_exception.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 exception that is thrown when a feature is used outside ** the logic that CVC4 is currently using diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp index 09559eb8d..dc6a2d6b7 100644 --- a/src/smt/logic_request.cpp +++ b/src/smt/logic_request.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file logic_request.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h index 94c6c2a5e..7b41886bd 100644 --- a/src/smt/logic_request.h +++ b/src/smt/logic_request.h @@ -1,13 +1,13 @@ /********************* */ /*! \file logic_request.h ** \verbatim - ** Original author: Martin Brain <> - ** Major contributors: none - ** Minor contributors (to current version): Tim King + ** Top contributors (to current version): + ** Martin Brain, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 object to request logic widening in the running SmtEngine ** diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index 1901f731d..cae6ac67f 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file managed_ostreams.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Wrappers to handle memory management of ostreams. ** diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index 6dc785027..56c517a87 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -1,13 +1,13 @@ /********************* */ /*! \file managed_ostreams.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Wrappers to handle memory management of ostreams. ** diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 15ecbadfb..a38862307 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file model.cpp ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 implementation of Model class **/ diff --git a/src/smt/model.h b/src/smt/model.h index 4bbcb5f7d..768cb3e6a 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -1,13 +1,13 @@ /********************* */ /*! \file model.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Model class **/ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index aa645954b..369c5d48f 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file model_postprocessor.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ** diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h index 024f4f3a3..d9e749677 100644 --- a/src/smt/model_postprocessor.h +++ b/src/smt/model_postprocessor.h @@ -1,13 +1,13 @@ /********************* */ /*! \file model_postprocessor.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 784d82228..bff8e187f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt_engine.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Clark Barrett - ** Minor contributors (to current version): Christopher L. Conway, Tianyi Liang, Martin Brain <>, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds + ** Top contributors (to current version): + ** Morgan Deters, Clark Barrett, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 The main entry point into the CVC4 library's SMT interface ** @@ -1846,6 +1846,11 @@ void SmtEngine::setDefaults() { } } //implied options... + if( options::strictTriggers() ){ + if( !options::userPatternsQuant.wasSetByUser() ){ + options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST ); + } + } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0a8f8099f..2741cea85 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,13 +1,13 @@ /********************* */ /*! \file smt_engine.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Martin Brain <>, Tim King, Clark Barrett, Christopher L. Conway, Andrew Reynolds, Kshitij Bansal, Dejan Jovanovic + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 SmtEngine: the main public entry point of libcvc4. ** diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 1712744d7..5634a4651 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt_engine_check_proof.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Guy Katz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** @@ -22,7 +22,7 @@ #include <fstream> #include <string> -#warning "TODO: Why is lfsc's check.h being included like this?" +// #warning "TODO: Why is lfsc's check.h being included like this?" #include "check.h" #include "base/configuration_private.h" diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 25004c85e..c31ea5736 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file smt_engine_scope.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 5a7e39849..e00be40d4 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -1,13 +1,13 @@ /********************* */ /*! \file smt_engine_scope.h ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Morgan Deters, Tim King, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp index 5aa9085f5..d34498697 100644 --- a/src/smt/smt_statistics_registry.cpp +++ b/src/smt/smt_statistics_registry.cpp @@ -1,13 +1,13 @@ /********************* */ -/*! \file smt_statistic_registry.cpp +/*! \file smt_statistics_registry.cpp ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Accessor for the SmtEngine's StatisticsRegistry. ** diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h index 60a5e7c53..7483e8215 100644 --- a/src/smt/smt_statistics_registry.h +++ b/src/smt/smt_statistics_registry.h @@ -1,13 +1,13 @@ /********************* */ -/*! \file smt_statistic_registry.h +/*! \file smt_statistics_registry.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 Accessor for the SmtEngine's StatisticsRegistry. ** diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h index b87ed69d2..9574c5460 100644 --- a/src/smt/update_ostream.h +++ b/src/smt/update_ostream.h @@ -1,13 +1,13 @@ /********************* */ /*! \file update_ostream.h ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 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 ]] ** |