projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-06-02
Andrew Reynolds
Do not handle universal quantification on functions...
commit
|
commitdiff
|
tree
2020-06-02
Aina Niemetz
New C++ API: Keep reference to solver object in non...
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
(proof-new) Proof step buffer utilities (#4533)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
commit
|
commitdiff
|
tree
2020-06-01
Andres Noetzli
Set theoryof-mode after theory widening (#4545)
commit
|
commitdiff
|
tree
2020-06-01
Andres Noetzli
Do not parse ->/lambda unless --uf-ho enabled (#4544)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
commit
|
commitdiff
|
tree
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
commit
|
commitdiff
|
tree
2020-05-31
yoni206
update example in README to use ctest. (#4540)
commit
|
commitdiff
|
tree
2020-05-30
Andrew Reynolds
Add the sequence type (#4539)
commit
|
commitdiff
|
tree
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
commit
|
commitdiff
|
tree
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
commit
|
commitdiff
|
tree
2020-05-27
Martin
Tweak the use of static_assert to support older compile...
commit
|
commitdiff
|
tree
2020-05-26
Martin
Fix an incorrect limit in conversion from real to float...
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
commit
|
commitdiff
|
tree
2020-05-26
Mathias Preiner
Fix mismatched iterators (CID 1493892). (#4531)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Update proof checker. (#4511)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Updates to strings skolem cache. (#4524)
commit
|
commitdiff
|
tree
2020-05-26
Mathias Preiner
Update to CaDiCaL version 1.2.1. (#4530)
commit
|
commitdiff
|
tree
2020-05-24
Andres Noetzli
[SMT-COMP] Redirect non-answers to /dev/null (#4528)
commit
|
commitdiff
|
tree
2020-05-23
mudathirmahgoub
remove unused field d_emp_exp in TheorySetsPrivate...
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Add the sequence datatype (#4153)
commit
|
commitdiff
|
tree
2020-05-23
Abdalrhman...
Fix mistakes in sygus API comments. (#4520)
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
commit
|
commitdiff
|
tree
2020-05-22
Andres Noetzli
[SMT-COMP] Use tear-down-incremental for arithmetic...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
CaDiCaL: Clean up initialization on creation. (#4516)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expres...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
Cryptominisat: Clean up initialization on creation...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Proof node to SExpr utility. (#4512)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
Update string kind names in new API (#4509)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Minor update to strings solver state (...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Disable re-elim by default (#4508)
commit
|
commitdiff
|
tree
2020-05-21
Abdalrhman...
Make Grammar reusable. (#4506)
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Throw logic exception for equality between regular...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Fix missing check for cardinality one in unconstrained...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Normal form equality conflicts and uniqueness check...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Add proof skolem cache (#4485)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix parametric datatype instantiation (#4493)
commit
|
commitdiff
|
tree
2020-05-20
Aina Niemetz
CegqiBv: Clean up after renaming options. (#4487)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Use debug-check-model to enable internal debugging...
commit
|
commitdiff
|
tree
2020-05-20
Abdalrhman...
Add a simple script to convert sygus v1 files to v2...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
commit
|
commitdiff
|
tree
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Use fresh variables when miniscoping (#4296)
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Update enum and option names for sygus languages (...
commit
|
commitdiff
|
tree
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
commit
|
commitdiff
|
tree
2020-05-12
Andrew Reynolds
Do not enable unconstrained simplification if arithmeti...
commit
|
commitdiff
|
tree
2020-05-06
Andres Noetzli
Update run scripts for SMT-COMP 2020 (#4454)
commit
|
commitdiff
|
tree
2020-05-05
Andrew Reynolds
Always introduce fresh variable for unconstrained APPLY...
commit
|
commitdiff
|
tree
2020-05-05
Aina Niemetz
Update copyright year and AUTHORS/THANKS files. (#4468)
commit
|
commitdiff
|
tree
2020-05-02
Aina Niemetz
SMT-COMP 2020: Enable --fp-exp for new FP logics. ...
commit
|
commitdiff
|
tree
2020-05-02
Andrew Reynolds
Move slow regression to regress3 (#4430)
commit
|
commitdiff
|
tree
2020-05-01
Andrew Reynolds
Fix regression (#4424)
commit
|
commitdiff
|
tree
2020-04-30
Andrew Reynolds
Remove skolem share involving pre_first_ctn. (#4423)
commit
|
commitdiff
|
tree
2020-04-30
Andrew Reynolds
Do not mark congruent terms are reduced (#4419)
commit
|
commitdiff
|
tree
2020-04-29
Aina Niemetz
SMT-COMP 2020: Fix scripts to use --no-type-checking...
commit
|
commitdiff
|
tree
2020-04-29
Andrew Reynolds
Avoid circular dependencies for justifying reductions...
commit
|
commitdiff
|
tree
2020-04-29
Andrew Reynolds
Fix strings 2.6 regression (#4413)
commit
|
commitdiff
|
tree
2020-04-28
Andres Noetzli
Register lower bound for str.to_int (#4408)
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Updates to SMT COMP script for 20 minute timeout (...
commit
|
commitdiff
|
tree
2020-04-28
Haniel Barbosa
update Haniel's affiliation (#4404)
commit
|
commitdiff
|
tree
2020-04-28
Aina Niemetz
contrib/get-gmp: Rename and update install instructions...
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Support the SMT-LIB Unicode string standard by default...
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Update cardinality in strings to unicode standard ...
commit
|
commitdiff
|
tree
2020-04-27
Andrew Reynolds
Fix sygus unit (#4371)
commit
|
commitdiff
|
tree
2020-04-27
Mathias Preiner
Fix examples instructions in INSTALL.md. (#4397)
commit
|
commitdiff
|
tree
2020-04-26
Andrew Reynolds
Fix sets cardinality cycle rule (#4392)
commit
|
commitdiff
|
tree
2020-04-23
Andres Noetzli
Introduce best content heuristic for strings (#4382)
commit
|
commitdiff
|
tree
2020-04-23
Andres Noetzli
Strings: Register skolems before sending lemma (#4381)
commit
|
commitdiff
|
tree
2020-04-22
Andrew Reynolds
Ensure disequality splits are processed as lemmas ...
commit
|
commitdiff
|
tree
2020-04-22
Andrew Reynolds
Allow eager bitblasting with solve bv as int in QF_NIA...
commit
|
commitdiff
|
tree
2020-04-22
Abdalrhman...
Convert V2.5 SMT regressions to V2.6. (#4319)
commit
|
commitdiff
|
tree
2020-04-22
Andres Noetzli
Reinstantiate support for conjunctions in facts (#4377)
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Update to sygus version 2 (#4372)
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Fix for parse options related to binary name (#4368)
commit
|
commitdiff
|
tree
2020-04-21
Abdalrhman...
Introduce a public interface for Sygus commands. (...
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
commit
|
commitdiff
|
tree
2020-04-20
Andrew Reynolds
Refactor inference manager in strings to be amenable...
commit
|
commitdiff
|
tree
2020-04-20
Andrew Reynolds
Add SCOPE proof rule (#4332)
commit
|
commitdiff
|
tree
2020-04-19
Andrew Reynolds
Disable unsat cores on nec regression (#4330)
commit
|
commitdiff
|
tree
2020-04-18
Andrew Reynolds
Track inference id for pending facts in strings (#4331)
commit
|
commitdiff
|
tree
2020-04-18
Haniel Barbosa
Improving EqProof printing (#4329)
commit
|
commitdiff
|
tree
2020-04-17
Andrew Reynolds
Add (context-dependent) Proof (#4323)
commit
|
commitdiff
|
tree
2020-04-17
Mathias Preiner
antlr: Use relative path in ANTLR script. (#4324)
commit
|
commitdiff
|
tree
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
commit
|
commitdiff
|
tree
2020-04-16
Andrew Reynolds
Add ProofNodeManager and ProofChecker (#4317)
commit
|
commitdiff
|
tree
2020-04-16
Andrew Reynolds
Eliminate remaining references to parent TheoryStrings...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Add ProofNode data structure (#4311)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Move regular expression inclusion test to RegExpEntail...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Change option names --default-dag-thresh and --default...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Split TermRegistry object from TheoryStrings (#4312)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Do not mark string extended functions as eliminated...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Fix assertion in enumerative instantiation (#4313)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Convert more cases of strings to words (#4206)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Abort if in conflict in enumerative instantiation ...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Always flush lemmas from downwards closure in sets...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Do not normalize to representatives for variable equali...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Always assign function values in higher order (#4279)
commit
|
commitdiff
|
tree
next