File metasmt.changes of Package metasmt
-------------------------------------------------------------------
Sat Mar 29 04:49:06 UTC 2025 - Jiri Slaby <jslaby@suse.cz>
- use %cmake_build
-------------------------------------------------------------------
Thu Feb 22 08:32:10 UTC 2024 - Jiri Slaby <jslaby@suse.cz>
- switch to obs_scm
- use %autosetup
-------------------------------------------------------------------
Thu Jan 30 10:23:29 UTC 2020 - jslaby@suse.com
- Update to version 0.0+20191203:
* add additional checks for indeterminate before comparing tribool with false
* fix more compilation failures due to tribool breaking changes in boost 1.69
* Work-around compilation failures with recent clang/boost.
* drop SWORD support
* detect Z3 API changes (since v4.7) and set compile flags accordingly
* Boolector 3 needs to be linked with pthread
* small improvement CUDD_Context::writeDotFile
* fix api use for cudd 3.0.0
* update recommended solver packages
* strengthen tests for result_wrapper
* update 64-bit tests to support 32-bit platforms
-------------------------------------------------------------------
Thu May 25 12:10:30 UTC 2017 - jslaby@suse.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 12:27:13 UTC 2017 - jslaby@suse.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<char> 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<bool>
* 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 @nbruns1
* include Yices2 with qf_abv support by @nbruns1
* install gperf in travis
* improved includes
* add missing operator(type::Array) (patch by @nbruns1)
* 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 10:53:28 UTC 2017 - jslaby@suse.com
- initial package
