projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix a subtle issue with double negations in coverings proof (#7967)
[cvc5.git]
/
src
/
theory
/
2022-01-19
Gereon Kremer
Fix a subtle issue with double negations in coverings...
tree
|
commitdiff
2022-01-19
Gereon Kremer
Make tracing for arithmetic rewriter more consistent...
tree
|
commitdiff
2022-01-18
Andrew Reynolds
Distinguish purification types for strings proof recons...
tree
|
commitdiff
2022-01-17
Andrew Reynolds
Refactor options related to rewriting and symmetry...
tree
|
commitdiff
2022-01-17
Andres Noetzli
[Strings] Fix rewriter for `re.loop` (#7956)
tree
|
commitdiff
2022-01-15
Andrew Reynolds
Add inverse inference for update-over-concat (#7954)
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Improve names for sygus enumeration option (#7945)
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Clean enumerative instantiation options (#7947)
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Implement -o subs to show learned top-level substitutio...
tree
|
commitdiff
2022-01-14
Gereon Kremer
Preprare central model building for RANs (#7951)
tree
|
commitdiff
2022-01-14
Gereon Kremer
refactor div rewriter, add support for ran (#7941)
tree
|
commitdiff
2022-01-14
Gereon Kremer
Add operator<<(RewriteStatus) (#7952)
tree
|
commitdiff
2022-01-14
Andrew Reynolds
Weaken assertion in relevance manager (#7943)
tree
|
commitdiff
2022-01-14
Gereon Kremer
Refactor arithmetic pre-rewriter for multiplication...
tree
|
commitdiff
2022-01-14
Gereon Kremer
Add support for RANs in rewriter for `MULT` (#7940)
tree
|
commitdiff
2022-01-14
Gereon Kremer
Add RAN support in UMINUS rewriter (#7933)
tree
|
commitdiff
2022-01-13
Gereon Kremer
Add arithmetic rewriter for RAN (#7929)
tree
|
commitdiff
2022-01-13
Andrew Reynolds
Fix bug in evaluator for division by zero (#7942)
tree
|
commitdiff
2022-01-13
Andres Noetzli
Unify abstract values and uninterpreted constants ...
tree
|
commitdiff
2022-01-13
Gereon Kremer
Refactor post rewriter for addition (#7931)
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Add -o learned-lits to output learned literals (#7934)
tree
|
commitdiff
2022-01-12
Gereon Kremer
Refactor atom rewriting to be RAN-aware (#7928)
tree
|
commitdiff
2022-01-12
Gereon Kremer
Refactor rewriteMinus (#7932)
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Ensure configuration of shared selectors is consistent...
tree
|
commitdiff
2022-01-12
Gereon Kremer
Add mkRealAlgebraicNumber (#7923)
tree
|
commitdiff
2022-01-12
Andrew Reynolds
Always use partial function for sqrt (#7926)
tree
|
commitdiff
2022-01-11
Gereon Kremer
Adds a kind to hold RealAlgebraicNumber constants ...
tree
|
commitdiff
2022-01-11
Abdalrhman Mohamed
Disable filtering of shapes in sygus-rcons pool. (...
tree
|
commitdiff
2022-01-11
Gereon Kremer
Remove static accesses to options (#7913)
tree
|
commitdiff
2022-01-11
Andrew Reynolds
Tighten policy for unsat cores in sygus core connective...
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Make alpha equivalence user context dependent (#7889)
tree
|
commitdiff
2022-01-06
Gereon Kremer
Improve theory combination in the presence of real...
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Fix non-idempotent rewrite in arrays (#7887)
tree
|
commitdiff
2022-01-06
Andrew Reynolds
Minor cleaning of non-clausal simplification (#7886)
tree
|
commitdiff
2022-01-05
Andrew Reynolds
Track input list for atoms in difficulty manager (...
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Fix proofs for datatype purify (#7841)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Add utility expr::isBooleanConnective (#7869)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Remove unused shutdown infrastructure (#7872)
tree
|
commitdiff
2022-01-04
Andrew Reynolds
Fix int blaster (#7856)
tree
|
commitdiff
2022-01-04
mudathirmahgoub
Add bag.member operator to theory of bags (#7857)
tree
|
commitdiff
2022-01-04
mudathirmahgoub
Refactor bag solver (#7770)
tree
|
commitdiff
2022-01-03
Andrew Reynolds
Update quantifiers compute elim symbols to be iterative...
tree
|
commitdiff
2022-01-03
Andres Noetzli
[BV] Remove non-existent `friend` class (#7864)
tree
|
commitdiff
2021-12-22
Andrew Reynolds
Remove most uses of mkRationalNode (#7854)
tree
|
commitdiff
2021-12-22
Andrew Reynolds
Add support for incremental + interpolants (#7853)
tree
|
commitdiff
2021-12-21
Andrew Reynolds
Eliminate remaining calls to callExtendedRewrite (...
tree
|
commitdiff
2021-12-21
yoni206
Rewrite (pow2 x) to (pow 2 x) when x is a constant...
tree
|
commitdiff
2021-12-21
Andrew Reynolds
Connect sequences array solver to strategy in theory...
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Eliminating some uses of const rational in arithmetic...
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Allow SyGuS subsolver to be reused in incremental mode...
tree
|
commitdiff
2021-12-20
Andres Noetzli
[Sequences/Array Solver] Minor refactoring (#7843)
tree
|
commitdiff
2021-12-17
Andres Noetzli
[Strings] Minor fixes/improvements (#7837)
tree
|
commitdiff
2021-12-17
Ying Sheng
Array-inspired Sequence Solver - Fixing several issues...
tree
|
commitdiff
2021-12-17
Andres Noetzli
Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)
tree
|
commitdiff
2021-12-17
Gereon Kremer
Fix tracker in SubstitutionMap (#7829)
tree
|
commitdiff
2021-12-17
mudathirmahgoub
Remove Rewriter::rewrite from bags type enumerator...
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Refactoring initialization of proofs (#7834)
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Implement model construction for the array extension...
tree
|
commitdiff
2021-12-17
Andrew Reynolds
Eliminate more uses of CONST_RATIONAL (#7816)
tree
|
commitdiff
2021-12-16
Andrew Reynolds
Eliminate most static calls to rewrite in quantifiers...
tree
|
commitdiff
2021-12-16
yoni206
bv-to-int: use pow2 operator (#7812)
tree
|
commitdiff
2021-12-16
mudathirmahgoub
Add regression bags-of-bags-subtypes.smt2 (#7814)
tree
|
commitdiff
2021-12-16
Andres Noetzli
Explicitly disallow `mkConst(Rational)` (#7818)
tree
|
commitdiff
2021-12-15
Andrew Reynolds
Ensure match terms are exhaustive in its type rule...
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Eliminate static calls to rewrite in strings (#7803)
tree
|
commitdiff
2021-12-14
mudathirmahgoub
Fix cvc5-projects issue 358 (#7804)
tree
|
commitdiff
2021-12-14
Abdalrhman Mohamed
Add a random Sygus enumerator. (#7782)
tree
|
commitdiff
2021-12-14
Gereon Kremer
Fix issues with tracing builds (#7809)
tree
|
commitdiff
2021-12-14
Andres Noetzli
Add switches to toggle eager and inclusion solvers...
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Connecting the core array solver in strings (#7800)
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Minor fix for sygus unsat query generator (#7811)
tree
|
commitdiff
2021-12-14
Andrew Reynolds
Eliminate use of rewrite, CONST_RATIONAL in ArithMSum...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Distinguishing more uses of CONST_RATIONAL (#7802)
tree
|
commitdiff
2021-12-13
mudathirmahgoub
A more efficient implementation for bag.card operator...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Fixes and additions for API for parametric datatypes...
tree
|
commitdiff
2021-12-13
Gereon Kremer
Improve nonlinear solver (#7787)
tree
|
commitdiff
2021-12-13
yoni206
Integrate new int-blaster (#7781)
tree
|
commitdiff
2021-12-13
mudathirmahgoub
Fix cvc5-projects issues #358 and #375 (#7743)
tree
|
commitdiff
2021-12-10
Andrew Reynolds
Refactor and fixes related to getSpecializedConstructor...
tree
|
commitdiff
2021-12-10
Ying Sheng
Array-inspired Sequence Solver - Adding the ArrayCoreSo...
tree
|
commitdiff
2021-12-10
Gereon Kremer
Eliminate more static rewrites (#7786)
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Consider polarity in relevance manager (#7768)
tree
|
commitdiff
2021-12-09
Gereon Kremer
Fix sine symmetry proof (#7783)
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Do not make SyGuS subsolver in unsat state after solvin...
tree
|
commitdiff
2021-12-08
Andrew Reynolds
Return bool for lemmaTheoryInference (#7773)
tree
|
commitdiff
2021-12-08
Gereon Kremer
Remove rewrites from iand and pow2 solvers (#7775)
tree
|
commitdiff
2021-12-08
Gereon Kremer
Eliminate rewriter from transcendental solver (#7772)
tree
|
commitdiff
2021-12-08
Gereon Kremer
Static options acceses again (#7771)
tree
|
commitdiff
2021-12-08
Andrew Reynolds
Fix type rule for datatype updater for parametric sorts...
tree
|
commitdiff
2021-12-08
Aina Niemetz
FP: Remove static call to Rewriter. (#7765)
tree
|
commitdiff
2021-12-07
Gereon Kremer
Remove more static accesses to options (#7764)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Add proof annotation option (#7750)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Make data structures in relevance manager SAT-context...
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Eliminate more static calls to Rewriter::rewrite (...
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-03
Andrew Reynolds
Check constructor is used in APPLY_CONSTRUCTOR (#7737)
tree
|
commitdiff
2021-12-02
mudathirmahgoub
add bag.fold operator (#7718)
tree
|
commitdiff
2021-12-01
Andrew Reynolds
Improvements for get-difficulty (#7720)
tree
|
commitdiff
next