projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
arrays: Move type enumerator implementation to .cpp. (#7216)
[cvc5.git] / src / CMakeLists.txt
2021-09-22 Aina Niemetzarrays: Move type enumerator implementation to .cpp... blob | commitdiff | raw
2021-09-22 Gereon KremerEliminate arithmetic proof macros (#7226) blob | commitdiff | raw | diff to current
2021-09-20 Haniel Barbosa[proofs] Alethe: adds a node converter blob | commitdiff | raw | diff to current
2021-09-20 Andrew ReynoldsAdd the LFSC proof post-processor (#7134) blob | commitdiff | raw | diff to current
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom... blob | commitdiff | raw | diff to current
2021-09-13 Aina NiemetzFP: Rename FpConverter to FpWordBlaster. (#7170) blob | commitdiff | raw | diff to current
2021-09-13 Gereon KremerAdd main options to cmake (#7178) blob | commitdiff | raw | diff to current
2021-09-09 Andrew ReynoldsAdd difficulty manager (#7151) blob | commitdiff | raw | diff to current
2021-09-09 Andrew ReynoldsAdd difficulty post-processor (#7150) blob | commitdiff | raw | diff to current
2021-09-08 Andrew ReynoldsAdd Lfsc print channel utilities (#7123) blob | commitdiff | raw | diff to current
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... blob | commitdiff | raw | diff to current
2021-09-08 Andrew ReynoldsAdd LFSC side condition conversion utility for list... blob | commitdiff | raw | diff to current
2021-09-02 Andrew ReynoldsAdd LFSC node converter (#6944) blob | commitdiff | raw | diff to current
2021-09-02 Aina NiemetzAdd class EnvObj. (#7113) blob | commitdiff | raw | diff to current
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... blob | commitdiff | raw | diff to current
2021-08-24 Andrew ReynoldsSplit higher-order term database (#7045) blob | commitdiff | raw | diff to current
2021-08-24 Andrew ReynoldsRefactor enumerator management in synth conjecture... blob | commitdiff | raw | diff to current
2021-08-22 Andrew ReynoldsSimplify model printing modes (#7049) blob | commitdiff | raw | diff to current
2021-08-19 Andrew ReynoldsSplit proof final callback to its own file (#6984) blob | commitdiff | raw | diff to current
2021-08-17 Andrew ReynoldsInitial refactoring of set defaults (#7021) blob | commitdiff | raw | diff to current
2021-08-09 Andres NoetzliSupport older CMake versions (#7003) blob | commitdiff | raw | diff to current
2021-08-06 Gereon KremerMerge options cmake into general cmake file (#6989) blob | commitdiff | raw | diff to current
2021-08-04 Gereon KremerRefactor managed streams (#6934) blob | commitdiff | raw | diff to current
2021-07-27 Andrew ReynoldsAdd basic LFSC utilities (#6879) blob | commitdiff | raw | diff to current
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941) blob | commitdiff | raw | diff to current
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
next