projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add missing null terminators for regexp (#8027)
[cvc5.git]
/
src
/
preprocessing
/
2022-02-02
Andrew Reynolds
Remove more static calls to rewrite (#8025)
tree
|
commitdiff
2022-01-28
Andres Noetzli
[Rewrite Synthesis] Fix args for non-chaining ops ...
tree
|
commitdiff
2022-01-18
Andrew Reynolds
Print original form for substitutions and learned liter...
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Implement -o subs to show learned top-level substitutio...
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Fix learned rewrite pass for non-real equalties (#7936)
tree
|
commitdiff
2022-01-11
Gereon Kremer
Remove static accesses to options (#7913)
tree
|
commitdiff
2022-01-07
Andrew Reynolds
Fix eager string preprocessing in incremental mode...
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Minor cleaning of non-clausal simplification (#7886)
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Eliminating some uses of const rational in arithmetic...
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Refactoring initialization of proofs (#7834)
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Eliminate more uses of CONST_RATIONAL (#7816)
tree
|
commitdiff
2021-12-16
yoni206
int-to-bv: fail if one of the arguments has type real...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-13
yoni206
Integrate new int-blaster (#7781)
tree
|
commitdiff
2021-12-10
Gereon Kremer
Eliminate more static rewrites (#7786)
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Do not make SyGuS subsolver in unsat state after solvin...
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Towards support for incremental sygus (#7736)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Eliminate more static calls to Rewriter::rewrite (...
tree
|
commitdiff
2021-12-07
makaimann
Add bitwise option to IntBlaster (#7721)
tree
|
commitdiff
2021-12-02
Andrew Reynolds
Fixes for sygus-rr-synth-input (#7716)
tree
|
commitdiff
2021-11-19
Andrew Reynolds
Remove n-ary builder (#7671)
tree
|
commitdiff
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
tree
|
commitdiff
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
tree
|
commitdiff
2021-11-09
Andrew Reynolds
Only eliminate lambdas in higher-order elimination...
tree
|
commitdiff
2021-11-09
Gereon Kremer
Remove `CVC5Message` (#7610)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Remove `Chat()` in favor of new `verbose()` (#7586)
tree
|
commitdiff
2021-11-05
Gereon Kremer
Eliminate `Warning` macro in favor of `EnvObj::warning...
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Fix debug trace for miplib (#7563)
tree
|
commitdiff
2021-11-03
Andrew Reynolds
Refactor skolem construction (#7561)
tree
|
commitdiff
2021-11-01
Mathias Preiner
bv: Remove layered solver. (#7455)
tree
|
commitdiff
2021-10-25
Andrew Reynolds
Fix more missing uses of CDProof::isSame (#7491)
tree
|
commitdiff
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
tree
|
commitdiff
2021-10-08
Andrew Reynolds
A few more miscellaneous uses of EnvObj (#7325)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Move preprocessor to smt solver (#7321)
tree
|
commitdiff
2021-10-07
Andrew Reynolds
Use skolem lemma in prop layer interfaces (#7320)
tree
|
commitdiff
2021-10-04
Andrew Reynolds
Eliminating static calls to rewriter from strings ...
tree
|
commitdiff
2021-10-01
Aina Niemetz
Rename SmtEngine to SolverEngine. (#7282)
tree
|
commitdiff
2021-09-30
Aina Niemetz
Rename files smt_engine.(cpp|h) to solver_engine.(cpp...
tree
|
commitdiff
2021-09-30
Mathias Preiner
bv: Refactor ppRewrite and move to TheoryBV. (#7271)
tree
|
commitdiff
2021-09-30
Mathias Preiner
Properly cache assertions in static learning preprocess...
tree
|
commitdiff
2021-09-30
Andrew Reynolds
Simplify the syntax and representation of the separatio...
tree
|
commitdiff
2021-09-30
Gereon Kremer
Remove usage of static options in arithmetic theory...
tree
|
commitdiff
2021-09-24
Andrew Reynolds
Eliminate calls to Rewriter::rewrite from strings entai...
tree
|
commitdiff
2021-09-11
Gereon Kremer
Use StatisticsRegistry from Env (#7166)
tree
|
commitdiff
2021-09-11
Mathias Preiner
bv: Move IsPowerOfTwo rule to preprocessing pass and...
tree
|
commitdiff
2021-09-10
Andres Noetzli
Use C++17 attributes (#7154)
tree
|
commitdiff
2021-09-10
Gereon Kremer
Use EnvObj-based options in preprocessing (#7165)
tree
|
commitdiff
2021-09-09
Aina Niemetz
pp passes: Use EnvObj::rewrite() instead of Rewriter...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Improve pre-skolemization, move quantifiers preprocess...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Towards standard usage of ExtendedRewriter (#7145)
tree
|
commitdiff
2021-09-03
Aina Niemetz
EnvObj: Add options(), context(), userContext(). (...
tree
|
commitdiff
2021-09-03
Aina Niemetz
pp: Have PreprocessingPassContext derive from EnvObj...
tree
|
commitdiff
2021-09-02
Aina Niemetz
EnvObj: Restrict access. (#7121)
tree
|
commitdiff
2021-09-02
Aina Niemetz
Remove PreprocessingPassContext::getSmt(). (#7118)
tree
|
commitdiff
2021-09-02
Aina Niemetz
pp: Derive PreprocessingPass from EnvObj. (#7112)
tree
|
commitdiff
2021-09-01
Aina Niemetz
Clean up and document PP context. (#7102)
tree
|
commitdiff
2021-09-01
Aina Niemetz
rewriter: Make clearCaches non-static. (#7100)
tree
|
commitdiff
2021-08-26
Andrew Reynolds
Eliminate currentSmtEngine for subsolver calls (#7068)
tree
|
commitdiff
2021-08-26
Mathias Preiner
int2bv: Fix conversion of signed bit-vector values...
tree
|
commitdiff
2021-08-25
Andrew Reynolds
Eliminate calls to currentSmtEngine (#7060)
tree
|
commitdiff
2021-08-17
Andres Noetzli
Replace `Maybe` with `std::optional` (#7005)
tree
|
commitdiff
2021-07-12
Andrew Reynolds
Fix for learned rewrite pass, add regression (#6850)
tree
|
commitdiff
2021-07-06
Andrew Reynolds
Integrate learned rewrite preprocessing pass (#6840)
tree
|
commitdiff
2021-07-06
Andrew Reynolds
Add implementation of learned rewrite pass (#6843)
tree
|
commitdiff
2021-07-06
Andrew Reynolds
Add learned rewrite preprocessing pass (#6842)
tree
|
commitdiff
2021-06-30
yoni206
int-to-bv: correct model values (#6811)
tree
|
commitdiff
2021-06-15
Gereon Kremer
Remove public option wrappers (#6716)
tree
|
commitdiff
2021-06-10
Andrew Reynolds
Ensure bv2nat and int2bv are not rewritten when using...
tree
|
commitdiff
2021-06-09
Andres Noetzli
Make `--solve-int-as-bv=X` robust to rewriting (#6722)
tree
|
commitdiff
2021-06-09
Andrew Reynolds
Integrate learned literal manager into preprocessing...
tree
|
commitdiff
2021-06-08
Andrew Reynolds
Add learned literal manager utility (#6709)
tree
|
commitdiff
2021-06-01
Andrew Reynolds
Use top-level substitutions in ITE simp (#6651)
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Update proof namespaces (#6614)
tree
|
commitdiff
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
tree
|
commitdiff
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-20
Haniel Barbosa
Remove old unsat cores (#6581)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-10
Andrew Reynolds
Unify top-level substitutions and model substitutions...
tree
|
commitdiff
2021-05-07
Andrew Reynolds
Simplifications to expand definitions (#6487)
tree
|
commitdiff
2021-05-06
Andrew Reynolds
Use constant folding for evaluating BV eager atom ...
tree
|
commitdiff
2021-04-30
Andrew Reynolds
Use substitutions for implementing defined functions...
tree
|
commitdiff
2021-04-22
Andrew Reynolds
Fix models for sygus-inference, bv2int, real2int (...
tree
|
commitdiff
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
tree
|
commitdiff
2021-04-19
Andrew Reynolds
Fully incorporate quantifiers macros into ppAssert...
tree
|
commitdiff
2021-04-15
Aina Niemetz
preprocessing context: Add wrapper for model substituti...
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
tree
|
commitdiff
2021-04-14
Haniel Barbosa
[unsat-cores] Improving new unsat cores (#6356)
tree
|
commitdiff
2021-04-13
Andrew Reynolds
Refactor quantifiers macros (#6348)
tree
|
commitdiff
2021-04-12
Gereon Kremer
Refactor resource manager (#6322)
tree
|
commitdiff
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
next