projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
(proof-new) Updates to assertions pipeline and preprocess generator (#5300)
2020-10-19
Andrew Reynolds
(proof-new) Updates to assertions pipeline and preprocess...
commit
|
commitdiff
|
tree
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proofs...
commit
|
commitdiff
|
tree
2020-10-19
Haniel Barbosa
[proof-new] Improving cycle checking in lazycdproofchain...
commit
|
commitdiff
|
tree
2020-10-19
Andrew Reynolds
Safer version of pending lemma processing in inference...
commit
|
commitdiff
|
tree
2020-10-19
Andrew Reynolds
(proof-new) Refactoring cyclic checks (#5291)
commit
|
commitdiff
|
tree
2020-10-18
Andrew Reynolds
(proof-new) Witness axiom reconstruction for purification...
commit
|
commitdiff
|
tree
2020-10-18
Andrew Reynolds
(proof-new) Implementation of trust substitution (...
commit
|
commitdiff
|
tree
2020-10-18
Andrew Reynolds
(proof-new) More features for SMT proof post-processor...
commit
|
commitdiff
|
tree
2020-10-18
Andrew Reynolds
(proof-new) Improvements for theory engine (#5292)
commit
|
commitdiff
|
tree
2020-10-16
Andrew Reynolds
Refactor SMT-level model object (#5277)
commit
|
commitdiff
|
tree
2020-10-16
Andrew Reynolds
Catch more cases of nested recursion in datatypes ...
commit
|
commitdiff
|
tree
2020-10-16
yoni206
bv2int: caching introduced terms (#5283)
commit
|
commitdiff
|
tree
2020-10-16
Andrew Reynolds
Add inference enumeration to datatypes (#5275)
commit
|
commitdiff
|
tree
2020-10-15
Alex Ozdemir
(proof-new) TheoryArithPrivate: farkas lemma proof...
commit
|
commitdiff
|
tree
2020-10-14
mudathirmahgoub
Fix issue #5269 (#5270)
commit
|
commitdiff
|
tree
2020-10-14
yoni206
bv2int: implementing the iand-sum mode (#5265)
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) debug statements & docs for INT_TRUST ...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) pfs in TheoryArith(Private) explainations...
commit
|
commitdiff
|
tree
2020-10-14
Andrew Reynolds
Guard uses of printing approximations for constants...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) pfs for conflicts in TheoryArithPrivate...
commit
|
commitdiff
|
tree
2020-10-14
yoni206
bv2int: rewritings and unsat cores (#5263)
commit
|
commitdiff
|
tree
2020-10-14
Haniel Barbosa
using NOT_NOT_ELIM rather than macros to do double...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) Prove lemmas in Constraint (#5254)
commit
|
commitdiff
|
tree
2020-10-14
Andrew Reynolds
(proof-new) Generalize preprocess proof generator ...
commit
|
commitdiff
|
tree
2020-10-14
Andrew Reynolds
(proof-new) Simplifications for proof rule checker...
commit
|
commitdiff
|
tree
2020-10-14
Andrew Reynolds
(proof-new) Miscellaneous minor improvements and fixes...
commit
|
commitdiff
|
tree
2020-10-13
Andrew Reynolds
(proof-new) New rules for Booleans (#5243)
commit
|
commitdiff
|
tree
2020-10-13
Andrew Reynolds
(proof-new) Change merge policy for proof node updater...
commit
|
commitdiff
|
tree
2020-10-13
yoni206
bv2int: improving bvand tables (#5235)
commit
|
commitdiff
|
tree
2020-10-12
Andrew Reynolds
Remove uf-ss-totality option (#5251)
commit
|
commitdiff
|
tree
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
commit
|
commitdiff
|
tree
2020-10-12
Andrew Reynolds
Ensure uninterpreted sort owner is UF if uf-ho or finite...
commit
|
commitdiff
|
tree
2020-10-11
Mathias Preiner
SyGuS instantiation modes (#5228)
commit
|
commitdiff
|
tree
2020-10-11
Gereon Kremer
Add conversion of poly polynomial to cvc node. (#5218)
commit
|
commitdiff
|
tree
2020-10-10
Abdalrhman Mohamed
Provide API version of some SMT Commands. (#5222)
commit
|
commitdiff
|
tree
2020-10-10
yoni206
bv2int: bvand translation code move (#5227)
commit
|
commitdiff
|
tree
2020-10-09
Mathias Preiner
Remove deprecated add-path commands and use $GITHUB_PATH...
...deprecated add-path commands and use $
GITHUB
_PATH instead. (#5232)
commit
|
commitdiff
|
tree
2020-10-09
Alex Ozdemir
use right arith explanation fn to fix regressions ...
commit
|
commitdiff
|
tree
2020-10-09
Alex Ozdemir
(proof-new) proofs for arith-constraint explanations...
commit
|
commitdiff
|
tree
2020-10-09
Andres Noetzli
reset-assertions: Remove all non-global symbols in...
commit
|
commitdiff
|
tree
2020-10-09
Andrew Reynolds
Simplify approach for collapsed selectors over non...
commit
|
commitdiff
|
tree
2020-10-09
Andrew Reynolds
(proof-new) Add lazy proof set utility (#5221)
commit
|
commitdiff
|
tree
2020-10-09
Andrew Reynolds
(proof-new) Theory engine proof producing (#5195)
commit
|
commitdiff
|
tree
2020-10-08
Andrew Reynolds
(proof-new) Fixes and improvements for smt proof postprocess...
commit
|
commitdiff
|
tree
2020-10-08
makaimann
Get correct NodeManagerScope for toStrings in API ...
commit
|
commitdiff
|
tree
2020-10-08
yoni206
fix unit failures on debug without symfpu (#5212)
commit
|
commitdiff
|
tree
2020-10-07
Alex Ozdemir
(proof-new) proofs in ee -> arith pipeline (#5215)
commit
|
commitdiff
|
tree
2020-10-07
Aina Niemetz
New C++ API: Rename Term::isConst() to Term::isValue...
commit
|
commitdiff
|
tree
2020-10-07
Gereon Kremer
Make sure conflicts are not rewritten (in arithmetic...
commit
|
commitdiff
|
tree
2020-10-07
Andrew Reynolds
(proof-new) Add the strings proof constructor (#4903)
commit
|
commitdiff
|
tree
2020-10-07
Malte Mues
Improve OSX support by adding os detection and adapting...
commit
|
commitdiff
|
tree
2020-10-07
Andrew Reynolds
Process pending inferences at the beginning of datatypes...
commit
|
commitdiff
|
tree
2020-10-06
yoni206
bv-to-int: change order of passes (#5208)
commit
|
commitdiff
|
tree
2020-10-06
Alex Ozdemir
(proof-new) proofs for ArithCongMan -> ee facts (#5207)
commit
|
commitdiff
|
tree
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
commit
|
commitdiff
|
tree
2020-10-06
Andrew Reynolds
(proof-new) Allow null proofs from generators in LazyCDProof...
commit
|
commitdiff
|
tree
2020-10-06
mudathirmahgoub
Add operators bag.from_set, bag.to_set to the theory...
commit
|
commitdiff
|
tree
2020-10-06
Andrew Reynolds
Add arithmetic preprocess module (#5188)
...strings preprocess module (https://
github
.com/CVC4/CVC4/blob/master/src...
commit
|
commitdiff
|
tree
2020-10-06
Abdalrhman Mohamed
Recover from some exceptions. (#5203)
commit
|
commitdiff
|
tree
2020-10-06
mudathirmahgoub
Remove subtyping for sets (#5205)
commit
|
commitdiff
|
tree
2020-10-05
Aina Niemetz
cmake: Add warning when unit testing is disabled due...
commit
|
commitdiff
|
tree
2020-10-05
Aina Niemetz
SyGuS: Add fp.sub to default FP grammar. (#5206)
commit
|
commitdiff
|
tree
2020-10-05
Aina Niemetz
Integer: GMP: Move implementation of member functions...
commit
|
commitdiff
|
tree
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
commit
|
commitdiff
|
tree
2020-10-04
mudathirmahgoub
Remove subtyping for sets theory (#5179)
commit
|
commitdiff
|
tree
2020-10-03
Aina Niemetz
sygus-inst: Add more special BV values. (#5191)
commit
|
commitdiff
|
tree
2020-10-03
Andrew Reynolds
Fix theory white unit test (#5194)
commit
|
commitdiff
|
tree
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
commit
|
commitdiff
|
tree
2020-10-02
Andrew Reynolds
Minor simplifications to substitution map class (#5180)
commit
|
commitdiff
|
tree
2020-10-02
Andrew Reynolds
(proof-new) Fixes for theory preprocessing proofs ...
commit
|
commitdiff
|
tree
2020-10-02
Andrew Reynolds
(proof-new) Make shared solver proof producing (#5169)
commit
|
commitdiff
|
tree
2020-10-02
Gereon Kremer
Allow for theory combination of strings with nonlinear...
commit
|
commitdiff
|
tree
2020-10-02
Andrew Reynolds
Decouple modules from TheoryArithPrivate (#5184)
commit
|
commitdiff
|
tree
2020-10-02
Alex Ozdemir
(proof-new) New proofs in arith::Constraint::externalExplain...
commit
|
commitdiff
|
tree
2020-10-02
Alex Ozdemir
Remove duplicate declarations in th_bv.plf (#5183)
commit
|
commitdiff
|
tree
2020-10-02
Aina Niemetz
SyGuS: Add min/max (sub)normal constants to FP default...
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
(proof-new) Make arrays proof producing (#5112)
commit
|
commitdiff
|
tree
2020-10-01
Mathias Preiner
Add additional ground terms to SyGuS instantiation...
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
Update theory of arithmetic to standard check (#5178)
commit
|
commitdiff
|
tree
2020-10-01
Aina Niemetz
FloatingPoint: Add utility functions for largest and...
commit
|
commitdiff
|
tree
2020-10-01
Gereon Kremer
Allow to use the initial assignment for CAD (#5177)
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
(proof-new) Preprocessing passes use proper interfaces...
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
Make SygusSolver use sygus attributes directly (#5172)
commit
|
commitdiff
|
tree
2020-10-01
Mathias Preiner
Add GH action to cancel previous pending/running CI...
commit
|
commitdiff
|
tree
2020-10-01
Aina Niemetz
BitVector: Extend interface of setBit to set it to...
commit
|
commitdiff
|
tree
2020-09-30
Aina Niemetz
FloatingPoint: Add utility functions for largest and...
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Remove too strict assertion to allow for approximate...
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Add missing includes. (#5170)
commit
|
commitdiff
|
tree
2020-09-30
Gereon Kremer
Add strategy for nonlinear extension (#5160)
commit
|
commitdiff
|
tree
2020-09-30
Andrew Reynolds
Dynamic allocation of equality engine for shared solver...
commit
|
commitdiff
|
tree
2020-09-30
Andrew Reynolds
(proof-new) Add the term conversion sequence generator...
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof manager for prop engine (...
commit
|
commitdiff
|
tree
2020-09-29
mudathirmahgoub
Fix bags headers (#5165)
commit
|
commitdiff
|
tree
2020-09-29
Alex Ozdemir
(proof-new) Add proof managers and eager gens to arith...
commit
|
commitdiff
|
tree
2020-09-29
Andrew Reynolds
(proof-new) Fixes for preprocess proof generator and...
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof post processor for the Prop...
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Updates to proof node updater (#5156)
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof-producing CNF converter (...
commit
|
commitdiff
|
tree
2020-09-29
Gereon Kremer
Clean up nonlinear extension (#5149)
commit
|
commitdiff
|
tree
2020-09-29
Andrew Reynolds
Reset assertions on resetAssertions (#5153)
commit
|
commitdiff
|
tree
next