projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Set incomplete if not applying ho extensionality (#6281)
[cvc5.git]
/
src
/
2021-04-07
Andrew Reynolds
Set incomplete if not applying ho extensionality (...
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Fixes for abducts (#6279)
tree
|
commitdiff
2021-04-07
Aina Niemetz
New C++ Api: Rename and move checks.h. (#6306)
tree
|
commitdiff
2021-04-07
Andrew Reynolds
(proof-new) Proper implementation of proof node cloning...
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Add term pools utility (#6243)
tree
|
commitdiff
2021-04-07
Aina Niemetz
New C++ Api: Initial setup of Api documentation. (...
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-07
Mathias Preiner
cmake: Do not always regenerate cvc4kinds.{pxi,pxd...
tree
|
commitdiff
2021-04-06
Mathias Preiner
cmake: Add helper to check if a given Python module...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
tree
|
commitdiff
2021-04-06
Andrew Reynolds
Fix tptp parser for negative rational (#6297)
tree
|
commitdiff
2021-04-06
Andrew Reynolds
Fix issue with lemma during equality engine iterator...
tree
|
commitdiff
2021-04-06
Mathias Preiner
genkinds: Do not use relative paths to find src directo...
tree
|
commitdiff
2021-04-06
Andrew Reynolds
Remove stdPrintAscii option (#6280)
tree
|
commitdiff
2021-04-06
Aina Niemetz
New C++ Api: Rename and move headers. (#6292)
tree
|
commitdiff
2021-04-06
Mathias Preiner
parsekinds: Remove DEFAULT_HEADER. (#6294)
tree
|
commitdiff
2021-04-05
mudathirmahgoub
Add documentation for theory_bags_type_rules.h (#6268)
tree
|
commitdiff
2021-04-05
Andrew Reynolds
Fix spurious antecedant for symbolic regular expression...
tree
|
commitdiff
2021-04-05
Haniel Barbosa
[proof-new] Registering proof checkers uniformly from...
tree
|
commitdiff
2021-04-05
Andrew Reynolds
Enable UF when pre-skolem nested option is enabled...
tree
|
commitdiff
2021-04-05
NicolaasWeideman
python: Fix type casting in mkBitVector (#6261)
tree
|
commitdiff
2021-04-05
Andrew Reynolds
Fix subtyping for sets care graph (#6278)
tree
|
commitdiff
2021-04-05
Andrew Reynolds
Add interface for skolem functions in SkolemManager...
tree
|
commitdiff
2021-04-05
Yancheng Ou
Optimizer for BitVectors (#6213)
tree
|
commitdiff
2021-04-03
Andrew Reynolds
Disable substring component contains in strip endpoints...
tree
|
commitdiff
2021-04-02
Mathias Preiner
cmake: Do not link against main object library. (#6269)
tree
|
commitdiff
2021-04-02
Gereon Kremer
New statistics registry (#6210)
tree
|
commitdiff
2021-04-02
Gereon Kremer
Minor refactoring (#6273)
tree
|
commitdiff
2021-04-02
Andrew Reynolds
Cleaning up friend relationships for commands (#6254)
tree
|
commitdiff
2021-04-02
Andrew Reynolds
Fix case where RE unfolding generates a trivially true...
tree
|
commitdiff
2021-04-01
Gereon Kremer
Add utility classes for new statistics (#6178)
tree
|
commitdiff
2021-04-01
Andrew Reynolds
Simplify caching of regular expression unfolding (...
tree
|
commitdiff
2021-04-01
Aina Niemetz
FP: Factor out symfpu traits. (#6246)
tree
|
commitdiff
2021-04-01
Andrew Reynolds
Fix type rule for to_real (#6257)
tree
|
commitdiff
2021-04-01
Gereon Kremer
Refactor CLN dependency & Cleanup (#6251)
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-04-01
Aina Niemetz
kinds: Remove non-existent properties. (#6253)
tree
|
commitdiff
2021-04-01
Andrew Reynolds
Add debug traces to theory inference manager (#6250)
tree
|
commitdiff
2021-04-01
Andrew Reynolds
Fix non-linear for unknown case (#6252)
tree
|
commitdiff
2021-04-01
Gereon Kremer
Make ResetCommand go through APISolver (#6172)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-31
Gereon Kremer
Refactor GMP and Poly dependencies (#6245)
tree
|
commitdiff
2021-03-31
Gereon Kremer
Refactor dependencies for external SAT solvers (#6215)
tree
|
commitdiff
2021-03-31
Gereon Kremer
Refactor SymFPU dependency (#6218)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Bags: Move implementation of type rules from header...
tree
|
commitdiff
2021-03-31
Andrew Reynolds
Eliminate dependencies on quantifiers engine in interna...
tree
|
commitdiff
2021-03-31
Andrew Reynolds
Add missing inference ids (#6242)
tree
|
commitdiff
2021-03-31
Aina Niemetz
FP: Move implementation of type rules from header to...
tree
|
commitdiff
2021-03-31
yoni206
Fix compilation of Python bindings for named build...
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Fix printing for double patterns (#6235)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Make SEXPR simply typed (#6160)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Implement simple tracking of instantiation lemmas ...
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Refactoring quantifier annotation kinds, add kinds...
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Eliminate use of rational from tptp parser (#6239)
tree
|
commitdiff
2021-03-30
Abdalrhman Mohamed
Give a better error when sygus grammar rules contain...
tree
|
commitdiff
2021-03-30
Gereon Kremer
Fix total time statistic (#6233)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Miscellaneous elimination of dependencies on quantifier...
tree
|
commitdiff
2021-03-29
Andrew Reynolds
Eliminate the use of quantifiers engine in sygus solver...
tree
|
commitdiff
2021-03-29
Andrew Reynolds
Eliminate use of quantifiers engine in enumerative...
tree
|
commitdiff
2021-03-29
Andrew Reynolds
Move decision manager into theory inference manager...
tree
|
commitdiff
2021-03-29
yoni206
Modular bv2int part 1 (#6212)
tree
|
commitdiff
2021-03-29
Aina Niemetz
FloatingPointLiteral: Constructor for special consts...
tree
|
commitdiff
2021-03-27
Gereon Kremer
Refactor ANTLR3 dependency (#6202)
tree
|
commitdiff
2021-03-26
Aina Niemetz
FloatingPointLiteral: Make constructors that shouldn...
tree
|
commitdiff
2021-03-26
Andrew Reynolds
Pass term registry to quantifiers modules (#6216)
tree
|
commitdiff
2021-03-25
Gereon Kremer
Ensure nonlinear extensions properly reconsiders its...
tree
|
commitdiff
2021-03-25
Aina Niemetz
FP: Refactor FloatingPointLiteral in preparation for...
tree
|
commitdiff
2021-03-25
Andrew Reynolds
Refactor construction of triggers (#6209)
tree
|
commitdiff
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
tree
|
commitdiff
2021-03-24
Andrew Reynolds
Use inference manager to access intantiate utility...
tree
|
commitdiff
2021-03-24
Gereon Kremer
Only consider relevant terms for integer branches ...
tree
|
commitdiff
2021-03-23
Andrew Reynolds
Remove unused code for axioms (#6197)
tree
|
commitdiff
2021-03-23
Haniel Barbosa
Removing unused build options and deprecated proof...
tree
|
commitdiff
2021-03-23
Andrew Reynolds
Passing term registry to ematching utilities (#6190)
tree
|
commitdiff
2021-03-23
Aina Niemetz
Remove internal includes of Api header. (#6193)
tree
|
commitdiff
2021-03-23
Abdalrhman Mohamed
Replace old sygus term reconstruction algorithm with...
tree
|
commitdiff
2021-03-23
Andrew Reynolds
Moving instantiate and skolemize into quantifiers infer...
tree
|
commitdiff
2021-03-22
Gereon Kremer
Move statistics from the driver into the SmtEngine...
tree
|
commitdiff
2021-03-22
Andrew Reynolds
Move equality query utility into quantifiers model...
tree
|
commitdiff
2021-03-22
Andrew Reynolds
Function types are always first-class (#6167)
tree
|
commitdiff
2021-03-22
Andrew Reynolds
Add skolem definition manager (#6187)
tree
|
commitdiff
2021-03-22
Aina Niemetz
FP: Add documentation for FloatingPointLiteral construc...
tree
|
commitdiff
2021-03-22
Andrew Reynolds
Guard for non-unique skolems in term formula removal...
tree
|
commitdiff
2021-03-21
Andrew Reynolds
Simplify strings term registration (#6174)
tree
|
commitdiff
2021-03-21
Andrew Reynolds
Clean up remaining raw uses of output channel (#6161)
tree
|
commitdiff
2021-03-20
Andrew Reynolds
Improved tracing for equivalence classes of EE (#6169)
tree
|
commitdiff
2021-03-20
mudathirmahgoub
Generate cvc/Kind.java for the java API (#6143)
tree
|
commitdiff
2021-03-19
Andrew Reynolds
Refactor initialization of quantifiers model and builde...
tree
|
commitdiff
2021-03-19
Aina Niemetz
BitVector: Change setBit to set the bit in place. ...
tree
|
commitdiff
2021-03-19
Aina Niemetz
FP: Use setBit instead of bv or in conversion from...
tree
|
commitdiff
2021-03-18
Haniel Barbosa
When giving an SMT-LIB version, defaulting to SMT-LIB...
tree
|
commitdiff
2021-03-18
Gereon Kremer
Move stats registry to env. (#6173)
tree
|
commitdiff
2021-03-18
Andrew Reynolds
Eliminate dependency on quantifiers engine in quantifie...
tree
|
commitdiff
2021-03-18
Abdalrhman Mohamed
Eliminate more uses of SExpr. (#6149)
tree
|
commitdiff
2021-03-18
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
tree
|
commitdiff
2021-03-17
Andrew Reynolds
(proof-new) Fixes to set defaults (#6163)
tree
|
commitdiff
2021-03-17
Andrew Reynolds
Move utilities for inferred bounds on quantifers to...
tree
|
commitdiff
2021-03-17
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
tree
|
commitdiff
2021-03-16
Mathias Preiner
ci: Enable checking of proofs + unsat cores. (#6088)
tree
|
commitdiff
2021-03-16
Haniel Barbosa
[proof-new] Activating proofs when dumping proofs ...
tree
|
commitdiff
next