projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Split sygus template inference to its own file (#5388)
[cvc5.git]
/
src
/
2020-11-06
Andrew Reynolds
Split sygus template inference to its own file (#5388)
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
tree
|
commitdiff
2020-11-05
mudathirmahgoub
Remove mkSingleton from the API (#5366)
tree
|
commitdiff
2020-11-04
Andres Noetzli
Add constants from equality engine evaluation to model...
tree
|
commitdiff
2020-11-03
Andrew Reynolds
Add scope methods constructing types in API (#5393)
tree
|
commitdiff
2020-11-03
Andres Noetzli
Add support for printing `re.loop` and `re.^` (#5392)
tree
|
commitdiff
2020-11-03
Andrew Reynolds
Reset built model flag at presolve in nonlinear (#5386)
tree
|
commitdiff
2020-11-03
Andrew Reynolds
Move sygus qe preproc to its own file (#5375)
tree
|
commitdiff
2020-11-02
Andrew Reynolds
Update strings proxy variable map to be context indepen...
tree
|
commitdiff
2020-11-02
Andrew Reynolds
Miscellaneous cleaning of parser (#5369)
tree
|
commitdiff
2020-11-02
Andrew Reynolds
Avoid dynamic allocation in symbol table implementation...
tree
|
commitdiff
2020-10-30
Gereon Kremer
Use BoundInference in nonlinear extension (#5359)
tree
|
commitdiff
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
tree
|
commitdiff
2020-10-29
Andrew Reynolds
Set strings pending conflict flag (#5364)
tree
|
commitdiff
2020-10-29
mudathirmahgoub
Add mkInteger to the API (#5274)
tree
|
commitdiff
2020-10-29
Andrew Reynolds
(proof-new) Update the strings inference manager for...
tree
|
commitdiff
2020-10-29
Gereon Kremer
Add NodeManager::mkOr() (#5360)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Fixes for unconstrained variables in nonlinear model...
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Convert symbol table from Expr-level to Term-level...
tree
|
commitdiff
2020-10-28
Gereon Kremer
Split NlSolver in multiple subsolvers (#5315)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Add rewrites for div/mod in the arithmetic rewriter...
tree
|
commitdiff
2020-10-27
Abdalrhman Mohamed
Refactor DeclareSygusVarCommand and SynthFunCommand...
tree
|
commitdiff
2020-10-27
Andrew Reynolds
Add missing methods involving datatype sorts to the...
tree
|
commitdiff
2020-10-27
Gereon Kremer
Disable --nl-cad option by default (#5350)
tree
|
commitdiff
2020-10-27
Gereon Kremer
Enable --nl-cad by default (#5345)
tree
|
commitdiff
2020-10-27
mudathirmahgoub
Add DUPICATE_REMOVAL operator to bags (#5336)
tree
|
commitdiff
2020-10-26
Andrew Reynolds
(proof-new) Add datatypes proof checker (#5340)
tree
|
commitdiff
2020-10-26
Andrew Reynolds
Send external equalities from collapse selector as...
tree
|
commitdiff
2020-10-24
mudathirmahgoub
Fix issue 5271 (#5335)
tree
|
commitdiff
2020-10-24
Haniel Barbosa
[proof-new] Fix n-ary kind handling in EqEngine explana...
tree
|
commitdiff
2020-10-23
Andrew Reynolds
Apply alpha equivalence to annotated quantified formula...
tree
|
commitdiff
2020-10-23
Andrew Reynolds
Change datatypes lemma policy for equalities not coming...
tree
|
commitdiff
2020-10-23
Andrew Reynolds
Fix related to preregistering boolean term variables...
tree
|
commitdiff
2020-10-22
Gereon Kremer
Use theoryof-mode=type for QF_NRA (#5326)
tree
|
commitdiff
2020-10-22
Andrew Reynolds
Remove unused equality engine types (#5319)
tree
|
commitdiff
2020-10-22
mudathirmahgoub
Fix issue 5309 (#5327)
tree
|
commitdiff
2020-10-22
Andrew Reynolds
(proof-new) Make theory preprocessor user-context depen...
tree
|
commitdiff
2020-10-21
Gereon Kremer
(proof-new) Make circuit propagator proof producing...
tree
|
commitdiff
2020-10-21
mudathirmahgoub
Implement bags evaluator (#5322)
tree
|
commitdiff
2020-10-21
Alex Ozdemir
(proof-new) Add arith proof macros file to CMake (...
tree
|
commitdiff
2020-10-21
Alex Ozdemir
(proof-new) arith: dedup literals in flattenImpl (...
tree
|
commitdiff
2020-10-21
Andrew Reynolds
(proof-new) Updates to lazy proof chain (#5317)
tree
|
commitdiff
2020-10-21
mudathirmahgoub
Add operator MakeBagOp for constructing bags (#5209)
tree
|
commitdiff
2020-10-21
Abdalrhman Mohamed
Add finishInit for getInterpol and getAbduct. (#5316)
tree
|
commitdiff
2020-10-21
Andrew Reynolds
(proof-new) Fixes for proofs in rewriter (#5307)
tree
|
commitdiff
2020-10-20
Aina Niemetz
Fix compiler warnings. (#5305)
tree
|
commitdiff
2020-10-20
Gereon Kremer
(proof-new) Add proofs for circuit propagator (#5301)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Fix for CDProof::isSame (#5297)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-20
Abdalrhman Mohamed
Remove some Commands from the API. (#5268)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Fix miscellaneous warnings (#5256)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Make seq.nth a trigger kind (#5314)
tree
|
commitdiff
2020-10-20
Gereon Kremer
Handle rewrite to bool in BoundInference (#5311)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Split CheckModels utility to its own file (#5303)
tree
|
commitdiff
2020-10-20
Aina Niemetz
Integer (CLN): Minor improvements. (#5306)
tree
|
commitdiff
2020-10-20
yoni206
Expand `seq.nth` lazily (#5287)
tree
|
commitdiff
2020-10-19
Aina Niemetz
Integer: CLN: Move implementation of member functions...
tree
|
commitdiff
2020-10-19
Haniel Barbosa
[proof-new] Fixing resolution proof checker (#5262)
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Updates to assertions pipeline and preproce...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proof...
tree
|
commitdiff
2020-10-19
Haniel Barbosa
[proof-new] Improving cycle checking in lazycdproofchai...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
Safer version of pending lemma processing in inference...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Refactoring cyclic checks (#5291)
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Witness axiom reconstruction for purificat...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Implementation of trust substitution (...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) More features for SMT proof post-processor...
tree
|
commitdiff
2020-10-18
Andrew Reynolds
(proof-new) Improvements for theory engine (#5292)
tree
|
commitdiff
2020-10-16
Andrew Reynolds
Refactor SMT-level model object (#5277)
tree
|
commitdiff
2020-10-16
Andrew Reynolds
Catch more cases of nested recursion in datatypes ...
tree
|
commitdiff
2020-10-16
yoni206
bv2int: caching introduced terms (#5283)
tree
|
commitdiff
2020-10-16
Andrew Reynolds
Add inference enumeration to datatypes (#5275)
tree
|
commitdiff
2020-10-15
Alex Ozdemir
(proof-new) TheoryArithPrivate: farkas lemma proof...
tree
|
commitdiff
2020-10-14
mudathirmahgoub
Fix issue #5269 (#5270)
tree
|
commitdiff
2020-10-14
yoni206
bv2int: implementing the iand-sum mode (#5265)
tree
|
commitdiff
2020-10-14
Alex Ozdemir
(proof-new) debug statements & docs for INT_TRUST ...
tree
|
commitdiff
2020-10-14
Alex Ozdemir
(proof-new) pfs in TheoryArith(Private) explainations...
tree
|
commitdiff
2020-10-14
Andrew Reynolds
Guard uses of printing approximations for constants...
tree
|
commitdiff
2020-10-14
Alex Ozdemir
(proof-new) pfs for conflicts in TheoryArithPrivate...
tree
|
commitdiff
2020-10-14
yoni206
bv2int: rewritings and unsat cores (#5263)
tree
|
commitdiff
2020-10-14
Haniel Barbosa
using NOT_NOT_ELIM rather than macros to do double...
tree
|
commitdiff
2020-10-14
Alex Ozdemir
(proof-new) Prove lemmas in Constraint (#5254)
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Generalize preprocess proof generator ...
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Simplifications for proof rule checker...
tree
|
commitdiff
2020-10-14
Andrew Reynolds
(proof-new) Miscellaneous minor improvements and fixes...
tree
|
commitdiff
2020-10-13
Andrew Reynolds
(proof-new) New rules for Booleans (#5243)
tree
|
commitdiff
2020-10-13
Andrew Reynolds
(proof-new) Change merge policy for proof node updater...
tree
|
commitdiff
2020-10-13
yoni206
bv2int: improving bvand tables (#5235)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Remove uf-ss-totality option (#5251)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Ensure uninterpreted sort owner is UF if uf-ho or finit...
tree
|
commitdiff
2020-10-11
Mathias Preiner
SyGuS instantiation modes (#5228)
tree
|
commitdiff
2020-10-11
Gereon Kremer
Add conversion of poly polynomial to cvc node. (#5218)
tree
|
commitdiff
2020-10-10
Abdalrhman Mohamed
Provide API version of some SMT Commands. (#5222)
tree
|
commitdiff
2020-10-10
yoni206
bv2int: bvand translation code move (#5227)
tree
|
commitdiff
2020-10-09
Alex Ozdemir
use right arith explanation fn to fix regressions ...
tree
|
commitdiff
2020-10-09
Alex Ozdemir
(proof-new) proofs for arith-constraint explanations...
tree
|
commitdiff
2020-10-09
Andres Noetzli
reset-assertions: Remove all non-global symbols in...
tree
|
commitdiff
2020-10-09
Andrew Reynolds
Simplify approach for collapsed selectors over non...
tree
|
commitdiff
2020-10-09
Andrew Reynolds
(proof-new) Add lazy proof set utility (#5221)
tree
|
commitdiff
next