summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-11Change re-elimreElimChangeAndres Noetzli
2020-05-11Add skolem stats and sharing toggleAndres Noetzli
2020-05-08Unify skolemsAndres Noetzli
2020-05-06Update run scripts for SMT-COMP 2020 (#4454)Andres Noetzli
2020-05-05Always introduce fresh variable for unconstrained APPLY_UF (#4472)Andrew Reynolds
2020-05-05Update copyright year and AUTHORS/THANKS files. (#4468)Aina Niemetz
2020-05-01SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432)Aina Niemetz
2020-05-01Move slow regression to regress3 (#4430)Andrew Reynolds
2020-04-30Fix regression (#4424)Andrew Reynolds
2020-04-30Remove skolem share involving pre_first_ctn. (#4423)Andrew Reynolds
2020-04-30Do not mark congruent terms are reduced (#4419)Andrew Reynolds
2020-04-29SMT-COMP 2020: Fix scripts to use --no-type-checking instead of --no-checking...Aina Niemetz
2020-04-29Avoid circular dependencies for justifying reductions in strings extf eval (#...Andrew Reynolds
2020-04-29Fix strings 2.6 regression (#4413)Andrew Reynolds
2020-04-28Register lower bound for str.to_int (#4408)Andres Noetzli
2020-04-28Updates to SMT COMP script for 20 minute timeout (#4406)Andrew Reynolds
2020-04-28update Haniel's affiliation (#4404)Haniel Barbosa
2020-04-28contrib/get-gmp: Rename and update install instructions with a warning. (#4407)Aina Niemetz
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-28Update cardinality in strings to unicode standard (#4402)Andrew Reynolds
2020-04-27Fix sygus unit (#4371)Andrew Reynolds
2020-04-27Fix examples instructions in INSTALL.md. (#4397)Mathias Preiner
2020-04-25 Fix sets cardinality cycle rule (#4392)Andrew Reynolds
2020-04-23Introduce best content heuristic for strings (#4382)Andres Noetzli
2020-04-22Strings: Register skolems before sending lemma (#4381)Andres Noetzli
2020-04-22Ensure disequality splits are processed as lemmas (#4380)Andrew Reynolds
2020-04-22Allow eager bitblasting with solve bv as int in QF_NIA (#4373)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-22Reinstantiate support for conjunctions in facts (#4377)Andres Noetzli
2020-04-21Update to sygus version 2 (#4372)Andrew Reynolds
2020-04-21Fix for parse options related to binary name (#4368)Andrew Reynolds
2020-04-20Introduce a public interface for Sygus commands. (#4204)Abdalrhman Mohamed
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-20Refactor inference manager in strings to be amenable to proofs (#4363)Andrew Reynolds
2020-04-20Add SCOPE proof rule (#4332)Andrew Reynolds
2020-04-18Disable unsat cores on nec regression (#4330)Andrew Reynolds
2020-04-18Track inference id for pending facts in strings (#4331)Andrew Reynolds
2020-04-18Improving EqProof printing (#4329)Haniel Barbosa
2020-04-17Add (context-dependent) Proof (#4323)Andrew Reynolds
2020-04-16antlr: Use relative path in ANTLR script. (#4324)Mathias Preiner
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-04-16Add ProofNodeManager and ProofChecker (#4317)Andrew Reynolds
2020-04-16Eliminate remaining references to parent TheoryStrings object (#4315)Andrew Reynolds
2020-04-15Add ProofNode data structure (#4311)Andrew Reynolds
2020-04-15Move regular expression inclusion test to RegExpEntail (#4310)Andrew Reynolds
2020-04-15Change option names --default-dag-thresh and --default-expr-depth (#4309)Andrew Reynolds
2020-04-15Split TermRegistry object from TheoryStrings (#4312)Andrew Reynolds
2020-04-15Do not mark string extended functions as eliminated after reduction lemmas (#...Andrew Reynolds
2020-04-15Fix assertion in enumerative instantiation (#4313)Andrew Reynolds
2020-04-15Convert more cases of strings to words (#4206)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback