projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
Alex Ozdemir
Add skip predicate to node traversal. (#4222)
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
Mathias Preiner
CI: Add a step to list dependencies. (#4255)
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
mudathirmahgoub
Added CHOOSE operator for sets (#4211)
commit
|
commitdiff
|
tree
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
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-06
Andres Noetzli
Refactor disequality processing in string solver (...
commit
|
commitdiff
|
tree
2020-04-06
Aina Niemetz
New C++ API: Rename Solver::mkTermInternal. (#4217)
commit
|
commitdiff
|
tree
2020-04-05
Andrew Reynolds
Add missing stat for lemmas based on inferences (#4214)
commit
|
commitdiff
|
tree
2020-04-05
Andres Noetzli
Add safe_print() support for Kind enum (#4213)
commit
|
commitdiff
|
tree
2020-04-05
Andrew Reynolds
Type-independent preregistration of empty word (#4205)
commit
|
commitdiff
|
tree
2020-04-04
Aina Niemetz
New C++ API: Remove Op::getSort(). (#4208)
commit
|
commitdiff
|
tree
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
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
Andres Noetzli
Remove undocumented/uncommon aliases (#4177)
commit
|
commitdiff
|
tree
2020-04-02
Andrew Reynolds
Introduce enums for all string inferences, excluding...
commit
|
commitdiff
|
tree
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
commit
|
commitdiff
|
tree
2020-04-01
Andrew Reynolds
Support char smt-lib syntax (#4188)
commit
|
commitdiff
|
tree
2020-04-01
Mathias Preiner
Fix install for ANTLR contrib script and CI dependency...
commit
|
commitdiff
|
tree
2020-04-01
Aina Niemetz
Rename checkValid/query to checkEntailed. (#4191)
commit
|
commitdiff
|
tree
2020-03-31
Mathias Preiner
Switch to GitHub actions for CI (#4190)
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
Mathias Preiner
Add coverage badge. (#4187)
commit
|
commitdiff
|
tree
2020-03-30
Andrew Reynolds
Fix arguments to print callback (#4171)
commit
|
commitdiff
|
tree
2020-03-30
mudathirmahgoub
Frontend support for the choice operator (#4175)
commit
|
commitdiff
|
tree
2020-03-29
Andrew Reynolds
Enumeration for String rewrites (#4173)
commit
|
commitdiff
|
tree
2020-03-28
Abdalrhman...
Change is-cons to (_ is cons) in Sygus benchmarks....
commit
|
commitdiff
|
tree
2020-03-28
Abdalrhman...
Convert the last few Sygus benchmarks to V2. (#4172)
commit
|
commitdiff
|
tree
2020-03-28
Abdalrhman...
Stop printing datatype declaration for Sygus V1 grammar...
commit
|
commitdiff
|
tree
2020-03-28
Alex Ozdemir
Node traversal iterator (#3845)
commit
|
commitdiff
|
tree
2020-03-28
Andrew Reynolds
Split transcendental solver to its own file (#4156)
commit
|
commitdiff
|
tree
2020-03-27
Andres Noetzli
Fix issues with unsat cores and reset-assertions (...
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Fix expected output on arith regression (#4162)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Do not require that function sorts are first class...
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
commit
|
commitdiff
|
tree
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
commit
|
commitdiff
|
tree
2020-03-26
Amalee
Added unit-cube-like test for branch and bound (#3922)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Disable slow regression (#4157)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Add stats for string reductions, lemmas and conflicts...
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Generalize more string-specific functions (#4152)
commit
|
commitdiff
|
tree
2020-03-26
Andrew Reynolds
Care graphs based on polymorphic operators in strings...
commit
|
commitdiff
|
tree
2020-03-25
Andres Noetzli
Support async-signal-safe printing of inferences (...
commit
|
commitdiff
|
tree
2020-03-25
Ahmed Irfan
bv2int : linear mult opt (#4142)
commit
|
commitdiff
|
tree
2020-03-25
Andrew Reynolds
Generalize more uses of string-specific functions...
commit
|
commitdiff
|
tree
2020-03-24
yoni206
Int2BV fail on demand (#4079)
commit
|
commitdiff
|
tree
2020-03-24
Andrew Reynolds
Restrict partial triggers to standard quantified formul...
commit
|
commitdiff
|
tree
2020-03-24
Andrew Reynolds
Restrict cases of sygus grammar reduction based on...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Infer when sygus operators are equivalent to builtin...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Simplify auxiliary variable handling in CEGQI (#4141)
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Throw exception for non-well-founded unimplemented...
commit
|
commitdiff
|
tree
2020-03-23
Andrew Reynolds
Change transcendental function app slave list to unorde...
commit
|
commitdiff
|
tree
2020-03-23
Andres Noetzli
Collect statistics about normal form inferences (#4127)
commit
|
commitdiff
|
tree
2020-03-22
Andrew Reynolds
Sort inference does not handle APPLY_UF when higher...
commit
|
commitdiff
|
tree
2020-03-22
Abdalrhman...
Convert V1 Sygus files to V2. (#4136)
commit
|
commitdiff
|
tree
2020-03-21
Andres Noetzli
Simplify heuristic in `processNEqc` (#4129)
commit
|
commitdiff
|
tree
2020-03-21
Andres Noetzli
Don't run bv_nat parse test with competition build...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Generalize mkConcat for types (#4123)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Fix variable shadowing issue in sygus-inference (#4121)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Fix sort comparison within assertion in cegis (#4113)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Guard cases of sort inference in quantifier free logics...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewri...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Do not assign higher-order representative if function...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Handle failures for sygus QE preprocess (#4072)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Parse error for SyGuS version 1.0 vs 2.0 (#4057)
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Make handling of illegal internal representatives in...
commit
|
commitdiff
|
tree
2020-03-20
Andrew Reynolds
Refactor enumerator for strings (#4014)
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
Fix regression output related to sygus+bv-div-zero...
commit
|
commitdiff
|
tree
2020-03-19
yoni206
Bv2int fail on demand
commit
|
commitdiff
|
tree
2020-03-19
Andres Noetzli
Only apply testConstStringInRegExp to const regexp...
commit
|
commitdiff
|
tree
2020-03-19
Andrew Reynolds
SyGuS must use total bitvector division (#4119)
commit
|
commitdiff
|
tree
next