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")
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()
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)
# 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
# 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
# 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
&& 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 ] \
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
+++ /dev/null
-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.
expr/emptyset.h
expr/expr_iomanip.h
expr/expr_stream.h
- expr/pickler.h
expr/record.h
expr/symbol_table.h
expr/type.h
util/bitvector.h
util/bool.h
util/cardinality.h
- util/channel.h
util/divisible.h
util/gmp_util.h
util/hash.h
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
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 */
class Solver;
}
-namespace expr {
- namespace pickle {
- class Pickler;
- }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
namespace prop {
class TheoryProxy;
}/* CVC4::prop namespace */
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);
class TypeNode;
class NodeManager;
-namespace expr {
- namespace pickle {
- class PicklerPrivate;
- }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
template <bool ref_count>
class NodeTemplate;
*/
friend class expr::NodeValue;
- friend class expr::pickle::PicklerPrivate;
friend class expr::ExportPrivate;
/** A convenient null-valued encapsulated pointer */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
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()
#-----------------------------------------------------------------------------#
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
** 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>
#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;
// 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;
// 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() != "")
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()
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 */
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");
read_only = true
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"
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();
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;
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();
/**
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];
}
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();
}
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);
}
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) {
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));
}
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,
namespace CVC4 {
-#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && !defined(CVC4_PORTFOLIO)
+#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
class CVC4_PUBLIC CVC4dumpstream
{
** \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"
bool.h
cardinality.cpp
cardinality.h
- channel.h
debug.h
dense_map.h
divisible.cpp
+++ /dev/null
-/********************* */
-/*! \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 */
projects / cvc5.git / commitdiff