projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Remove template argument from `NodeBuilder` (#6290)
[cvc5.git]
/
src
/
preprocessing
/
passes
/
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-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
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
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Move ownership of term formula removal to theory prepro...
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Consolidate basic sygus utilities regarding sygus conje...
tree
|
commitdiff
2020-12-08
yoni206
bv-to-int: Expand definitions of bvudiv and bvurem...
tree
|
commitdiff
2020-12-07
makaimann
Add bitwise refinement mode for IAND (#5328)
tree
|
commitdiff
2020-12-04
Alex Ozdemir
Use NodeDfsIterable for makeBinary (#5595)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Minor cleanup of SmtEngine (#5450)
tree
|
commitdiff
2020-11-14
Andrew Reynolds
(proof-new) Proofs for non-clausal simplification ...
tree
|
commitdiff
2020-10-22
Andrew Reynolds
(proof-new) Make theory preprocessor user-context depen...
tree
|
commitdiff
2020-10-21
Gereon Kremer
(proof-new) Make circuit propagator proof producing...
tree
|
commitdiff
2020-10-19
Andrew Reynolds
(proof-new) Update preprocessing pass context for proof...
tree
|
commitdiff
2020-10-16
yoni206
bv2int: caching introduced terms (#5283)
tree
|
commitdiff
2020-10-14
yoni206
bv2int: rewritings and unsat cores (#5263)
tree
|
commitdiff
2020-10-13
yoni206
bv2int: improving bvand tables (#5235)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Eliminate uses of Expr in SmtEngine interface (#5240)
tree
|
commitdiff
2020-10-10
yoni206
bv2int: bvand translation code move (#5227)
tree
|
commitdiff
2020-10-09
Andres Noetzli
reset-assertions: Remove all non-global symbols in...
tree
|
commitdiff
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
tree
|
commitdiff
2020-10-01
Andrew Reynolds
(proof-new) Preprocessing passes use proper interfaces...
tree
|
commitdiff
2020-09-24
Andrew Reynolds
Function definition fmf preprocessing pass (#5064)
tree
|
commitdiff
2020-09-23
yoni206
bv2int: new options for bvand translation (#5096)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-18
yoni206
bv2int: quantifiers support (#5080)
tree
|
commitdiff
2020-09-16
yoni206
bv2int: support models in tests (#5068)
tree
|
commitdiff
2020-09-14
yoni206
bv2int: simpler translation for plus and times (#5055)
tree
|
commitdiff
2020-09-14
Andres Noetzli
Fix type for Windows build (#5062)
tree
|
commitdiff
2020-09-10
yoni206
bv2int: refactoring the main translation loop (#5051)
tree
|
commitdiff
2020-09-10
yoni206
bv2int: improvement in lazy failures (#5020)
tree
|
commitdiff
2020-09-03
yoni206
Changing the handled operators in bv2int preprocessing...
tree
|
commitdiff
2020-09-03
Andrew Reynolds
(proof-new) Support proofs of quantifier instantiation...
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically differ...
tree
|
commitdiff
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
tree
|
commitdiff
2020-07-27
Andrew Reynolds
(proof-new) Proof production for term formula removal...
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
tree
|
commitdiff
2020-07-11
yoni206
Changing bv_to_int options (#4721)
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-06-24
Andres Noetzli
[unconstrained] Fix gathering of visited-once vars...
tree
|
commitdiff
2020-06-20
Alex Ozdemir
Use traversal iterators in IntToBv (#4169)
tree
|
commitdiff
2020-06-19
yoni206
Bv to int elimination bugfix (#4435)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifi...
tree
|
commitdiff
2020-05-21
Andrew Reynolds
Fix missing check for cardinality one in unconstrained...
tree
|
commitdiff
2020-05-05
Andrew Reynolds
Always introduce fresh variable for unconstrained APPLY...
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Towards proper use of resource managers (#4233)
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-25
Ahmed Irfan
bv2int : linear mult opt (#4142)
tree
|
commitdiff
2020-03-24
yoni206
Int2BV fail on demand (#4079)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Fix variable shadowing issue in sygus-inference (#4121)
tree
|
commitdiff
2020-03-19
yoni206
Bv2int fail on demand
tree
|
commitdiff
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Do not allow quantifiers over real variables in real...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
tree
|
commitdiff
2020-03-11
Aina Niemetz
bv-gauss-elim: Fix handling of inconsistent case. ...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
tree
|
commitdiff
next