diff options
34 files changed, 8 insertions, 2331 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index f761fbf88..b6bc5b452 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -63,7 +63,6 @@ cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc4_option(ENABLE_DUMPING "Enable dumping") cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") cvc4_option(ENABLE_OPTIMIZED "Enable optimization") -cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support") cvc4_option(ENABLE_PROOFS "Enable proof support") cvc4_option(ENABLE_REPLAY "Enable the replay feature") cvc4_option(ENABLE_STATISTICS "Enable statistics") @@ -323,28 +322,6 @@ if(ENABLE_MUZZLE) add_definitions(-DCVC4_MUZZLE) endif() -# This check needs to come before the USE_CLN check. -if(ENABLE_PORTFOLIO) - find_package(Boost 1.50.0 REQUIRED COMPONENTS thread) - if (ENABLE_DUMPING) - message(FATAL_ERROR "Dumping not supported with a portfolio build.") - endif() - # Disable CLN for portfolio builds since it is not thread safe (uses an - # unlocked hash table internally). - if(USE_CLN) - message(WARNING "Disabling CLN support since portfolio is enabled.") - set(USE_CLN OFF) - endif() - set(THREADS_PREFER_PTHREAD_FLAG ON) - find_package(Threads REQUIRED) - if(THREADS_HAVE_PTHREAD_ARG) - add_c_cxx_flag(-pthread) - endif() - add_definitions(-DCVC4_PORTFOLIO) - set(BOOST_HAS_THREAD_ATTR 1) -endif() - -# This has to be processed after ENABLE_PORTFOLIO (disables dumping support). if(ENABLE_DUMPING) add_definitions(-DCVC4_DUMPING) endif() @@ -555,8 +532,6 @@ print_config("Python bindings :" BUILD_BINDINGS_PYTHON) print_config("Python2 :" USE_PYTHON2) print_config("Python3 :" USE_PYTHON3) message("") -print_config("Portfolio :" ENABLE_PORTFOLIO) -message("") print_config("ABC :" USE_ABC) print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index a4331bfce..9f58d3548 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -18,15 +18,7 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=yes cvc4_set_option(ENABLE_TRACING ON) # enable_dumping=yes -if(ENABLE_PORTFOLIO) - # Only print warning if dumping was not explicitely disabled by the user. - if(${ENABLE_DUMPING} STREQUAL "IGNORE") - message(WARNING - "Disabling dumping support, not supported with a portfolio build.") - endif() -else() - cvc4_set_option(ENABLE_DUMPING ON) -endif() +cvc4_set_option(ENABLE_DUMPING ON) # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=optional diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 99f2a7b93..1b30dc1aa 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -15,15 +15,7 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=no cvc4_set_option(ENABLE_TRACING OFF) # enable_dumping=yes -if(ENABLE_PORTFOLIO) - # Only print warning if dumping was not explicitely disabled by the user. - if(${ENABLE_DUMPING} STREQUAL "IGNORE") - message(WARNING - "Disabling dumping support, not supported with a portfolio build.") - endif() -else() - cvc4_set_option(ENABLE_DUMPING ON) -endif() +cvc4_set_option(ENABLE_DUMPING ON) # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 7feaf5129..9627bcd52 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -15,15 +15,7 @@ cvc4_set_option(ENABLE_PROOFS ON) # enable_tracing=yes cvc4_set_option(ENABLE_TRACING ON) # enable_dumping=yes -if(ENABLE_PORTFOLIO) - # Only print warning if dumping was not explicitely disabled by the user. - if(${ENABLE_DUMPING} STREQUAL "IGNORE") - message(WARNING - "Disabling dumping support, not supported with a portfolio build.") - endif() -else() - cvc4_set_option(ENABLE_DUMPING ON) -endif() +cvc4_set_option(ENABLE_DUMPING ON) # enable_muzzle=no cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no diff --git a/configure.sh b/configure.sh index d7e807c65..2057dd512 100755 --- a/configure.sh +++ b/configure.sh @@ -366,8 +366,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" [ $optimized != default ] \ && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" -[ $portfolio != default ] \ - && cmake_opts="$cmake_opts -DENABLE_PORTFOLIO=$portfolio" [ $proofs != default ] \ && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" [ $replay != default ] \ diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index 5f71dd2b4..c68dfa42f 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -36,10 +36,6 @@ configure_file( install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1) install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5) -if(ENABLE_PORTFOLIO) - install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1 - RENAME pcvc4.1) -endif() install(FILES ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3 ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3 diff --git a/licenses/channel.h-LICENSE b/licenses/channel.h-LICENSE deleted file mode 100644 index 36b7cd93c..000000000 --- a/licenses/channel.h-LICENSE +++ /dev/null @@ -1,23 +0,0 @@ -Boost Software License - Version 1.0 - August 17th, 2003 - -Permission is hereby granted, free of charge, to any person or organization -obtaining a copy of the software and accompanying documentation covered by -this license (the "Software") to use, reproduce, display, distribute, -execute, and transmit the Software, and to prepare derivative works of the -Software, and to permit third-parties to whom the Software is furnished to -do so, all subject to the following: - -The copyright notices in the Software and this entire statement, including -the above license grant, this restriction and the following disclaimer, -must be included in all copies of the Software, in whole or in part, and -all derivative works of the Software, unless such copies or derivative -works are solely in the form of machine-executable object code generated by -a source language processor. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT -SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE -FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE, -ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER -DEALINGS IN THE SOFTWARE. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c75e5576f..becc0be88 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -858,7 +858,6 @@ install(FILES expr/emptyset.h expr/expr_iomanip.h expr/expr_stream.h - expr/pickler.h expr/record.h expr/symbol_table.h expr/type.h @@ -922,7 +921,6 @@ install(FILES util/bitvector.h util/bool.h util/cardinality.h - util/channel.h util/divisible.h util/gmp_util.h util/hash.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 300af8e8c..cae23054c 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,10 +33,6 @@ libcvc4_add_sources( node_trie.h node_value.cpp node_value.h - pickle_data.cpp - pickle_data.h - pickler.cpp - pickler.h symbol_table.cpp symbol_table.h term_canonize.cpp diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 17affaef0..a4efa7286 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -44,12 +44,6 @@ class IntStat; struct ExprManagerMapCollection; class ResourceManager; -namespace expr { - namespace pickle { - class Pickler; - }/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ - class CVC4_PUBLIC ExprManager { private: /** The internal node manager */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index a32590050..458255c06 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -64,12 +64,6 @@ namespace api { class Solver; } -namespace expr { - namespace pickle { - class Pickler; - }/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ - namespace prop { class TheoryProxy; }/* CVC4::prop namespace */ @@ -218,7 +212,6 @@ class CVC4_PUBLIC Expr { friend class TypeCheckingException; friend class api::Solver; friend class expr::ExportPrivate; - friend class expr::pickle::Pickler; friend class prop::TheoryProxy; friend class smt::SmtEnginePrivate; friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e); diff --git a/src/expr/node.h b/src/expr/node.h index 768d7b948..f0ee7a56c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -52,12 +52,6 @@ namespace CVC4 { class TypeNode; class NodeManager; -namespace expr { - namespace pickle { - class PicklerPrivate; - }/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ - template <bool ref_count> class NodeTemplate; @@ -182,7 +176,6 @@ class NodeTemplate { */ friend class expr::NodeValue; - friend class expr::pickle::PicklerPrivate; friend class expr::ExportPrivate; /** A convenient null-valued encapsulated pointer */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp deleted file mode 100644 index fd3b69d26..000000000 --- a/src/expr/pickle_data.cpp +++ /dev/null @@ -1,58 +0,0 @@ -/********************* */ -/*! \file pickle_data.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 This is a "pickle" for expressions, CVC4-internal view - ** - ** This is the CVC4-internal view (private data structure) for a - ** "pickle" for expressions. The public-facing view is a "Pickle", - ** which just points to a PickleData. A pickle is a binary - ** serialization of an expression that can be converted back into an - ** expression in the same or another ExprManager. - **/ - -#include <iostream> -#include <sstream> -#include <string> - -#include "base/cvc4_assert.h" -#include "expr/pickle_data.h" -#include "expr/expr.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "expr/node_value.h" -#include "expr/expr_manager_scope.h" -#include "expr/variable_type_map.h" -#include "expr/kind.h" -#include "expr/metakind.h" - -namespace CVC4 { -namespace expr { -namespace pickle { - -void PickleData::writeToStringStream(std::ostringstream& oss) const { - BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end(); - for(; i != end; ++i) { - Block b = *i; - Assert(sizeof(b) * 8 == NBITS_BLOCK); - oss << b.d_body.d_data << " "; - } -} - -std::string PickleData::toString() const { - std::ostringstream oss; - oss.flags(std::ios::oct | std::ios::showbase); - writeToStringStream(oss); - return oss.str(); -} - -}/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h deleted file mode 100644 index 316b6285c..000000000 --- a/src/expr/pickle_data.h +++ /dev/null @@ -1,120 +0,0 @@ -/********************* */ -/*! \file pickle_data.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 This is a "pickle" for expressions, CVC4-internal view - ** - ** This is the CVC4-internal view (private data structure) for a - ** "pickle" for expressions. The public-facing view is a "Pickle", - ** which just points to a PickleData. A pickle is a binary - ** serialization of an expression that can be converted back into an - ** expression in the same or another ExprManager. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PICKLE_DATA_H -#define CVC4__PICKLE_DATA_H - -#include <sstream> -#include <deque> -#include <stack> -#include <exception> - -#include "expr/expr.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "expr/expr_manager.h" -#include "expr/variable_type_map.h" -#include "expr/kind.h" -#include "expr/metakind.h" - -namespace CVC4 { - -class NodeManager; - -namespace expr { -namespace pickle { - -const unsigned NBITS_BLOCK = 64; -const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND; -const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; -const unsigned NBITS_CONSTBLOCKS = 32; - -struct BlockHeader { - uint64_t d_kind : NBITS_KIND; -};/* struct BlockHeader */ - -struct BlockHeaderOperator { - uint64_t d_kind : NBITS_KIND; - uint64_t d_nchildren : NBITS_NCHILDREN; - uint64_t : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN); -};/* struct BlockHeaderOperator */ - -struct BlockHeaderConstant { - uint64_t d_kind : NBITS_KIND; - uint64_t d_constblocks : NBITS_BLOCK - NBITS_KIND; -};/* struct BlockHeaderConstant */ - -struct BlockHeaderVariable { - uint64_t d_kind : NBITS_KIND; - uint64_t : NBITS_BLOCK - NBITS_KIND; -};/* struct BlockHeaderVariable */ - -struct BlockBody { - uint64_t d_data : NBITS_BLOCK; -};/* struct BlockBody */ - -union Block { - BlockHeader d_header; - BlockHeaderConstant d_headerConstant; - BlockHeaderOperator d_headerOperator; - BlockHeaderVariable d_headerVariable; - - BlockBody d_body; -};/* union Block */ - -class PickleData { - typedef std::deque<Block> BlockDeque; - BlockDeque d_blocks; - -public: - PickleData& operator<<(Block b) { - enqueue(b); - return (*this); - } - - std::string toString() const; - - void enqueue(Block b) { - d_blocks.push_back(b); - } - - Block dequeue() { - Block b = d_blocks.front(); - d_blocks.pop_front(); - return b; - } - - bool empty() const { return d_blocks.empty(); } - uint32_t size() const { return d_blocks.size(); } - - void swap(PickleData& other){ - d_blocks.swap(other.d_blocks); - } - - void writeToStringStream(std::ostringstream& oss) const; -};/* class PickleData */ - -}/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__PICKLE_DATA_H */ diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp deleted file mode 100644 index 42198d676..000000000 --- a/src/expr/pickler.cpp +++ /dev/null @@ -1,481 +0,0 @@ -/********************* */ -/*! \file pickler.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 This is a "pickler" for expressions - ** - ** This is a "pickler" for expressions. It produces a binary - ** serialization of an expression that can be converted back - ** into an expression in the same or another ExprManager. - **/ - -#include <iostream> -#include <sstream> -#include <string> - -#include "base/cvc4_assert.h" -#include "base/output.h" -#include "expr/pickler.h" -#include "expr/pickle_data.h" -#include "expr/expr.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "expr/node_value.h" -#include "expr/expr_manager_scope.h" -#include "expr/variable_type_map.h" -#include "expr/kind.h" -#include "expr/metakind.h" - -namespace CVC4 { -namespace expr { -namespace pickle { - -class PicklerPrivate { -public: - typedef std::stack<Node> NodeStack; - NodeStack d_stack; - - PickleData d_current; - - Pickler& d_pickler; - - NodeManager* const d_nm; - - PicklerPrivate(Pickler& pickler, ExprManager* em) : - d_pickler(pickler), - d_nm(NodeManager::fromExprManager(em)) { - } - - bool atDefaultState(){ - return d_stack.empty() && d_current.empty(); - } - - /* Helper functions for toPickle */ - void toCaseNode(TNode n); - void toCaseVariable(TNode n); - void toCaseConstant(TNode n); - void toCaseOperator(TNode n); - void toCaseString(Kind k, const std::string& s); - - /* Helper functions for toPickle */ - Node fromCaseOperator(Kind k, uint32_t nchildren); - Node fromCaseConstant(Kind k, uint32_t nblocks); - std::string fromCaseString(uint32_t nblocks); - Node fromCaseVariable(Kind k); - -};/* class PicklerPrivate */ - -static Block mkBlockBody4Chars(char a, char b, char c, char d) { - Block newBody; - newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d; - return newBody; -} - -static char getCharBlockBody(BlockBody body, int i) { - Assert(0 <= i && i <= 3); - - switch(i) { - case 0: return (body.d_data & 0xff000000) >> 24; - case 1: return (body.d_data & 0x00ff0000) >> 16; - case 2: return (body.d_data & 0x0000ff00) >> 8; - case 3: return (body.d_data & 0x000000ff); - default: - Unreachable(); - } - return '\0'; -} - -static Block mkBlockBody(unsigned data) { - Block newBody; - newBody.d_body.d_data = data; - return newBody; -} - -static Block mkOperatorHeader(Kind k, unsigned numChildren) { - Block newHeader; - newHeader.d_headerOperator.d_kind = k; - newHeader.d_headerOperator.d_nchildren = numChildren; - return newHeader; -} - -static Block mkVariableHeader(Kind k) { - Block newHeader; - newHeader.d_header.d_kind = k; - return newHeader; -} - -static Block mkConstantHeader(Kind k, unsigned numBlocks) { - Block newHeader; - newHeader.d_headerConstant.d_kind = k; - newHeader.d_headerConstant.d_constblocks = numBlocks; - return newHeader; -} - -Pickler::Pickler(ExprManager* em) : - d_private(new PicklerPrivate(*this, em)) { -} - -Pickler::~Pickler() { - delete d_private; -} - -void Pickler::toPickle(Expr e, Pickle& p) -{ - Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); - Assert(d_private->atDefaultState()); - - try{ - d_private->d_current.swap(*p.d_data); - d_private->toCaseNode(e.getTNode()); - d_private->d_current.swap(*p.d_data); - }catch(PicklingException& pe){ - d_private->d_current = PickleData(); - Assert(d_private->atDefaultState()); - throw pe; - } - - Assert(d_private->atDefaultState()); -} - -void PicklerPrivate::toCaseNode(TNode n) -{ - Debug("pickler") << "toCaseNode: " << n << std::endl; - Kind k = n.getKind(); - kind::MetaKind m = metaKindOf(k); - switch(m) { - case kind::metakind::CONSTANT: - toCaseConstant(n); - break; - case kind::metakind::VARIABLE: - toCaseVariable(n); - break; - case kind::metakind::OPERATOR: - case kind::metakind::PARAMETERIZED: - toCaseOperator(n); - break; - default: - Unhandled(m); - } -} - -void PicklerPrivate::toCaseOperator(TNode n) -{ - Kind k = n.getKind(); - kind::MetaKind m = metaKindOf(k); - Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR); - if(m == kind::metakind::PARAMETERIZED) { - toCaseNode(n.getOperator()); - } - for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { - toCaseNode(*i); - } - d_current << mkOperatorHeader(k, n.getNumChildren()); -} - -void PicklerPrivate::toCaseVariable(TNode n) -{ - Kind k = n.getKind(); - Assert(metaKindOf(k) == kind::metakind::VARIABLE); - - const NodeValue* nv = n.d_nv; - uint64_t asInt = reinterpret_cast<uint64_t>(nv); - uint64_t mapped = d_pickler.variableToMap(asInt); - - uint32_t firstHalf = mapped >> 32; - uint32_t secondHalf = mapped & 0xffffffff; - - d_current << mkVariableHeader(k); - d_current << mkBlockBody(firstHalf); - d_current << mkBlockBody(secondHalf); -} - - -void PicklerPrivate::toCaseConstant(TNode n) { - Kind k = n.getKind(); - Assert(metaKindOf(k) == kind::metakind::CONSTANT); - switch(k) { - case kind::CONST_BOOLEAN: - d_current << mkConstantHeader(k, 1); - d_current << mkBlockBody(n.getConst<bool>()); - break; - case kind::CONST_RATIONAL: { - std::string asString; - Assert(k == kind::CONST_RATIONAL); - const Rational& q = n.getConst<Rational>(); - asString = q.toString(16); - toCaseString(k, asString); - break; - } - case kind::BITVECTOR_EXTRACT_OP: { - BitVectorExtract bve = n.getConst<BitVectorExtract>(); - d_current << mkConstantHeader(k, 2); - d_current << mkBlockBody(bve.high); - d_current << mkBlockBody(bve.low); - break; - } - case kind::CONST_BITVECTOR: { - // irritating: we incorporate the size of the string in with the - // size of this constant, so it appears as one big constant and - // doesn't confuse anybody - BitVector bv = n.getConst<BitVector>(); - std::string asString = bv.getValue().toString(16); - d_current << mkConstantHeader(k, 2 + asString.size()); - d_current << mkBlockBody(bv.getSize()); - toCaseString(k, asString); - break; - } - case kind::BITVECTOR_SIGN_EXTEND_OP: { - BitVectorSignExtend bvse = n.getConst<BitVectorSignExtend>(); - d_current << mkConstantHeader(k, 1); - d_current << mkBlockBody(bvse.signExtendAmount); - break; - } - default: - Unhandled(k); - } -} - -void PicklerPrivate::toCaseString(Kind k, const std::string& s) { - d_current << mkConstantHeader(k, s.size()); - - unsigned size = s.size(); - unsigned i; - for(i = 0; i + 4 <= size; i += 4) { - d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]); - } - switch(size % 4) { - case 0: break; - case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break; - case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break; - case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break; - default: - Unreachable(); - } - -} - -void Pickler::debugPickleTest(Expr e) { - - //ExprManager *em = e.getExprManager(); - //Expr e1 = mkVar("x", makeType()); - //return ; - - Pickler pickler(e.getExprManager()); - - Pickle p; - pickler.toPickle(e, p); - - uint32_t size = p.d_data->size(); - std::string str = p.d_data->toString(); - - Expr from = pickler.fromPickle(p); - ExprManagerScope ems(e); - - Debug("pickle") << "before: " << e << std::endl; - Debug("pickle") << "after: " << from.getNode() << std::endl; - Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl; - - Assert(p.d_data->empty()); - Assert(e == from); -} - -Expr Pickler::fromPickle(Pickle& p) { - Assert(d_private->atDefaultState()); - - d_private->d_current.swap(*p.d_data); - - while(!d_private->d_current.empty()) { - Block front = d_private->d_current.dequeue(); - - Kind k = (Kind)front.d_header.d_kind; - kind::MetaKind m = metaKindOf(k); - - Node result = Node::null(); - switch(m) { - case kind::metakind::VARIABLE: - result = d_private->fromCaseVariable(k); - break; - case kind::metakind::CONSTANT: - result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks); - break; - case kind::metakind::OPERATOR: - case kind::metakind::PARAMETERIZED: - result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren); - break; - default: - Unhandled(m); - } - Assert(result != Node::null()); - d_private->d_stack.push(result); - } - - Assert(d_private->d_current.empty()); - Assert(d_private->d_stack.size() == 1); - Node res = d_private->d_stack.top(); - d_private->d_stack.pop(); - - Assert(d_private->atDefaultState()); - - return d_private->d_nm->toExpr(res); -} - -Node PicklerPrivate::fromCaseVariable(Kind k) { - Assert(metaKindOf(k) == kind::metakind::VARIABLE); - - Block firstHalf = d_current.dequeue(); - Block secondHalf = d_current.dequeue(); - - uint64_t asInt = firstHalf.d_body.d_data; - asInt = asInt << 32; - asInt = asInt | (secondHalf.d_body.d_data); - - uint64_t mapped = d_pickler.variableFromMap(asInt); - - NodeValue* nv = reinterpret_cast<NodeValue*>(mapped); - Node fromNodeValue(nv); - - Assert(fromNodeValue.getKind() == k); - - return fromNodeValue; -} - -Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { - switch(k) { - case kind::CONST_BOOLEAN: { - Assert(constblocks == 1); - Block val = d_current.dequeue(); - - bool b= val.d_body.d_data; - return d_nm->mkConst<bool>(b); - } - case kind::CONST_RATIONAL: { - std::string s = fromCaseString(constblocks); - Rational q(s, 16); - return d_nm->mkConst<Rational>(q); - } - case kind::BITVECTOR_EXTRACT_OP: { - Block high = d_current.dequeue(); - Block low = d_current.dequeue(); - BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data); - return d_nm->mkConst<BitVectorExtract>(bve); - } - case kind::CONST_BITVECTOR: { - unsigned size = d_current.dequeue().d_body.d_data; - Block header CVC4_UNUSED = d_current.dequeue(); - Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR); - Assert(header.d_headerConstant.d_constblocks == constblocks - 2); - Integer value(fromCaseString(constblocks - 2)); - BitVector bv(size, value); - return d_nm->mkConst(bv); - } - case kind::BITVECTOR_SIGN_EXTEND_OP: { - Block signExtendAmount = d_current.dequeue(); - BitVectorSignExtend bvse(signExtendAmount.d_body.d_data); - return d_nm->mkConst<BitVectorSignExtend>(bvse); - } - default: - Unhandled(k); - } -} - -std::string PicklerPrivate::fromCaseString(uint32_t size) { - std::stringstream ss; - unsigned i; - for(i = 0; i + 4 <= size; i += 4) { - Block front = d_current.dequeue(); - BlockBody body = front.d_body; - - ss << getCharBlockBody(body,0) - << getCharBlockBody(body,1) - << getCharBlockBody(body,2) - << getCharBlockBody(body,3); - } - Assert(i == size - (size%4) ); - if(size % 4 != 0) { - Block front = d_current.dequeue(); - BlockBody body = front.d_body; - switch(size % 4) { - case 1: - ss << getCharBlockBody(body,0); - break; - case 2: - ss << getCharBlockBody(body,0) - << getCharBlockBody(body,1); - break; - case 3: - ss << getCharBlockBody(body,0) - << getCharBlockBody(body,1) - << getCharBlockBody(body,2); - break; - default: - Unreachable(); - } - } - return ss.str(); -} - -Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) { - kind::MetaKind m = metaKindOf(k); - bool parameterized = (m == kind::metakind::PARAMETERIZED); - uint32_t npops = nchildren + (parameterized? 1 : 0); - - NodeStack aux; - while(npops > 0) { - Assert(!d_stack.empty()); - Node top = d_stack.top(); - aux.push(top); - d_stack.pop(); - --npops; - } - - NodeBuilder<> nb(d_nm, k); - while(!aux.empty()) { - Node top = aux.top(); - nb << top; - aux.pop(); - } - - return nb; -} - -Pickle::Pickle() { - d_data = new PickleData(); -} - -// Just copying the pointer isn't right, we have to copy the -// underlying data. Otherwise user-level Pickles will delete the data -// twice! (once in each thread) -Pickle::Pickle(const Pickle& p) { - d_data = new PickleData(*p.d_data); -} - -Pickle& Pickle::operator = (const Pickle& other) { - if (this != &other) { - delete d_data; - d_data = new PickleData(*other.d_data); - } - return *this; -} - - -Pickle::~Pickle() { - delete d_data; -} - -uint64_t MapPickler::variableFromMap(uint64_t x) const -{ - VarMap::const_iterator i = d_fromMap.find(x); - Assert(i != d_fromMap.end()); - return i->second; -} - -}/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h deleted file mode 100644 index 02abdf18d..000000000 --- a/src/expr/pickler.h +++ /dev/null @@ -1,129 +0,0 @@ -/********************* */ -/*! \file pickler.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 This is a "pickler" for expressions - ** - ** This is a "pickler" for expressions. It produces a binary - ** serialization of an expression that can be converted back - ** into an expression in the same or another ExprManager. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__PICKLER_H -#define CVC4__PICKLER_H - -#include "expr/variable_type_map.h" -#include "expr/expr.h" -#include "base/exception.h" - -#include <exception> -#include <stack> - -namespace CVC4 { - -class ExprManager; - -namespace expr { -namespace pickle { - -class Pickler; -class PicklerPrivate; - -class PickleData;// CVC4-internal representation - -class CVC4_PUBLIC Pickle { - PickleData* d_data; - friend class Pickler; - friend class PicklerPrivate; -public: - Pickle(); - Pickle(const Pickle& p); - ~Pickle(); - Pickle& operator=(const Pickle& other); -};/* class Pickle */ - -class CVC4_PUBLIC PicklingException : public Exception { -public: - PicklingException() : - Exception("Pickling failed") { - } -};/* class PicklingException */ - -class CVC4_PUBLIC Pickler { - PicklerPrivate* d_private; - - friend class PicklerPrivate; - -protected: - virtual uint64_t variableToMap(uint64_t x) const { return x; } - virtual uint64_t variableFromMap(uint64_t x) const { return x; } -public: - Pickler(ExprManager* em); - virtual ~Pickler(); - - /** - * Constructs a new Pickle of the node n. - * n must be a node allocated in the node manager specified at initialization - * time. The new pickle has variables mapped using the VariableIDMap provided - * at initialization. - * TODO: Fix comment - * - * @return the pickle, which should be dispose()'d when you're done with it - */ - void toPickle(Expr e, Pickle& p); - - /** - * Constructs a node from a Pickle. - * This destroys the contents of the Pickle. - * The node is created in the NodeManager getNM(); - * TODO: Fix comment - */ - Expr fromPickle(Pickle& p); - - static void debugPickleTest(Expr e); - -};/* class Pickler */ - -class CVC4_PUBLIC MapPickler : public Pickler { -private: - const VarMap& d_toMap; - const VarMap& d_fromMap; - -public: - MapPickler(ExprManager* em, const VarMap& to, const VarMap& from): - Pickler(em), - d_toMap(to), - d_fromMap(from) { - } - -protected: - uint64_t variableToMap(uint64_t x) const override - { - VarMap::const_iterator i = d_toMap.find(x); - if (i != d_toMap.end()) - { - return i->second; - } - else - { - throw PicklingException(); - } - } - - uint64_t variableFromMap(uint64_t x) const override; -};/* class MapPickler */ - -}/* CVC4::expr::pickle namespace */ -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__PICKLER_H */ diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index fad4e77c5..356b0e199 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -62,48 +62,10 @@ if(ENABLE_STATIC_BINARY) set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() -if(ENABLE_PORTFOLIO) - set(pcvc4_src_files - command_executor_portfolio.cpp - command_executor_portfolio.h - driver_unified.cpp - main.cpp - portfolio.cpp - portfolio.h - portfolio_util.cpp - portfolio_util.h - ) - - add_executable(pcvc4-bin ${pcvc4_src_files} $<TARGET_OBJECTS:main>) - target_compile_definitions(pcvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER) - target_compile_definitions(pcvc4-bin PRIVATE -DPORTFOLIO_BUILD) - set_target_properties(pcvc4-bin - PROPERTIES - OUTPUT_NAME pcvc4 - RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) - target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES}) - target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS}) - if(PROGRAM_PREFIX) - install(PROGRAMS - $<TARGET_FILE:pcvc4-bin> DESTINATION bin RENAME ${PROGRAM_PREFIX}pcvc4) - else() - install(TARGETS pcvc4-bin DESTINATION bin) - endif() - - if(ENABLE_STATIC_BINARY) - set_target_properties(pcvc4-bin PROPERTIES LINK_FLAGS -static) - set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) - set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) - endif() -endif() - if(USE_READLINE) target_link_libraries(cvc4-bin ${Readline_LIBRARIES}) target_link_libraries(main-test ${Readline_LIBRARIES}) target_include_directories(main PRIVATE ${Readline_INCLUDE_DIR}) - if(ENABLE_PORTFOLIO) - target_link_libraries(pcvc4-bin ${Readline_LIBRARIES}) - endif() endif() #-----------------------------------------------------------------------------# diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp deleted file mode 100644 index fde1b59d3..000000000 --- a/src/main/command_executor_portfolio.cpp +++ /dev/null @@ -1,445 +0,0 @@ -/********************* */ -/*! \file command_executor_portfolio.cpp - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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. - ** - ** The portfolio executor branches check-sat queries to several - ** threads. - **/ - -#include "main/command_executor_portfolio.h" - -#if HAVE_UNISTD_H -# include <unistd.h> -#endif /* HAVE_UNISTD_H */ - -#include <boost/exception_ptr.hpp> -#include <boost/lexical_cast.hpp> -#include <boost/thread.hpp> -#include <boost/thread/condition.hpp> -#include <string> - -#include "api/cvc4cpp.h" -#include "cvc4autoconfig.h" -#include "expr/pickler.h" -#include "main/main.h" -#include "main/portfolio.h" -#include "options/options.h" -#include "options/set_language.h" -#include "smt/command.h" - -using namespace std; - -namespace CVC4 { -namespace main { - -CommandExecutorPortfolio::CommandExecutorPortfolio(api::Solver* solver, - Options& options, - OptionsList& tOpts) - : CommandExecutor(solver, options), - d_numThreads(options.getThreads()), - d_smts(), - d_seq(new CommandSequence()), - d_threadOptions(tOpts), - d_vmaps(), - d_lastWinner(0), - d_channelsOut(), - d_channelsIn(), - d_ostringstreams(), - d_statLastWinner("portfolio::lastWinner"), - d_statWaitTime("portfolio::waitTime") -{ - assert(d_threadOptions.size() == d_numThreads); - - d_statLastWinner.setData(d_lastWinner); - d_stats.registerStat(&d_statLastWinner); - - d_stats.registerStat(&d_statWaitTime); - - /* Duplication, individualization */ - d_solvers.push_back(d_solver); - d_exprMgrs.push_back(d_solver->getExprManager()); - d_smts.push_back(d_solver->getSmtEngine()); - assert(d_vmaps.size() == 0); - d_vmaps.push_back(new ExprManagerMapCollection()); - for (unsigned i = 1; i < d_numThreads; ++i) - { - api::Solver* solver = new api::Solver(&d_threadOptions[i]); - d_solvers.push_back(solver); - d_exprMgrs.push_back(solver->getExprManager()); - d_smts.push_back(solver->getSmtEngine()); - d_vmaps.push_back(new ExprManagerMapCollection()); - } -} - -CommandExecutorPortfolio::~CommandExecutorPortfolio() -{ - assert(d_seq != NULL); - delete d_seq; - - assert(d_smts.size() == d_numThreads); - for (unsigned i = 1; i < d_numThreads; ++i) - { - // the 0-th one is responsibility of parent class - delete d_solvers[i]; - } - d_solvers.clear(); - d_exprMgrs.clear(); - d_smts.clear(); - - d_stats.unregisterStat(&d_statLastWinner); - d_stats.unregisterStat(&d_statWaitTime); -} - -void CommandExecutorPortfolio::lemmaSharingInit() -{ - /* Sharing channels */ - assert(d_channelsIn.size() == 0); - assert(d_channelsOut.size() == 0); - - if(d_numThreads == 1) { - // Disable sharing - d_threadOptions[0].setSharingFilterByLength(0); - } else { - // Setup sharing channels - const unsigned int sharingChannelSize = 1000000; - - for(unsigned i = 0; i < d_numThreads; ++i){ - d_channelsOut.push_back( - new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); - d_channelsIn.push_back( - new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); - } - - /* Lemma I/O channels */ - for(unsigned i = 0; i < d_numThreads; ++i) { - int thread_id = d_threadOptions[i].getThreadId(); - string tag = "thread #" + boost::lexical_cast<string>(thread_id); - LemmaOutputChannel* outputChannel = - new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to); - LemmaInputChannel* inputChannel = - new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to); - d_smts[i]->channels()->setLemmaInputChannel(inputChannel); - d_smts[i]->channels()->setLemmaOutputChannel(outputChannel); - } - - /* Output to string stream */ - assert(d_ostringstreams.size() == 0); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_ostringstreams.push_back(new ostringstream); - d_threadOptions[i].setOut(d_ostringstreams[i]); - - OutputLanguage outputLanguage = d_threadOptions[i].getOutputLanguage(); - // important even for muzzled builds (to get result output right) - *(d_threadOptions[i].getOut()) << language::SetLanguage(outputLanguage); - } - } -}/* CommandExecutorPortfolio::lemmaSharingInit() */ - -void CommandExecutorPortfolio::lemmaSharingCleanup() -{ - assert(d_numThreads == d_options.getThreads()); - - if(d_numThreads == 1) - return; - - // Channel cleanup - assert(d_channelsIn.size() == d_numThreads); - assert(d_channelsOut.size() == d_numThreads); - for(unsigned i = 0; i < d_numThreads; ++i) { - delete d_channelsIn[i]; - delete d_channelsOut[i]; - delete d_smts[i]->channels()->getLemmaInputChannel(); - d_smts[i]->channels()->setLemmaInputChannel(NULL); - delete d_smts[i]->channels()->getLemmaOutputChannel(); - d_smts[i]->channels()->setLemmaOutputChannel(NULL); - } - d_channelsIn.clear(); - d_channelsOut.clear(); - - // sstreams cleanup (if used) - if(d_ostringstreams.size() != 0) { - assert(d_ostringstreams.size() == d_numThreads); - for(unsigned i = 0; i < d_numThreads; ++i) { - d_threadOptions[i].setOut(d_options.getOut()); - delete d_ostringstreams[i]; - } - d_ostringstreams.clear(); - } - -}/* CommandExecutorPortfolio::lemmaSharingCleanup() */ - - -bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) -{ - /** - * save the command and if check sat or query command, run a - * porfolio of SMT solvers. - */ - - int mode = 0; - // mode = 0 : run command on lastWinner, saving the command - // to be run on all others - // - // mode = 1 : run a race of the command, update lastWinner - // - // mode = 2 : run _only_ the lastWinner thread, not saving the - // command - - if( dynamic_cast<CheckSynthCommand*>(cmd) != NULL ){ - // sygus not supported in portfolio : FIXME: can support once datatypes exportTo is supported - return CommandExecutor::doCommandSingleton(cmd); - } - - if(dynamic_cast<CheckSatCommand*>(cmd) != NULL || - dynamic_cast<QueryCommand*>(cmd) != NULL ) { - mode = 1; - } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL || - dynamic_cast<GetAssignmentCommand*>(cmd) != NULL || - dynamic_cast<GetModelCommand*>(cmd) != NULL || - dynamic_cast<GetProofCommand*>(cmd) != NULL || - dynamic_cast<GetInstantiationsCommand*>(cmd) != NULL || - dynamic_cast<GetUnsatCoreCommand*>(cmd) != NULL || - dynamic_cast<GetAssertionsCommand*>(cmd) != NULL || - dynamic_cast<GetInfoCommand*>(cmd) != NULL || - dynamic_cast<GetOptionCommand*>(cmd) != NULL || - false) { - mode = 2; - } - - Debug("portfolio::outputmode") << "Mode is " << mode - << "lastWinner is " << d_lastWinner - << "d_seq is " << d_seq << std::endl; - - if(mode == 0) { - d_seq->addCommand(cmd->clone()); - Command* cmdExported = - d_lastWinner == 0 ? - cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner]) ); - std::ostream* winnersOut = d_options.getVerbosity() >= -1 ? - (d_threadOptions[d_lastWinner]).getOut() : NULL; - bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, winnersOut); - if(d_lastWinner != 0) delete cmdExported; - return ret; - } else if(mode == 1) { // portfolio - d_seq->addCommand(cmd->clone()); - - // We currently don't support changing number of threads for each - // command, but things have been architected in a way so that this - // can be achieved without a lot of work. - Command *seqs[d_numThreads]; - - if(d_lastWinner == 0) - seqs[0] = cmd; - else - seqs[0] = d_seq; - - /* variable maps and exporting */ - for(unsigned i = 1; i < d_numThreads; ++i) { - /** - * vmaps[i].d_from [x] = y means - * that in thread #0's expr manager id is y - * and in thread #i's expr manager id is x - * opposite for d_to - * - * d_from[x] : in a sense gives the id if converting *from* it to - * first thread - */ - try { - seqs[i] = - int(i) == d_lastWinner ? - cmd->exportTo(d_exprMgrs[i], *(d_vmaps[i])) : - d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - } catch(ExportUnsupportedException& e) { - if(d_options.getFallbackSequential()) { - Notice() << "Unsupported theory encountered." - << "Switching to sequential mode."; - return CommandExecutor::doCommandSingleton(cmd); - } - else - throw Exception("Certain theories (e.g., datatypes) are (currently)" - " unsupported in portfolio\n mode. Please see option" - " --fallback-sequential to make this a soft error."); - } - } - - /** - * Create identity variable map for the first thread, with only - * those variables which have a corresponding variable in - * another thread. (TODO: Also assert, all threads have the same - * set of variables mapped.) - */ - if(d_numThreads >= 2) { - VarMap& thread_0_from = d_vmaps[0]->d_from; - VarMap& thread_1_to = d_vmaps[1]->d_to; - for(VarMap::iterator i=thread_1_to.begin(); - i != thread_1_to.end(); ++i) { - thread_0_from[i->first] = i->first; - } - d_vmaps[0]->d_to = thread_0_from; - } - - lemmaSharingInit(); - - /* Portfolio */ - boost::function<bool()>* fns = new boost::function<bool()>[d_numThreads]; - for(unsigned i = 0; i < d_numThreads; ++i) { - std::ostream* current_out_or_null = d_options.getVerbosity() >= -1 ? - d_threadOptions[i].getOut() : NULL; - - fns[i] = boost::bind(smtEngineInvoke, d_smts[i], seqs[i], - current_out_or_null); - } - - assert(d_channelsIn.size() == d_numThreads - || d_numThreads == 1); - assert(d_channelsOut.size() == d_numThreads - || d_numThreads == 1); - assert(d_smts.size() == d_numThreads); - assert( !d_statWaitTime.running() ); - - boost::function<void()> - smFn = d_numThreads <= 1 ? boost::function<void()>() : - boost::bind(sharingManager<ChannelFormat>, - d_numThreads, - &d_channelsOut[0], - &d_channelsIn[0], - &d_smts[0]); - - size_t threadStackSize = d_options.getThreadStackSize(); - threadStackSize *= 1024 * 1024; - - pair<int, bool> portfolioReturn = - runPortfolio(d_numThreads, smFn, fns, threadStackSize, - d_options.getWaitToJoin(), d_statWaitTime); - -#ifdef CVC4_STATISTICS_ON - assert( d_statWaitTime.running() ); - d_statWaitTime.stop(); -#endif /* CVC4_STATISTICS_ON */ - - d_lastWinner = portfolioReturn.first; - d_result = d_smts[d_lastWinner]->getStatusOfLastCommand(); - - if(d_ostringstreams.size() != 0) { - assert(d_numThreads == d_options.getThreads()); - assert(portfolioReturn.first >= 0); - assert(unsigned(portfolioReturn.first) < d_numThreads); - - std::ostream& out = *d_options.getOut(); - if(Debug.isOn("treat-unknown-error")) { - if(d_ostringstreams[portfolioReturn.first]->str() == "unknown\n") { - out << "portfolioReturn = (" << portfolioReturn.first << ", " - << portfolioReturn.second << ")\n"; - for(unsigned i = 0; i < d_numThreads; ++i) - out << "thread " << i << ": " << d_ostringstreams[i]->str() - << std::endl; - throw Exception("unknown encountered"); - } - } - - out << d_ostringstreams[portfolioReturn.first]->str() - << std::flush; - -#ifdef CVC4_COMPETITION_MODE - // We use CVC4 in competition with --no-wait-to-join. If - // destructors run, they will destroy(!) us. So, just exit now. - _exit(0); -#endif /* CVC4_COMPETITION_MODE */ - } - - /* cleanup this check sat specific stuff */ - lemmaSharingCleanup(); - - delete d_seq; - d_seq = new CommandSequence(); - - delete[] fns; - - bool status = portfolioReturn.second; - - // dump the model/proof/unsat core if option is set - if(status) { - if( d_options.getProduceModels() && - d_options.getDumpModels() && - ( d_result.asSatisfiabilityResult() == Result::SAT || - (d_result.isUnknown() && - d_result.whyUnknown() == Result::INCOMPLETE) ) ) - { - Command* gm = new GetModelCommand(); - status = doCommandSingleton(gm); - } else if( d_options.getProof() && - d_options.getDumpProofs() && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { - Command* gp = new GetProofCommand(); - status = doCommandSingleton(gp); - } else if( d_options.getDumpInstantiations() && - ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS && - ( d_result.asSatisfiabilityResult() == Result::SAT || - (d_result.isUnknown() && - d_result.whyUnknown() == Result::INCOMPLETE) ) ) || - d_result.asSatisfiabilityResult() == Result::UNSAT ) ) { - Command* gi = new GetInstantiationsCommand(); - status = doCommandSingleton(gi); - } else if( d_options.getDumpSynth() && - d_result.asSatisfiabilityResult() == Result::UNSAT ){ - Command* gi = new GetSynthSolutionCommand(); - status = doCommandSingleton(gi); - } else if( d_options.getDumpUnsatCores() && - d_result.asSatisfiabilityResult() == Result::UNSAT ) { - Command* guc = new GetUnsatCoreCommand(); - status = doCommandSingleton(guc); - } - } - - return status; - } else if(mode == 2) { - Command* cmdExported = d_lastWinner == 0 ? - cmd : cmd->exportTo(d_exprMgrs[d_lastWinner], *(d_vmaps[d_lastWinner])); - std::ostream* winner_out_if_verbose = d_options.getVerbosity() >= -1 ? - d_threadOptions[d_lastWinner].getOut() : NULL; - bool ret = smtEngineInvoke(d_smts[d_lastWinner], cmdExported, - winner_out_if_verbose); - if(d_lastWinner != 0){ - delete cmdExported; - } - return ret; - } else { - // Unreachable(); - assert(false); - return false; - } - -}/* CommandExecutorPortfolio::doCommandSingleton() */ - -void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { - assert(d_numThreads == d_exprMgrs.size() && - d_exprMgrs.size() == d_smts.size()); - for(size_t i = 0; i < d_numThreads; ++i) { - string emTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); - Statistics stats = d_exprMgrs[i]->getStatistics(); - stats.setPrefix(emTag); - stats.flushInformation(out); - - string smtTag = "thread#" - + boost::lexical_cast<string>(d_threadOptions[i].getThreadId()); - stats = d_smts[i]->getStatistics(); - stats.setPrefix(smtTag); - stats.flushInformation(out); - } - d_stats.flushInformation(out); -} - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h deleted file mode 100644 index ef3329ef5..000000000 --- a/src/main/command_executor_portfolio.h +++ /dev/null @@ -1,85 +0,0 @@ -/********************* */ -/*! \file command_executor_portfolio.h - ** \verbatim - ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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. - ** - ** The portfolio executer branches check-sat queries to several - ** threads. - **/ - -#ifndef CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H -#define CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H - -#include "main/command_executor.h" -#include "main/portfolio_util.h" - -#include <iosfwd> -#include <sstream> -#include <string> -#include <vector> - -namespace CVC4 { - -class CommandSequence; - -namespace api { -class Solver; -} - -namespace main { - -class CommandExecutorPortfolio : public CommandExecutor { - // Solvers are created/deleted during initialization - std::vector<api::Solver*> d_solvers; - - std::vector<ExprManager*> d_exprMgrs; - const unsigned d_numThreads; // Currently const, but designed so it is - // not too hard to support this changing - std::vector<SmtEngine*> d_smts; - CommandSequence* d_seq; - OptionsList& d_threadOptions; - std::vector<ExprManagerMapCollection*> d_vmaps; - - int d_lastWinner; - - // These shall be reset for each check-sat - std::vector< SharedChannel<ChannelFormat>* > d_channelsOut; - std::vector< SharedChannel<ChannelFormat>* > d_channelsIn; - std::vector<std::ostringstream*> d_ostringstreams; - - // Stats - ReferenceStat<int> d_statLastWinner; - TimerStat d_statWaitTime; - -public: - CommandExecutorPortfolio(api::Solver* solver, - Options& options, - OptionsList& tOpts); - - ~CommandExecutorPortfolio(); - - std::string getSmtEngineStatus(); - - void flushStatistics(std::ostream& out) const override; - -protected: - bool doCommandSingleton(Command* cmd) override; - -private: - CommandExecutorPortfolio(); - void lemmaSharingInit(); - void lemmaSharingCleanup(); -};/* class CommandExecutorPortfolio */ - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index de840cb07..c4800a3ac 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -9,8 +9,7 @@ ** 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 + ** \brief Driver for CVC4 executable (cvc4) **/ #include <stdio.h> @@ -42,13 +41,6 @@ #include "util/result.h" #include "util/statistics_registry.h" -// The PORTFOLIO_BUILD is defined when compiling pcvc4 (the parallel version of -// CVC4) and undefined otherwise. The macro can only be used in -// driver_unified.cpp because we do not recompile all files for pcvc4. -#ifdef PORTFOLIO_BUILD -# include "main/command_executor_portfolio.h" -#endif - using namespace std; using namespace CVC4; using namespace CVC4::parser; @@ -106,14 +98,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Parse the options vector<string> filenames = Options::parseOptions(&opts, argc, argv); -# ifndef PORTFOLIO_BUILD - if( opts.wasSetByUserThreads() || - opts.wasSetByUserThreadStackSize() || - (! opts.getThreadArgv().empty()) ) { - throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); - } -# endif - string progNameStr = opts.getBinaryName(); progName = &progNameStr; @@ -199,46 +183,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Create the expression manager using appropriate options std::unique_ptr<api::Solver> solver; -# ifndef PORTFOLIO_BUILD solver.reset(new api::Solver(&opts)); pExecutor = new CommandExecutor(solver.get(), opts); -# else - OptionsList threadOpts; - parseThreadSpecificOptions(threadOpts, opts); - - bool useParallelExecutor = true; - // incremental? - if(opts.wasSetByUserIncrementalSolving() && - opts.getIncrementalSolving() && - (! opts.getIncrementalParallel()) ) { - Notice() << "Notice: In --incremental mode, using the sequential solver" - << " unless forced by...\n" - << "Notice: ...the experimental --incremental-parallel option.\n"; - useParallelExecutor = false; - } - // proofs? - if(opts.getCheckProofs()) { - if(opts.getFallbackSequential()) { - Warning() << "Warning: Falling back to sequential mode, as cannot run" - << " portfolio in check-proofs mode.\n"; - useParallelExecutor = false; - } - else { - throw OptionException("Cannot run portfolio in check-proofs mode."); - } - } - // pick appropriate one - if (useParallelExecutor) - { - solver.reset(new api::Solver(&threadOpts[0])); - pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); - } - else - { - solver.reset(new api::Solver(&opts)); - pExecutor = new CommandExecutor(solver.get(), opts); - } -# endif std::unique_ptr<Parser> replayParser; if (opts.getReplayInputFilename() != "") @@ -277,14 +223,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { throw OptionException( "--tear-down-incremental doesn't work in interactive mode"); } -#ifndef PORTFOLIO_BUILD if(!opts.wasSetByUserIncrementalSolving()) { cmd = new SetOptionCommand("incremental", SExpr(true)); cmd->setMuted(true); pExecutor->doCommand(cmd); delete cmd; } -#endif /* PORTFOLIO_BUILD */ InteractiveShell shell(solver.get()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp deleted file mode 100644 index 89a6d8253..000000000 --- a/src/main/portfolio.cpp +++ /dev/null @@ -1,149 +0,0 @@ -/********************* */ -/*! \file portfolio.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - **/ - -#include <boost/function.hpp> -#include <boost/thread.hpp> -#include <boost/bind.hpp> -#include <boost/thread/condition.hpp> -#include <boost/exception_ptr.hpp> - -#include "base/output.h" -#include "options/options.h" -#include "smt/smt_engine.h" -#include "util/result.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -/** Mutex to make sure at most one thread is winner */ -boost::mutex mutex_done; - -/** Mutex / condition variable to notify main when winner data written */ -boost::mutex mutex_main_wait; -boost::condition_variable condition_var_main_wait; - -bool global_flag_done; -int global_winner; - -template<typename S> -void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue) -{ - /* Uncomment line to delay first thread, useful to unearth errors/debug */ - // if(thread_id == 0) { sleep(1); } - returnValue = threadFn(); - - if( mutex_done.try_lock() ) { - if(global_flag_done == false) - { - { - boost::lock_guard<boost::mutex> lock(mutex_main_wait); - global_winner = thread_id; - global_flag_done = true; - } - condition_var_main_wait.notify_all(); // we want main thread to quit - } - mutex_done.unlock(); - } -} - -template<typename T, typename S> -std::pair<int, S> runPortfolio(int numThreads, - boost::function<T()> driverFn, - boost::function<S()> threadFns[], - size_t stackSize, - bool optionWaitToJoin, - TimerStat& statWaitTime) { - boost::thread thread_driver; - boost::thread* threads = new boost::thread[numThreads]; - S* threads_returnValue = new S[numThreads]; - - global_flag_done = false; - global_winner = -1; - - for(int t = 0; t < numThreads; ++t) { - -#if BOOST_HAS_THREAD_ATTR - boost::thread::attributes attrs; - - if(stackSize > 0) { - attrs.set_stack_size(stackSize); - } - - threads[t] = - boost::thread(attrs, boost::bind(runThread<S>, t, threadFns[t], - boost::ref(threads_returnValue[t]) ) ); -#else /* BOOST_HAS_THREAD_ATTR */ - if(stackSize > 0) { - throw OptionException("cannot specify a stack size for worker threads; requires CVC4 to be built with Boost thread library >= 1.50.0"); - } - - threads[t] = - boost::thread(boost::bind(runThread<S>, t, threadFns[t], - boost::ref(threads_returnValue[t]) ) ); - -#endif /* BOOST_HAS_THREAD_ATTR */ - -#if defined(BOOST_THREAD_PLATFORM_PTHREAD) - if(Chat.isOn()) { - void *stackaddr; - size_t stacksize; - pthread_attr_t attr; - pthread_getattr_np(threads[t].native_handle(), &attr); - pthread_attr_getstack(&attr, &stackaddr, &stacksize); - Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl; - } -#endif - } - - if(not driverFn.empty()) - thread_driver = boost::thread(driverFn); - - boost::unique_lock<boost::mutex> lock(mutex_main_wait); - while(global_flag_done == false) { - condition_var_main_wait.wait(lock); - } - - statWaitTime.start(); - - if(not driverFn.empty()) { - thread_driver.interrupt(); - thread_driver.join(); - } - - for(int t = 0; t < numThreads; ++t) { - if(optionWaitToJoin) { - threads[t].join(); - } - } - - std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]); - - delete[] threads; - delete[] threads_returnValue; - - return retval; -} - -// instantiation -template -std::pair<int, bool> -runPortfolio<void, bool>(int, - boost::function<void()>, - boost::function<bool()>*, - size_t, - bool, - TimerStat&); - -}/* CVC4 namespace */ diff --git a/src/main/portfolio.h b/src/main/portfolio.h deleted file mode 100644 index 2cb23d5c5..000000000 --- a/src/main/portfolio.h +++ /dev/null @@ -1,41 +0,0 @@ -/********************* */ -/*! \file portfolio.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - **/ - -#ifndef CVC4__PORTFOLIO_H -#define CVC4__PORTFOLIO_H - -#include <boost/function.hpp> -#include <utility> - -#include "options/options.h" -#include "smt/command.h" -#include "smt/smt_engine.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -template<typename T, typename S> -std::pair<int, S> runPortfolio(int numThreads, - boost::function<T()> driverFn, - boost::function<S()> threadFns[], - size_t stackSize, - bool optionWaitToJoin, - TimerStat& statWaitTime); -// as we have defined things, S=void would give compile errors -// do we want to fix this? yes, no, maybe? - -}/* CVC4 namespace */ - -#endif /* CVC4__PORTFOLIO_H */ diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp deleted file mode 100644 index a3b6767c7..000000000 --- a/src/main/portfolio_util.cpp +++ /dev/null @@ -1,161 +0,0 @@ -/********************* */ -/*! \file portfolio_util.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Kshitij Bansal - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - **/ - -#include "main/portfolio_util.h" - -#include <unistd.h> - -#include <cassert> -#include <vector> - -#include "options/options.h" - -using namespace std; - -namespace CVC4 { - -OptionsList::OptionsList() : d_options() {} - -OptionsList::~OptionsList(){ - for(std::vector<Options*>::iterator i = d_options.begin(), - iend = d_options.end(); i != iend; ++i) - { - Options* current = *i; - delete current; - } - d_options.clear(); -} - -void OptionsList::push_back_copy(const Options& opts) { - Options* copy = new Options; - copy->copyValues(opts); - d_options.push_back(copy); -} - -Options& OptionsList::operator[](size_t position){ - return *(d_options[position]); -} - -const Options& OptionsList::operator[](size_t position) const { - return *(d_options[position]); -} - -Options& OptionsList::back() { - return *(d_options.back()); -} - -size_t OptionsList::size() const { - return d_options.size(); -} - -void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts) -{ - - unsigned numThreads = opts.getThreads(); - - for(unsigned i = 0; i < numThreads; ++i) { - threadOptions.push_back_copy(opts); - Options& tOpts = threadOptions.back(); - - // Set thread identifier - tOpts.setThreadId(i); - const std::vector<std::string>& optThreadArgvs = opts.getThreadArgv(); - if(i < optThreadArgvs.size() && (! optThreadArgvs[i].empty())) { - // separate out the thread's individual configuration string - stringstream optidss; - optidss << "--thread" << i; - string optid = optidss.str(); - int targc = 1; - char* tbuf = strdup(optThreadArgvs[i].c_str()); - char* p = tbuf; - // string length is certainly an upper bound on size needed - char** targv = new char*[optThreadArgvs[i].size()]; - char** vp = targv; - *vp++ = strdup(optid.c_str()); - p = strtok(p, " "); - while(p != NULL) { - *vp++ = p; - ++targc; - p = strtok(NULL, " "); - } - *vp++ = NULL; - if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " - try { - Options::parseOptions(&tOpts, targc, targv); - } catch(OptionException& e) { - stringstream ss; - ss << optid << ": " << e.getMessage(); - throw OptionException(ss.str()); - } - if(tOpts.getThreads() != numThreads || - tOpts.getThreadArgv() != opts.getThreadArgv()) { - stringstream ss; - ss << "not allowed to set thread options in " << optid << " !"; - throw OptionException(ss.str()); - } - } - free(targv[0]); - delete [] targv; - free(tbuf); - } - } - - assert(numThreads >= 1); //do we need this? -} - -void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { - if(int(lemma.getNumChildren()) > Options::currentGetSharingFilterByLength()) { - return; - } - ++cnt; - Trace("sharing") << d_tag << ": " << lemma << std::endl; - expr::pickle::Pickle pkl; - try { - d_pickler.toPickle(lemma, pkl); - d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { - (*(Options::currentGetOut())) - << "thread #0: notifyNewLemma: " << lemma << std::endl; - } - } catch(expr::pickle::PicklingException& p){ - Trace("sharing::blocked") << lemma << std::endl; - } -} - - -PortfolioLemmaInputChannel::PortfolioLemmaInputChannel(std::string tag, - SharedChannel<ChannelFormat>* c, - ExprManager* em, - VarMap& to, - VarMap& from) - : d_tag(tag), d_sharedChannel(c), d_pickler(em, to, from) -{} - -bool PortfolioLemmaInputChannel::hasNewLemma(){ - Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl; - return !d_sharedChannel->empty(); -} - -Expr PortfolioLemmaInputChannel::getNewLemma() { - Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl; - expr::pickle::Pickle pkl = d_sharedChannel->pop(); - - Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { - (*Options::currentGetOut()) << "thread #0: getNewLemma: " << e << std::endl; - } - return e; -} - -}/*CVC4 namespace */ diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h deleted file mode 100644 index e5ca296ae..000000000 --- a/src/main/portfolio_util.h +++ /dev/null @@ -1,180 +0,0 @@ -/********************* */ -/*! \file portfolio_util.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - **/ - -#ifndef CVC4__PORTFOLIO_UTIL_H -#define CVC4__PORTFOLIO_UTIL_H - -#include <queue> - -#include "base/output.h" -#include "expr/pickler.h" -#include "smt/smt_engine.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" -#include "util/channel.h" - -namespace CVC4 { - -typedef expr::pickle::Pickle ChannelFormat; - -class PortfolioLemmaOutputChannel : public LemmaOutputChannel { -private: - std::string d_tag; - SharedChannel<ChannelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - int cnt; - PortfolioLemmaOutputChannel(std::string tag, - SharedChannel<ChannelFormat> *c, - ExprManager* em, - VarMap& to, - VarMap& from) : - d_tag(tag), - d_sharedChannel(c), - d_pickler(em, to, from), - cnt(0) - {} - - ~PortfolioLemmaOutputChannel() {} - - void notifyNewLemma(Expr lemma) override; -};/* class PortfolioLemmaOutputChannel */ - -class PortfolioLemmaInputChannel : public LemmaInputChannel { -private: - std::string d_tag; - SharedChannel<ChannelFormat>* d_sharedChannel; - expr::pickle::MapPickler d_pickler; - -public: - PortfolioLemmaInputChannel(std::string tag, - SharedChannel<ChannelFormat>* c, - ExprManager* em, - VarMap& to, - VarMap& from); - - ~PortfolioLemmaInputChannel() {} - - bool hasNewLemma() override; - Expr getNewLemma() override; - -};/* class PortfolioLemmaInputChannel */ - -class OptionsList { - public: - OptionsList(); - ~OptionsList(); - - void push_back_copy(const Options& options); - - Options& operator[](size_t position); - const Options& operator[](size_t position) const; - - Options& back(); - - size_t size() const; - private: - OptionsList(const OptionsList&) = delete; - OptionsList& operator=(const OptionsList&) = delete; - std::vector<Options*> d_options; -}; - -void parseThreadSpecificOptions(OptionsList& list, const Options& opts); - -template<typename T> -void sharingManager(unsigned numThreads, - SharedChannel<T> *channelsOut[], // out and in with respect - SharedChannel<T> *channelsIn[], - SmtEngine *smts[]) // to smt engines -{ - Trace("sharing") << "sharing: thread started " << std::endl; - std::vector <int> cnt(numThreads); // Debug("sharing") - - std::vector< std::queue<T> > queues; - for(unsigned i = 0; i < numThreads; ++i){ - queues.push_back(std::queue<T>()); - } - - const unsigned int sharingBroadcastInterval = 1; - - boost::mutex mutex_activity; - - /* Disable interruption, so that we can check manually */ - boost::this_thread::disable_interruption di; - - while(not boost::this_thread::interruption_requested()) { - - boost::this_thread::sleep - (boost::posix_time::milliseconds(sharingBroadcastInterval)); - - for(unsigned t = 0; t < numThreads; ++t) { - - /* No activity on this channel */ - if(channelsOut[t]->empty()) continue; - - /* Alert if channel full, so that we increase sharingChannelSize - or decrease sharingBroadcastInterval */ - assert(not channelsOut[t]->full()); - - T data = channelsOut[t]->pop(); - - if(Trace.isOn("sharing")) { - ++cnt[t]; - Trace("sharing") << "sharing: Got data. Thread #" << t - << ". Chunk " << cnt[t] << std::endl; - } - - for(unsigned u = 0; u < numThreads; ++u) { - if(u != t){ - Trace("sharing") << "sharing: adding to queue " << u << std::endl; - queues[u].push(data); - } - }/* end of inner for: broadcast activity */ - - } /* end of outer for: look for activity */ - - for(unsigned t = 0; t < numThreads; ++t){ - /* Alert if channel full, so that we increase sharingChannelSize - or decrease sharingBroadcastInterval */ - assert(not channelsIn[t]->full()); - - while(!queues[t].empty() && !channelsIn[t]->full()){ - Trace("sharing") << "sharing: pushing on channel " << t << std::endl; - T data = queues[t].front(); - channelsIn[t]->push(data); - queues[t].pop(); - } - } - } /* end of infinite while */ - - Trace("interrupt") - << "sharing thread interrupted, interrupting all smtEngines" << std::endl; - - for(unsigned t = 0; t < numThreads; ++t) { - Trace("interrupt") << "Interrupting thread #" << t << std::endl; - try{ - smts[t]->interrupt(); - }catch(ModalException &e){ - // It's fine, the thread is probably not there. - Trace("interrupt") << "Could not interrupt thread #" << t << std::endl; - } - } - - Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; -}/* sharingManager() */ - -}/* CVC4 namespace */ - -#endif /* CVC4__PORTFOLIO_UTIL_H */ diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp index c6d92c97b..df1dfa5cc 100644 --- a/src/options/didyoumean_test.cpp +++ b/src/options/didyoumean_test.cpp @@ -289,8 +289,6 @@ set<string> getDebugTags() { a.insert("parser-param"); a.insert("partial_model"); a.insert("pb"); - a.insert("pickle"); - a.insert("pickler"); a.insert("pipe"); a.insert("portfolio::outputmode"); a.insert("prec"); diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 71c964678..84ac7d955 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -79,55 +79,6 @@ header = "options/main_options.h" help = "do not run destructors at exit; default on except in debug builds" [[option]] - name = "threads" - category = "regular" - long = "threads=N" - type = "unsigned" - default = "2" - predicates = ["unsignedGreater0"] - read_only = true - help = "Total number of threads for portfolio" - -[[option]] - category = "regular" - long = "threadN=string" - type = "void" - handler = "threadN" - read_only = true - help = "configures portfolio thread N (0..#threads-1)" - -[[option]] - name = "threadStackSize" - category = "regular" - long = "thread-stack=N" - type = "unsigned" - default = "0" - read_only = true - help = "stack size for worker threads in MB (0 means use Boost/thread lib default)" - -[[option]] - name = "threadArgv" - category = "regular" - type = "std::vector<std::string>" - includes = ["<vector>", "<string>"] - help = "Thread configuration (a string to be passed to parseOptions)" - -[[option]] - name = "thread_id" - category = "regular" - type = "int" - default = "-1" - help = "Thread ID, for internal use in case of multi-threaded run" - -[[option]] - name = "sharingFilterByLength" - category = "regular" - long = "filter-lemma-length=N" - type = "int" - default = "-1" - help = "don't share (among portfolio threads) lemmas strictly longer than N" - -[[option]] name = "fallbackSequential" category = "regular" long = "fallback-sequential" diff --git a/src/options/options.h b/src/options/options.h index 0d26c60b9..a21ce4583 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -228,8 +228,6 @@ public: bool getWaitToJoin() const; const std::string& getForceLogicString() const; const std::vector<std::string>& getThreadArgv() const; - int getSharingFilterByLength() const; - int getThreadId() const; int getVerbosity() const; std::istream* getIn() const; std::ostream* getErr(); @@ -238,16 +236,12 @@ public: std::string getBinaryName() const; std::string getReplayInputFilename() const; unsigned getParseStep() const; - unsigned getThreadStackSize() const; - unsigned getThreads() const; // TODO: Document these. void setInputLanguage(InputLanguage); void setInteractive(bool); void setOut(std::ostream*); void setOutputLanguage(OutputLanguage); - void setSharingFilterByLength(int length); - void setThreadId(int); bool wasSetByUserCeGuidedInst() const; bool wasSetByUserDumpSynth() const; @@ -255,13 +249,9 @@ public: bool wasSetByUserForceLogicString() const; bool wasSetByUserIncrementalSolving() const; bool wasSetByUserInteractive() const; - bool wasSetByUserThreadStackSize() const; - bool wasSetByUserThreads() const; // Static accessor functions. // TODO: Document these. - static int currentGetSharingFilterByLength(); - static int currentGetThreadId(); static std::ostream* currentGetOut(); /** diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 43b44b93e..a753c08de 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -170,18 +170,6 @@ const std::string& Options::getForceLogicString() const{ return (*this)[options::forceLogicString]; } -const std::vector<std::string>& Options::getThreadArgv() const{ - return (*this)[options::threadArgv]; -} - -int Options::getSharingFilterByLength() const{ - return (*this)[options::sharingFilterByLength]; -} - -int Options::getThreadId() const{ - return (*this)[options::thread_id]; -} - int Options::getVerbosity() const{ return (*this)[options::verbosity]; } @@ -215,22 +203,6 @@ unsigned Options::getParseStep() const{ return (*this)[options::parseStep]; } -unsigned Options::getThreadStackSize() const{ - return (*this)[options::threadStackSize]; -} - -unsigned Options::getThreads() const{ - return (*this)[options::threads]; -} - -int Options::currentGetSharingFilterByLength() { - return current()->getSharingFilterByLength(); -} - -int Options::currentGetThreadId() { - return current()->getThreadId(); -} - std::ostream* Options::currentGetOut() { return current()->getOut(); } @@ -254,14 +226,6 @@ void Options::setOutputLanguage(OutputLanguage value) { set(options::outputLanguage, value); } -void Options::setSharingFilterByLength(int length) { - set(options::sharingFilterByLength, length); -} - -void Options::setThreadId(int value) { - set(options::thread_id, value); -} - bool Options::wasSetByUserCeGuidedInst() const { return wasSetByUser(options::ceGuidedInst); } @@ -286,14 +250,6 @@ bool Options::wasSetByUserInteractive() const { return wasSetByUser(options::interactive); } -bool Options::wasSetByUserThreadStackSize() const { - return wasSetByUser(options::threadStackSize); -} - -bool Options::wasSetByUserThreads() const { - return wasSetByUser(options::threads); -} - void Options::flushErr() { if(getErr() != NULL) { diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index b28d77437..b3c2975bb 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -734,50 +734,6 @@ ${options_handler}$ case '?': default: - if( ( optopt == 0 || - ( optopt >= ${option_value_begin}$ && - optopt <= ${option_value_end}$ ) - ) && !strncmp(argv[optind - 1], "--thread", 8) && - strlen(argv[optind - 1]) > 8 ) - { - if(! isdigit(argv[optind - 1][8])) { - throw OptionException(formatThreadOptionException(option)); - } - std::vector<std::string>& threadArgv = holder->threadArgv; - char *end; - long tnum = strtol(argv[optind - 1] + 8, &end, 10); - if(tnum < 0 || (*end != '\0' && *end != '=')) { - throw OptionException(formatThreadOptionException(option)); - } - if(threadArgv.size() <= size_t(tnum)) { - threadArgv.resize(tnum + 1); - } - if(threadArgv[tnum] != "") { - threadArgv[tnum] += " "; - } - if(*end == '\0') { // e.g., we have --thread0 "foo" - if(argc <= optind) { - throw OptionException(std::string("option `") + option + - "' missing its required argument"); - } - Debug("options") << "thread " << tnum << " gets option " - << argv[optind] << std::endl; - threadArgv[tnum] += argv[main_optind]; - main_optind++; - } else { // e.g., we have --thread0="foo" - if(end[1] == '\0') { - throw OptionException(std::string("option `") + option + - "' missing its required argument"); - } - Debug("options") << "thread " << tnum << " gets option " - << (end + 1) << std::endl; - threadArgv[tnum] += end + 1; - } - Debug("options") << "thread " << tnum << " now has " - << threadArgv[tnum] << std::endl; - break; - } - throw OptionException(std::string("can't understand option `") + option + "'" + suggestCommandLineOptions(option)); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index b12573085..55d8f7222 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -95,12 +95,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, d_registrar, userContext, - // fullLitToNode Map = - options::threads() > 1 || - options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY || - ( CVC4_USE_REPLAY && replayLog != NULL )); + d_cnfStream = new CVC4::prop::TseitinCnfStream( + d_satSolver, d_registrar, userContext, true); d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, diff --git a/src/smt/dump.h b/src/smt/dump.h index 4946341af..fc2452423 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -24,7 +24,7 @@ namespace CVC4 { -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && !defined(CVC4_PORTFOLIO) +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) class CVC4_PUBLIC CVC4dumpstream { diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h index e2218775d..e5c5cffe2 100644 --- a/src/smt_util/lemma_output_channel.h +++ b/src/smt_util/lemma_output_channel.h @@ -12,8 +12,7 @@ ** \brief Mechanism for communication about new lemmas ** ** This file defines an interface for use by the theory and propositional - ** engines to communicate new lemmas to the "outside world," for example - ** for lemma sharing between threads. + ** engines to communicate new lemmas to the "outside world". **/ #include "cvc4_public.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index f107ad95f..cf4a288c3 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -11,7 +11,6 @@ libcvc4_add_sources( bool.h cardinality.cpp cardinality.h - channel.h debug.h dense_map.h divisible.cpp diff --git a/src/util/channel.h b/src/util/channel.h deleted file mode 100644 index 00776921f..000000000 --- a/src/util/channel.h +++ /dev/null @@ -1,121 +0,0 @@ -/********************* */ -/*! \file channel.h - ** \verbatim - ** Top contributors (to current version): - ** none - ** This file is part of the CVC4 project but is excluded from the - ** standard CVC4 licensing because it is a derivative work of - ** circular_buffer.hpp in the BOOST 1.46.1 distribution. - ** Thus this file is covered by the Boost Software License, version 1.0. - ** See below. - ** - ** The combined work is: - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** Copyright (c) 2003-2008 Jan Gaspar - ** \endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__CHANNEL_H -#define CVC4__CHANNEL_H - -#include <boost/circular_buffer.hpp> -#include <boost/thread/mutex.hpp> -#include <boost/thread/condition.hpp> -#include <boost/thread/thread.hpp> -#include <boost/call_traits.hpp> -#include <boost/progress.hpp> -#include <boost/bind.hpp> - -namespace CVC4 { - -template <typename T> -class CVC4_PUBLIC SharedChannel { -private: - int d_maxsize; // just call it size? -public: - SharedChannel() {} - SharedChannel(int maxsize) : d_maxsize(maxsize) {} - virtual ~SharedChannel() {} - - /* Tries to add element and returns true if successful */ - virtual bool push(const T&) = 0; - - /* Removes an element from the channel */ - virtual T pop() = 0; - - /* */ - virtual bool empty() = 0; - - /* */ - virtual bool full() = 0; -};/* class SharedChannel<T> */ - -/* -This code is from - -http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer - -and is covered by the Boost Software License, version 1.0. -*/ -template <typename T> -class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel<T> { -public: - typedef boost::circular_buffer<T> container_type; - typedef typename container_type::size_type size_type; - typedef typename container_type::value_type value_type; - typedef typename boost::call_traits<value_type>::param_type param_type; - - explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {} - - bool push(param_type item) override - { - // param_type represents the "best" way to pass a parameter of type - // value_type to a method - - boost::mutex::scoped_lock lock(m_mutex); - m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this)); - m_container.push_front(item); - ++m_unread; - lock.unlock(); - m_not_empty.notify_one(); - return true; - }//function definitions need to be moved to cpp - - value_type pop() override - { - value_type ret; - boost::mutex::scoped_lock lock(m_mutex); - m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this)); - ret = m_container[--m_unread]; - lock.unlock(); - m_not_full.notify_one(); - return ret; - } - - bool empty() override { return not is_not_empty(); } - bool full() override { return not is_not_full(); } - - private: - SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor - SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator - - bool is_not_empty() const { return m_unread > 0; } - bool is_not_full() const { return m_unread < m_container.capacity(); } - - size_type m_unread; - container_type m_container; - boost::mutex m_mutex; - boost::condition m_not_empty; - boost::condition m_not_full; -};/* class SynchronizedSharedChannel<T> */ - -}/* CVC4 namespace */ - -#endif /* CVC4__CHANNEL_H */ |