summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/command_executor.cpp16
-rw-r--r--src/main/command_executor.h12
-rw-r--r--src/main/command_executor_portfolio.cpp15
-rw-r--r--src/main/command_executor_portfolio.h12
-rw-r--r--src/main/driver_unified.cpp14
-rw-r--r--src/main/interactive_shell.cpp12
-rw-r--r--src/main/interactive_shell.h12
-rw-r--r--src/main/main.cpp12
-rw-r--r--src/main/main.h12
-rw-r--r--src/main/portfolio.cpp12
-rw-r--r--src/main/portfolio.h12
-rw-r--r--src/main/portfolio_util.cpp14
-rw-r--r--src/main/portfolio_util.h12
-rw-r--r--src/main/util.cpp12
14 files changed, 92 insertions, 87 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 672dedc50..320be701d 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file command_executor.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds, Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, 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 An additional layer between commands and invoking them.
**/
@@ -115,6 +115,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
if(q != NULL) {
d_result = res = q->getResult();
}
+ CheckSynthCommand* csy = dynamic_cast<CheckSynthCommand*>(cmd);
+ if(csy != NULL) {
+ d_result = res = csy->getResult();
+ }
if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) {
std::ostringstream ossCurStats;
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d8294212a..4018aeda1 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file command_executor.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, 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 additional layer between commands and invoking them.
**/
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 15165e82c..1902e1817 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file command_executor_portfolio.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, 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 An additional layer between commands and invoking them.
**
@@ -198,7 +198,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
// command
if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
- dynamic_cast<QueryCommand*>(cmd) != NULL) {
+ dynamic_cast<QueryCommand*>(cmd) != NULL ||
+ dynamic_cast<CheckSynthCommand*>(cmd) != NULL) {
mode = 1;
} else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index ce9a80a4e..be980a01b 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file command_executor_portfolio.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, 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 additional layer between commands and invoking them.
**
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b83907bd3..bab70e98f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file driver_unified.cpp
** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Francois Bobot
+ ** 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 Driver for CVC4 executable (cvc4) unified for both
** sequential and portfolio versions
@@ -101,7 +101,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
progPath = argv[0];
// Parse the options
- vector<string> filenames = opts.parseOptions(argc, argv);
+ vector<string> filenames = Options::parseOptions(&opts, argc, argv);
# ifndef PORTFOLIO_BUILD
if( opts.wasSetByUserThreads() ||
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 4982cb2bb..e11f82a40 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file interactive_shell.cpp
** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot
+ ** Top contributors (to current version):
+ ** Morgan Deters, Christopher L. Conway, 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 Interactive shell for CVC4
**
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 844fddf45..18e42f1e5 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file interactive_shell.h
** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Christopher L. Conway, 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 Interactive shell for CVC4
**/
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 56fc3ef40..7b6b9ad86 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file main.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Christopher L. Conway
- ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Christopher L. Conway
** 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 Main driver for CVC4 executable
**
diff --git a/src/main/main.h b/src/main/main.h
index 2ba688a98..8277d366a 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file main.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 Header for main CVC4 driver
**
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 22f3a67ae..1e1b41bea 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file portfolio.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Kshitij Bansal, 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 Provides (somewhat) generic functionality to simulate a
** (potentially cooperative) race
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index a7f15a04d..b96efda51 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file portfolio.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, 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 Provides (somewhat) generic functionality to simulate a
** (potentially cooperative) race
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index e42787fea..03827a917 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file portfolio_util.cpp
** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ ** Tim King, 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 Code relevant only for portfolio builds
**/
@@ -92,7 +92,7 @@ void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts)
*vp++ = NULL;
if(targc > 1) { // this is necessary in case you do e.g. --thread0=" "
try {
- tOpts.parseOptions(targc, targv);
+ Options::parseOptions(&tOpts, targc, targv);
} catch(OptionException& e) {
stringstream ss;
ss << optid << ": " << e.getMessage();
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 50cf0060a..32cc04540 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file portfolio_util.h
** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, 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 Code relevant only for portfolio builds
**/
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 71b46e67a..e14b508de 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file util.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Christopher L. Conway, Tim King, ACSYS
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, 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 Utilities for the main driver.
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback