Changelog for libmetaSMT4_0-0.0+20170523-1.5.x86_64.rpm :
Thu May 25 14:00:00 2017 jslabyAATTsuse.com
- Update to version 0.0+20170523:

* test Z3 on travis with gcc-4.8 (which supports openmp) instead of clang-3.5 (which does not)

* improve boost handling in cmake, build metaSMT tests without RTTI if supported

* add travis entry for boost-1.60.0

* add CVC4_WITHOUT_KIND_IFF cxx flag to support upstream cvc4, where kind::IFF is removed

* use cmake PIC property

* install a file that sets LD_LIBRARY_PATH

* support boolector version > 2.2 (API-breaking changes)

* fix missing include for sprintf

* improve query construction for STP: use vc_assertFormula incrementally instead of creating a big conjunction

* upgrade solvers to new version

Sat Feb 25 13:00:00 2017 jslabyAATTsuse.com
- Update to version 0.0+20170218:

* metaSMT Version 4

* merge of python bindings Conflicts: CMakeLists.txt README

* added contradiction_analysis

* added support for solve_with_random_bits to AssignRandomBits

* extended testcase test_unsat for contradiction analysis

* fixed python bindings includes: Z3_Context was renamed to Z3_Backend

* fixed CMake dependencies of toolbox/sortnets and missing scope \"solver\" in sortnets/logic.hpp

* added library OpenMP to the build dependencies of Z3

* removed global using declarations from cardinality.hpp, added explicit scopes where necessary

* added scope ``logic\'\' to function equal in test_Types

* made SMT_Tag_Mapping of implies_tag compliant to SMTLIB2-Standard

* moved Lookup table into namespace of test suite annotate_t

* implemented support for equality (operator==) of predicate, bitvector, bit constants, array, and Uninterpreted_Function

* adapted check for Z3 interactive responses compliant to Z3 version 3.2

* implemented logic_expressions

* implemented API/Simplify.hpp which allows for trivial simplification of logic_expressions

* implemented new SMT2 backend which supports Z3 version 3.2

* increased boost\' variant visitation unrolling limit from 20 (default) to 60

* removed no-return warnings which appear when ``pedantic\'\' is used

* implemented support for 64-bit bit-vector constants in Z3 and SMT2 backend, added test cases for unsigned long to test_result_wrapper and test_QF_BV

* refactored operator==() using boost::tuple

* moved boost::mpl::vector limit extension to an individual file

* allow multi-line comments

* fixed missing visitation of extend_expressions for simplify(.) and added a test case

* a more SMT-LIB 2 standard compliant SMT2 backend response parser

* added missing return statement to test case helper function

* added capability to print the test cases to python test operators

* added testcase for operator precedence to python tests

* disable a warning in boost function for GCC

* declared various frontend operator== to be inline

* added missind #if to python solver.cpp (around including SAT_Aiger)

* added headers support/{dis,en}able_warnings.hpp to suppress boost warnings

* include missing header from SAT_Clause

* declared expression::simplify inline to avoid linker errors

* supress more warnings from boost

* Fixed CMake error on CentOS 6 systems (ignore local Boost version)

* fixed error in QF_BV with GCC 4.4.6 (typename outside template)

* fixed more warnings on to many typenames

* removed unused picosat includes from testcases

* updated cmake in bootstrap to 2.8.7

* fixed order of build cmake and using it.

* removed mathsat backend (incomplete, unused)

* more robust searching and using for Z3 dependencies (gmp, omp)

* skip python if dependencies are missing

* fixed check for Python Libraries, added Warning if requested but not found

* fixed typo in detection of libomp

* removed the last occurences of mathsat

* fixed compiler errors due to name ambiguities on CentOS 6

* fixed typos in python bindings

* removed unused variables from test_unsat

* fixed or suppressed more warnings.

* fixed handling of large bvu/sint constants in BitBlast

* fixed handling of large constants in Boolector

* repeat QF_BV constant_64bit test for bvsint

* minor cleanup in comments (closed namespaces in wrong order)

* added -G option to bootstrap.sh

* added missing include to test_solver.cpp

* extracted parts of CMake config file to seperate files

* gitignore: be more specific on the cmake folder (only exclude config files)

* removed unused functions from Priority_Context

* added addclause_api to clausewriter

* added missing cmake file that creates the Profiling build type

* added addclause_api to minisat

* cleanup of test_unsat

* calling simplify before solving (MiniSAT)

* try to calculate the metaSMT_VERSION using git-describe if available

* added target package_doxygen to build tar.
* of the doxygen documentation

* Threaded_Context takes a template parameter to configure join behaviour

* fixed namespace issues in cardinality.

* fixed doxygen warnings

* fixed missing namespace in TypedSymbol.hpp

* options to turn on/off SMT2 and clause writer backends

* removed unnecessary namespace prefixes from SMT2_ResultParser

* minor cleanup in backend Boolector bvsint_tag

* fixed test case QF_BV/bvsint_t

* implemented support for bit-widths greater than 64 in SMT2 backend bvsint_tag

* minor fix for SMT2 bvsint map SMT2 bvsint to bvbin only if the bit-width exceeds size of int and the value is negative

* implemented support for bit-widths greater than 64 in SWORD backend bvsint_tag

* use disable_/enable_warnings.hpp in MiniSAT backend

* use disable_/enable_warnings.hpp in SMT_Graph

* add pragmas for clang to disable_/enable_warnings.hpp

* fix map name in SMT_Tag_Mapping

* STP backend

* STP-backend deletes expressions at destruction

* always enable clause writer (CW) backend per default

* replaced lexical_cast hex to uint with a spirit parser

* added BOOST_VARIANT_VISITATION_UNROLLING_LIMIT to graph_SMT2

* implemented generic expression solver backend

* added checks to disable z3 if it is not working (e.g. old gcc, missing omp)

* added fake return statement to ExpressionSolver uf operator

* fixed error in BitBlast concat operator

* added QF_BV test for unchecked QF_BV concat behaviour

* replaced to_string visitor with karma grammar printer

* added type::Array which maps a bit-vector index type to a bit-vector element type

* fixed missing return value warnings in STP

* added type::Array to domain_type_visitor Z3 backend

* removed semicolons from BOOST_FUSION_ADAPT_
*_STRUCT macros

* added missing scopes to TypedSymbol

* changed absolute include paths to relative include paths

* removed unused iterator variable from BitBlast

* fixed BitBlast buint function

* fixed warning in Direct/GraphSolver about indeterminate (clang)

* fixed warning in python bindings

* added default flags for GCC to reduce compile time and memory consumption

* changed Z3 test to catch linker and runtime library problems

* added test case using stacked annotations

* improved SMT2 backend
* SMT-LIB2 backend writes SMT-LIB2 output to solver and result stream
* separated implementation into generic template-based code and library code with std::ostream_iterator instantiation

* implemented stack_push and stack_pop commands for SMT2 backend

* added a preprocessor warning which complains when BOOST_VARIANT_VISITATION_UNROLLING_LIMIT is too small

* increased BOOST_VARIANT_VISITATION_UNROLLING_LIMIT where necessary

* implemented sign_extension for TypedSymbols

* fixed cpack ignore pattern to still include cmake/build_type.cmake

* build libmetaSMT always in release mode (GCC, Clang)

* fixed error in cmakelists change.

* metaSMTConfig.cmake also includes the libraries by path.

* implemented Evaluator API which allows for the extension of the list of metaSMT\'s primitive types replaced bool_tag / predicate_const by Evaluator

* fixed typo in CMake message

* updated disable_ / enable_warnings.hpp to work around a gcc 4.4 problem

* implemented specialization of Evaluator for TypedSymbols

* added test case for bvbin constant > 64bit, extended 64bit tests

* cleanup of ClauseWriter Backend. Remove temporary files after solving.

* made Z3 Backend handle large constanst (>32bit) better

* Suppressed warnings from boost in concurrent_queue.

* added assumption to python bindings

* made bootstrap.sh script really work with symlinks to dependencies folder

* added description that subversion and git is required for downloading dependencies

* cleanup of python bindings tests.

* removed symlink to python libray from source tree. use pymetaSMT instead

* use pymetaSMT for test discovery

* cleanup of python code, removed automatic conversion from bv too boolean

* disable \"-Wlogical-op-parentheses\" for clang in disable warnings

* fixed warnings on empty macro arguments when compiling with --pedantic

* added missing include to run_algorithm

* fixed warning on zero-sized array in Z3_Backend

* added a warning for low visitation unrolling limit and included default_visitation_unrolling_limit where necessary moved default_visitation_unrolling_limit.hpp from directory expression to directory support

* implemented solver options proposal for DirectSolvers and GraphSolvers

* restructured python bindings to use metaSMT::expression

* fixed name of python test module __init__ file

* added tests for python nary or, and

* python test main now has correct exit code

* handle python nary expression using boost::python::list

* correctly handle nary expression in python solvers

* added missing case for nary operators to python operators

* use print_expression as python __repr__ for logic_expressions

* added as_boolean to python support, use it for cardinality

* fixed core tests, wrong oder in extract, detection of number of args

* check python operator shifting with a constant value to avoid rand failures

* Do not rebuld python binding after cmake rerun if config did not change

* add python_config.hxx dependency to build python bindings

* try to make Priority_Context::ready thread safe

* array support for python bindings

* removed unecessary template Tag

* replaced notify_option_change_cmd by set_option, extended the number of parameters of NOP command

* implemented set_option and get_option for Priority_Context and Threaded_Context

* implemented Evaluator extension for evaluate(.)

* disabled grammar checking in Graph_Context

* new cardinality API based on Evaluator
* support for deprecated cardinality API
* adder network implementation

* added cardinality tests to direct_MiniSAT, graph_SMT2, and direct_Priority_Boolector_CUDD

* fixed generation of metaSMT.makefile

* link against system gmpxx/gmp library if not found by find_library

* Added missing include to boost/any.hpp to Aiger backend

* added missing includes and forward declarations to SMT2

* fixed debug output from BitBlast

* added missing includes for std::set

* fixed Doxygen errors for special characters

* fixed const correctness of TypedSymbol converters

* fixed default name of metaSMT solution file

* changed UnpackFuture_Context to take shared_futures by values

* added common dependencies path to gitignore

* added missing header for boost any to SAT_Clause

* added support for Pseudo-Boolean minimize and maximize constraints

* enabled test cases for Pseudo-Boolean minimize and maximize constraints

* avoid to confuse search_tests.awk and simplified test cases

* disabled cout statements in Z3_Backend

* added test_optimization to direct_Z3

* added Stack to direct_SWORD to fix compiler error with test_optimizations

* added explicit cast to boost::any() in ExpressionSolver fixes several broken test cases

* reimplemented Z3_Backend utilizing Z3 4.1 API

* improved Array test cases

* added an example to toolbox which shows how to pretty print expressions using ExpressionSolver

* added Array test cases to ExpressionSolver and fixed ExpressionSolver forward for store_tag()

* enabled stack emulation in direct_ExprSolver_
*

* fixed search_tests.awk identify the name of a test case between the first pair of parenthesis ( ... ) after the keyword BOOST_AUTO_TEST_CASE

* improved the formatting of the optimization test cases

* fixed bug with interleaved assertions in SMT2

* CMake checks for Z3 4.x API

* SMT2 removed ``-m\'\' from the Z3 flags

* SMT2 refactored solver configuration

* added two options (solver_executable and solver_arguments) to select particular command line solver

* fixed linking issues with duplicate named symbol support::execute

* Z3_backend: reimplemented bvbin(.) using GMP to support bitwidths > 64bit

* Boolector: avoid to depend on Btor
* directly use result_type instead

* Boolector: adapted result_type to the Boolector API 1.5.115

* switched to boost 1.50.0 for compatibility with Fedora 17

* required fix to compile under Fedora 17

* Added requirements on zlib and Python to READEME file.

* Use CMake FeatureSummary only with cmake 2.8.3 or later

* rewrote BtorExp
* to BtorNode
* in boolector_factorization

* removed executable flag from Priority_Context.hpp

* added an evaluator test case

* updated bootstrap.sh to boolector-1.5.116

* implemented reading from select expressions in SMT2 (fixes Array/read_value_t)

* generalized constructor of metaSMT::type::TypedSymbol

* renamed Array test case read_value_t to read_value_from_select

* updated boolector version in bootstrap to 1.5.118

* implemented Evaluator extension for read_value(.)

* Search by boost package only once.

* added UtreeEvaluator methods to analyse parsed SMT2 formulas and transform them to metaSMT

* added recognition of constants true, false

* added recognition of more bv operators

* added \"ToString\" to Methodnames generating strings as preparation for generating result_types instead of strings

* added Method to create Boolector::assumption/assertion instead of std::string (does not calc result_type yet)

* added method to translate SMT2 to result_types, works only for constants yet

* ctx.solve() will now be called at every check-sat return value printed to std::cout

* added new testcases: =(T,!F), =(!F,T) there is a bug translating those

* fixed a bug where translation to String was wrong

* removed function isOperator, check will new be done directly with the operatorMap

* calling ctx through metaSMT now

* added result_type recognition for ite and binary operators

* changed UTreeEvaluator::solve() to return bool Testcases will now run BOOST_REQUIRE( !solve(ctx) ); to check if parsed formula is true or false

* added result_type creation for bv-bin/hex/sint

* added recognition of variables with declare-fun. evaluator will lookup variable declaration while solving

* fixed a Bug where access to boost::spirit::utree::type was denied access will now be through boost::spirit::utree_type

* Initial Version

* separated UTreeEvaluator ToString and ToResultType methods. ToString methods are now in a derived class from UTreeEvaluator, UTreeEvaluatorToCode, reimplementing most of its methods to produce C++ Code.

* using metaSMT/API/Stack for SMT2-Symbols push and pop

* added recognition of SMT2-Symbol get-value. when parsing this, the Evaluator will call mataSMT::read_value and print the returnvalue to std::cerr

* added transformation of 1 bit values to metaSMT::bit0/1 added recognition of BitVector relational operators

* fixed a Bug, where #b01 would be converted to metaSMT::bit1

* added toolbox programm smt2File_evaluator. It reads a .smt2 file, runs the SMT_LIB2 Parser on the file content. Afterwards it runs UTreeEvaluator on parsed content.

* disabled assertion in evaluator in order to fire an exception instead

* sat/unsat will now be printed to std::cout instead of 1/0 to std::cerr

* Working version of SMT2Parser.cpp, invoking smt2Input_evaluator as executable, which runs SMT-LIB2 Parser and UTreeEvaluator

* fixed a bug where the last operand was given the operator as the first an the first as the last. fixed output of bool variables received from metaSMT::read_value

* removed a print to std::cout in Z3 Backend, which interfered with SMT2-Parser testframework

* added missing QF_BV operators added logic for QF_BV modify length operators

* replace platform dependent include to gmp

* splits connection handling into a class

* adds precompiled headers to metaSMT-server for compilation speedup

* set clang as default compiler to further speed up the compilation process

* smt2Input_evaluator: separated typedef of context from main program

* UTreeEvaluator: removed namespace boost::spirit and made some code style changes

* smt2Input_evaluator: added main files for more backends

* solved conflict between boost::assertion and metaSMT::assertion

* bugfix for build files, boost 1_52_0 is required

* UTreeEvaluator: added a constructor which gets variableMaps as parameter

* changed PicoSAT SAT::tag::lit_tag to typedef result_type

* smt2Input_evaluator: changed Context to ContextType bugfix for PicoSAT

* defined result_type in MiniSAT backend to allow for stack emulation

* inlined execvp to avoid duplicate function errors in python bindings

* fixed ContextType of MiniSAT for SMT-LIB2 evaluator

* fixed ContextType of SMT2 for SMT-LIB2 evaluator

* removed untested SMT-LIB2 evaluators from toolbox

* fixed pointer bug in UTreeEvaluator

* removed stack emulation from Z3_Backend SMT-LIB2 evaluator

* removed unnecessary iostreams header from SMT2Parser.cpp

* removed absolute path from SMT2Parser assuming that the PATH to the solver executable is known by the environment

* catch dependency errors in bootstrap.sh

* fix wrong -l flag for libmetaSMT in generated metaSMT.makefile

* include Boost libraries in generated metaSMT.makefile

* replace platform dependent include to gmp

* include Boost.system library when searching for boost.

* fixed picoSAT dependency in CMakeLists.txt of smt2Input_evaluator

* added missing default target for switch-case in UTreeEvaluator

* adds template to concatenate two boost::mpl::string

* adds missing tags to SMT_Tag_Mapping

* removes redundant function from UTreeEvaluator

* removed dead code from UTreeEvaluator

* refactored initialization of predicate and bitvector map in UTreeEvaluator

* new method evaluateExpressions(.) which evaluate expressions to result_types in UTreeEvaluator

* avoid building temporary shared_ptrs in UTreeEvaluator

* removed unnecessary namespaces from UTreeEvaluator

* refactored smt2operator and OperatorMap utilizing a compile-time index lookup template the indices are the positions of the tags in the AllTags vector and the string-names are taken from the SMT_NameMap

* refactored PredicateMap and BitVectorMap into a single VarMap in UTreeEvalator

* fixed memory leaks of UTreeEvaluator by using shared_ptr

* improved const correctness of UTreeEvaluator

* adds TODO for metaSMT-server

* metaSMT-server: remove local variables (solver,bitvectors,etc.) in favor of object variables

* metaSMT-server: fix parser to handle newlines consisting of carriage return and line feed

* metSMT-server: fix bug where every incoming line but the first is dropped, if all they are sent all at once

* metaSMT-server: fix debug output to contain a newline

* metaSMT-server: adds test file to check for proper interpretation on the serverside

* implemented functionality to evaluate SMT-LIB2 strings

* implement tag attributes

* create result_type from index in UTreeEvaluator

* use attributes to deduce arity of a tag in UTreeEvaluator

* use SMT_NameMap explicitly when get_index API is invoked

* removed incomplete error handling from SMT2Parser

* fixed compile-time error due to missing namespace in UTreeEvaluator

* removed redundant header from test_optimization

* fixed minimization algorithm: when witness is smaller than the minimum return with the minimum as a possible solution

* add isBinary function for json subtree

* add support for all binary operations to metaSMT-server

* don\'t let exceptions take down a whole connection

* adds support for unary operations to metaSMT-server

* don\'t let a solver exception take down the whole metaSMT-server

* update metaSMT-server test file

* provide hash_value overloads for predicate, bitvector, and array

* improves test cases QF_BV/bvuint_t and QF_BV/bvsint_t

* fixes bvuint in Z3_Backend for long unsigned integer constants

* simplifies bvuint and bvsint in Z3_Backend utilizing Z3_mk_unsigned_int64 and Z3_mk_int64

* fixed signed extension in test case QF_BV/bvsint_t

* templatifiy Connection class

* move line parsing into separate function for future use

* move next_line out of Connection class

* hopefully temporarily requires a buffer-object beside the socket to create an instance of Connection

* add support for picosat

* add support for multiple types of solvers to metaSMT-server

* Added predicates and not operation

* initial commit to support multiple solvers in metaSMT-server

* metaSMT-server: update TODO

* metaSMT-server: update TODO

* reworked the concurrent usage of multiple solvers

* work around picosat \"one instance per process\"

* Remove precompiled header command from metaSMT-server

* fixes library dependencies for boost_thread and boost_system in toolbox/metaSMT-server

* fixes MiniSat dependencies

* fixes variable name PicoSAT_FOUND

* adds missing dependencies to metaSMT-server

* added librt to Z3_LIBRARIES (required on some platforms)

* Added support for using the QF_ABV fragment in the STP backend

* fixed compile-time error in metaSMT-server due to ambiguity (occuring e.g. with GCC 4.4.7)

* implemented SMT-LIB2 attributes in order to parse nary commands

* adapted maximum input line length to 65535 for all smt2input_evaluators

* replaced boost::lexical_casts with boost::spirit::qi-parsers

* implemented nary predtags::and_tag and pretags::or_tag in Z3_Backend

* implemented nary predtags::and_tag and predtags::or_tag in STP

* implemented a binary version of SMT-LIB2 command distinct(.)

* SMT2 only push before check-sat if there is at least one assumption

* DirectSolver_Context additionally operates on vectors of expressions (support for nary-commands)

* reimplemented UTreeEvaluator using a compile-time Command mapping

* included missing headers

* fixed utree namespace in SMT2Parser

* introduced mapping from solver name to solver type

* create solver from solver name

* SMT-LIB2 compatible version of metaSMT-server

* add missing include

* removed output from CheckSat command

* updated evaluate command to parse results from CheckSat and GetValue commands

* smt2Input_evaluator reads strings of unlimited length and does not wait for an command ``(exit)\'\'

* fixed newline suffix in Connection::write(.)

* implemented nary-and and nary-or operators for Boolector

* implemented nary-and and nary-or operators for SMT2

* added a simple version of a symbol table

* implemented set-logic command

* updated attributes in Logic.hpp

* nary operator with left associativity attribute are forwarded to the solver backend

* added simple_symbol_table to UTreeEvaluator, i.e., SMT2 preserves the names of the variables

* created SMT2Parser test suites for Boolector, STP, Z3_Backend, and SMT2

* implemented error message for metaSMT-server in case of invalid input

* metaSMT-server passes error messages to the client

* metaSMT-server throws exceptions in case of unsupported commands

* improved error handling and error messages of metaSMT-server

* metaSMT-server: fix parent_read_command_available()

* metaSMT-server: add support for timeouts

* metaSMT-server: timeouts

* metaSMT-server: sanify return messages of solvers

* metaSMT-server: only measure time consumed for (check-sat)

* metaSMT-server: at \"(exit)\" report time needed since \"start\"

* metaSMT-server: close pipes while shutting solvers down

* fixes possible call to pthread_kill on negative ids (which may lead to killing the xserver and other applications)

* removed unneeded code from metaSMT-server

* implemented support for ``set-option [timeout|solver|...]\'\' in metaSMT-server

* implemented special cardinality tags

* adapted ad-hoc cardinality tags (object.hpp) to new implementation (tags/Cardinality.hpp)

* moved treatment of special cases of cardinality to cardinality_simplify
* added includes (object.hpp, adder_impl.hpp, bdd_impl.hpp)
* made nps const
* removed usage on ps.size() when nps should have been used

* refactored test_cardinality.cpp

* fixed compile-time errors in ``bdd_impl.hpp\'\' and ``test_unsat.cpp\'\' due to ambiguity (occuring e.g. with GCC 4.4.7)

* metaSMT-server: implement incremental sat

* fixed syntax of command set-option according to SMT-LIB2 standard

* registered names of cardinality tags in SMT_Tag_Mapping

* allow SimpleSymbolTable to use unanmed, internal variables (e.g., cardinality)

* implemented SetOption command in SMT-LIB2 parser

* inserted cardinality tags to all_Tags

* implemented support for cardinality logic in SMT-LIB2 parser

* added missing default impl (BDD) for card_eq

* Fixed arity problem with left-associative tags

* Server ignores comments in smt input

* removed unneccessary debug output

* Added debug output in case of unfound variable

* removed unused connection.hpp file

* Added safety check for (get-value)

* added support for solvers STP, SWORD, MiniSAT, PicoSAT, and CUDD to metaSMT-server

* Command throws exception on error

* removed unused variable from source

* fixed result_wrapper test

* preliminary support for CVC4, only boolean level

* implemented BitVector support to CVC4

* added missing include files

* added lingeling SAT solver version: ayv

* converted to markdown

* move sections one level lower

* fix renaming from README to README.md

* added test files for lingeling (direct, graph)

* added lingeling backend implementation

* clarified error message for missing dependencies

* use boolector-2.0 dependency and license splitting

* renamed booststrap parameter to --academic

* adapted Boolector backend for boolector-2.0 API

* use boost::atomic_uint for new_variable

* fix implicit conversion yielding a warning

* bootstrap.sh: fixed handling of -G

* Extend usage manual

* Explain \'dependencies\' folder in README.md

* Fix typos as mentioned by hriener

* added bootstrap option to add custom dependencies

* switched from Z3-4.1 to Z3-git

* moved lingeling from --free to --non-free

* check missing dependencies on metaSMT-server

* Update README.md

* fixed minimum CMake version

* bootstrap version 3.2.2 of cmake if requested

* support -j in bootstrap.sh

* use the git version of stp

* add_all_tests: removed trailing list seperator

* fixed warnings in library_rpath.cmake

* cvc4 should be linked with gmp

* bugfix STP shl/shr: bitwidth greater than 32bit

* STP: bvshl, bvshr, bvashr

* STP (removed comment)

* disable SWORD on OS X

* cleanup else() and endif() expressions in CMakeLists.txt

* rewrite of GoTmp using boost.filesystem

* renamed test_stack for OS X compability

* missing include to boost/optional.hpp in cardinality Evaluator

* added missing dependency to STP in metaSMT-server

* disable STP when cryptominisat was not found

* refactored sortnet example

* fixed bvsrem in STP

* fixed division-by-zero errors from bvudiv in STP

* added helper to compare arrays for equal/nequal

* switched array tests to use array_equal helper

* also run array tests for STP

* The CUDD backend also uses functions from CUDD_cudd

* allow to control randomness of CUDD_Distributed

* added travis conf

* excluded some backends from travis conf

* excluded z3 from travis too

* add badges

* included all CUDD libs

* fixed includes

* workaround for the boost::atomic issue

* link Z3 with pthread (required now)

* Update boolector_factorization.cpp

* Update boolector_factorization.cpp

* del bindings and toolbox

* remove binding and toolbox from cmake

* del files that are not used by crave

* remove unused files

* remove api/group from tests

* fix tests

* readd SAT.hpp

* fix sat include

* fix tests

* remove some unused functions from result_wrapper

* remove unused function

* Revert \"remove unused function\"

* update Boolector backend

* added TIMEOUT to python binding tests

* reset btor settings, allow to change from subclasses

* Revert \"remove some unused functions from result_wrapper\"

* del ExpressionSolver and smt2

* del expression

* del unused flags for smt2 and expression

* del simpleSymbolTable

* fix list_of operation

* fix convert errors

* include array tests

* update tests

* remove unpackfuture

* remove Array tests for backend without support

* fix test_Array

* add check for c++11 compiler

* use BOOST_ROOT

* update PROFILING flags

* removed warnings

* Update .travis.yml

* Update .travis.yml

* Update .travis.yml

* Update bootstrap.sh

* Update bootstrap.sh

* Update bootstrap.sh

* Update bootstrap.sh

* Update README.md

* Update .travis.yml

* update CMakeLists to link Z3

* remove more warnings

* CI test all backends

* Update .travis.yml

* update coverity badge [ci skip]

* switch to Z3-4.4.1 (recent Z3-git won\'t compile with older gcc and clang due to std::hexfloat)

* implement distinct for cudd

* fix read_value() of Z3 and STP to return BV with width > 64

* Find boost headers only [ci skip]

* Update .travis.yml

* need boost program options

* remove unused model_parser

* Update test_cardinality.cpp

* include support for boolector 1.x again

* add boolector version to metaSMT_CXX_FLAGS

* use std::unordered_map

* fix to compile with boolector 1.x

* remove unused boost deps

* Update .travis.yml

* switch to a simple stp version without cmsat & program_options

* enable compilation of Z3_Backend with C++03

* add switch for C++03 and C++11 unordered_map

* remove deprecated --travis from bootstrap

* fix --build in bootstrap

* fix -D option

* do not set not-found-lib

* enable generation of makefile config using -L and -l style in addition to absolute library path

* improve Z3_WORKS check

* handle -fopenmp correctly

* switch back to default clang (v3.4) until llvm apt works again

* add test for get_bv_width()

* implement get_bv_width

* include array support for CVC4 by AATTnbruns1

* include Yices2 with qf_abv support by AATTnbruns1

* install gperf in travis

* improved includes

* add missing operator(type::Array) (patch by AATTnbruns1)

* improved error msgs

* add new test that checks whether multiple instances of a solver can be used simulaneously

* up to Yices-2.5.1

* add two new incremental tests

* improve Yices2

* refactor Yices2

* set logic QF_AUFBV for Z3

* set logic QF_ABV for CVC4

* switch to cvc4-1.5pre-smtcomp2016

* remove lazy

* remove test for lazy

* add metaSMT_AVAILABLE_QF_ABV_SOLVERS string to config

* add flag metaSMT_REQUIRE_RTTI based on Boost version

* update boost handling (DEPS_BOOST is exported so that the same version can be used in other dependencies)

* update gitignore

* split build config in travis

* add travis matrix excludes

* optimize yices2 config

* replace boost::atomic with std::atomic

* replace gmp usage with boost::mp::cpp_int in Z3_Backend::bvin

* just use std::unordered_map assuming C++11

* cmake modifications for Windows environment (tested with VS2017-RC)

Sat Feb 25 13:00:00 2017 jslabyAATTsuse.com
- initial package