projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Minor cleaning of instantiation utilities (#7334)
[cvc5.git]
/
src
/
CMakeLists.txt
2021-10-11
Aina Niemetz
Rename SmtEngineStatistics to SolverEngineStatistics...
blob
|
commitdiff
|
raw
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
blob
|
commitdiff
|
raw
|
diff to current
2021-10-11
Gereon Kremer
Revert #7257 (#7337)
blob
|
commitdiff
|
raw
|
diff to current
2021-10-11
Gereon Kremer
Restore compatibility with cmake 3.9 (#7329)
blob
|
commitdiff
|
raw
|
diff to current
2021-10-07
Gereon Kremer
Add new versioning scheme (#7253)
blob
|
commitdiff
|
raw
|
diff to current
2021-10-07
Gereon Kremer
Fix/Improve static and shared builds with CLN or Poly...
blob
|
commitdiff
|
raw
|
diff to current
2021-10-01
Andrew Reynolds
Add the LFSC printer (#7158)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-30
Aina Niemetz
Rename files smt_engine.(cpp|h) to solver_engine.(cpp...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-30
Gereon Kremer
Refactor our static builds (#7251)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-29
Andrew Reynolds
Add the strings array solver (#7232)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-29
Gereon Kremer
remove stuff (#7258)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-28
Gereon Kremer
Remove linking against RT (#7257)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-23
Gereon Kremer
Eliminate 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 Preiner
Remove CVC language support (#7219)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-22
Aina Niemetz
arrays: Move type enumerator implementation to .cpp...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-22
Gereon Kremer
Eliminate 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 Reynolds
Add the LFSC proof post-processor (#7134)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-14
Mathias Preiner
proofs: Properly track pre- and post-rewrites in bbAtom...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-13
Aina Niemetz
FP: Rename FpConverter to FpWordBlaster. (#7170)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-13
Gereon Kremer
Add main options to cmake (#7178)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-09
Andrew Reynolds
Add difficulty manager (#7151)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-09
Andrew Reynolds
Add difficulty post-processor (#7150)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-08
Andrew Reynolds
Add Lfsc print channel utilities (#7123)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-08
Andrew Reynolds
Improve pre-skolemization, move quantifiers preprocess...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-08
Andrew Reynolds
Add LFSC side condition conversion utility for list...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-02
Andrew Reynolds
Add LFSC node converter (#6944)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-02
Aina Niemetz
Add class EnvObj. (#7113)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-30
Andrew Reynolds
Fix proof equality engine for "no-explain" premises...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-24
Andrew Reynolds
Split higher-order term database (#7045)
blob
|
commitdiff
|
raw
|
diff to current
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
next