projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Move enum value generator to own file (#6941)
[cvc5.git] / src / CMakeLists.txt
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941) blob | commitdiff | raw
2021-07-27 Andrew ReynoldsAdd proof letify utility (#6881) blob | commitdiff | raw | diff to current
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923) blob | commitdiff | raw | diff to current
2021-07-22 Andrew ReynoldsAdd the central equality engine manager (#6893) blob | commitdiff | raw | diff to current
2021-07-15 Andrew ReynoldsConnect the equality solver to theory arith (#6894) blob | commitdiff | raw | diff to current
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file... blob | commitdiff | raw | diff to current
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891) blob | commitdiff | raw | diff to current
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889) blob | commitdiff | raw | diff to current
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) blob | commitdiff | raw | diff to current
2021-07-14 Andrew ReynoldsMove synthesis verification check to own file (#6882) blob | commitdiff | raw | diff to current
2021-07-12 Andrew ReynoldsAdd branch and bound (#6865) blob | commitdiff | raw | diff to current
2021-07-12 Andrew ReynoldsAdd arithmetic preprocess rewrite equality module ... blob | commitdiff | raw | diff to current
2021-07-06 Gereon KremerIntegrate Lazard into CAD module (#6812) blob | commitdiff | raw | diff to current
2021-07-06 Andrew ReynoldsIntegrate learned rewrite preprocessing pass (#6840) blob | commitdiff | raw | diff to current
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760) blob | commitdiff | raw | diff to current
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761) blob | commitdiff | raw | diff to current
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) blob | commitdiff | raw | diff to current
2021-06-15 yoni206pow2: adding a kind, inference rules, and some implemen... blob | commitdiff | raw | diff to current
2021-06-11 Gereon KremerAdd skeleton for new Lazard evaluation (#6732) blob | commitdiff | raw | diff to current
2021-06-08 Andrew ReynoldsAdd learned literal manager utility (#6709) blob | commitdiff | raw | diff to current
2021-06-04 yoni206pow2: header file for pow2 solver (#6676) blob | commitdiff | raw | diff to current
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) blob | commitdiff | raw | diff to current
2021-05-24 Andrew ReynoldsImplementation of the new justification heuristic ... blob | commitdiff | raw | diff to current
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) blob | commitdiff | raw | diff to current
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) blob | commitdiff | raw | diff to current
2021-05-18 Abdalrhman MohamedLoop over terms to reconstruct instead of obligations... blob | commitdiff | raw | diff to current
2021-05-05 Andrew ReynoldsMove current decision engine to decision engine old... blob | commitdiff | raw | diff to current
2021-04-30 Andrew ReynoldsUse substitutions for implementing defined functions... blob | commitdiff | raw | diff to current
2021-04-29 Andrew ReynoldsAdd assertion list utility for justification heuristic... blob | commitdiff | raw | diff to current
2021-04-27 Aina NiemetzBool: Move implementation of type rules to cpp. (#6420) blob | commitdiff | raw | diff to current
2021-04-23 Andrew ReynoldsMove implementation of UF rewriter to cpp (#6393) blob | commitdiff | raw | diff to current
2021-04-21 Aina NiemetzArithmetic: Move implementation of type rules to cpp... blob | commitdiff | raw | diff to current
2021-04-21 Aina NiemetzUF: Move implementation of type rules to cpp. (#6403) blob | commitdiff | raw | diff to current
2021-04-21 Aina NiemetzDatatypes: Move implementation of type rules to cpp... blob | commitdiff | raw | diff to current
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) blob | commitdiff | raw | diff to current
2021-04-21 Aina NiemetzSets: Move implementation of type rules to cpp. (#6401) blob | commitdiff | raw | diff to current
2021-04-21 Aina NiemetzArrays: Move implementation of type rules to cpp. ... blob | commitdiff | raw | diff to current
2021-04-21 Andrew ReynoldsAdd basic utilities for new implementation of justifica... blob | commitdiff | raw | diff to current
2021-04-20 Andrew ReynoldsSplit FP expand definitions to own module (#6392) blob | commitdiff | raw | diff to current
2021-04-20 Aina NiemetzBV: Move implementation of type rules from header to... blob | commitdiff | raw | diff to current
2021-04-20 Aina NiemetzSep: Move implementation of type rules to cpp. (#6402) blob | commitdiff | raw | diff to current
2021-04-20 Aina NiemetzQuantifiers: Move implementation of type rules to cpp... blob | commitdiff | raw | diff to current
2021-04-20 Andrew ReynoldsAdd instantiation pool feature to the API (#6358) blob | commitdiff | raw | diff to current
2021-04-19 Andrew ReynoldsFully incorporate quantifiers macros into ppAssert... blob | commitdiff | raw | diff to current
2021-04-16 Mathias Preinercmake: Build object libraries for base and context... blob | commitdiff | raw | diff to current
2021-04-15 Mathias PreinerBuild support library from base and context. (#6368) blob | commitdiff | raw | diff to current
2021-04-13 Andrew ReynoldsAdd pool instantiation strategy (#6308) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzStrings: Move implementation of type rules from header... blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) blob | commitdiff | raw | diff to current
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
next