projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Minor cleaning of instantiation utilities (#7334)
[cvc5.git] / src / CMakeLists.txt
2021-10-11 Aina NiemetzRename SmtEngineStatistics to SolverEngineStatistics... blob | commitdiff | raw
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) blob | commitdiff | raw | diff to current
2021-10-11 Gereon KremerRevert #7257 (#7337) blob | commitdiff | raw | diff to current
2021-10-11 Gereon KremerRestore compatibility with cmake 3.9 (#7329) blob | commitdiff | raw | diff to current
2021-10-07 Gereon KremerAdd new versioning scheme (#7253) blob | commitdiff | raw | diff to current
2021-10-07 Gereon KremerFix/Improve static and shared builds with CLN or Poly... blob | commitdiff | raw | diff to current
2021-10-01 Andrew ReynoldsAdd the LFSC printer (#7158) blob | commitdiff | raw | diff to current
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... blob | commitdiff | raw | diff to current
2021-09-30 Gereon KremerRefactor our static builds (#7251) blob | commitdiff | raw | diff to current
2021-09-29 Andrew ReynoldsAdd the strings array solver (#7232) blob | commitdiff | raw | diff to current
2021-09-29 Gereon Kremerremove stuff (#7258) blob | commitdiff | raw | diff to current
2021-09-28 Gereon KremerRemove linking against RT (#7257) blob | commitdiff | raw | diff to current
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... blob | commitdiff | raw | diff to current
2021-09-23 Lachnitt[proofs] Alethe: Add Alethe Files to be Compiled ... blob | commitdiff | raw | diff to current
2021-09-22 Mathias PreinerRemove CVC language support (#7219) blob | commitdiff | raw | diff to current
2021-09-22 Aina Niemetzarrays: Move type enumerator implementation to .cpp... blob | commitdiff | raw | diff to current
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
next