projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Convert more uses of strings to words (#4527)
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
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-23
Andrew Reynolds
Add the sequence datatype (#4153)
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expression...
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
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
Andrew Reynolds
Use debug-check-model to enable internal debugging...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluatable...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
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-12
Andrew Reynolds
Do not enable unconstrained simplification if arithmetic...
commit
|
commitdiff
|
tree
2020-05-05
Andrew Reynolds
Always introduce fresh variable for unconstrained APPLY_UF...
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
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
Andrew Reynolds
Updates to SMT COMP script for 20 minute timeout (...
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-26
Andrew Reynolds
Fix sets cardinality cycle rule (#4392)
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-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
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-17
Andrew Reynolds
Add (context-dependent) Proof (#4323)
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 equalities...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Always assign function values in higher order (#4279)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Fix combinations of cegqi and non-standard triggers...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Disable preregistration of instantiations for cegqi...
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Disable macros when higher-order (#4266)
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Fix relevant domain computation for nested quantifiers...
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Remove a few options (#4295)
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Remove a few spurious assertions (#4294)
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Remove early type check option (#4234)
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Remove argument extender (#4223)
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Remove mergePredicates from EqualityEngine interface...
commit
|
commitdiff
|
tree
2020-04-14
Andrew Reynolds
Fix dump-unsat-cores-full (#4303)
commit
|
commitdiff
|
tree
2020-04-13
Andrew Reynolds
Fix SyGuS define-fun printing from benchmarks coming...
commit
|
commitdiff
|
tree
2020-04-12
Andrew Reynolds
Fixes for extended rewriter (#4278)
commit
|
commitdiff
|
tree
2020-04-12
Andrew Reynolds
Move slow nl regression to regress3 (#4276)
commit
|
commitdiff
|
tree
2020-04-11
Andrew Reynolds
Ensure exported sygus solutions match grammar (#4270)
commit
|
commitdiff
|
tree
2020-04-11
Andrew Reynolds
Split the non-linear solver (#4219)
commit
|
commitdiff
|
tree
2020-04-10
Andrew Reynolds
Explain non-emptiness by non-zero length in strings...
commit
|
commitdiff
|
tree
2020-04-10
Andrew Reynolds
Add a few stats to strings (#4252)
commit
|
commitdiff
|
tree
2020-04-10
Andrew Reynolds
Towards proper use of resource managers (#4233)
commit
|
commitdiff
|
tree
2020-04-09
Andrew Reynolds
Disable slow sygus regression (#4232)
commit
|
commitdiff
|
tree
2020-04-09
Andrew Reynolds
Split ProcessAssertions module from SmtEngine (#4210)
commit
|
commitdiff
|
tree
2020-04-08
Andrew Reynolds
Fix dump models and dump proofs (#4230)
commit
|
commitdiff
|
tree
2020-04-08
Andrew Reynolds
Eliminate call to currentNM within NodeManager (#4227)
commit
|
commitdiff
|
tree
2020-04-07
Andrew Reynolds
Cleanup deprecated quantifiers attribute features ...
commit
|
commitdiff
|
tree
2020-04-07
Andrew Reynolds
Disable slow regression (#4221)
commit
|
commitdiff
|
tree
2020-04-07
Andrew Reynolds
Enum for all remaining string inferences (#4220)
commit
|
commitdiff
|
tree
2020-04-06
Andrew Reynolds
Remove links field in all toml files (#4201)
commit
|
commitdiff
|
tree
2020-04-05
Andrew Reynolds
Add missing stat for lemmas based on inferences (#4214)
commit
|
commitdiff
|
tree
2020-04-05
Andrew Reynolds
Type-independent preregistration of empty word (#4205)
commit
|
commitdiff
|
tree
2020-04-03
Andrew Reynolds
Only rewrite lambdas via array representations when...
commit
|
commitdiff
|
tree
2020-04-03
Andrew Reynolds
Split sequences rewriter (#4194)
commit
|
commitdiff
|
tree
2020-04-02
Andrew Reynolds
Introduce enums for all string inferences, excluding...
commit
|
commitdiff
|
tree
2020-04-01
Andrew Reynolds
Support char smt-lib syntax (#4188)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fix fmf benchmark (#4193)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Remove replay and use-theory options and idl (#4186)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fix strange bound regression (#4192)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Convert more uses of string-specific functions (#4158)
commit
|
commitdiff
|
tree
2020-03-31
Andrew Reynolds
Fixing regressions (#4189)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Rewrites for all remaining return statements in strings...
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Support indexed operators re.loop and re.^ (#4167)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Remove ref skolem datatype option (#4185)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Fix arguments to print callback (#4171)
commit
|
commitdiff
|
tree
2020-03-29
Andrew Reynolds
Enumeration for String rewrites (#4173)
commit
|
commitdiff
|
tree
2020-03-28
Andrew Reynolds
Split transcendental solver to its own file (#4156)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Fix expected output on arith regression (#4162)
commit
|
commitdiff
|
tree
next