projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Revert #7257 (#7337)
[cvc5.git]
/
src
/
preprocessing
/
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
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-25
Gereon Kremer
Add missing includes. (#6207)
tree
|
commitdiff
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
tree
|
commitdiff
2021-03-15
Gereon Kremer
Replace HistogramStat by IntegralHistogramStat (#6126)
tree
|
commitdiff
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
tree
|
commitdiff
2021-03-09
Andrew Reynolds
Remove logic request (#6089)
tree
|
commitdiff
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove partial UDIV/UREM operators. (#6069)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-03-02
Mathias Preiner
Remove non-ASCII characters from source files. (#6039)
tree
|
commitdiff
2021-03-02
Mathias Preiner
Fix nightly errors. (#6034)
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-25
Gereon Kremer
Move (optional) rewrite from TrustSubstitutionMap to...
tree
|
commitdiff
2021-02-25
Mathias Preiner
Enable -Werror. (#5969)
tree
|
commitdiff
2021-02-24
Gereon Kremer
Ensure static-learning adds rewritten assertions. ...
tree
|
commitdiff
2021-02-24
Andrew Reynolds
Add interface to TheoryState for sort inference and...
tree
|
commitdiff
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
tree
|
commitdiff
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
tree
|
commitdiff
2021-02-12
Andrew Reynolds
Simplify and fix decision engine's handling of skolem...
tree
|
commitdiff
2021-02-02
Andrew Reynolds
Cleanup some includes (#5847)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Always theory-preprocess lemmas (#5817)
tree
|
commitdiff
2021-01-27
Andrew Reynolds
Split pattern term selector from trigger (#5811)
tree
|
commitdiff
2021-01-15
Andrew Reynolds
Implement --no-strings-lazy-pp as a preprocessing pass...
tree
|
commitdiff
2021-01-14
Andrew Reynolds
Updates to theory preprocess equality (#5776)
tree
|
commitdiff
2021-01-13
Andrew Reynolds
Do not call ppRewrite on Boolean equalities (#5762)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
tree
|
commitdiff
2021-01-09
yoni206
Strings arith checks preprocessing pass: step 2 (#5750)
tree
|
commitdiff
2021-01-08
yoni206
bv-to-int: avoid binarizing nodes twice (#5749)
tree
|
commitdiff
2021-01-06
yoni206
strings arith checks preprocessing pass: step 1 (#5747)
tree
|
commitdiff
2020-12-24
Haniel Barbosa
[proof-new] Only use old proofs for unsat cores if...
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Make theory preprocess rewrite equalities a preprocessi...
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Move ownership of theory preprocessor to TheoryProxy...
tree
|
commitdiff
next