projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Eliminate more static uses of rewrite (#8040)
[cvc5.git] / src / CMakeLists.txt
2022-02-03 mudathirmahgoubAdd table.product operator (#8020) blob | commitdiff | raw
2022-02-03 Gereon KremerAdd node utils for the arithmetic rewriter (#8012) blob | commitdiff | raw | diff to current
2022-02-01 Gereon KremerAdd new ordering utility (#8008) blob | commitdiff | raw | diff to current
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) blob | commitdiff | raw | diff to current
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986) blob | commitdiff | raw | diff to current
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945) blob | commitdiff | raw | diff to current
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) blob | commitdiff | raw | diff to current
2022-01-06 Gereon KremerImprove theory combination in the presence of real... blob | commitdiff | raw | diff to current
2022-01-04 Haniel Barbosa[proofs] [sat] Add manager for optimized clauses and... blob | commitdiff | raw | diff to current
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) blob | commitdiff | raw | diff to current
2021-12-14 Abdalrhman MohamedAdd a random Sygus enumerator. (#7782) blob | commitdiff | raw | diff to current
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) blob | commitdiff | raw | diff to current
2021-12-10 Ying ShengArray-inspired Sequence Solver - Adding the ArrayCoreSo... blob | commitdiff | raw | diff to current
2021-12-07 Andrew ReynoldsAdd proof annotation option (#7750) blob | commitdiff | raw | diff to current
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) blob | commitdiff | raw | diff to current
2021-11-30 Lachnitt[proofs] Alethe: Implementation of Printer (#7674) blob | commitdiff | raw | diff to current
2021-11-30 Lachnitt[proofs] Alethe: Printer Specification (#7673) blob | commitdiff | raw | diff to current
2021-11-22 Gereon KremerRefactor IO stream manipulators (#7555) blob | commitdiff | raw | diff to current
2021-11-19 Andrew ReynoldsRemove n-ary builder (#7671) blob | commitdiff | raw | diff to current
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... blob | commitdiff | raw | diff to current
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... blob | commitdiff | raw | diff to current
2021-11-08 Andrew ReynoldsAdd lambda lift utility (#7601) blob | commitdiff | raw | diff to current
2021-11-08 Haniel Barbosa[proofs] Adding NoSubtype node converter to Alethe... blob | commitdiff | raw | diff to current
2021-11-05 Andrew ReynoldsMove functions and lambdas from builtin to uf (#7570) blob | commitdiff | raw | diff to current
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) blob | commitdiff | raw | diff to current
2021-11-04 Gereon KremerRefactor cmake to build either static or shared (#7534) blob | commitdiff | raw | diff to current
2021-11-01 Mathias Preinerbv: Remove layered solver. (#7455) blob | commitdiff | raw | diff to current
2021-11-01 Gereon KremerRefactor DidYouMean (#7535) blob | commitdiff | raw | diff to current
2021-10-29 Andrew ReynoldsAdd PfRule ARITH_POLY_NORM (#7501) blob | commitdiff | raw | diff to current
2021-10-28 Gereon KremerCombine `--static` and `--static-binary` (#7520) blob | commitdiff | raw | diff to current
2021-10-26 Gereon KremerFix frequent rebuild of options target (#7450) blob | commitdiff | raw | diff to current
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... blob | commitdiff | raw | diff to current
2021-10-21 Gereon KremerWorking on windows builds (#7381) blob | commitdiff | raw | diff to current
2021-10-20 Andrew ReynoldsReimplement support for relational triggers (#7063) blob | commitdiff | raw | diff to current
2021-10-20 Andrew ReynoldsAdd basic regular expression type enumerator (#7416) blob | commitdiff | raw | diff to current
2021-10-14 Andrew ReynoldsSplit entailment check from term database (#7342) blob | commitdiff | raw | diff to current
2021-10-14 Gereon KremerFix GLPK linking (#7357) blob | commitdiff | raw | diff to current
2021-10-12 Aina NiemetzRename SmtEngineState to SolverEngineState. (#7344) blob | commitdiff | raw | diff to current
2021-10-12 Gereon KremerFix glpk, add antlr.so (#7341) blob | commitdiff | raw | diff to current
2021-10-11 Aina NiemetzRename SmtEngineStatistics to SolverEngineStatistics... blob | commitdiff | raw | diff to current
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
next