projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Update strings proxy variable map to be context independent (#5377)
2020-11-02
Andrew Reynolds
Update strings proxy variable map to be context independent...
commit
|
commitdiff
|
tree
2020-11-02
Andrew Reynolds
Miscellaneous cleaning of parser (#5369)
commit
|
commitdiff
|
tree
2020-11-02
Andrew Reynolds
Avoid dynamic allocation in symbol table implementation...
commit
|
commitdiff
|
tree
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
commit
|
commitdiff
|
tree
2020-10-29
Andrew Reynolds
Set strings pending conflict flag (#5364)
commit
|
commitdiff
|
tree
2020-10-29
Andrew Reynolds
(proof-new) Update the strings inference manager for...
commit
|
commitdiff
|
tree
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
commit
|
commitdiff
|
tree
2020-10-28
Andrew Reynolds
Fixes for unconstrained variables in nonlinear model...
commit
|
commitdiff
|
tree
2020-10-28
Andrew Reynolds
Convert symbol table from Expr-level to Term-level...
commit
|
commitdiff
|
tree
2020-10-28
Andrew Reynolds
Add rewrites for div/mod in the arithmetic rewriter...
commit
|
commitdiff
|
tree
2020-10-27
Andrew Reynolds
Add missing methods involving datatype sorts to the...
commit
|
commitdiff
|
tree
2020-10-26
Andrew Reynolds
(proof-new) Add datatypes proof checker (#5340)
commit
|
commitdiff
|
tree
2020-10-26
Andrew Reynolds
Send external equalities from collapse selector as...
commit
|
commitdiff
|
tree
2020-10-23
Andrew Reynolds
Apply alpha equivalence to annotated quantified formulas...
commit
|
commitdiff
|
tree
2020-10-23
Andrew Reynolds
Change datatypes lemma policy for equalities not coming...
commit
|
commitdiff
|
tree
2020-10-23
Andrew Reynolds
Fix related to preregistering boolean term variables...
commit
|
commitdiff
|
tree
2020-10-22
Andrew Reynolds
Remove unused equality engine types (#5319)
commit
|
commitdiff
|
tree
2020-10-22
Andrew Reynolds
(proof-new) Make theory preprocessor user-context dependent...
commit
|
commitdiff
|
tree
2020-10-21
Andrew Reynolds
(proof-new) Updates to lazy proof chain (#5317)
commit
|
commitdiff
|
tree
2020-10-21
Andrew Reynolds
(proof-new) Fixes for proofs in rewriter (#5307)
commit
|
commitdiff
|
tree
2020-10-20
Andrew Reynolds
(proof-new) Fix for CDProof::isSame (#5297)
commit
|
commitdiff
|
tree
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDProof...
commit
|
commitdiff
|
tree
2020-10-20
Andrew Reynolds
Fix miscellaneous warnings (#5256)
commit
|
commitdiff
|
tree
2020-10-20
Andrew Reynolds
Make seq.nth a trigger kind (#5314)
commit
|
commitdiff
|
tree
2020-10-20
Andrew Reynolds
Split CheckModels utility to its own file (#5303)
commit
|
commitdiff
|
tree
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
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
Andrew Reynolds
Add inference enumeration to datatypes (#5275)
commit
|
commitdiff
|
tree
2020-10-14
Andrew Reynolds
Guard uses of printing approximations for constants...
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-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-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-07
Andrew Reynolds
(proof-new) Add the strings proof constructor (#4903)
commit
|
commitdiff
|
tree
2020-10-07
Andrew Reynolds
Process pending inferences at the beginning of datatypes...
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
Andrew Reynolds
Add arithmetic preprocess module (#5188)
commit
|
commitdiff
|
tree
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
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
Andrew Reynolds
Decouple modules from TheoryArithPrivate (#5184)
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
(proof-new) Make arrays proof producing (#5112)
commit
|
commitdiff
|
tree
2020-10-01
Andrew Reynolds
Update theory of arithmetic to standard check (#5178)
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-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
Andrew Reynolds
(proof-new) Fixes for preprocess proof generator and...
commit
|
commitdiff
|
tree
2020-09-29
Andrew Reynolds
Reset assertions on resetAssertions (#5153)
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-27
Andrew Reynolds
Fix sygus quantifier elimination preprocess for multiple...
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-25
Andrew Reynolds
Make sygus refinement step more robust to unevaluatable...
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
Andrew Reynolds
Allow E-matching by default when strings are enabled...
commit
|
commitdiff
|
tree
2020-09-23
Andrew Reynolds
Fix type issue with term formula removal (#5107)
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 functions...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Add the shared solver (#4982)
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
Logic exception for arrays indexed by arrays (#5073)
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
(proof-new) Updates to proof node updater algorithm...
commit
|
commitdiff
|
tree
2020-09-18
Andrew Reynolds
(proof-new) Rewrites involving operators in term conversion...
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
(proof-new) Fixes for theory engine proof generator...
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
Reduce recursion in term formula removal (#5052)
commit
|
commitdiff
|
tree
2020-09-17
Andrew Reynolds
Further standardization of datatypes (#5076)
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
Add buffered inference manager to TheorySep (#5038)
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
Refactor collectModelInfo in TheoryArith (#5027)
commit
|
commitdiff
|
tree
2020-09-16
Andrew Reynolds
(proof-new) Make proofs mandatory in proof equality...
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Move sets member propagation to SolverState (#5045)
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Move quantifiers engine private to own file (#5053)
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Fix needsModel method for CEGQI (#5048)
commit
|
commitdiff
|
tree
2020-09-15
Andrew Reynolds
Standard equality engine notify class for Theory (...
commit
|
commitdiff
|
tree
2020-09-14
Andrew Reynolds
Refactoring the rewriter of sets (#4856)
commit
|
commitdiff
|
tree
2020-09-14
Andrew Reynolds
Standardize uses of inference manager in datatypes...
commit
|
commitdiff
|
tree
next