projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Split higher-order term database (#7045)
[cvc5.git]
/
src
/
CMakeLists.txt
2021-08-24
Andrew Reynolds
Split higher-order term database (#7045)
blob
|
commitdiff
|
raw
2021-08-24
Andrew Reynolds
Refactor enumerator management in synth conjecture...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-22
Andrew Reynolds
Simplify model printing modes (#7049)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-19
Andrew Reynolds
Split proof final callback to its own file (#6984)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-17
Andrew Reynolds
Initial refactoring of set defaults (#7021)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-09
Andres Noetzli
Support older CMake versions (#7003)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-06
Gereon Kremer
Merge options cmake into general cmake file (#6989)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-04
Gereon Kremer
Refactor managed streams (#6934)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-27
Andrew Reynolds
Add basic LFSC utilities (#6879)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-27
Andrew Reynolds
Move enum value generator to own file (#6941)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-27
Andrew Reynolds
Add proof letify utility (#6881)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-27
Andrew Reynolds
Add sygus enumerator callback (#6923)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-22
Andrew Reynolds
Add the central equality engine manager (#6893)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-15
Andrew Reynolds
Connect the equality solver to theory arith (#6894)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-15
Andrew Reynolds
Move master equality engine notification to own file...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-15
Mathias Preiner
bv: Rename BBSimple to NodeBitblaster. (#6891)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-15
Mathias Preiner
bv: Rename lazy solver to layered solver. (#6889)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-15
Mathias Preiner
bv: Rename simple solver to bitblast-internal. (#6888)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-14
Andrew Reynolds
Move synthesis verification check to own file (#6882)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-12
Andrew Reynolds
Add branch and bound (#6865)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-12
Andrew Reynolds
Add arithmetic preprocess rewrite equality module ...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-06
Gereon Kremer
Integrate Lazard into CAD module (#6812)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-06
Andrew Reynolds
Integrate learned rewrite preprocessing pass (#6840)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-22
yoni206
modular bv2int: Stubs and some implementations (#6760)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-21
Mathias Preiner
Make CaDiCaL a required dependency. (#6761)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-16
Aina Niemetz
Make symfpu a required dependency. (#6749)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-15
yoni206
pow2: adding a kind, inference rules, and some implemen...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-11
Gereon Kremer
Add skeleton for new Lazard evaluation (#6732)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-08
Andrew Reynolds
Add learned literal manager utility (#6709)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-04
yoni206
pow2: header file for pow2 solver (#6676)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andrew Reynolds
Update proof namespaces (#6614)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-24
Andrew Reynolds
Implementation of the new justification heuristic ...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-18
Abdalrhman Mohamed
Loop over terms to reconstruct instead of obligations...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-05
Andrew Reynolds
Move current decision engine to decision engine old...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-30
Andrew Reynolds
Use substitutions for implementing defined functions...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-29
Andrew Reynolds
Add assertion list utility for justification heuristic...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-27
Aina Niemetz
Bool: Move implementation of type rules to cpp. (#6420)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-23
Andrew Reynolds
Move implementation of UF rewriter to cpp (#6393)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Aina Niemetz
Arithmetic: Move implementation of type rules to cpp...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Aina Niemetz
UF: Move implementation of type rules to cpp. (#6403)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Aina Niemetz
Datatypes: Move implementation of type rules to cpp...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Aina Niemetz
Sets: Move implementation of type rules to cpp. (#6401)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Aina Niemetz
Arrays: Move implementation of type rules to cpp. ...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Andrew Reynolds
Add basic utilities for new implementation of justifica...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Andrew Reynolds
Split FP expand definitions to own module (#6392)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Aina Niemetz
BV: Move implementation of type rules from header to...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Aina Niemetz
Sep: Move implementation of type rules to cpp. (#6402)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Aina Niemetz
Quantifiers: Move implementation of type rules to cpp...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Andrew Reynolds
Add instantiation pool feature to the API (#6358)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-19
Andrew Reynolds
Fully incorporate quantifiers macros into ppAssert...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-16
Mathias Preiner
cmake: Build object libraries for base and context...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-15
Mathias Preiner
Build support library from base and context. (#6368)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-13
Andrew Reynolds
Add pool instantiation strategy (#6308)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Strings: Move implementation of type rules from header...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-07
Aina Niemetz
New C++ Api: Rename and move checks.h. (#6306)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-07
Andrew Reynolds
Add term pools utility (#6243)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-06
Aina Niemetz
New C++ Api: Rename and move headers. (#6292)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-05
Yancheng Ou
Optimizer for BitVectors (#6213)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Gereon Kremer
Refactor CLN dependency & Cleanup (#6251)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Gereon Kremer
Refactor GMP and Poly dependencies (#6245)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Gereon Kremer
Refactor dependencies for external SAT solvers (#6215)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Gereon Kremer
Refactor SymFPU dependency (#6218)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
Bags: Move implementation of type rules from header...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
FP: Move implementation of type rules from header to...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-29
yoni206
Modular bv2int part 1 (#6212)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-25
Andrew Reynolds
Refactor construction of triggers (#6209)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Haniel Barbosa
Removing unused build options and deprecated proof...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Abdalrhman Mohamed
Replace old sygus term reconstruction algorithm with...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-22
Andrew Reynolds
Add skolem definition manager (#6187)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-17
Andrew Reynolds
Move utilities for inferred bounds on quantifers to...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-15
Andrew Reynolds
Split 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 Niemetz
New C++ Api: Move checks to separate file. (#6138)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-12
Mathias Preiner
cmake: Remove install rules for old API headers. (...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-11
MikolasJanota
Improvements 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 Reynolds
Add Env class (#6093)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Andrew Reynolds
Remove logic request (#6089)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Aina Niemetz
Update 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
mcjuneho
Initial implementation of an optimization solver with...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-04
Aina Niemetz
Add initial bit-blaster for proof logging. (#6053)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-03
mudathirmahgoub
Add tuple projection operator (#5904)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-02
Andrew Reynolds
Introduce quantifiers term registry (#5983)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-27
Aina Niemetz
google 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 Kremer
Add the LazyTreeProofGenerator. (#5948)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-19
Gereon Kremer
Cleanup of inferences in arithmetic theory (#5927)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-18
Andrew Reynolds
Move first order model for full model check to own...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-13
Andrew Reynolds
Moving methods from quantifiers engine to quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
blob
|
commitdiff
|
raw
|
diff to current
next