projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add new interfaces to term formula removal and theory preprocess (#5717)
[cvc5.git] / src / theory / strings /
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if... tree | commitdiff
2020-12-23 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714) tree | commitdiff
2020-12-16 mudathirmahgoubRenamed InferInfo::getAntecedant to InferInfo::getAntec... tree | commitdiff
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679) tree | commitdiff
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... tree | commitdiff
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Aina NiemetzFix compiler warnings. (#5644) tree | commitdiff
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... tree | commitdiff
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... tree | commitdiff
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) tree | commitdiff
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... tree | commitdiff
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) tree | commitdiff
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) tree | commitdiff
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-06 Andrew Reynolds(proof-new) Miscellaneous changes to strings for proofs... tree | commitdiff
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... tree | commitdiff
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... tree | commitdiff
2020-10-29 Andrew ReynoldsSet strings pending conflict flag (#5364) tree | commitdiff
2020-10-29 Andrew Reynolds(proof-new) Update the strings inference manager for... tree | commitdiff
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... tree | commitdiff
2020-10-20 yoni206Expand `seq.nth` lazily (#5287) tree | commitdiff
2020-10-14 Andrew Reynolds(proof-new) Simplifications for proof rule checker... tree | commitdiff
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903) tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092) tree | commitdiff
2020-09-16 Andres NoetzliOnly rewrite replace_re(_all) if regexp is const (... tree | commitdiff
2020-09-09 Andrew Reynolds(proof-new) Generalize single step helper in eager... tree | commitdiff
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-31 Andrew Reynolds(new theory) Update TheoryStrings to new standard ... tree | commitdiff
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... tree | commitdiff
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931) tree | commitdiff
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-19 Andrew ReynoldsMake sets and strings solver states inherit from Theory... tree | commitdiff
2020-08-19 Andres NoetzliRequire `--strings-exp` when using `str.substr` (#4916) tree | commitdiff
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to... tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-17 Andrew Reynolds(proof-new) Prepare the theory of strings for proof... tree | commitdiff
2020-08-16 Andrew ReynoldsAdd non-emptiness to conclusion of positive RE star... tree | commitdiff
2020-08-15 Andrew ReynoldsMinor cleanup related to notifications (#4898) tree | commitdiff
2020-08-15 Andrew Reynolds(proof-new) Add the strings proof checker (#4858) tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-08-12 Andrew Reynolds(proof-new) Proof support in the strings term registry... tree | commitdiff
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... tree | commitdiff
2020-08-06 Andrew Reynolds(proof-new) Refactor regular expression operation ... tree | commitdiff
2020-08-05 Andres Noetzli[Strings] Add eager context-dependent evaluation (... tree | commitdiff
2020-08-02 Andres NoetzliEnsure strict length constraint for decompose rule... tree | commitdiff
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring... tree | commitdiff
2020-07-28 Andrew ReynoldsFix regular expression delta for complement (#4765) tree | commitdiff
2020-07-28 yoni206Supporting seq.nth (#4723) tree | commitdiff
2020-07-17 Andrew Reynolds(proof-new) Updates to strings core solver (#4642) tree | commitdiff
2020-07-16 Andrew ReynoldsMake ExtTheory a utility and not a member of Theory... tree | commitdiff
2020-07-14 Andrew Reynolds(proof-new) Skeleton proof support in the Rewriter... tree | commitdiff
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) tree | commitdiff
2020-07-13 Andres NoetzliRemove ExprSequence (#4724) tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) tree | commitdiff
2020-07-01 Andrew Reynolds Inferences and model construction taking into account... tree | commitdiff
2020-06-30 Andrew ReynoldsFix normal form for re.comp (#4676) tree | commitdiff
2020-06-28 Andrew ReynoldsFix non-termination issues in simpleRegExpConsume ... tree | commitdiff
2020-06-20 Andrew Reynolds(proof-new) Make static methods in re-elim (#4623) tree | commitdiff
2020-06-19 Andrew Reynolds(proof-new) Updates to strings term registry (#4599) tree | commitdiff
2020-06-19 Andrew ReynoldsConvert more uses of strings to words (#4584) tree | commitdiff
2020-06-19 Andrew ReynoldsClean the header file of TheoryStrings (#4272) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-15 Andrew Reynolds Do RE derivation inference only for concrete constant... tree | commitdiff
2020-06-12 Andrew Reynolds(proof-new) Minor updates to strings base solver (... tree | commitdiff
2020-06-12 Andrew ReynoldsCardinality-related inferences per type in theory of... tree | commitdiff
2020-06-12 Andrew ReynoldsAdd rewrite for str.replace_re. (#4601) tree | commitdiff
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... tree | commitdiff
2020-06-05 Andrew Reynolds(proof-new) Rename ProofSkolemCache to SkolemManager... tree | commitdiff
2020-06-04 Andrew ReynoldsTheory strings preprocess (#4534) tree | commitdiff
2020-06-01 Andrew ReynoldsIncorporate sequences into the word interface (#4543) tree | commitdiff
2020-05-30 Andrew ReynoldsAdd the sequence type (#4539) tree | commitdiff
2020-05-28 Andrew ReynoldsFix term registry for constant case, simplify. (#4538) tree | commitdiff
2020-05-27 Andrew ReynoldsAdd the Expr-level sequence datatype (#4526) tree | commitdiff
2020-05-26 Andrew ReynoldsConvert more uses of strings to words (#4527) tree | commitdiff
2020-05-26 Andrew Reynolds(proof-new) Updates to strings skolem cache. (#4524) tree | commitdiff
2020-05-22 Andrew Reynolds(proof-new) Add rewrite corresponding to regular expres... tree | commitdiff
2020-05-22 Andrew Reynolds(proof-new) Minor update to strings solver state (... tree | commitdiff
2020-05-21 Andrew ReynoldsThrow logic exception for equality between regular... tree | commitdiff
2020-05-20 Andrew ReynoldsNormal form equality conflicts and uniqueness check... tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-04-30 Andrew ReynoldsRemove skolem share involving pre_first_ctn. (#4423) tree | commitdiff
2020-04-30 Andrew ReynoldsDo not mark congruent terms are reduced (#4419) tree | commitdiff
2020-04-29 Andrew ReynoldsAvoid circular dependencies for justifying reductions... tree | commitdiff
2020-04-28 Andres NoetzliRegister lower bound for str.to_int (#4408) tree | commitdiff
next