projects / cvc5.git / history
? search:
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 KremerFix a subtle issue with double negations in coverings... tree | commitdiff
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent... tree | commitdiff
2022-01-18 Andrew ReynoldsDistinguish purification types for strings proof recons... tree | commitdiff
2022-01-17 Andrew ReynoldsRefactor 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 ReynoldsAdd inverse inference for update-over-concat (#7954) tree | commitdiff
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945) tree | commitdiff
2022-01-14 Andrew ReynoldsClean enumerative instantiation options (#7947) tree | commitdiff
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio... tree | commitdiff
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951) tree | commitdiff
2022-01-14 Gereon Kremerrefactor div rewriter, add support for ran (#7941) tree | commitdiff
2022-01-14 Gereon KremerAdd operator<<(RewriteStatus) (#7952) tree | commitdiff
2022-01-14 Andrew ReynoldsWeaken assertion in relevance manager (#7943) tree | commitdiff
2022-01-14 Gereon KremerRefactor arithmetic pre-rewriter for multiplication... tree | commitdiff
2022-01-14 Gereon KremerAdd support for RANs in rewriter for `MULT` (#7940) tree | commitdiff
2022-01-14 Gereon KremerAdd RAN support in UMINUS rewriter (#7933) tree | commitdiff
2022-01-13 Gereon KremerAdd arithmetic rewriter for RAN (#7929) tree | commitdiff
2022-01-13 Andrew ReynoldsFix bug in evaluator for division by zero (#7942) tree | commitdiff
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... tree | commitdiff
2022-01-13 Gereon KremerRefactor post rewriter for addition (#7931) tree | commitdiff
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) tree | commitdiff
2022-01-12 Gereon KremerRefactor atom rewriting to be RAN-aware (#7928) tree | commitdiff
2022-01-12 Gereon KremerRefactor rewriteMinus (#7932) tree | commitdiff
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent... tree | commitdiff
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923) tree | commitdiff
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926) tree | commitdiff
2022-01-11 Gereon KremerAdds a kind to hold RealAlgebraicNumber constants ... tree | commitdiff
2022-01-11 Abdalrhman MohamedDisable filtering of shapes in sygus-rcons pool. (... tree | commitdiff
2022-01-11 Gereon KremerRemove static accesses to options (#7913) tree | commitdiff
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective... tree | commitdiff
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) tree | commitdiff
2022-01-06 Gereon KremerImprove theory combination in the presence of real... tree | commitdiff
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887) tree | commitdiff
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) tree | commitdiff
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... tree | commitdiff
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841) tree | commitdiff
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) tree | commitdiff
2022-01-04 Andrew ReynoldsFix int blaster (#7856) tree | commitdiff
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) tree | commitdiff
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) tree | commitdiff
2022-01-03 Andrew ReynoldsUpdate 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 ReynoldsRemove most uses of mkRationalNode (#7854) tree | commitdiff
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) tree | commitdiff
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... tree | commitdiff
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... tree | commitdiff
2021-12-21 Andrew ReynoldsConnect sequences array solver to strategy in theory... tree | commitdiff
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... tree | commitdiff
2021-12-20 Andrew ReynoldsAllow 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 ShengArray-inspired Sequence Solver - Fixing several issues... tree | commitdiff
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) tree | commitdiff
2021-12-17 Gereon KremerFix tracker in SubstitutionMap (#7829) tree | commitdiff
2021-12-17 mudathirmahgoubRemove Rewriter::rewrite from bags type enumerator... tree | commitdiff
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) tree | commitdiff
2021-12-17 Andrew ReynoldsImplement model construction for the array extension... tree | commitdiff
2021-12-17 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#7816) tree | commitdiff
2021-12-16 Andrew ReynoldsEliminate most static calls to rewrite in quantifiers... tree | commitdiff
2021-12-16 yoni206bv-to-int: use pow2 operator (#7812) tree | commitdiff
2021-12-16 mudathirmahgoubAdd regression bags-of-bags-subtypes.smt2 (#7814) tree | commitdiff
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818) tree | commitdiff
2021-12-15 Andrew ReynoldsEnsure match terms are exhaustive in its type rule... tree | commitdiff
2021-12-14 Andrew ReynoldsEliminate static calls to rewrite in strings (#7803) tree | commitdiff
2021-12-14 mudathirmahgoubFix cvc5-projects issue 358 (#7804) tree | commitdiff
2021-12-14 Abdalrhman MohamedAdd a random Sygus enumerator. (#7782) tree | commitdiff
2021-12-14 Gereon KremerFix issues with tracing builds (#7809) tree | commitdiff
2021-12-14 Andres NoetzliAdd switches to toggle eager and inclusion solvers... tree | commitdiff
2021-12-14 Andrew ReynoldsConnecting the core array solver in strings (#7800) tree | commitdiff
2021-12-14 Andrew ReynoldsMinor fix for sygus unsat query generator (#7811) tree | commitdiff
2021-12-14 Andrew ReynoldsEliminate use of rewrite, CONST_RATIONAL in ArithMSum... tree | commitdiff
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) tree | commitdiff
2021-12-13 mudathirmahgoubA more efficient implementation for bag.card operator... tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... tree | commitdiff
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) tree | commitdiff
2021-12-13 yoni206Integrate new int-blaster (#7781) tree | commitdiff
2021-12-13 mudathirmahgoubFix cvc5-projects issues #358 and #375 (#7743) tree | commitdiff
2021-12-10 Andrew ReynoldsRefactor and fixes related to getSpecializedConstructor... tree | commitdiff
2021-12-10 Ying ShengArray-inspired Sequence Solver - Adding the ArrayCoreSo... tree | commitdiff
2021-12-10 Gereon KremerEliminate more static rewrites (#7786) tree | commitdiff
2021-12-09 Andrew ReynoldsConsider polarity in relevance manager (#7768) tree | commitdiff
2021-12-09 Gereon KremerFix sine symmetry proof (#7783) tree | commitdiff
2021-12-09 Andrew ReynoldsDo not make SyGuS subsolver in unsat state after solvin... tree | commitdiff
2021-12-08 Andrew ReynoldsReturn bool for lemmaTheoryInference (#7773) tree | commitdiff
2021-12-08 Gereon KremerRemove rewrites from iand and pow2 solvers (#7775) tree | commitdiff
2021-12-08 Gereon KremerEliminate rewriter from transcendental solver (#7772) tree | commitdiff
2021-12-08 Gereon KremerStatic options acceses again (#7771) tree | commitdiff
2021-12-08 Andrew ReynoldsFix type rule for datatype updater for parametric sorts... tree | commitdiff
2021-12-08 Aina NiemetzFP: Remove static call to Rewriter. (#7765) tree | commitdiff
2021-12-07 Gereon KremerRemove more static accesses to options (#7764) tree | commitdiff
2021-12-07 Andrew ReynoldsAdd proof annotation option (#7750) tree | commitdiff
2021-12-07 Andrew ReynoldsMake data structures in relevance manager SAT-context... tree | commitdiff
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... tree | commitdiff
2021-12-07 Andrew ReynoldsEliminate more static calls to Rewriter::rewrite (... tree | commitdiff
2021-12-07 makaimannAdd bitwise option to IntBlaster (#7721) tree | commitdiff
2021-12-03 Andrew ReynoldsCheck constructor is used in APPLY_CONSTRUCTOR (#7737) tree | commitdiff
2021-12-02 mudathirmahgoubadd bag.fold operator (#7718) tree | commitdiff
2021-12-01 Andrew ReynoldsImprovements for get-difficulty (#7720) tree | commitdiff
next