summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-05-21Disable re-elim by default (#4508)Andrew Reynolds
2020-05-21Make Grammar reusable. (#4506)Abdalrhman Mohamed
2020-05-20Throw logic exception for equality between regular expressions (#4505)Andrew Reynolds
2020-05-20Fix missing check for cardinality one in unconstrained simplifier (#4504)Andrew Reynolds
2020-05-20Normal form equality conflicts and uniqueness check (#4497)Andrew Reynolds
2020-05-20Add proof skolem cache (#4485)Andrew Reynolds
2020-05-20Fix parametric datatype instantiation (#4493)Andrew Reynolds
2020-05-20CegqiBv: Clean up after renaming options. (#4487)Aina Niemetz
2020-05-20Use debug-check-model to enable internal debugging in check-model (#4480)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-05-19Use fresh variables when miniscoping (#4296)Andrew Reynolds
2020-05-19Update enum and option names for sygus languages (#4388)Andrew Reynolds
2020-05-19Make SolveEq and PlusCombineLikeTerms idempotent (#4438)Andres Noetzli
2020-05-12Do not enable unconstrained simplification if arithmetic is present (#4489)Andrew Reynolds
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-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-29Avoid circular dependencies for justifying reductions in strings extf eval (#...Andrew Reynolds
2020-04-28Register lower bound for str.to_int (#4408)Andres Noetzli
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-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-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-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-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
2020-04-15Abort if in conflict in enumerative instantiation (#4298)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback