projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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 datatype...
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 LazyCD...
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)
commit
|
commitdiff
|
tree
2020-10-06
Abdalrhman...
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
Mathias Preiner
Fix CI builds and add cancel workflow.
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::externalEx...
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
2020-09-29
Alex Ozdemir
Add utilities for arith/proof_checker and build it...
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Removing spurious forward declaration in...
commit
|
commitdiff
|
tree
2020-09-29
Haniel Barbosa
[proof-new] Adds a proof node hash function (#5154)
commit
|
commitdiff
|
tree
2020-09-29
Andrew Reynolds
Disable regression that is timing out (#5142)
commit
|
commitdiff
|
tree
2020-09-28
Andrew Reynolds
Minor fixes to quantifiers proofs (#5151)
commit
|
commitdiff
|
tree
2020-09-28
Haniel Barbosa
[proof-new] Adds a proof manager for the SAT solver...
commit
|
commitdiff
|
tree
2020-09-28
mudathirmahgoub
Implement bags rewriter (#5132)
commit
|
commitdiff
|
tree
2020-09-28
Gereon Kremer
Add new arithmetic BoundInference class (#5148)
commit
|
commitdiff
|
tree
2020-09-27
Andrew Reynolds
Fix sygus quantifier elimination preprocess for multipl...
commit
|
commitdiff
|
tree
2020-09-26
Gereon Kremer
Use inference manager for nl_solver (#5125)
commit
|
commitdiff
|
tree
2020-09-26
Andrew Reynolds
Connect the shared solver to theory engine (#5103)
commit
|
commitdiff
|
tree
2020-09-26
Andrew Reynolds
Use original quantified formula for single invocation...
commit
|
commitdiff
|
tree
2020-09-26
Aina Niemetz
Restrict bvxnor to only allow two operands (was n-ary...
commit
|
commitdiff
|
tree
2020-09-25
Andrew Reynolds
Make sygus refinement step more robust to unevaluatable...
commit
|
commitdiff
|
tree
2020-09-25
Haniel Barbosa
Cleaning and documenting cnf stream (#5134)
commit
|
commitdiff
|
tree
2020-09-24
Aina Niemetz
SyGuS: Add default grammar for FP. (#5133)
commit
|
commitdiff
|
tree
2020-09-24
Andrew Reynolds
Function definition fmf preprocessing pass (#5064)
commit
|
commitdiff
|
tree
2020-09-24
Andrew Reynolds
Modify lemma vs fact policy for datatype equalities...
commit
|
commitdiff
|
tree
2020-09-23
Andrew Reynolds
Disable cegqi-bv when using sygus (#5124)
commit
|
commitdiff
|
tree
2020-09-23
Gereon Kremer
Make IAND solver use inference manager. (#5126)
commit
|
commitdiff
|
tree
2020-09-23
Aina Niemetz
Missing format from #5112.
commit
|
commitdiff
|
tree
2020-09-23
yoni206
bv2int: new options for bvand translation (#5096)
commit
|
commitdiff
|
tree
2020-09-23
Andrew Reynolds
Allow E-matching by default when strings are enabled...
commit
|
commitdiff
|
tree
2020-09-23
Aina Niemetz
New C++ API: Catch and throw recoverable exception...
commit
|
commitdiff
|
tree
2020-09-23
Aina Niemetz
FP: Use Assert instead of AlwaysAssert in traits::...
commit
|
commitdiff
|
tree
2020-09-23
Abdalrhman...
Refactor Commands to use the Public API. (#5105)
commit
|
commitdiff
|
tree
2020-09-23
Andrew Reynolds
Fix type issue with term formula removal (#5107)
commit
|
commitdiff
|
tree
2020-09-23
Andres Noetzli
[Python API] Conversion to/from Unicode strings (#5120)
commit
|
commitdiff
|
tree
2020-09-22
Aina Niemetz
FP: Use Assert instead of PRECONDITION macro in convert...
commit
|
commitdiff
|
tree
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
commit
|
commitdiff
|
tree
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
commit
|
commitdiff
|
tree
2020-09-22
Andres Noetzli
Fix compilation without LibPoly (#5118)
commit
|
commitdiff
|
tree
2020-09-22
makaimann
Add method to get Python object from constant value...
commit
|
commitdiff
|
tree
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
commit
|
commitdiff
|
tree
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
commit
|
commitdiff
|
tree
2020-09-22
yoni206
Require dumping in a dumping test (#5108)
commit
|
commitdiff
|
tree
2020-09-21
Andrew Reynolds
(proof-new) Add the arrays proof checker (#5047)
commit
|
commitdiff
|
tree
2020-09-20
Andrew Reynolds
More flexible design for model manager distributed...
commit
|
commitdiff
|
tree
2020-09-19
Andrew Reynolds
Standardize equality engine notifications in sets ...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Fix assertion list for globally defined recursive funct...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Add the shared solver (#4982)
commit
|
commitdiff
|
tree
2020-09-18
yoni206
bv2int: quantifiers support (#5080)
commit
|
commitdiff
|
tree
2020-09-18
Andres Noetzli
Fix muzzled builds (#5093)
commit
|
commitdiff
|
tree
2020-09-18
Haniel Barbosa
[proof-new] Proof utilities for normalizing clauses...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Logic exception for arrays indexed by arrays (#5073)
commit
|
commitdiff
|
tree
2020-09-18
Andres Noetzli
[Strings] Fix extended equality rewriter (#5092)
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
(proof-new) Updates to proof node updater algorithm...
commit
|
commitdiff
|
tree
next