projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Replace Expr-level datatype with Node-level DType (#4875)
[cvc5.git]
/
test
/
unit
/
theory
/
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Split SmtEngineState from SmtEngine (#4855)
tree
|
commitdiff
2020-08-11
Andrew Reynolds
Update Expr-level unit tests that depend on datatypes...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
(proof-new) Refactor regular expression operation ...
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use TypeNode in UninterpretedConstant (#4748)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode in EmptySet (#4740)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
tree
|
commitdiff
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-06-29
Andres Noetzli
Make ExprManager constructor private (#4669)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
tree
|
commitdiff
2020-04-30
Andrew Reynolds
Remove skolem share involving pre_first_ctn. (#4423)
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-03
Andrew Reynolds
Split sequences rewriter (#4194)
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewri...
tree
|
commitdiff
2020-03-19
Andres Noetzli
Only apply testConstStringInRegExp to const regexp...
tree
|
commitdiff
2020-03-17
Aina Niemetz
SmtEngine: Convert members owned by SmtEngine to unique...
tree
|
commitdiff
2020-03-16
Andres Noetzli
Create master equality engine at context level 0 (...
tree
|
commitdiff
2020-03-03
mudathirmahgoub
Refactoring and cleaning the type enumerator for sets...
tree
|
commitdiff
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
tree
|
commitdiff
2020-02-24
Andrew Reynolds
Utilities for words (#3797)
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-01-31
Andres Noetzli
Fix arithmetic rewriter for exponential (#3688)
tree
|
commitdiff
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
tree
|
commitdiff
2019-12-07
Andres Noetzli
Simplify rewrite for character matching (#3545)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
Add ExprManager as argument to Datatype (#3535)
tree
|
commitdiff
2019-12-03
Andres Noetzli
Rewrite `str.contains` used for character matching...
tree
|
commitdiff
2019-12-01
Andres Noetzli
Prevent ref count from reaching zero in BV instantiator...
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-09-30
Andres Noetzli
Add rewrite for splitting equalities (#2957)
tree
|
commitdiff
2019-08-30
Andres Noetzli
Infer conflicts based on regular expression inclusion...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Properly implement logic info for separation logic...
tree
|
commitdiff
2019-06-04
Andres Noetzli
Enable proof checking for QF_LRA benchmarks (#2928)
tree
|
commitdiff
2019-05-18
Andres Noetzli
Fix BV ITE rewrite (#3004)
tree
|
commitdiff
2019-04-01
Andres Noetzli
Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-23
Andres Noetzli
Strip non-matching beginning from indexof operator...
tree
|
commitdiff
2019-03-22
Andres Noetzli
Fix stripConstantEndpoints in strings rewriter (#2883)
tree
|
commitdiff
2019-02-13
Andres Noetzli
Rewrite simple regexp pattern to str.contains (#2827)
tree
|
commitdiff
2019-02-05
Andres Noetzli
Make stripConstantEndpoints() less aggressive (#2830)
tree
|
commitdiff
2019-02-04
Andres Noetzli
Add rewrite for contains + const strings replace (...
tree
|
commitdiff
2019-02-02
Andres Noetzli
Fix corner case in stripConstantEndpoints (#2824)
tree
|
commitdiff
2019-01-29
Andres Noetzli
Strings: Remove redundant replace rewrite (#2822)
tree
|
commitdiff
2019-01-23
Andres Noetzli
Strings: Strengthen multiset reasoning (#2817)
tree
|
commitdiff
2018-11-28
Andres Noetzli
Improve skolem caching by normalizing skolem args ...
tree
|
commitdiff
2018-11-22
Andres Noetzli
Add rewrite for (str.substr s x y) --> "" (#2695)
tree
|
commitdiff
2018-11-08
Andres Noetzli
Evaluator: add support for str.code (#2696)
tree
|
commitdiff
2018-11-07
Andres Noetzli
Fix collectEmptyEqs in string rewriter (#2692)
tree
|
commitdiff
2018-10-20
Andres Noetzli
Add substr, contains and equality rewrites (#2665)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Add helper to detect length one string terms (#2654)
tree
|
commitdiff
2018-10-15
Andrew Reynolds
Delay initialization of theory engine (#2621)
tree
|
commitdiff
2018-10-15
Andres Noetzli
Add more (str.replace x y z) rewrites (#2628)
tree
|
commitdiff
2018-10-12
Andres Noetzli
Add rewrites for str.replace in str.contains (#2623)
tree
|
commitdiff
2018-10-11
Andres Noetzli
Improve reasoning about empty strings in rewriter ...
tree
|
commitdiff
2018-10-10
Andres Noetzli
Add length-based rewrites for (str.substr _ _ _) (...
tree
|
commitdiff
2018-10-09
Aina Niemetz
BV instantiator: Factor out util functions. (#2604)
tree
|
commitdiff
2018-10-09
Aina Niemetz
BV inverter: Factor out util functions. (#2603)
tree
|
commitdiff
2018-10-02
Andres Noetzli
Fix "catching polymorphic type by value" warnings ...
tree
|
commitdiff
2018-09-28
Andres Noetzli
Rewrites for (= "" _) and (= (str.replace _) _) (#2546)
tree
|
commitdiff
2018-09-24
Andres Noetzli
Unify rewrites related to (str.contains x y) --> (...
tree
|
commitdiff
2018-09-24
Andres Noetzli
Make string rewriter unit tests more robust (#2520)
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Refactor cvc4_add_unit_test macro to support...
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Add support for CxxTest.
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-19
Andres Noetzli
Add rewrites for str.contains + str.replace/substr...
tree
|
commitdiff
2018-09-18
Andres Noetzli
Fix issue with str.idof in evaluator (#2493)
tree
|
commitdiff
2018-09-10
Andres Noetzli
Add (str.replace (str.replace y w y) y z) rewrite ...
tree
|
commitdiff
2018-08-23
Andres Noetzli
Add missing overrides in unit tests (#2362)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Remove support for flipDecision (#2319)
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-05
Andres Noetzli
sygusComp2018: Improve string rewriter (#2141)
tree
|
commitdiff
2018-06-28
Andrew Reynolds
Split and document ceg theory instantiators (#2094)
tree
|
commitdiff
2018-06-26
Andres Noetzli
sygusComp2018: Add evaluator (#2090)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-05
Andres Noetzli
Only enable transcendentals if logic is N[I]RAT (#2052)
tree
|
commitdiff
2018-04-11
Aina Niemetz
Refactored BVGauss preprocessing pass. (#1766)
tree
|
commitdiff
2018-04-02
Mathias Preiner
Reorganize bitblaster code. (#1695)
tree
|
commitdiff
2018-03-27
Andres Noetzli
Better normalization of string concatenation (#1719)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Add reasoning for inequalities in str rewriter (#1713)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Rewrites for substr of strings of length one (#1712)
tree
|
commitdiff
2018-03-09
Mathias Preiner
Fix Travis for unit test compilation errors. (#1651)
tree
|
commitdiff
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
tree
|
commitdiff
2018-02-08
Aina Niemetz
Updated copyright
tree
|
commitdiff
2018-01-25
Aina Niemetz
Added unit tests for PLUS, NEG, NOT ICs for CBQI BV...
tree
|
commitdiff
2018-01-22
Aina Niemetz
Refactor and fix solveBvLit for CBQI BV. (#1526)
tree
|
commitdiff
2018-01-10
Mathias Preiner
Fix linearization for terms where the solve variable...
tree
|
commitdiff
2018-01-05
Mathias Preiner
Add UGT/SGT side conditions for AND/OR + other fixes...
tree
|
commitdiff
2018-01-03
Aina Niemetz
Add side conditions for inequalities over BITVECTOR_UDI...
tree
|
commitdiff
2018-01-03
Mathias Preiner
Fix handling for UGT/SGT. (#1467)
tree
|
commitdiff
2017-12-30
Aina Niemetz
Add side conditions for inequalities over BITVECTOR_URE...
tree
|
commitdiff
2017-12-29
Aina Niemetz
Fix unit tests for ineq for CBQI BV. (#1456)
tree
|
commitdiff
next