projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Remove experimental symmetry breaker (#4005)
[cvc5.git] / src / CMakeLists.txt
2020-03-11 Andrew ReynoldsRemove experimental symmetry breaker (#4005) blob | commitdiff | raw
2020-03-11 Andrew ReynoldsRemove partial instantiation for local theory extension... blob | commitdiff | raw | diff to current
2020-03-10 Andrew ReynoldsRemove instantiation propagator infrastructure (#3975) blob | commitdiff | raw | diff to current
2020-03-06 Andres NoetzliRemove --apply-to-const preprocessing pass (#3919) blob | commitdiff | raw | diff to current
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... blob | commitdiff | raw | diff to current
2020-03-03 Andrew ReynoldsStandardize the interface for SMT engine subsolvers... blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) blob | commitdiff | raw | diff to current
2020-02-26 Andrew ReynoldsMove equivalence class info to its own file in strings... blob | commitdiff | raw | diff to current
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) blob | commitdiff | raw | diff to current
2020-02-25 yoni206bv_to_int preprocessing pass blob | commitdiff | raw | diff to current
2020-02-24 Andrew ReynoldsUtilities for words (#3797) blob | commitdiff | raw | diff to current
2020-02-21 Andrew ReynoldsSplit extended functions solver in strings (#3768) blob | commitdiff | raw | diff to current
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) blob | commitdiff | raw | diff to current
2020-02-14 Andrew ReynoldsUpdate sygus v1 parser to use ParseOp utility (#3756) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsSplit strings finite model finding strategy (#3727) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsSplit core solver from the theory of strings (#3713) blob | commitdiff | raw | diff to current
2020-02-08 Andrew ReynoldsInterface for example evaluation cache utilities (... blob | commitdiff | raw | diff to current
2020-02-04 Andrew ReynoldsSplit base solver from the theory of strings (#3680) blob | commitdiff | raw | diff to current
2020-02-03 Andrew ReynoldsExample inference utility (#3670) blob | commitdiff | raw | diff to current
2020-01-31 Andrew ReynoldsRefactor sygus stats (#3684) blob | commitdiff | raw | diff to current
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671) blob | commitdiff | raw | diff to current
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) blob | commitdiff | raw | diff to current
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) blob | commitdiff | raw | diff to current
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... blob | commitdiff | raw | diff to current
2019-11-06 Andrew ReynoldsSupport for SyGuS PBE + recursive functions (#3433) blob | commitdiff | raw | diff to current
2019-11-05 Andrew ReynoldsSeparate model object in non-linear extension (#3426) blob | commitdiff | raw | diff to current
2019-11-01 Andrew ReynoldsRename datatypes sygus solver (#3417) blob | commitdiff | raw | diff to current
2019-10-30 Andrew ReynoldsSplit some generic utilities from the non-linear extens... blob | commitdiff | raw | diff to current
2019-10-17 Andrew Reynolds Move datatype utility functions to own file (#3397) blob | commitdiff | raw | diff to current
2019-10-16 Andrew ReynoldsSolver state for theory of strings (#3181) blob | commitdiff | raw | diff to current
2019-10-11 Aina NiemetzMake order of theories explicit in the source code... blob | commitdiff | raw | diff to current
2019-10-08 Ying ShengMake ackermannization generally applicable rather than... blob | commitdiff | raw | diff to current
2019-09-25 Mathias PreinerUse separate CMake project for CVC4 examples. (#3196) blob | commitdiff | raw | diff to current
2019-09-16 Andrew ReynoldsSygus type info class (#3187) blob | commitdiff | raw | diff to current
2019-09-16 Andrew ReynoldsMove virtual term substitution utilities to own file... blob | commitdiff | raw | diff to current
2019-09-13 Andrew ReynoldsSplit, refactor and document the theory of sets (#3085) blob | commitdiff | raw | diff to current
2019-09-12 Andrew Reynolds Rename UF with cardinality extension (#3241) blob | commitdiff | raw | diff to current
2019-09-12 Andrew ReynoldsRefactoring finite bounds in Quantifiers Engine (#3261) blob | commitdiff | raw | diff to current
2019-09-07 Andrew ReynoldsRemove portfolio (#3236) blob | commitdiff | raw | diff to current
2019-08-23 Andrew ReynoldsDocument transition inference utility (#3207) blob | commitdiff | raw | diff to current
2019-08-14 Mathias Preinercmake: Export CVC4 library interface. (#3179) blob | commitdiff | raw | diff to current
2019-08-02 Andrew Reynolds Move basic sygus enumerator to its own file (#3149) blob | commitdiff | raw | diff to current
2019-08-01 Andrew ReynoldsMove some generic utilities out of quantifiers (#3139) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsModel blocker feature (#3112) blob | commitdiff | raw | diff to current
2019-07-29 Andrew ReynoldsSupport get-abduct smt2 command (#3122) blob | commitdiff | raw | diff to current
2019-07-25 Andrew ReynoldsSplit infer info data structure in strings (#3107) blob | commitdiff | raw | diff to current
2019-07-08 Andrew ReynoldsTowards refactoring relations (#3078) blob | commitdiff | raw | diff to current
2019-07-06 Andrew ReynoldsRefactor strings to use an inference manager object... blob | commitdiff | raw | diff to current
2019-07-02 Alex OzdemirOptimize DRAT optimization: clause matching (#3074) blob | commitdiff | raw | diff to current
2019-07-01 Andrew Reynolds Split higher-order UF solver (#2890) blob | commitdiff | raw | diff to current
2019-07-01 Andrew ReynoldsAdd higher-order elimination preprocessing pass (#2865) blob | commitdiff | raw | diff to current
2019-06-05 Alex OzdemirDRAT-Optimization (#2971) blob | commitdiff | raw | diff to current
2019-04-23 Andrew ReynoldsRefactor normal forms in strings (#2897) blob | commitdiff | raw | diff to current
2019-04-16 makaimannCheck for rt library in configuration -- support for... blob | commitdiff | raw | diff to current
2019-03-24 Andrew Reynolds Split regular expression solver (#2891) blob | commitdiff | raw | diff to current
2019-03-20 Andrew ReynoldsSygus abduction feature (#2744) blob | commitdiff | raw | diff to current
2019-03-13 Andres NoetzliAdd statistics for proof gen./checking time, size ... blob | commitdiff | raw | diff to current
2019-03-13 Mathias PreinerFix public headers for make install. (#2856) blob | commitdiff | raw | diff to current
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812) blob | commitdiff | raw | diff to current
2019-01-18 Alex OzdemirExtract DIMACS Printing (#2800) blob | commitdiff | raw | diff to current
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786) blob | commitdiff | raw | diff to current
2019-01-06 Alex Ozdemir[DRAT] DRAT data structure (#2767) blob | commitdiff | raw | diff to current
2019-01-04 Alex Ozdemir[LRAT] A C++ data structure for LRAT. (#2737) blob | commitdiff | raw | diff to current
2018-12-17 Alex Ozdemir Configured for linking against drat2er (#2754) blob | commitdiff | raw | diff to current
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747) blob | commitdiff | raw | diff to current
2018-12-11 Andrew ReynoldsRemove alternate versions of mbqi (#2742) blob | commitdiff | raw | diff to current
2018-12-03 Alex OzdemirBit vector proof superclass (#2599) blob | commitdiff | raw | diff to current
2018-10-31 Andrew ReynoldsAdd optimized sygus enumeration (#2677) blob | commitdiff | raw | diff to current
2018-10-20 Andrew ReynoldsSygus streaming non-implied predicates (#2660) blob | commitdiff | raw | diff to current
2018-10-19 Andrew ReynoldsNon-implied mode for model cores (#2653) blob | commitdiff | raw | diff to current
2018-10-18 Andrew ReynoldsSygus query generator (#2465) blob | commitdiff | raw | diff to current
2018-10-15 Mathias Preinercmake: Generate git_versioninfo.cpp on build time.... blob | commitdiff | raw | diff to current
2018-10-09 Aina NiemetzBV instantiator: Factor out util functions. (#2604) blob | commitdiff | raw | diff to current
2018-10-09 Aina Niemetz BV inverter: Factor out util functions. (#2603) blob | commitdiff | raw | diff to current
2018-09-29 Haniel BarbosaStream concrete values for variable agnostic enumerator... blob | commitdiff | raw | diff to current
2018-09-24 Mathias Preinercmake: Fix theory order #2. (#2522) blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Build fully static binaries with option --static. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add more documentation, some fixes and cleanup. blob | commitdiff | raw | diff to current
2018-09-22 Aina Niemetzcmake: More documentation, clean up. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add make install rule. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Only build libcvc4 and libcvc4parser as libraries. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add library versioning for libcvc4.so. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Rebase with current master, add new tests/source... blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Use target specific includes for libcvc4. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add SWIG support + Python and Java bindings. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Fix some includes. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Cleanup CMakeLists.txt files, remove SHARED. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add module finder for SymFPU. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Add libsignatures for proofs. blob | commitdiff | raw | diff to current
2018-09-22 Mathias Preinercmake: Working build infrastructure. blob | commitdiff | raw | diff to current
2018-09-22 Aina Niemetzcmake: .cpp generation done, .h generation not yet... blob | commitdiff | raw | diff to current
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. blob | commitdiff | raw | diff to current