projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
New C++ API: Keep reference to solver object in non-solver objects. (#4549)
2020-06-01
Andres Noetzli
Set theoryof-mode after theory widening (#4545)
commit
|
commitdiff
|
tree
2020-06-01
Andres Noetzli
Do not parse ->/lambda unless --uf-ho enabled (#4544)
commit
|
commitdiff
|
tree
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
commit
|
commitdiff
|
tree
2020-05-24
Andres Noetzli
[SMT-COMP] Redirect non-answers to /dev/null (#4528)
commit
|
commitdiff
|
tree
2020-05-22
Andres Noetzli
[SMT-COMP] Use tear-down-incremental for arithmetic...
commit
|
commitdiff
|
tree
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
commit
|
commitdiff
|
tree
2020-05-06
Andres Noetzli
Update run scripts for SMT-COMP 2020 (#4454)
commit
|
commitdiff
|
tree
2020-04-28
Andres Noetzli
Register lower bound for str.to_int (#4408)
commit
|
commitdiff
|
tree
2020-04-23
Andres Noetzli
Introduce best content heuristic for strings (#4382)
commit
|
commitdiff
|
tree
2020-04-23
Andres Noetzli
Strings: Register skolems before sending lemma (#4381)
commit
|
commitdiff
|
tree
2020-04-22
Andres Noetzli
Reinstantiate support for conjunctions in facts (#4377)
commit
|
commitdiff
|
tree
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
commit
|
commitdiff
|
tree
2020-04-06
Andres Noetzli
Refactor disequality processing in string solver (...
commit
|
commitdiff
|
tree
2020-04-05
Andres Noetzli
Add safe_print() support for Kind enum (#4213)
commit
|
commitdiff
|
tree
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
commit
|
commitdiff
|
tree
2020-04-02
Andres Noetzli
Remove undocumented/uncommon aliases (#4177)
commit
|
commitdiff
|
tree
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
commit
|
commitdiff
|
tree
2020-03-27
Andres Noetzli
Fix issues with unsat cores and reset-assertions (...
commit
|
commitdiff
|
tree
2020-03-25
Andres Noetzli
Support async-signal-safe printing of inferences (...
commit
|
commitdiff
|
tree
2020-03-23
Andres Noetzli
Collect statistics about normal form inferences (#4127)
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-19
Andres Noetzli
Only apply testConstStringInRegExp to const regexp...
commit
|
commitdiff
|
tree
2020-03-19
Andres Noetzli
Only allow bv2nat/int2bv with BV and integer logic...
commit
|
commitdiff
|
tree
2020-03-16
Andres Noetzli
Create master equality engine at context level 0 (...
commit
|
commitdiff
|
tree
2020-03-11
Andres Noetzli
reset-assertions: Update TheoryEngine's PropEngine...
commit
|
commitdiff
|
tree
2020-03-11
Andres Noetzli
Introduce tables in the rewriter (#3742)
commit
|
commitdiff
|
tree
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Increase stack size for Windows builds to 100 MB (...
commit
|
commitdiff
|
tree
2020-03-09
Andres Noetzli
Fix quoting of options on Travis (#3981)
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Ignore model check warning in regression test (#3926)
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Make output of regression script more readable (#3911)
commit
|
commitdiff
|
tree
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
commit
|
commitdiff
|
tree
2020-03-05
Andres Noetzli
Add a new arith constraint proof rule: IntTightenAP...
commit
|
commitdiff
|
tree
2020-03-03
Andres Noetzli
Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
commit
|
commitdiff
|
tree
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
commit
|
commitdiff
|
tree
2020-02-27
Andres Noetzli
Fix -Wshadow warnings in common headers (#3826)
commit
|
commitdiff
|
tree
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
commit
|
commitdiff
|
tree
2020-02-24
Andres Noetzli
Make lambda rewriter more robust (#3806)
commit
|
commitdiff
|
tree
2020-02-20
Andres Noetzli
Remove unused code (#3782)
commit
|
commitdiff
|
tree
2020-02-20
Andres Noetzli
Remove parser from bindings (#3779)
commit
|
commitdiff
|
tree
2020-02-16
Andres Noetzli
Activate reverse variant of F-Split inference (#3745)
commit
|
commitdiff
|
tree
2020-02-13
Andres Noetzli
[Python] Properly destroy CVC4 object (#3753)
commit
|
commitdiff
|
tree
2020-02-12
Andres Noetzli
Rename Java package to edu.stanford.CVC4 (#3752)
commit
|
commitdiff
|
tree
2020-02-11
Andres Noetzli
Remove `--strings-binary-csp` option (#3743)
commit
|
commitdiff
|
tree
2020-02-11
Andres Noetzli
Refactor `CoreSolver::processSimpleNEq()` (#3736)
commit
|
commitdiff
|
tree
2020-02-08
Andres Noetzli
Make "unknown" non-critical for unsat cores check ...
commit
|
commitdiff
|
tree
2020-02-04
Andres Noetzli
Revert semantic change from refactoring (#3711)
commit
|
commitdiff
|
tree
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
commit
|
commitdiff
|
tree
2020-01-30
Andres Noetzli
Better heuristics for marking congruent variables ...
commit
|
commitdiff
|
tree
2020-01-14
Andres Noetzli
Disable unsat cores for regression that times out ...
commit
|
commitdiff
|
tree
2020-01-13
Andres Noetzli
Support arbitrary unsigned integer attributes (#3591)
commit
|
commitdiff
|
tree
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
commit
|
commitdiff
|
tree
2020-01-10
Andres Noetzli
Optimize str.substr reduction (#3595)
commit
|
commitdiff
|
tree
2019-12-18
Andres Noetzli
Avoid calling rewriter from type checker (#3548)
commit
|
commitdiff
|
tree
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
commit
|
commitdiff
|
tree
2019-12-08
Andres Noetzli
[Regressions] Require proof support for abduction ...
commit
|
commitdiff
|
tree
2019-12-07
Andres Noetzli
Simplify rewrite for character matching (#3545)
commit
|
commitdiff
|
tree
2019-12-07
Andres Noetzli
Use str.subtr in str.to.int/int.to.str reduction (...
commit
|
commitdiff
|
tree
2019-12-06
Andres Noetzli
Add lemma for str.to.int/int.to.str (#3541)
commit
|
commitdiff
|
tree
2019-12-05
Andres Noetzli
Bi-directional unrolling of R* regular expressions...
commit
|
commitdiff
|
tree
2019-12-04
Andres Noetzli
Fix corner case in model construction of strings (...
commit
|
commitdiff
|
tree
2019-12-03
Andres Noetzli
Rewrite `str.contains` used for character matching...
commit
|
commitdiff
|
tree
2019-12-02
Andres Noetzli
[SMT2 Printer] Quote symbols starting with digit (...
commit
|
commitdiff
|
tree
2019-12-01
Andres Noetzli
Prevent ref count from reaching zero in BV instantiator...
commit
|
commitdiff
|
tree
2019-11-30
Andres Noetzli
Competition build: Skip parsing error regression (...
commit
|
commitdiff
|
tree
2019-11-19
Andres Noetzli
Fix reduction of `sqrt` (#3478)
commit
|
commitdiff
|
tree
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
commit
|
commitdiff
|
tree
2019-11-17
Andres Noetzli
Add support for ThreadSanitizer instrumentation (#3467)
commit
|
commitdiff
|
tree
2019-11-13
Andres Noetzli
Allow (set-logic ...) after (reset) (#3457)
commit
|
commitdiff
|
tree
2019-11-11
Andres Noetzli
Fix mkConst<RoundingMode>() for Python bindings (#3447)
commit
|
commitdiff
|
tree
2019-11-06
Andres Noetzli
[Regressions] Remove leading whitespace in output ...
commit
|
commitdiff
|
tree
2019-11-06
Andres Noetzli
Remove casts to subclasses of Type in API (#3420)
commit
|
commitdiff
|
tree
2019-11-05
Andres Noetzli
[Regressions] Support for running w/ default args ...
commit
|
commitdiff
|
tree
2019-11-01
Andres Noetzli
Fix and refactor TheoryStrings::checkFlatForms() (...
commit
|
commitdiff
|
tree
2019-10-28
Andres Noetzli
Fix integer division rewrite (#3415)
commit
|
commitdiff
|
tree
2019-10-27
Andres Noetzli
Fix global-declarations support (#3403)
commit
|
commitdiff
|
tree
2019-10-15
Andres Noetzli
Fix line numbers in templates (#3391)
commit
|
commitdiff
|
tree
2019-10-15
Andres Noetzli
Remove remaining references to Boost and Autotools...
commit
|
commitdiff
|
tree
2019-10-15
Andres Noetzli
Fix OOB access (#3383)
commit
|
commitdiff
|
tree
2019-10-15
Andres Noetzli
Fix regression (#3393)
commit
|
commitdiff
|
tree
2019-10-14
Andres Noetzli
Disable regression test for competition build (#3388)
commit
|
commitdiff
|
tree
2019-10-11
Andres Noetzli
Add support for UBSan instrumentation (#3382)
commit
|
commitdiff
|
tree
2019-10-09
Andres Noetzli
Avoid printing success for `--force-logic` (#3363)
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
[CVC Parser] Add support for regular expressions (...
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
Disallow --proof and --incremental (#3332)
commit
|
commitdiff
|
tree
2019-10-08
Andres Noetzli
[SMT2 Parser] Move code of `rewriterulesCommand` (...
commit
|
commitdiff
|
tree
2019-10-03
Andres Noetzli
Add missing type definitions to CDHashMap iterator...
commit
|
commitdiff
|
tree
2019-10-03
Andres Noetzli
[SMT2 Parser] Move code of `sygusCommand` (#3335)
commit
|
commitdiff
|
tree
2019-10-02
Andres Noetzli
[SMT-COMP] Remove --unconstrained-simp for incremental...
commit
|
commitdiff
|
tree
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
commit
|
commitdiff
|
tree
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
commit
|
commitdiff
|
tree
2019-09-27
Andres Noetzli
Make substitution index context-independent (#2474)
commit
|
commitdiff
|
tree
2019-09-18
Andres Noetzli
Add run script for next SMT-COMP (#3298)
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Fix out-of-bounds access in regexp inclusion test ...
Signed-off-by:
Andres Noetzli
<andres.noetzli@gmail.com>
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Better heuristic for str.code/re.range (#3220)
Signed-off-by:
Andres Noetzli
<anoetzli@amazon.com>
commit
|
commitdiff
|
tree
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
Signed-off-by:
Andres Noetzli
<anoetzli@amazon.com>
commit
|
commitdiff
|
tree
2019-08-14
Andres Noetzli
Enable Clang-Format for Java (#3064)
commit
|
commitdiff
|
tree
2019-07-22
Andres Noetzli
Avoid move constructor of std::fstream for GCC < 5...
commit
|
commitdiff
|
tree
next