projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add identifiers for extended function reductions (#6314)
[cvc5.git] / src / CMakeLists.txt
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) blob | commitdiff | raw
2021-04-07 Aina NiemetzNew C++ Api: Rename and move checks.h. (#6306) blob | commitdiff | raw | diff to current
2021-04-07 Andrew ReynoldsAdd term pools utility (#6243) blob | commitdiff | raw | diff to current
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) blob | commitdiff | raw | diff to current
2021-04-05 Yancheng OuOptimizer for BitVectors (#6213) blob | commitdiff | raw | diff to current
2021-04-01 Gereon KremerRefactor CLN dependency & Cleanup (#6251) blob | commitdiff | raw | diff to current
2021-03-31 Gereon KremerRefactor GMP and Poly dependencies (#6245) blob | commitdiff | raw | diff to current
2021-03-31 Gereon KremerRefactor dependencies for external SAT solvers (#6215) blob | commitdiff | raw | diff to current
2021-03-31 Gereon KremerRefactor SymFPU dependency (#6218) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzBags: Move implementation of type rules from header... blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzFP: Move implementation of type rules from header to... blob | commitdiff | raw | diff to current
2021-03-29 yoni206Modular bv2int part 1 (#6212) blob | commitdiff | raw | diff to current
2021-03-25 Andrew ReynoldsRefactor construction of triggers (#6209) blob | commitdiff | raw | diff to current
2021-03-23 Haniel BarbosaRemoving unused build options and deprecated proof... blob | commitdiff | raw | diff to current
2021-03-23 Abdalrhman MohamedReplace old sygus term reconstruction algorithm with... blob | commitdiff | raw | diff to current
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187) blob | commitdiff | raw | diff to current
2021-03-17 Andrew ReynoldsMove utilities for inferred bounds on quantifers to... blob | commitdiff | raw | diff to current
2021-03-16 Mathias Preinercmake: Generate cvc4_export.h and set visibility to... blob | commitdiff | raw | diff to current
2021-03-15 Andrew ReynoldsSplit inst match generator class to own file (#6125) blob | commitdiff | raw | diff to current
2021-03-14 Diego Della Rocca... [proof-new] Adding a dot printer for proof nodes (... blob | commitdiff | raw | diff to current
2021-03-12 Aina NiemetzNew C++ Api: Move checks to separate file. (#6138) blob | commitdiff | raw | diff to current
2021-03-12 Mathias Preinercmake: Remove install rules for old API headers. (... blob | commitdiff | raw | diff to current
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) blob | commitdiff | raw | diff to current
2021-03-11 MikolasJanotaImprovements and refactoring for enumeratative strategy... blob | commitdiff | raw | diff to current
2021-03-11 Andrew Reynolds(proof-new) Clean up uses of witness with skolem lemmas... blob | commitdiff | raw | diff to current
2021-03-10 Andrew ReynoldsAdd Env class (#6093) blob | commitdiff | raw | diff to current
2021-03-09 Andrew ReynoldsRemove logic request (#6089) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-08 Andrew Reynolds(proof-new) Prepare arithmetic for changes to ppRewrite... blob | commitdiff | raw | diff to current
2021-03-05 mcjunehoInitial implementation of an optimization solver with... blob | commitdiff | raw | diff to current
2021-03-04 Aina NiemetzAdd initial bit-blaster for proof logging. (#6053) blob | commitdiff | raw | diff to current
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) blob | commitdiff | raw | diff to current
2021-03-02 Andrew ReynoldsIntroduce quantifiers term registry (#5983) blob | commitdiff | raw | diff to current
2021-02-27 Aina Niemetzgoogle test: theory: Migrate theory_white. (#6006) blob | commitdiff | raw | diff to current
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964) blob | commitdiff | raw | diff to current
2021-02-22 Gereon KremerAdd the LazyTreeProofGenerator. (#5948) blob | commitdiff | raw | diff to current
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) blob | commitdiff | raw | diff to current
2021-02-18 Andrew ReynoldsMove first order model for full model check to own... blob | commitdiff | raw | diff to current
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... blob | commitdiff | raw | diff to current
2021-02-13 Andrew ReynoldsMoving methods from quantifiers engine to quantifiers... blob | commitdiff | raw | diff to current
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) blob | commitdiff | raw | diff to current
2021-02-04 Andrew ReynoldsIntroduce quantifiers registry utility (#5829) blob | commitdiff | raw | diff to current
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) blob | commitdiff | raw | diff to current
2021-01-27 Andrew ReynoldsSplit pattern term selector from trigger (#5811) blob | commitdiff | raw | diff to current
2021-01-26 Andrew ReynoldsIntroduce quantifiers inference manager (#5821) blob | commitdiff | raw | diff to current
2021-01-26 Andrew ReynoldsRemove deprecated quantifiers modules (#5820) blob | commitdiff | raw | diff to current
2021-01-25 Andrew ReynoldsSplit inst match generator into multiple files (#5805) blob | commitdiff | raw | diff to current
2021-01-25 Andrew ReynoldsSplit E-matching strategies to own files (#5807) blob | commitdiff | raw | diff to current
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) blob | commitdiff | raw | diff to current
2021-01-15 Andrew ReynoldsImplement --no-strings-lazy-pp as a preprocessing pass... blob | commitdiff | raw | diff to current
2021-01-13 Andrew ReynoldsSplit eager solver from strings solver state (#5775) blob | commitdiff | raw | diff to current
2021-01-11 Andrew ReynoldsMerge theory registrar and theory proxy (#5758) blob | commitdiff | raw | diff to current
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) blob | commitdiff | raw | diff to current
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747) blob | commitdiff | raw | diff to current
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716) blob | commitdiff | raw | diff to current
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores... blob | commitdiff | raw | diff to current
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... blob | commitdiff | raw | diff to current
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... blob | commitdiff | raw | diff to current
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... blob | commitdiff | raw | diff to current
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680) blob | commitdiff | raw | diff to current
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje... blob | commitdiff | raw | diff to current
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... blob | commitdiff | raw | diff to current
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) blob | commitdiff | raw | diff to current
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) blob | commitdiff | raw | diff to current
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) blob | commitdiff | raw | diff to current
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) blob | commitdiff | raw | diff to current
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) blob | commitdiff | raw | diff to current
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... blob | commitdiff | raw | diff to current
2020-11-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500) blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422) blob | commitdiff | raw | diff to current
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) blob | commitdiff | raw | diff to current
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) blob | commitdiff | raw | diff to current
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436) blob | commitdiff | raw | diff to current
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) blob | commitdiff | raw | diff to current
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347) blob | commitdiff | raw | diff to current
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) blob | commitdiff | raw | diff to current
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388) blob | commitdiff | raw | diff to current
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375) blob | commitdiff | raw | diff to current
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter... blob | commitdiff | raw | diff to current
2020-10-21 Alex Ozdemir(proof-new) Add arith proof macros file to CMake (... blob | commitdiff | raw | diff to current
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) blob | commitdiff | raw | diff to current
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301) blob | commitdiff | raw | diff to current
2020-10-20 Andrew ReynoldsSplit CheckModels utility to its own file (#5303) blob | commitdiff | raw | diff to current
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275) blob | commitdiff | raw | diff to current
2020-10-10 yoni206bv2int: bvand translation code move (#5227) blob | commitdiff | raw | diff to current
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903) blob | commitdiff | raw | diff to current
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... blob | commitdiff | raw | diff to current
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188) blob | commitdiff | raw | diff to current
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) blob | commitdiff | raw | diff to current
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184) blob | commitdiff | raw | diff to current
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112) blob | commitdiff | raw | diff to current
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (... blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop... blob | commitdiff | raw | diff to current
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (... blob | commitdiff | raw | diff to current
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it... blob | commitdiff | raw | diff to current
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... blob | commitdiff | raw | diff to current
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132) blob | commitdiff | raw | diff to current
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148) blob | commitdiff | raw | diff to current
next